This entry is about * Bart Jacobs, categorical logic and type theory ## 11.5 Full higher order dependent type theory (Fho DTT) (p.684) Definition (dependency): (...) $s\succ t$ reads "$s$ depends on $p$". In Fho DTT we have: $Type\succ Kind$, $Kind\succ Type$, $Type\succ Type$, and $Kind\succ Kind$. It is a main difference to polymorphic dependent type theory (PDTT) that there we do not have $Kind\succ Type$. For sorts $s_1, s_2$ such that $s_1\succ s_2$ the *$(s_1,s_2)$-product resp. -sum resp. equality rules are defined by $$\frac{\Gamma \vdash C:s_1\;\;\;\Gamma,x:C\vdash D:s_2}{\Gamma\vdash \Pi 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}$$ $$\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)$-sums is $$\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 (p.692) First we import a definition from ยง9: Definition (p.539): Let $p:E\to B$ be a fibration. A functor $P:E\to B$ is called a *comprehension category on $p$* if we have: (1) $cod P=p$. (2) For each cartesian map $f$ in$E$, the induced square $P(f)$ in $B$ is a pullback. Definition (p.694): A *weak Fho DTT-structure* is defined to be a diagram $$\array{ D&\stackrel{\stackrel{R}{\leftarrow}}{\underset{I}{\hookrightarrow}}&E&\stackrel{P}{\to}&Arr(B)\\ &\searrow^q&\downarrow&\swarrow^{cod}\\ &&B }$$ where * $P:E\to Arr(B)$ is a closed comprehension category of kinds. * $q=cod P I$ is a fibration (of types), and $D\stackrel{\stackrel{R}{\leftarrow}}{\underset{I}{\hookrightarrow}}E$ is a fibered reflection. * There is an object $\Omega\in E$ over $\{\omega\}=dom P(\Omega)\in B$. In this case the composite $Q:=PI:D\to Arr(B)$ is a comprehension category which has a unit $R 1:B\to D$ where $1:B\to E$ is the unit of $P$. The following example of an $Fho DTT$ is a degenerate one since the subobject fibration for types is a poset. Example (p.695): Let $E$ be a topos. Then $B$ is a regular category, such that there is a fibered reflection $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)\to Arr(B)$ is a closed comprehension category. So we obtain a Fho DTT-structure $$\array{ Sub(B)&\stackrel{\stackrel{R}{\leftarrow}}{\underset{I}{\hookrightarrow}}&Arr(B)&\stackrel{id}{\to}&Arr(B)\\ &\searrow^q&\downarrow&\swarrow^{cod}\\ &&B }$$