open import NeilPrelude1
open import BoolProps1
open import Ord1
module BoolOrd1 where
infix 3 _<₂_
≤false : {b : Bool} → false ≤ b
≤false {false} = refl
≤false {true} = f≤t
≤true : {b : Bool} → b ≤ true
≤true {false} = f≤t
≤true {true} = refl
≤antisym : {a b : Bool} → a ≤ b → b ≤ a → a ≡ b
≤antisym refl _ = refl
≤antisym f≤t ()
≤trans : {a b c : Bool} → a ≤ b → b ≤ c → a ≤ c
≤trans refl lt2 = lt2
≤trans f≤t lt2 = ≤false
≤total : {a b : Bool} → Either (a ≤ b) (b ≤ a)
≤total {false} = left ≤false
≤total {true} = right ≤true
data _<₂_ : Bool → Bool → Set where
f<t : false <₂ true
<trans : {a b c : Bool} → a <₂ b → b <₂ c → a <₂ c
<trans f<t ()
<trich : {a b : Bool} → Either (a ≡ b × Not (a <₂ b) × Not (b <₂ a))
(Either (Not (a ≡ b) × a <₂ b × Not (b <₂ a))
(Not (a ≡ b) × Not (a <₂ b) × b <₂ a))
<trich {false} {false} = left (refl & fork (\ ()))
<trich {false} {true} = right (left ((\ ()) & f<t & \ ()))
<trich {true} {false} = right (right ( (\ ()) & (\ ()) & f<t))
<trich {true} {true} = left (refl & fork (\ ()))
∨max : {a b : Bool} → a ≤ a ∨ b
∨max {false} = ≤false
∨max {true} = refl
∨maxR : {b : Bool} → (a : Bool) → b ≤ a ∨ b
∨maxR false = refl
∨maxR true = ≤true
∧min : {a b : Bool} → a ∧ b ≤ a
∧min {false} = refl
∧min {true} = ≤true
∧minR : {b : Bool} → (a : Bool) → a ∧ b ≤ b
∧minR true = refl
∧minR false = ≤false
≤resp∧ : {a b c d : Bool} → a ≤ c → b ≤ d → (a ∧ b) ≤ (c ∧ d)
≤resp∧ refl refl = refl
≤resp∧ {a} refl f≤t = ≤trans (∧minR a) ≤false
≤resp∧ f≤t refl = ≤false
≤resp∧ f≤t f≤t = f≤t
≤resp∧L : {a b c : Bool} → a ≤ c → (a ∧ b) ≤ (c ∧ b)
≤resp∧L = flip ≤resp∧ refl
≤resp∧R : {b c : Bool} → (a : Bool) → b ≤ c → (a ∧ b) ≤ (a ∧ c)
≤resp∧R a = ≤resp∧ {a} refl
≤false≡min : {b : Bool} → b ≤ false → b ≡ false
≤false≡min refl = refl
≥max≡max : {b : Bool} → b ≥ true → b ≡ true
≥max≡max refl = refl
≤∧L : {a b c : Bool} → a ≤ c → a ∧ b ≤ c
≤∧L = ≤trans ∧min
≤∧R : {b c : Bool} → (a : Bool) → b ≤ c → a ∧ b ≤ c
≤∧R a = ≤trans (∧minR a)
≤∨L : {a b c : Bool} → a ≤ b → a ≤ b ∨ c
≤∨L = flip ≤trans ∨max
≤∨R : {a c : Bool} → (b : Bool) → a ≤ c → a ≤ b ∨ c
≤∨R b = flip ≤trans (∨maxR b)