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.