A.2.8 The unit type 1

*[right=$\mathrm{𝟏}$-form]Γ $\mathrm{𝖼𝗍𝗑}$Γ ⊢$\mathrm{𝟏}$ : $𝒰$ _i*[right=$\mathrm{𝟏}$-intro]Γ $\mathrm{𝖼𝗍𝗑}$Γ ⊢$\star$ : $\mathrm{𝟏}$*[right=$\mathrm{𝟏}$-elim]Γ,x : $\mathrm{𝟏}$ ⊢C : $𝒰$ _i
Γ,y : $\mathrm{𝟏}$ ⊢c : C[y/x]
Γ ⊢a : $\mathrm{𝟏}$Γ ⊢ind_$\mathrm{𝟏}$(x.C,y.c,a) : C[a/x]*[right=$\mathrm{𝟏}$-comp]Γ,x : $\mathrm{𝟏}$ ⊢C : $𝒰$ _i
Γ,y : $\mathrm{𝟏}$ ⊢c : C[y/x]Γ ⊢ind_$\mathrm{𝟏}$(x.C,y.c,$\star$) ≡c[$\star$/y] : C[$\star$/x]In ${\mathrm{𝗂𝗇𝖽}}_{\mathrm{𝟏}}$, $x$ is bound in $C$, and $y$ is bound in $c$.

Notice that we don’t postulate a judgmental uniqueness principle for the unittype; see §1.5 (http://planetmath.org/15producttypes) for a proof of the correspondingpropositional uniqueness statement.