proposition: Lemma isassoc_intersection_binop : isassoc intersection_binop.
proof: Proof. intros W Y Z. apply (invweq (hsubtype_univalence _ _)), subtype_equal_cond. use make_dirprod; cbn; intros z f b; induction b; cbn in *. + exact (f true true). + intro b; induction b; cbn in *. * exact (f true false). * exact (f false). + intro b; induction b; cbn in *. * exact (f true). * exact (f false true). + exact (f false false). 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