nLab
Sandbox

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

  1. a category CC,
  2. a presheaf Ty:C^Ty : \hat C of types in context.
  3. a presheaf Tm:Ty^Tm : \widehat {\int Ty} of typed terms in context.
  4. a functor ext:Ty^Cext : \widehat {\int Ty} \to C of context extension that represents the profunctor Tm(,ty=)Tm(ctx(ty()),=):TyC{\int Tm}(-,ty=) \odot {\int Tm}(ctx(ty(-)),=) : \int Ty ⇸ C where ty:TmTyty : \int Tm \to \int Ty and ctx:TyCctx : \int Ty \to C are the projections of the Grothendieck construction.

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

P(Δ,(Γ,A))=(γ:ΔΓ)×(a:Tm(Γ,A[γ]))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 Δext(Γ,A)P(Δ,(Γ,A))\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.