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): (…) sts\succ t reads “ss depends on pp”.

In Fho DTT we have: TypeKindType\succ Kind, KindTypeKind\succ Type, TypeTypeType\succ Type, and KindKindKind\succ Kind.

For sorts s 1,s 2s_1, s_2 such that s 1s 2s_1\succ s_2 the (s 1,s 2)(s_1,s_2)-product resp. -sum resp. equality rules are defined by

ΓC:s 1Γ,x:CD:s 2ΓΠx:C.D:s 2\frac{\Gamma \vdash C:s_1\;\;\;\Gamma,x:C\vdash D:s_2}{\Gamma\vdash \Pi x :C.D:s_2}
ΓC:s 1Γ,x:CD:s 2ΓΣ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}
ΓC:s 1Γ,x,x :CEq C(x,x ):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)s_1,s_2)-sums is

ΓB:s 2Γ,x:C,y:DQ:BΓ,z:Σx:C.DQ:B\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.