module equality where
  -- in this module we define propositional equality and some helper syntax.

  infix 4 _≡_
  data _≡_ {A : Set} (a : A) : A → Set where
    instance refl : a ≡ a
  {-# BUILTIN EQUALITY _≡_ #-}

  -- ≡ is a equivalence relation
  sym : ∀ {A : Set} {x y : A} → x ≡ y → y ≡ x
  sym refl = refl

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

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

  -- Equational reasoning
  infix 3 _∎
  infixr 2 _≡⟨⟩_ step-≡
  infix 1 begin_
  begin_ : ∀ {A : Set} {x y : A} → x ≡ y → x ≡ y
  begin x = x

  _≡⟨⟩_ : ∀ {A : Set} (x y : A) → x ≡ y → x ≡ y
  _ ≡⟨⟩ _ = λ x → x

  _∎ : ∀ {A : Set} (x : A) → x ≡ x
  _ ∎ = refl

  step-≡ : ∀ {A : Set} (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
  step-≡ _ y≡z x≡y = trans x≡y y≡z

  syntax step-≡ x eq1 eq2 = x ≡⟨ eq2 ⟩ eq1