Proposition strongly_maximal_pr2 {a : A} {b : B} (Hab : @is_strongly_maximal (A × B)%dcpo (a ,, b)) : is_strongly_maximal b. Proof. assert (H := nullary_interpolation CA a). revert H. use factor_through_squash_hProp. intros ( al & p ). intros x y q. pose (qp := @to_way_below_prod A B (al ,, x) (a ,, y) p q). assert (H := Hab (al ,, x) (a ,, y) qp). revert H. use factor_through_squash_hProp. intros [ H | H ]. - use hdisj_in1. exact (way_below_prod_pr2 basis_A H). - use hdisj_in2. revert H. use factor_through_squash_hProp. intros ( P₁ & P₂ & H₁ & H₂ & H₃ ). use hinhpr. refine (scott_open_pr2 P₁ a ,, scott_open_pr2 P₂ a ,, _ ,, _ ,, _) ; cbn. + exact H₁. + exact H₂. + intros z n. refine (H₃ (a ,, z) _). exact n. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets.Basics. Require Import UniMath.OrderTheory.Posets.PointedPosets. Require Import UniMath.OrderTheory.Posets.MonotoneFunctions. Require Import UniMath.OrderTheory.DCPOs.Core.DirectedSets. Require Import UniMath.OrderTheory.DCPOs.Core.Basics. Require Import UniMath.OrderTheory.DCPOs.Core.ScottContinuous. Require Import UniMath.OrderTheory.DCPOs.Core.ScottTopology. Require Import UniMath.OrderTheory.DCPOs.Core.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Elements.Maximal.