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).

*[right=$=$-form]Γ ⊢A : $𝒰$ _i
Γ ⊢a : A
Γ ⊢b : AΓ ⊢$a{=}_{A}b$ : $𝒰$ _i*[right=$=$-intro]Γ ⊢A : $𝒰$ _i
Γ ⊢a : AΓ ⊢${\mathrm{𝗋𝖾𝖿𝗅}}_a$ : $a{=}_{A}a$*[right=$=$-elim]Γ,x : A,y : A,p : $x{=}_{A}y$ ⊢C : $𝒰$ _i
Γ,z : A ⊢c : C[z,z,${\mathrm{𝗋𝖾𝖿𝗅}}_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]*[right=$=$-comp]Γ,x : A,y : A,p : $x{=}_{A}y$ ⊢C : $𝒰$ _i
Γ,z : A ⊢c : C[z,z,${\mathrm{𝗋𝖾𝖿𝗅}}_z$/x,y,p]
Γ ⊢a : AΓ ⊢ind_=_A’(x.y.p.C,z.c,a,a,${\mathrm{𝗋𝖾𝖿𝗅}}_a$) ≡c[a/z] : C[a,a,${\mathrm{𝗋𝖾𝖿𝗅}}_a$/x,y,p]In ${\mathrm{𝗂𝗇𝖽}}_{{=}_A}^{\prime }$, $x$, $y$, and $p$ are bound in $C$, and $z$ is bound in$c$.