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