Definition complement (x : X) : UU := ∑ y : X, (x ⊕ y = ⊤) × (x ⊗ y = ⊥).
Require Import UniMath.Foundations.Preamble. Require Import UniMath.Foundations.Sets. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.