Categories with Families: Unityped, Simply Typed, and Dependently Typed

Simon Castellan, Pierre Clairambault, Peter Dybjer

We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we i…