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