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