# Contents

## Idea

In dependent type theory, context extension introduces new free variables into the context.

## Definition

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.)

## Categorical semantics

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}}{\to}}{\stackrel{\overset{(-)\times T}{\leftarrow}}{\underset{\sum_{x : T}}{\to}}} \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.)

## References

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 November 23, 2012 02:26:33 by Urs Schreiber (82.169.65.155)