------------------------------------------------------------------------
-- 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 ⊥