Spahn categorical logic and type theory (Rev #1, changes)

Showing changes from revision #0 to #1: Added | Removed | Changed

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

The weak elimination rule for $s_1,s_2)$-sums is

(…)

(p.692)