Lemma isassoc_intersection_binop : isassoc intersection_binop. 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.
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.