module Lib.PropEq where

open import Agda.Builtin.Equality


variable
  ℓ : Agda.Primitive.Level
  A B : Set ℓ
  a b c : A

sym : a ≡ b → b ≡ a
sym refl = refl

trans : a ≡ b → b ≡ c → a ≡ c
trans refl refl = refl

cong : (f : A → B) → a ≡ b → f a ≡ f b
cong f refl = refl