```\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 4 <= (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 4 < (x y : Bool) \with
| false, true => false<true
}
```