Abstracts.2019.CwFs

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

by Peter Dybjer

Abstract

We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with families (cwf). To this end we introduce subcategories of simply typed cwfs (scwfs), where types do not depend on variables, and unityped cwfs (ucwfs), where there is only one type.

This is joint work with Simon Castellan, IRISA Rennes and Pierre Clairambault, ENS Lyon.

Keywords

Essentially algebraic theory, generalized algebraic theory, covariant functor, contravariant functor, presheaf, natural transformation, category of elements (of a functor), category with families, contextual category, multicategory, cartesian operad, Lawvere theory, hyperdoctrine.

Notes

Definition (Democratic cwf, [2, Definition 6]). A cwf (𝒞 : 𝐂𝐚𝐭,(T,T̃) : 𝒞ᵒᵖ → 𝐅𝐚𝐦) is democratic iff each context is represented by a type, that is for each object Γ of 𝒞 there is an element Γ̅ ∈ T(∅) and an isomorphism Γ ≅ ∅.Γ̅.

Remark (Democracy, [2, below Definition 6]). Democracy does not correspond to a rule of Martin-Löf type theory. However, a cwf generated inductively by the standard rules of Martin-Löf type theory with a one element type N₁ and Σ-types is democratic, since we can associate N₁ to the empty context and the closed type Σ_{x₁ : A₁} Σ_{x₂ : A₂}… Aₙ to a context x₁ : A₁, x₂ : A₂,…, xₙ : Aₙ by induction on n.

References

1. Simon Castellan, Pierre Clairambault, Peter Dybjer. Categories with Families: Unityped, Simply Typed, and Dependently Typed. 2019. Foundations and Applications of Univalent Mathematics slides, arXiv preprint.
2. Pierre Clairambault, Peter Dybjer. The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories. 2011. Typed Lambda Calculus and Applications paper with appendix.