Lemma iscomm_intersection_binop : iscomm intersection_binop. 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.
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.