module Equality where

open import Logic

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

infix  30 _≡_

_≠_ : {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