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

open import NeilPrelude

module CompletePartialOrder {A : Set}

                    (_≤_ : A → A → Set)

                    (_⊔_ : A → A → A)

                    (⊥ : A)

                    (reflex   : {a : A} → a ≤ a)
                    (antisym  : {a b : A} → a ≤ b → b ≤ a → a ≡ b)
                    (transit  : {a b c : A} → a ≤ b → b ≤ c → a ≤ c)

                    (supL     : {a b : A} → a ≤ (a ⊔ b))
                    (supR     : {a b : A} → a ≤ (b ⊔ a))

                    (leastSup : {x a b : A} → a ≤ x → b ≤ x → (a ⊔ b) ≤ x)

                    (bottom   : {a : A} → ⊥ ≤ a)

where

import DirectedCompletePartialOrder
open DirectedCompletePartialOrder _≤_ _⊔_ reflex antisym transit supL supR leastSup public

unitL : {a : A} → ⊥ ⊔ a ≡ a
unitL = antisym (leastSup bottom reflex) supR

import CommMonoid
open CommMonoid _⊔_ associative commutative ⊥ unitL public

≤bot : {a : A} → a ≤ ⊥ → a ≡ ⊥
≤bot p = antisym p bottom

botSplit : {a b : A} → (a ⊔ b) ≡ ⊥ → (a ≡ ⊥) × (b ≡ ⊥)
botSplit = (≤bot ∥ ≤bot) ∘ leastSupR ∘ ≡implies≤