------------------------------------------------------------------------
-- The Agda standard library
--
-- The universal binary relation
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Relation.Binary.Construct.Always where

open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Structures using (IsEquivalence)
open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
open import Relation.Binary.Construct.Constant using (Const)
open import Data.Unit.Polymorphic using (⊤; tt)

------------------------------------------------------------------------
-- Definition

Always : ∀ {a ℓ} {A : Set a} → Rel A ℓ
Always = Const ⊤

------------------------------------------------------------------------
-- Properties

module _ {a} (A : Set a) ℓ where

  refl : Reflexive {A = A} {ℓ = ℓ} Always
  refl = _

  sym : Symmetric {A = A} {ℓ = ℓ} Always
  sym _ = _

  trans : Transitive {A = A} {ℓ = ℓ} Always
  trans _ _ = _

  isEquivalence : IsEquivalence {ℓ = ℓ} {A} Always
  isEquivalence = record {}

  setoid : Setoid a ℓ
  setoid = record
    { isEquivalence = isEquivalence
    }