\import Data.Bool
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.LinearOrder

\instance BoolLattice : Bounded.DistributiveLattice Bool
  | <= => <=
  | <=-refl {x} => cases x constructor
  | <=-transitive {x} {y} {z} p q => cases (x,y,z,p,q) constructor
  | <=-antisymmetric {x} {y} p q => cases (x,y,p,q) idp
  | meet => and
  | meet-left {x} {y} => cases (x,y) constructor
  | meet-right {x} {y} => cases (x,y) constructor
  | meet-univ {x} {y} {z} p q => cases (x,y,z,p,q) constructor
  | join => or
  | join-left {x} {y} => cases x constructor
  | join-right {x} {y} => cases (x,y) constructor
  | join-univ {x} {y} {z} p q => cases (x,y,z,p,q) constructor
  | top => true
  | top-univ {x} => cases x constructor
  | bottom => false
  | bottom-univ => false<=_
  | ldistr>= {x} {y} {z} => cases (x,y,z) constructor
  \where {
    \data \infix  <= (x y : Bool) \with
      | false, _ => false<=_
      | true, true => true<=true
  }

\instance BoolPoset : Dec Bool
  | < => <
  | <-irreflexive => \lam {(true)} ()
  | <-transitive {x} {y} {z} => \case \elim x, \elim y, \elim z, __, __
  | trichotomy => \case \elim __, \elim __ \with {
    | true, true => equals idp
    | true, false => greater false<true
    | false, true => less false<true
    | false, false => equals idp
  }
  \where {
    \open LinearOrder

    \data \infix  < (x y : Bool) \with
      | false, true => false<true
  }