Lemma distributive_lattice_complements_are_unique : is_distributive L -> ∏ x, isaprop (complement L x). Proof. intros is_distr x; apply invproofirrelevance; intros b a. apply subtypePath. - intro. apply isapropdirprod; apply setproperty. - refine (!islunit_Lmin_Ltop L (pr1 b) @ _ @ islunit_Lmin_Ltop L (pr1 a)). refine (_ @ maponpaths (fun z => Lmin L z _) (complement_top_axiom _ _ b)). refine (iscomm_Lmin _ _ _ @ _ @ iscomm_Lmin _ _ _). refine (!maponpaths (fun z => Lmin L _ z) (complement_top_axiom _ _ a) @ _). refine (is_distr _ _ _ @ _ @ !is_distr _ _ _). refine (iscomm_Lmax _ _ _ @ _ @iscomm_Lmax _ _ _ ). refine (maponpaths _ (iscomm_Lmin _ _ _) @ _ @ maponpaths _ (iscomm_Lmin _ _ _)). refine (maponpaths _ (complement_bottom_axiom _ _ b) @ _). refine (_ @ !maponpaths _ (complement_bottom_axiom _ _ a)). refine (_ @ maponpaths (fun z => Lmax L z _) (iscomm_Lmin _ _ _)). reflexivity. Qed.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.Algebra.Monoids. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.OrderTheory.Lattice.Complement.