{ additive =
    { unit = λ(_ : {}) → False
    , product = λ(p : { _1 : Bool, _2 : Bool }) → p._1 != p._2
    , inverse = λ(a : Bool) → a == False
    , le = λ(a : Bool) → λ(b : Bool) → if a == False then True else b
    }
  , multiplicative =
    { unit = λ(_ : {}) → True
    , product = λ(p : { _1 : Bool, _2 : Bool }) → p._1 && p._2
    , le = λ(a : Bool) → λ(b : Bool) → if b == False then True else a
    }
  }
: ../Ring/Commutative/Set Bool