proposition: Lemma iscomm_intersection_binop : iscomm intersection_binop.
proof: Proof. intros ? ?; unfold intersection_binop, infinitary_op_to_binop; cbn. apply (invweq (hsubtype_univalence _ _)), subtype_equal_cond. use make_dirprod; intro; cbn; intros f b; induction b. - exact (f false). - exact (f true). - exact (f false). - exact (f true). Qed.
imports: UniMath.Foundations.Preamble UniMath.Foundations.PartA UniMath.Foundations.Sets UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Propositions UniMath.MoreFoundations.Subtypes UniMath.Algebra.BinaryOperations UniMath.OrderTheory.Lattice.Lattice UniMath.OrderTheory.Lattice.Bounded UniMath.OrderTheory.Lattice.Distributive UniMath.OrderTheory.Lattice.Complement UniMath.OrderTheory.Lattice.Boolean