# PLFA: Equality

There is no interesting exercise in this chapter.

##
Equality `≡`

The built-in equality `≡`

is the *identity type* in Martin-Lof dependent type theory.

*identity type*of $A$ at $x$ is an inductive family of types $\operatorname{Id}_A(x,a)$ indexed by $x:A$, of which the constructor is $\mathsf{refl}_x : \operatorname{Id}_A(x,a)F$.

In particular, the type formation rule reads $$ \frac{\Gamma\vdash x:A}{\Gamma, a:A \vdash \operatorname{Id}_A(a,x): \text{Type}}. $$ and the constructor is given by the introduction rule $$ \frac{\Gamma\vdash x:A}{\Gamma\vdash \mathsf{refl}_A: \operatorname{Id}_A(x,x)}. $$

First some words about the type `Set`

in Agda. This is the type of all small types, not just a set or the type of sets. `A : Set`

means `A`

is a small type. A function `(x : A) → Set`

takes `x : A`

and gives a type, these kind of entities are called *predicates*.

In the Agda standard library, the implementation is given by

```
1data _≡_ {a} {A : Set a} (x : A) : A → Set a where
2 refl : x ≡ x
```

but in PLFA the implicit argument `a`

, related to sort system introduced in a version later relative to the writing, is not present, and the implementation is really

```
1infix 4 _≡_
2data _≡_ {A : Set} (x : A) : A → Set where
3 refl : x ≡ x
```

The syntax here is confusingly not explained in PLFA. `(x:A) : A → Set`

here should be read as `(x : A) : (A → Set)`

. Given `y : A`

, one gets a function `(y ≡ · ): A → Set`

, evaluating on `z : A`

yields a *type* `y ≡ z : Set`

meaning that `y ≡ z`

is a small type. In other words, The first argument for the operator `≡`

should be an element $y:A$, and the second should be another element `z`

that serve as a function argument for `A → Set`

. Some explanations are given in the Agda language reference.

Carrying out an interactive development of transivity for the operator, the result can be

```
1trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
2trans refl refl = refl
```

or can equivalently be

```
1trans : ∀ {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z
2trans refl = λ z → z
```

when one just press `C-c C-a`

in the hole: `trans refl`

is of the type `x ≡ z → x ≡ z`

. Since `refl`

is nothing but `x ≡ x`

, the argument `y`

is pattern matched to `x`

.

## Rewriting

`rewrite`

is relatively easier to understand, it just rewrites the is to the left, via a given rule, to a new expression. Nothing worthy of saying in detail.

## Leibniz equality

The implementation is

```
1_≐_ : ∀ {A : Set} (x y : A) → Set₁
2_≐_ {A} x y = ∀ (P : A → Set) → P x → P y
```

meaning that if for all predicates `P`

with variables in `A`

, `P x`

implies `P y`

, then `x ≐ y`

. The type `x ≐ y`

itself is not small: `P x`

and `P y`

are both of type `Set`

.