categorical logic and type theory

This entry is about

11.5 Full higher order dependent type theory (Fho DTT)


Definition (dependency): (…) sts\succ t reads “ss depends on pp”.

In Fho DTT we have: TypeKindType\succ Kind, KindTypeKind\succ Type, TypeTypeType\succ Type, and KindKindKind\succ Kind. It is a main difference to polymorphic dependent type theory (PDTT) that there we do not have KindTypeKind\succ Type.

For sorts s 1,s 2s_1, s_2 such that s 1s 2s_1\succ s_2 the (s 1,s 2)(s_1,s_2)-product resp. -sum resp. equality rules are defined by

ΓC:s 1Γ,x:CD:s 2ΓΠx:C.D:s 2\frac{\Gamma \vdash C:s_1\;\;\;\Gamma,x:C\vdash D:s_2}{\Gamma\vdash \Pi x :C.D:s_2}
ΓC:s 1Γ,x:CD:s 2ΓΣx:C.D:s 2\frac{\Gamma \vdash C:s_1\;\;\;\Gamma,x:C\vdash D:s_2}{\Gamma\vdash \Sigma x :C.D:s_2}
ΓC:s 1Γ,x,x :CEq C(x,x ):s 2\frac{\Gamma\vdash C:s_1}{\Gamma, x,x^\prime:C\vdash Eq_C(x,x^\prime):s_2}

The weak elimination rule for s 1,s 2)s_1,s_2)-sums is

ΓB:s 2Γ,x:C,y:DQ:BΓ,z:Σx:C.DQ:B\frac{\Gamma\vdash B:s_2\;\;\;\Gamma,x:C,y:D\vdash Q:B}{\Gamma,z:\Sigma x:C.D\vdash Q:B}


11.6 Fho DTT categorically


First we import a definition from §9:

Definition (p.539): Let p:EBp:E\to B be a fibration. A functor P:EBP:E\to B is called a comprehension category on pp if we have:

(1) codP=pcod P=p. (2) For each cartesian map ff inEE, the induced square P(f)P(f) in BB is a pullback.

Definition (p.694): A weak Fho DTT-structure is defined to be a diagram

D IR E P Arr(B) q cod B\array{ D&\stackrel{\stackrel{R}{\leftarrow}}{\underset{I}{\hookrightarrow}}&E&\stackrel{P}{\to}&Arr(B)\\ &\searrow^q&\downarrow&\swarrow^{cod}\\ &&B }


In this case the composite Q:=PI:DArr(B)Q:=PI:D\to Arr(B) is a comprehension category which has a unit R1:BDR 1:B\to D where 1:BE1:B\to E is the unit of PP.

The following example of an FhoDTTFho DTT is a degenerate one since the subobject fibration for types is a poset.

Example (p.695): Let EE be a topos. Then BB is a regular category, such that there is a fibered reflection Sub(B)Arr(B)Sub(B)\stackrel{\leftarrow}{\hookrightarrow} Arr(B) as in Theorem 4.4.4. where the reflector sends a morphism to its monic part (using the epi-mono factorization in a topos). Since monos are closed under composition, Sub(B)Arr(B)Sub(B)\to Arr(B) is a closed comprehension category. So we obtain a Fho DTT-structure

Sub(B) IR Arr(B) id Arr(B) q cod B\array{ Sub(B)&\stackrel{\stackrel{R}{\leftarrow}}{\underset{I}{\hookrightarrow}}&Arr(B)&\stackrel{id}{\to}&Arr(B)\\ &\searrow^q&\downarrow&\swarrow^{cod}\\ &&B }