Proposition is_closed_sieve_exponential (S₁ S₂ : closed_sieve) : is_closed_sieve (sieve_exponential S₁ S₂). Proof. intros x C p H y q. induction q as [ q₁ q₂ ]. cbn in *. pose (U := λ (z : X), S₁ z ∧ ∃ (a : X), C a ∧ z ≤ a). assert (∏ (w : X), U w → S₂ w) as H₁. { intro w. intros r. induction r as [ r₁ r₂ ]. revert r₂. use factor_through_squash_hProp. intros ( z & r₂ & r₃ ). use (H z r₂). split ; [ | exact r₃ ]. refine (sieve_downwards_closed S₁ _ r₁). apply isrefl_posetRelation. } assert (∏ (w : X), S₁ w → w ≤ y → S₂ w) as H₂. { intros w Hw₁ Hw₂. pose proof (cover_sharpen C (istrans_posetRelation _ _ _ _ Hw₂ q₂) p) as s. revert s. use factor_through_squash_hProp. intros ( C' & r & HC' ). use (is_closed_closed_sieve S₂ _ C' r). intros v Hv. use H₁. specialize (HC' v Hv). split ; [ | exact HC' ]. revert HC'. use factor_through_squash_hProp. intros ( s & Hs₁ & Hs₂ ). refine (sieve_downwards_closed S₁ _ Hw₁). exact (cover_downwards_closed r Hv). } use H₂. - exact q₁. - apply isrefl_posetRelation. 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.