A.1.8 Identity types

We introduce primitive constants c= and c𝗋𝖾𝖿𝗅. We write a=Ab for c=⁒(A,a,b) and 𝗋𝖾𝖿𝗅a for c𝗋𝖾𝖿𝗅⁒(A,a), when a:A is understood:

  • β€’

    If A:𝒰n, a:A, and b:A then a=Ab:𝒰n.

  • β€’

    If a:A then 𝗋𝖾𝖿𝗅a:a=Aa.

Given a:A, if y:A,z:a=Ay⊒C:𝒰m and ⊒d:C[a,𝗋𝖾𝖿𝗅a/y,z] then we can introduce a defined constant


with defining equation

Title A.1.8 Identity types