Contents

# Contents

## 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))$