{ join =
    { unit = λ(_ : {}) → False
    , product = λ(p : { _1 : Bool, _2 : Bool }) → p._1 || p._2
    , le = λ(a : Bool) → λ(b : Bool) → if a == False then True else b
    }
  , meet =
    { unit = λ(_ : {}) → True
    , product = λ(p : { _1 : Bool, _2 : Bool }) → p._1 && p._2
    , le = λ(a : Bool) → λ(b : Bool) → if b == False then True else a
    }
  , complement = λ(a : Bool) → a == False
  }
: ../Lattice/Complemented/Set Bool