Proposition lattice_laws_set_of_sieves : @islatticeop set_of_sieves sieve_intersection sieve_union. Proof. repeat split. - intros S₁ S₂ S₃. use eq_sieve ; intro x ; cbn. + intros pqr. induction pqr as [ [ p q ] r ]. exact (p ,, q ,, r). + intros pqr. induction pqr as [ p [ q r ]]. exact ((p ,, q) ,, r). - intros S₁ S₂. use eq_sieve ; intro x ; cbn. + intros pq. induction pq as [ p q ]. exact (q ,, p). + intros pq. induction pq as [ p q ]. exact (q ,, p). - intros S₁ S₂ S₃. use eq_sieve ; intro x. + use factor_through_squash_hProp. intros pqr. induction pqr as [ pq | r ]. * revert pq. use factor_through_squash_hProp. intros pq. induction pq as [ p | q ]. ** exact (hinhpr (inl p)). ** exact (hinhpr (inr (hinhpr (inl q)))). * exact (hinhpr (inr (hinhpr (inr r)))). + use factor_through_squash_hProp. intros pqr. induction pqr as [ p | qr ]. * exact (hinhpr (inl (hinhpr (inl p)))). * revert qr. use factor_through_squash_hProp. intros qr. induction qr as [ q | r ]. ** exact (hinhpr (inl (hinhpr (inr q)))). ** exact (hinhpr (inr r)). - intros S₁ S₂. use eq_sieve ; intro x. + use factor_through_squash_hProp. intros pq. induction pq as [ p | q ]. * exact (hinhpr (inr p)). * exact (hinhpr (inl q)). + use factor_through_squash_hProp. intros pq. induction pq as [ p | q ]. * exact (hinhpr (inr p)). * exact (hinhpr (inl q)). - intros S₁ S₂. use eq_sieve ; intro x. + intros pq. induction pq as [ p pq ]. exact p. + intros p. exact (p ,, hinhpr (inl p)). - intros S₁ S₂. use eq_sieve ; intro x. + use factor_through_squash_hProp. intros pq. induction pq as [ p | pq ]. * exact p. * exact (pr1 pq). + intros p. exact (hinhpr (inl p)). Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. 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.Heyting. Require Import UniMath.OrderTheory.Lattice.CompleteHeyting. Require Import UniMath.OrderTheory.Lattice.Examples.FromPartialOrder.