PLFA: Equality

Mar 9 2023 · LastMod: Mar 9 2023

There is no interesting exercise in this chapter.


The built-in equality is the identity type in Martin-Lof dependent type theory.

Definition. Given a type $A$ and let $x:A$, then the 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.


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.