Lemma subset_lattice_is_complemented : LEM -> complemented_structure (make_bounded_lattice subset_lattice_is_bounded). Proof. intros lem sub. exists (subtype_complement sub). use make_dirprod. - apply (invweq (hsubtype_univalence _ _)). eapply (subtype_complement_union lem). + exists true; reflexivity. + exists false; reflexivity. - apply (invweq (hsubtype_univalence _ _)). eapply subtype_complement_intersection_empty. + exists true; reflexivity. + exists false; reflexivity. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Sets. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.OrderTheory.Lattice.Distributive. Require Import UniMath.OrderTheory.Lattice.Complement. Require Import UniMath.OrderTheory.Lattice.Boolean.