------------------------------------------------------------------------
-- The Agda standard library
--
-- Every respectful unary relation induces a preorder. No claim is
-- made that this preorder is unique.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Core using (Rel; _⇒_)
open import Relation.Binary.Bundles using (Setoid; Preorder)
open import Relation.Binary.Structures using (IsPreorder)
open import Relation.Binary.Definitions using (_Respects_; Reflexive; Transitive)
open import Relation.Unary using (Pred)
module Relation.Binary.Construct.FromPred
{s₁ s₂} (S : Setoid s₁ s₂) -- The underlying equality
{p} (P : Pred (Setoid.Carrier S) p) -- The predicate
where
open import Function.Base
open module Eq = Setoid S using (_≈_) renaming (Carrier to A)
------------------------------------------------------------------------
-- Definition
Resp : Rel A p
Resp x y = P x → P y
------------------------------------------------------------------------
-- Properties
reflexive : P Respects _≈_ → _≈_ ⇒ Resp
reflexive resp = resp
refl : P Respects _≈_ → Reflexive Resp
refl resp = resp Eq.refl
trans : Transitive Resp
trans x⇒y y⇒z = y⇒z ∘ x⇒y
isPreorder : P Respects _≈_ → IsPreorder _≈_ Resp
isPreorder resp = record
{ isEquivalence = Eq.isEquivalence
; reflexive = reflexive resp
; trans = flip _∘′_
}
preorder : P Respects _≈_ → Preorder _ _ _
preorder resp = record
{ isPreorder = isPreorder resp
}
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