{-# OPTIONS --type-in-type
    #-}

open import NeilPrelude

module PreOrder {A : Set} (_≤'_ : A → A → Set)

                    (reflex  : Reflexive _≤'_)
                    (transit : Transitive _≤'_)

where

infix  _≤_ _≥_

_≤_ : A → A → Set
_≤_ = _≤'_

_≥_ : A → A → Set
a ≥ b = b ≤ a

reflexive : Reflexive _≤_
reflexive = reflex

transitive : Transitive _≤_
transitive = transit

transitive2 : Transitive2 _≤_
transitive2 ab bc cd = transitive ab (transitive bc cd)

transitive3 : Transitive3 _≤_
transitive3 ab bc cd de = transitive2 ab bc (transitive cd de)

≡implies≤ : {a b : A} → a ≡ b → a ≤ b
≡implies≤ refl = reflex

≤subst : {a b c d : A} → b ≡ a → d ≡ c → a ≤ c → b ≤ d
≤subst refl refl = id

≤substL : {a b c : A} → b ≡ a → a ≤ c → b ≤ c
≤substL = flip ≤subst refl

≤substR : {a b c : A} → c ≡ b → a ≤ b → a ≤ c
≤substR = ≤subst refl

-----------------------------------------------------------------

infixr  _≤⟨_⟩_
infix   _QED

_≤⟨_⟩_ : {b c : A} → (a : A) → a ≤ b → b ≤ c → a ≤ c
_ ≤⟨ ab ⟩ bc = transitive ab bc

_QED : (a : A) → a ≤ a
_ QED = reflex

-----------------------------------------------------------------