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