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