```------------------------------------------------------------------------
-- The Agda standard library
--
-- Conversion of ≤ to <, along with a number of properties
------------------------------------------------------------------------

-- Possible TODO: Prove that a conversion ≤ → < → ≤ returns a
-- relation equivalent to the original one (and similarly for
-- < → ≤ → <).

open import Relation.Binary

module Relation.Binary.NonStrictToStrict
{a ℓ₁ ℓ₂} {A : Set a}
(_≈_ : Rel A ℓ₁) (_≤_ : Rel A ℓ₂)
where

open import Relation.Nullary
open import Relation.Binary.Consequences
open import Function
open import Data.Product
open import Data.Sum

------------------------------------------------------------------------
-- Conversion

-- _≤_ can be turned into _<_ as follows:

_<_ : Rel A _
x < y = (x ≤ y) × ¬ (x ≈ y)

------------------------------------------------------------------------
-- The converted relations have certain properties
-- (if the original relations have certain other properties)

irrefl : Irreflexive _≈_ _<_
irrefl x≈y x<y = proj₂ x<y x≈y

trans : IsPartialOrder _≈_ _≤_ → Transitive _<_
trans po = λ x<y y<z →
( PO.trans (proj₁ x<y) (proj₁ y<z)
, λ x≈z → proj₂ x<y \$ lemma (proj₁ x<y) (proj₁ y<z) x≈z
)
where
module PO = IsPartialOrder po

lemma : ∀ {x y z} → x ≤ y → y ≤ z → x ≈ z → x ≈ y
lemma x≤y y≤z x≈z =
PO.antisym x≤y \$ PO.trans y≤z (PO.reflexive \$ PO.Eq.sym x≈z)

antisym⟶asym : Antisymmetric _≈_ _≤_ → Asymmetric _<_
antisym⟶asym antisym (x≤y , ¬x≈y) (y≤x , ¬y≈x) =
¬x≈y (antisym x≤y y≤x)

<-resp-≈ : IsEquivalence _≈_ → _≤_ Respects₂ _≈_ → _<_ Respects₂ _≈_
<-resp-≈ eq ≤-resp-≈ =
(λ {x y' y} y'≈y x<y' →
( proj₁ ≤-resp-≈ y'≈y (proj₁ x<y')
, λ x≈y → proj₂ x<y' (Eq.trans x≈y (Eq.sym y'≈y))
)
) ,
(λ {y x' x} x'≈x x'<y →
( proj₂ ≤-resp-≈ x'≈x (proj₁ x'<y)
, λ x≈y → proj₂ x'<y (Eq.trans x'≈x x≈y)
))
where module Eq = IsEquivalence eq

trichotomous : Symmetric _≈_ → Decidable _≈_ →
Antisymmetric _≈_ _≤_ → Total _≤_ →
Trichotomous _≈_ _<_
trichotomous ≈-sym ≈-dec antisym total x y with ≈-dec x y
... | yes x≈y = tri≈ (irrefl x≈y) x≈y (irrefl (≈-sym x≈y))
... | no  x≉y with total x y
...   | inj₁ x≤y = tri< (x≤y , x≉y) x≉y
(x≉y ∘ antisym x≤y ∘ proj₁)
...   | inj₂ x≥y = tri> (x≉y ∘ flip antisym x≥y ∘ proj₁) x≉y
(x≥y , x≉y ∘ ≈-sym)

decidable : Decidable _≈_ → Decidable _≤_ → Decidable _<_
decidable ≈-dec ≤-dec x y with ≈-dec x y | ≤-dec x y
... | yes x≈y | _       = no (flip proj₂ x≈y)
... | no  x≉y | yes x≤y = yes (x≤y , x≉y)
... | no  x≉y | no  x≰y = no (x≰y ∘ proj₁)

isPartialOrder⟶isStrictPartialOrder :
IsPartialOrder _≈_ _≤_ → IsStrictPartialOrder _≈_ _<_
isPartialOrder⟶isStrictPartialOrder po = record
{ isEquivalence = PO.isEquivalence
; irrefl        = irrefl
; trans         = trans po
; <-resp-≈      = <-resp-≈ PO.isEquivalence PO.≤-resp-≈
} where module PO = IsPartialOrder po

isTotalOrder⟶isStrictTotalOrder :
Decidable _≈_ → IsTotalOrder _≈_ _≤_ → IsStrictTotalOrder _≈_ _<_
isTotalOrder⟶isStrictTotalOrder dec-≈ tot = record
{ isEquivalence = TO.isEquivalence
; trans         = trans TO.isPartialOrder
; compare       = trichotomous TO.Eq.sym dec-≈ TO.antisym TO.total
; <-resp-≈      = <-resp-≈ TO.isEquivalence TO.≤-resp-≈
} where module TO = IsTotalOrder tot

isDecTotalOrder⟶isStrictTotalOrder :
IsDecTotalOrder _≈_ _≤_ → IsStrictTotalOrder _≈_ _<_
isDecTotalOrder⟶isStrictTotalOrder dtot =
isTotalOrder⟶isStrictTotalOrder DTO._≟_ DTO.isTotalOrder
where module DTO = IsDecTotalOrder dtot
```