Definition complemented_structure : UU := ∏ x : X, complement x.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.Foundations.Sets. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded.