# A.2.7 The empty type 0

{mathparpagebreakable}\inferrule

*[right=$\mathbf{0}$-form] Γ $\mathsf{ctx}$ Γ ⊢$\mathbf{0}$ : $\mathcal{U}$ _i \inferrule*[right=$\mathbf{0}$-elim] Γ,x : $\mathbf{0}$ ⊢C : $\mathcal{U}$ _i
Γ ⊢a : $\mathbf{0}$ Γ ⊢ind_$\mathbf{0}$(x.C,a) : C[a/x] In $\mathsf{ind}_{\mathbf{0}}$, $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