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

open import NeilPrelude

module CompleteTotalOrder {A : Set}

                    (_≤_ : A → A → Set)

                    (_⊔_ : 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)
                    (total   : {a b : A} → (a ≤ b) ⊎ (b ≤ a))

                    (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 TotalOrder
open TotalOrder _≤_ antisym transit total

import CompletePartialOrder
open CompletePartialOrder _≤_ _⊔_ ⊥ reflexive antisym transit supL supR leastSup bottom public