module Equality where

open import Logic

-- Definition (Intensional equality).
data _≡_ {X : Set} : X → X → Prp where
  refl : {x : X} → x ≡ x

infix   _≡_

-- Definition (Negation of intensional Equality).
_≠_ : {X : Set} → (x y : X) → Prp
x ≠ y = x ≡ y → ⊥


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

cong : {X Y : Set} →
---------------------------------------------------------
  ∀(f : X → Y) → {x₀ x₁ : X} → x₀ ≡ x₁ → f x₀ ≡ f x₁
---------------------------------------------------------
cong f refl = refl

Lemma[x≡y→x≡z→z≡y] : {X : Set} →
------------------------------------------
  ∀{x y z : X} → x ≡ y → x ≡ z → z ≡ y
------------------------------------------
Lemma[x≡y→x≡z→z≡y] refl refl = refl