This is the Overture.Equality module of the Agda Universal Algebra Library.
{-# OPTIONS --without-K --exact-split --safe #-} module Overture.Equality where open import Overture.Preliminaries public
Here we discuss what is probably the most important type in MLTT. It is called definitional equality. This concept is easily understood, at least heuristically, with the following slogan:
Definitional equality is the substitution-preserving equivalence relation generated by definitions.
We will make this precise below, but first let us quote from a primary source.
In An Intuitionistic Theory of Types: Predicative Part, Per Martin-Löf offers the following definition (italics added):1
“Definitional equality is defined to be the equivalence relation, that is, reflexive, symmetric and transitive relation, which is generated by the principles that a definiendum is always definitionally equal to its definiens and that definitional equality is preserved under substitution.”2
To be sure we understand what this means, let := denote the relation with respect to which x is related to y (denoted x := y) if and only if y is the definition of x. Then the definitional equality relation ≡ is the reflexive, symmetric, transitive, substitutive closure of :=. By subsitutive closure we mean closure under the following substitution rule.
{A : 𝓤 ̇} {B : A → 𝓦 ̇} {x y : A} x ≡ y
------------------------------------------ (subst)
B x ≡ B y
The datatype we use to represent definitional equality is imported from the Identity-Type module of the Type Topology library, but apart from superficial syntactic differences, it is equivalent to the standard Paulin-Mohring style identity type found in most other Agda libraries. We repeat the definition here for easy reference.
module hide-refl where data _≡_ {A : 𝓤 ̇} : A → A → 𝓤 ̇ where refl : {x : A} → x ≡ x open import Identity-Type renaming (_≡_ to infix 0 _≡_) public
Whenever we need to complete a proof by simply asserting that x is definitionally equal to itself, we invoke refl. If we need to make explicit the implicit argument x, then we use refl {x = x}.
The ≡ type just defined is an equivalence relation and the formal proof of this fact is trivial. We don’t need to prove reflexivity since it is the defining property of ≡. Here are the (trivial) proofs of symmetry and transitivity of ≡.
≡-sym : {A : 𝓤 ̇}{x y : A} → x ≡ y → y ≡ x ≡-sym refl = refl ≡-trans : {A : 𝓤 ̇}{x y z : A} → x ≡ y → y ≡ z → x ≡ z ≡-trans refl refl = refl
We prove that ≡ obeys the substitution rule (subst) in the next subsection (see the definition of ap below), but first we define some syntactic sugar that will make it easier to apply symmetry and transitivity of ≡ in proofs.3
module hide-sym-trans {A : 𝓤 ̇} where _⁻¹ : {x y : A} → x ≡ y → y ≡ x p ⁻¹ = ≡-sym p
If we have a proof p : x ≡ y, and we need a proof of y ≡ x, then instead of ≡-sym p we can use the more intuitive p ⁻¹ . Similarly, the following syntactic sugar makes abundant appeals to transitivity easier to stomach.
_∙_ : {x y z : A} → x ≡ y → y ≡ z → x ≡ z p ∙ q = ≡-trans p q
As usual, we import the original definitions from the Type Topology library.
open import MGS-MLTT using (_⁻¹; _∙_) public
Alonzo Church characterized equality by declaring two things equal iff no property (predicate) can distinguish them.4 In other terms, x and y are equal iff for all P we have P x → P y. One direction of this implication is sometimes called substitution or transport or transport along an identity. It asserts that if two objects are equal and one of them satisfies a predicate, then so does the other. A type representing this notion is defined in the MGS-MLTT module of the Type Topology library as follows.3
module hide-id-transport where 𝑖𝑑 : (A : 𝓤 ̇ ) → A → A 𝑖𝑑 A = λ x → x transport : {A : 𝓤 ̇}(B : A → 𝓦 ̇){x y : A} → x ≡ y → B x → B y transport B (refl {x = x}) = 𝑖𝑑 (B x) open import MGS-MLTT using (𝑖𝑑; transport) public
As usual, we display definitions of existing types (here, 𝑖𝑑 and transport) in a hidden module and then imported their original definition from Type Topology.
A function is well defined if and only if it maps equivalent elements to a single element and we often use this nature of functions in Agda proofs. If we have a function f : X → Y, two elements a b : X of the domain, and an identity proof p : a ≡ b, then we obtain a proof of f a ≡ f b by simply applying the ap function like so, ap f p : f a ≡ f b. Escardó defines ap in the Type Topology library as follows.
module hide-ap {A : 𝓤 ̇}{B : 𝓦 ̇} where ap : (f : A → B){x y : A} → x ≡ y → f x ≡ f y ap f {x} p = transport (λ - → f x ≡ f -) p (refl {x = f x}) open import MGS-MLTT using (ap) public
Here’s a useful variation of ap that we borrow from the Relation/Binary/Core.agda module of the Agda Standard Library (transcribed into TypeTopology/UALib notation of course).
cong-app : {A : 𝓤 ̇}{B : A → 𝓦 ̇}{f g : Π B} → f ≡ g → ∀ x → f x ≡ g x cong-app refl _ = refl
1 Per Martin-Löf, An intuitionistic theory of types: predicative part, Logic Colloquium ‘73 (Bristol, 1973), 73–118, Studies in Logic and the Foundations of Mathematics, Vol. 80, 1975.
2 The definiendum is the left-hand side of a defining equation, the definiens is the right-hand side. For readers who have never generated an equivalence relation: the reflexive closure of R ⊆ A × A is the union of R and all pairs of the form (a , a); the symmetric closure is the union of R and its inverse {(y , x) : (x , y) ∈ R}; we leave it to the reader to come up with the correct definition of transitive closure.
3 Unicode Hints (agda2-mode). \^-\^1 ↝ ⁻¹; \Mii\Mid ↝ 𝑖𝑑; \. ↝ ∙. In general, for information about a character, place the cursor over that character and type M-x describe-char (or M-x h d c).
4 Alonzo Church, “A Formulation of the Simple Theory of Types,” Journal of Symbolic Logic, (2)5:56–68, 1940 JSOR link. See also this section of Escardó’s HoTT/UF in Agda notes for a discussion of transport; cf. HoTT-Agda’s definition.