categorical logic and type theory (Rev #2, changes)

Showing changes from revision #1 to #2:
Added | ~~Removed~~ | ~~Chan~~ged

This entry is about

- Bart Jacobs, categorical logic and type theory

(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}$

(…)

(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
}$