module Equality where

open import Logic

data _≡_ {X : Set} : X → X → Ω where
  refl : {x : X} → x ≡ x

infix   _≡_

_≠_ : {X : Set} → (x y : X) → Ω
x ≠ y = x ≡ y → ⊥

two-things-equal-to-a-third-are-equal : {X : Set} →
             ∀{x y z : X} → x ≡ y → x ≡ z → y ≡ z

two-things-equal-to-a-third-are-equal refl refl = refl


transitivity : {X : Set} → {x y z : X} →  x ≡ y  →  y ≡ z  →  x ≡ z
transitivity refl refl = refl


symmetry : {X : Set} → {x y : X} → x ≡ y → y ≡ x
symmetry refl = refl


extensionality : {X Y : Set} → ∀(f : X → Y) → {x₀ x₁ : X} →

  x₀ ≡ x₁ → f x₀ ≡ f x₁

extensionality f refl = refl


equals-for-equals : {X Y : Set} → (f : X → Y) → {x x' : X} → {y : Y} →

  f x ≡ y →  x ≡ x' → f x' ≡ y

equals-for-equals f refl refl = refl