Extensional equality type

So-called $𝐄 𝐪$ -types, also known as extensional equality types, are perhaps the simplest form of propositional equality one can add to a type theory. The idea is, given terms $Γ ⊢ 𝑥, 𝑦 : 𝐴$ , we have a term $Γ ⊢ 𝐫 𝐞 𝐟 𝐥 : 𝐄 𝐪 (𝐴, 𝑥, 𝑦)$ iff we have the judgemental equality $Γ ⊢ 𝑥 = 𝑦 : 𝐴$ . Thus $𝐄 𝐪$ -types internalize the equality judgement.

A type theory with $𝐄 𝐪$ -types is called extensional, the canonical example being ETT. Despite its friendly appearance, equality reflection has far-reaching consequences which make the type theory very badly behaved — See ETT has undecidable equality.

Standard presentation

We give a formal presentation of $𝐄 𝐪$ -types in the cartesian calculus of substitutions, following Principles of dependent type theory. #m/def/type The formation, introduction, and elimination rules are given by

Γ ⊢ 𝑎, 𝑏 : 𝐴 Γ ⊢ 𝐄 𝐪 (𝐴, 𝑎, 𝑏) (E q) Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝐫 𝐞 𝐟 𝐥 : 𝐄 𝐪 (𝐴, 𝑎, 𝑎) (E q I)

Γ ⊢ 𝑝 : 𝐄 𝐪 (𝐴, 𝑎, 𝑏) Γ ⊢ 𝑎 = 𝑏 : 𝐴 (E q E)

where the elimination rule is called equality reflection. We also have a substitution naturality rule

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝑎, 𝑏 : 𝐴 Δ ⊢ 𝐄 𝐪 (𝐴, 𝑎, 𝑏) [𝛾] = 𝐄 𝐪 (𝐴 [𝛾], 𝑎 [𝛾], 𝑏 [𝛾]) (E q - N)

and an $𝜂$ -unicity rule

Γ ⊢ 𝑝 : 𝐄 𝐪 (𝐴, 𝑎, 𝑏) Γ ⊢ 𝑝 = 𝐫 𝐞 𝐟 𝐥 : 𝐄 𝐪 (𝐴, 𝑎, 𝑏) (E q 𝜂)

validating Uniqueness of identity proofs and removing the need for separate naturality rules for $E q I$ .

Internalizing judgemental structure

The manner in which $𝐄 𝐪$ -types internalize judgemental structure is straightforward: We have an operation

𝐄 𝐪 Γ : ⎛ ⎜ ⎜ ⎝ ∐ 𝐴 \in T y (Γ) T m (Γ, 𝐴) \times T m (Γ, 𝐵) ⎞ ⎟ ⎟ ⎠ \to T y (Γ)

natural in $Γ$ with a family of bijections

𝜄 Γ, 𝐴, 𝑎, 𝑏 : T m (Γ, 𝐄 𝐪 (𝐴, 𝑎, 𝑏)) ≅ {⋆ : ∣ : 𝑎 = 𝑏}

also natural in $Γ$ .

#state/tidy | #lang/en | #SemBr