context extension

**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

$\Gamma, x\colon T$

(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}$

$(\mathbf{H}_{/\Gamma})_{/T}
\stackrel{\overset{\prod_{x : T}}{\longrightarrow}}{\stackrel{\overset{(-)\times T}{\longleftarrow}}{\underset{\sum_{x : T}}{\longrightarrow}}}
\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.)

The observation that context extension forms an adjoint pair/adjoint triple with quantifiers is due to

- Bill Lawvere,
*Adjointness in Foundations*, (TAC), Dialectica 23 (1969), 281-296

and further developed in

- Bill Lawvere,
*Equality in hyperdoctrines and comprehension schema as an adjoint functor*, Proceedings of the AMS Symposium on Pure Mathematics XVII (1970), 1-14.

Revised on March 2, 2016 13:51:39
by Urs Schreiber
(109.144.228.190)