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