A.2.7 The empty type 0


{mathparpagebreakable}\inferrule

*[right=𝟎-form] Γ 𝖼𝗍𝗑 Ξ“ ⊒𝟎 : 𝒰 _i \inferrule*[right=𝟎-elim] Ξ“,x : 𝟎 ⊒C : 𝒰 _i
Ξ“ ⊒a : 𝟎 Ξ“ ⊒ind_𝟎(x.C,a) : C[a/x] In π—‚π—‡π–½πŸŽ, x is bound in C. The empty type has no introduction rule and no computation rule.

Title A.2.7 The empty type 0
\metatable