{-# OPTIONS --type-in-type #-}

-- Equational reasoning about relations over one specific set can be found in PreOrder.agda

open import NeilPrelude
open import Properties

module Equational

  (_≈_ : {A : Set} → Rel A)
  (reflexivity : {A : Set} → Reflexive {A} _≈_)
  (transitive : {A : Set} → Transitive {A} _≈_)

where

infixr  _⟨_⟩_
infix   _QED

_⟨_⟩_ : {A : Set} → {b c : A} → (a : A) → a ≈ b → b ≈ c → a ≈ c
_⟨_⟩_ _ = transitive

_QED : {A : Set} → (a : A) → a ≈ a
_ QED = reflexivity