------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties satisfied by strict partial orders
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
open import Relation.Binary.Bundles using (StrictPartialOrder; Poset)
module Relation.Binary.Properties.StrictPartialOrder
{s₁ s₂ s₃} (SPO : StrictPartialOrder s₁ s₂ s₃) where
import Relation.Binary.Construct.Flip.EqAndOrd as EqAndOrd
using (strictPartialOrder)
import Relation.Binary.Construct.StrictToNonStrict using (isPartialOrder)
open StrictPartialOrder SPO
------------------------------------------------------------------------
-- The converse relation is also a strict partial order.
>-strictPartialOrder : StrictPartialOrder s₁ s₂ s₃
>-strictPartialOrder = EqAndOrd.strictPartialOrder SPO
open StrictPartialOrder >-strictPartialOrder public
using ()
renaming
( _<_ to _>_
; irrefl to >-irrefl
; trans to >-trans
; <-resp-≈ to >-resp-≈
; isStrictPartialOrder to >-isStrictPartialOrder
)
------------------------------------------------------------------------
-- Strict partial orders can be converted to posets
open Relation.Binary.Construct.StrictToNonStrict _≈_ _<_
poset : Poset _ _ _
poset = record
{ isPartialOrder = isPartialOrder isStrictPartialOrder
}
open Poset poset public
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