proposition: Proposition strongly_maximal_pr1 {a : A} {b : B} (Hab : @is_strongly_maximal (A × B)%dcpo (a ,, b)) : is_strongly_maximal a.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets.Basics UniMath.OrderTheory.Posets.PointedPosets UniMath.OrderTheory.Posets.MonotoneFunctions UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.ScottTopology UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.Continuous UniMath.OrderTheory.DCPOs.Elements.Maximal