natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In dependent type theory, context extension introduces new free variables into the context.
If $T$ is a type in a context $\Gamma$, then the extension of $\Gamma$ by (a free variable of) the type $T$ is the context denoted
(where $x$ is a new variable).
(We have said ‘the’ extension of $\Gamma$ by $T$ using the generalised the; but it may literally be unique using certain conventions for handling alpha equivalence.)
The categorical semantics of context extension is the inverse image of the base change geometric morphism (or its analog for hyperdoctrines) along the projection morphism $T \to \Gamma$ in the slice $\mathbf{H}_{/\Gamma}$
Generally speaking, a morphism $\Delta \to \Gamma$ in the category of contexts (an interpretation of $\Gamma$ in $\Delta$) is a display morphism iff there is an isomorphism $\Delta \leftrightarrow \Theta$ where $\Theta$ is an extension of $\Gamma$. (This might not actually be true in all type theories, or maybe it should be taken as the definition of ‘display morphism’; I'm not sure.)
Notions of pullback:
pullback, fiber product (limit over a cospan)
lax pullback, comma object (lax limit over a cospan)
(∞,1)-pullback, homotopy pullback, ((∞,1)-limit over a cospan)
The observation that context extension forms an adjoint pair/adjoint triple with quantifiers is due to
and further developed in
comprehension schema as an adjoint functor_, Proceedings of the AMS Symposium on Pure Mathematics XVII (1970), 1-14.
Last revised on December 2, 2020 at 12:30:15. See the history of this page for a list of all contributions to it.