open import Relation.Binary
module Relation.Binary.Props.StrictPartialOrder
(spo : StrictPartialOrder)
where
open Relation.Binary.StrictPartialOrder spo
renaming (trans to <-trans)
import Relation.Binary.StrictToNonStrict as Conv
open Conv _≈_ _<_
poset : Poset
poset = record
{ isPartialOrder = record
{ isPreorder = record
{ isEquivalence = isEquivalence
; reflexive = reflexive
; trans = trans isEquivalence <-resp-≈ <-trans
; ∼-resp-≈ = ≤-resp-≈ isEquivalence <-resp-≈
}
; antisym = antisym isEquivalence <-trans irrefl
}
}
open Poset poset public