proposition: Lemma iscomm_union_binop : iscomm union_binop.
proof: Proof. intros ? ?; unfold union_binop, infinitary_op_to_binop; cbn. apply (invweq (hsubtype_univalence _ _)), subtype_equal_cond. use make_dirprod; intro; cbn; intros ain; apply (squash_to_prop_ishinh ain); clear ain; intro ain; induction ain as [b bin]; induction b; cbn in *; apply hinhpr. - exists false; assumption. - exists true; assumption. - exists false; assumption. - exists true; assumption. 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