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 unit type; see §1.5 (http://planetmath.org/15producttypes) for a proof of the corresponding propositional uniqueness statement.

Title	A.2.8 The unit type 1