Lemma isassoc_union_binop : isassoc union_binop. 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.
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.