Proposition exponential_scott_open_law (P Q R : scott_open_set D) : scott_open_set_intersection R (scott_open_set_exp P Q) = R <-> scott_open_set_intersection (scott_open_set_intersection R P) Q = scott_open_set_intersection R P. Proof. split ; intro H ; use eq_scott_open_set ; intro x. - cbn. exact pr1. - cbn. intros p. refine (p ,, _). refine (factor_through_squash_hProp _ _ (pr2 (pr2 (weqlogeq _ _ (maponpaths (λ R, pr1 R x) H)) (pr1 p)))). intro j. induction j as [ [ S HS₁ ] HS₂ ] ; cbn in HS₂. apply HS₁. exact (pr2 p ,, HS₂). - intro p. induction p as [ p q ]. exact p. - intro p. refine (p ,, _). use hinhpr. simple refine ((_ ,, _) ,, _). + exact R. + cbn. intros y q. apply (pr2 (weqlogeq _ _ (maponpaths (λ R, pr1 R y) H))) ; cbn. exact (pr2 q ,, pr1 q). + exact p. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Examples.IdealCompletion. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.OrderTheory.Lattice.Heyting. Require Import UniMath.OrderTheory.Lattice.CompleteHeyting.