open import Relation.Binary
module Relation.Binary.Props.DecTotalOrder (dt : DecTotalOrder) where
open Relation.Binary.DecTotalOrder dt hiding (trans)
import Relation.Binary.NonStrictToStrict as Conv
open Conv _≈_ _≤_
strictTotalOrder : StrictTotalOrder
strictTotalOrder = record
{ isStrictTotalOrder = record
{ isEquivalence = isEquivalence
; trans = trans isPartialOrder
; compare = trichotomous Eq.sym _≟_ antisym total
; <-resp-≈ = <-resp-≈ isEquivalence ≤-resp-≈
}
}
open StrictTotalOrder strictTotalOrder public