------------------------------------------------------------------------ -- Some simple binary relations ------------------------------------------------------------------------ module Relation.Binary.Simple where open import Relation.Binary open import Data.Unit open import Data.Empty -- Constant relations. Const : ∀ {a} → Set → Rel a Const I = λ _ _ → I -- The universally true relation. Always : ∀ {a} → Rel a Always = Const ⊤ -- The universally false relation. Never : ∀ {a} → Rel a Never = Const ⊥ -- Always is an equivalence. Always-isEquivalence : ∀ {a} → IsEquivalence (Always {a}) Always-isEquivalence = record {}