-
Notifications
You must be signed in to change notification settings - Fork 6
Abstracts.2019.CwFs
by 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 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.
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.
Definition (Contextual cwf, [2, Definition 2]). A cwf (𝒞 : 𝐂𝐚𝐭,(T,T̃) : 𝒞ᵒᵖ → 𝐅𝐚𝐦) is contextual iff each context is generated by ∅ and -.-, that is there is an assignment of natural numbers l(Δ) ∈ ℕ to each object Δ of 𝒞 such that 1. l(Δ) = 0 iff Δ = ∅, and 2. l(Δ) = n + 1 iff there is a unique object Γ of 𝒞 and a unique element A ∈ T(Γ) such that Δ = Γ.A and l(Γ) = n.
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 [both contextual and] 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.
- 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.
- 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.