Proposition strongly_maximal_pr1 {a : A} {b : B} (Hab : @is_strongly_maximal (A × B)%dcpo (a ,, b)) : is_strongly_maximal a. Proof. assert (H := nullary_interpolation CB b). revert H. use factor_through_squash_hProp. intros ( bl & p ). intros x y q. pose (qp := @to_way_below_prod A B (x ,, bl) (y ,, b) q p). assert (H := Hab (x ,, bl) (y ,, b) qp). revert H. use factor_through_squash_hProp. intros [ H | H ]. - use hdisj_in1. exact (way_below_prod_pr1 basis_B H). - use hdisj_in2. revert H. use factor_through_squash_hProp. intros ( P₁ & P₂ & H₁ & H₂ & H₃ ). use hinhpr. refine (scott_open_pr1 P₁ b ,, scott_open_pr1 P₂ b ,, _ ,, _ ,, _) ; cbn. + exact H₁. + exact H₂. + intros z n. refine (H₃ (z ,, b) _). 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.