Proposition exponential_laws_set_of_closed_sieves (S₁ S₂ S₃ : closed_sieve) : Lle bounded_lattice_set_of_closed_sieves S₃ (closed_sieve_exponential S₁ S₂) <-> Lle bounded_lattice_set_of_closed_sieves (Lmin bounded_lattice_set_of_closed_sieves S₃ S₁) S₂. Proof. split ; cbn. - intro H. use eq_closed_sieve. use eq_sieve ; intro x ; cbn. + intros rpq. exact (pr11 rpq ,, pr21 rpq). + intros rp. refine (rp ,, _). use (pr2 (eq_sieve_r (maponpaths pr1 H) x (pr1 rp))). refine (pr2 rp ,, _). apply isrefl_posetRelation. - intro H. use eq_closed_sieve. use eq_sieve ; intro x ; cbn. + intros rpq. exact (pr1 rpq). + intros r. refine (r ,, _). intros y pq. induction pq as [ p q ]. refine (pr2 (eq_sieve_r (maponpaths pr1 H) y _)) ; cbn. exact (sieve_downwards_closed S₃ q r ,, 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.