nLab observational equality

Idea

In dependent type theory, sometimes one could inductively define an equality type directly on an inductive type, rather than using Martin-Loef’s identity types using the j-rule. This equality type is called observational equality.

Examples

Empty type

Observational equality for the empty type $\mathrm{Eq}_\mathbb{0}(x, y)$ is an indexed inductive type on the empty type $\mathbb{0}$ inductively defined by no constructors

Unit type

Observational equality for the unit type $\mathrm{Eq}_\mathbb{1}(x, y)$ is an indexed inductive type on the unit type $\mathbb{1}$ inductively defined by the following constructor

$$\mathrm{eq}_*: \mathrm{Eq}_\mathbb{1}(*, *)$$

Booleans type

Observational equality for the booleans type $\mathrm{Eq}_\mathbb{2}(x, y)$ is an indexed inductive type on the booleans type $\mathbb{2}$ inductively defined by the following constructors

$$\mathrm{eq}_0: \mathrm{Eq}_\mathbb{2}(0, 0)$$

$$\mathrm{eq}_1: \mathrm{Eq}_\mathbb{2}(1, 1)$$

Natural numbers

Observational equality for the natural numbers $\mathrm{Eq}_\mathbb{N}(x, y)$ is an indexed inductive type on the natural numbers $\mathbb{N}$ inductively defined by the following constructors

$$\mathrm{eq}_0: \mathrm{Eq}_\mathbb{N}(0, 0)$$

$$\mathrm{eq}_s: \prod_{x:\mathbb{N}} \prod_{y:\mathbb{N}} \mathrm{Eq}_\mathbb{N}(x, y) \to \mathrm{Eq}_\mathbb{N}(s(x), s(y))$$

See also

• identity type

References

• Egbert Rijke, Introduction to Homotopy Type Theory (2019) (web, pdf, GitHub)

• Univalent mathematics in Agda