module Equality where -- A datatype of equality proofs. There is only one way to construct an -- equality proof: both sides must be *the same* (modulo simplification). data I (A : Set) (a : A) : A → Set where refl : I A a a -- Another implementation, perhaps closer to the “usual“ equality notation -- can be given by making the type parameter A implicit. data _≡_ {A : Set} (a : A) : A → Set where refl : a ≡ a -- When case-splitting (C-c C-c) on a proof (a₁≡a₂ : I A a₁ a₂), Agda -- replaces it by the only possible constructor refl, and unifies a₁ -- with a₂. -- Symmetry sym : {A : Set} → {a₁ a₂ : A} → I A a₁ a₂ → I A a₁ a₂ sym refl = refl -- Transitivity trans : {A : Set} → {a₁ a₂ a₃ : A} → I A a₁ a₂ → I A a₂ a₃ → I A a₁ a₃ trans refl refl = refl -- Leibniz property (substitutivity): If a property is true for a₂, then it's -- also true for any a₁ equal to a₁ subst : {A : Set} -> {P : A → Set} → {a₁ a₂ : A} → I A a₁ a₂ -> P a₂ -> P a₁ subst refl pa₂ = pa₂ -- Congruence: the images of equal inputs by a function f are equal. cong : {A B : Set} → {a₁ a₂ : A} → (f : A → B) → I A a₁ a₂ → I B (f a₁) (f a₂) cong f refl = refl -- See the end of the joint ‘NaturalNumbers‘ module for other examples.