# A.2.10 Identity types

The presentation here corresponds to the (unbased) path induction principle for identity types in Β§1.12 (http://planetmath.org/112identitytypes).

{mathparpagebreakable}\inferrule

*[right=${=}$-form] Ξ β’A : $\mathcal{U}$ _i
Ξ β’a : A
Ξ β’b : A Ξ β’$a=_{A}b$ : $\mathcal{U}$ _i \inferrule*[right=${=}$-intro] Ξ β’A : $\mathcal{U}$ _i
Ξ β’a : A Ξ β’$\mathsf{refl}_{a}$ : $a=_{A}a$ \inferrule*[right=${=}$-elim] Ξ,x : A,y : A,p : $x=_{A}y$ β’C : $\mathcal{U}$ _i
Ξ,z : A β’c : C[z,z,$\mathsf{refl}_{z}$/x,y,p]
Ξ β’a : A
Ξ β’b : A
Ξ β’pβ : $a=_{A}b$ Ξ β’ind_=_Aβ(x.y.p.C,z.c,a,b,pβ) : C[a,b,pβ/x,y,p] \inferrule*[right=${=}$-comp] Ξ,x : A,y : A,p : $x=_{A}y$ β’C : $\mathcal{U}$ _i
Ξ,z : A β’c : C[z,z,$\mathsf{refl}_{z}$/x,y,p]
Ξ β’a : A Ξ β’ind_=_Aβ(x.y.p.C,z.c,a,a,$\mathsf{refl}_{a}$) β‘c[a/z] : C[a,a,$\mathsf{refl}_{a}$/x,y,p] In $\mathsf{ind}_{=_{A}}^{\prime}$, $x$, $y$, and $p$ are bound in $C$, and $z$ is bound in $c$.

Title A.2.10 Identity types
\metatable