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