Sandbox

Which can be restated in terms of representable profunctors as follows. A cwf consists of

- a category $C$,
- a presheaf $Ty : \hat C$ of types in context.
- a presheaf $Tm : \widehat {\int Ty}$ of typed terms in context.
- a functor $ext : \widehat {\int Ty} \to C$ of context extension that represents the profunctor ${\int Tm}(-,ty=) \odot {\int Tm}(ctx(ty(-)),=) : \int Ty ⇸ C$ where $ty : \int Tm \to \int Ty$ and $ctx : \int Ty \to C$ are the projections of the Grothendieck construction.

Writing the profunctor as P, it is equivalent to the following definition:

$P(\Delta, (\Gamma, A)) = (\gamma : \Delta \to \Gamma) \times (a : Tm(\Gamma, A[\gamma]))$

then the universal property of the context extension is that there is a natural isomorphism $\Delta \to ext(\Gamma, A) \cong P(\Delta,(\Gamma,A))$

Last revised on October 19, 2018 at 11:04:51. See the history of this page for a list of all contributions to it.