A.2.7 The empty type 0

*[right=$\mathrm{𝟎}$-form] Γ $\mathrm{𝖼𝗍𝗑}$ Γ ⊢$\mathrm{𝟎}$ : $𝒰$ _i *[right=$\mathrm{𝟎}$-elim] Γ,x : $\mathrm{𝟎}$ ⊢C : $𝒰$ _i
Γ ⊢a : $\mathrm{𝟎}$ Γ ⊢ind_$\mathrm{𝟎}$(x.C,a) : C[a/x] In ${\mathrm{𝗂𝗇𝖽}}_{\mathrm{𝟎}}$, $x$ is bound in $C$. The empty type has no introduction rule and no computation rule.

Title	A.2.7 The empty type 0