------------------------------------------------------------------------
-- Properties satisfied by strict partial orders
------------------------------------------------------------------------

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 _≈_ _<_

------------------------------------------------------------------------
-- Strict partial orders can be converted to posets

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