module Identity where -- A datatype of identity (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 -- ... with user friendly notation with an infix = sign and the type 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} → a₁ ≡ a₂ → a₂ ≡ a₁ sym refl = refl -- Transitivity trans : {A : Set} → {a₁ a₂ a₃ : A} → a₁ ≡ a₂ → a₂ ≡ 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} → a₁ ≡ a₂ -> P a₂ -> P a₁ subst refl q = q -- Congruence: functions map equal inputs to equal outputs cong : {A B : Set} → {a₁ a₂ : A} → (f : A → B) → a₁ ≡ a₂ → f a₁ ≡ f a₂ cong f refl = refl