module equality where

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
sym refl = refl

sym′ : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
sym′ {A} {x} {.x} refl = refl

trans : ∀ {A : Set} {x y z : A}
  → x ≡ y → y ≡ z → x ≡ z
trans refl q = q

trans′ : ∀ {A : Set} {x y z : A}
  → x ≡ y → y ≡ z → x ≡ z
trans′ {A} {x} {.x} {z} refl q = q

cong : ∀ {A B : Set} (f : A → B) {x y} → x ≡ y → f x ≡ f y
cong f refl = refl