Spahn categorical logic and type theory (Rev #1)

• 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$.

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)

Revision on February 19, 2013 at 01:16:56 by Stephan Alexander Spahn?. See the history of this page for a list of all contributions to it.