------------------------------------------------------------------------
-- 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
}
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4