Luna Strah: Heyting-valued Types

Abstract: Categories with families (CwFs) are a form of categorical semantics of dependent type theory. In the first half I aim to introduce the concept with an eye towards concrete calculations, and then in the second half to work out the details of Heyting-valued types as a CwF. This establishes a "Heyting-valued type theory" and if time permits I will explore what principles it validates.