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 = ?

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

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