nLab Initiality Project - Semantics - Pi-types

Given a presheaf TT on a CwF CC, let T Π(Γ)=Σ ATy(Γ)T(Γ.A)T^\Pi(\Gamma) = \Sigma_{A \in Ty(\Gamma)}T(\Gamma . A), so that Ty ΠTy^\Pi is the presheaf consisting of pairs of a type AA and a type BB in a context extended by AA and Tm ΠTm^\Pi is the presheaf of pairs of a type AA and a term in a context extended by AA.

Definition

Let CC be a CwF. A Π\Pi-type structure on CC consists of :

  • a natural transformation Π:Ty ΠTy\Pi : Ty^\Pi \to Ty
  • a natural transformation λ:Tm ΠTm\lambda : Tm^\Pi \to Tm
  • and a natural isomorphism
    ,:[C op,Set](,Ty Π)×[C op,Set](,Tm)[C op,Set](,Tm Π)\langle -, -\rangle : [C^{op}, Set]( -, Ty^\Pi) \times [C^{op}, Set](-, Tm) \to [C^{op}, Set](-, Tm^\Pi)

    exhibiting the following square as a pullback-square

    Tm Π λ Tm of Π of Ty Π Π Ty \array{ Tm^\Pi & \xrightarrow{\lambda} & Tm \\ of^\Pi \downarrow & & \downarrow of \\ Ty^\Pi & \xrightarrow{\Pi} & Ty }

Last revised on November 12, 2018 at 21:53:46. See the history of this page for a list of all contributions to it.