module EquationalReasoning where open import Equality open import Level infix 1 proof:_ proof:_ : {ℓ : Level} {A : Set ℓ} {x y : A} → --------------------- x ≡ y → x ≡ y proof: refl = refl -- infixr 2 _≡[_]_ -- _≡[_]_ : -- {ℓ : Level} -- {A : Set ℓ} -- (x : A) -- {y z : A} -- → ------------------- -- x ≡ y → y ≡ z → x ≡ z -- _ ≡[ refl ] q = q -- optimization from -- <https://lists.chalmers.se/pipermail/agda/2016/009090.html> infixr 2 step≡ step≡ : {ℓ : Level} {A : Set ℓ} (x : A) {y z : A} → ------------------- y ≡ z → x ≡ y → x ≡ z step≡ _ refl p = p syntax step≡ x p q = x ≡[ q ] p infix 3 _qed _qed : {ℓ : Level} {A : Set ℓ} (x : A) → --------- x ≡ x _ qed = refl