------------------------------------------------------------------------ -- 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 ⊤ Always-setoid : ∀ {a} (A : Set a) → Setoid _ _ Always-setoid A = record { Carrier = A ; _≈_ = Always ; isEquivalence = record {} } -- The universally false relation. Never : ∀ {a} {A : Set a} → Rel A zero Never = Const ⊥