Proposition strongly_maximal_pair {a : A} {b : B} (Ha : is_strongly_maximal a) (Hb : is_strongly_maximal b) : @is_strongly_maximal (A × B)%dcpo (a ,, b). Proof. intros ( x₁ & y₁ ) ( x₂ & y₂ ) q. pose (p₁ := way_below_prod_pr1 basis_B q : x₁ ≪ x₂). pose (p₂ := way_below_prod_pr2 basis_A q : y₁ ≪ y₂). assert (H := Ha x₁ x₂ p₁). revert H. use factor_through_squash_hProp. intros H₁. assert (H := Hb y₁ y₂ p₂). revert H. use factor_through_squash_hProp. intros H₂. induction H₁ as [ H₁ | H₁ ], H₂ as [ H₂ | H₂ ]. - use hdisj_in1. use to_way_below_prod. + exact H₁. + exact H₂. - use hdisj_in2. revert H₂. use factor_through_squash_hProp. intros ( P₁ & P₂ & r₁ & r₂ & r₃ ). refine (hinhpr _). refine (prod_scott_open (true_scott_open_set _) P₁ ,, _). refine (prod_scott_open (true_scott_open_set _) P₂ ,, _ ,, _ ,, _) ; cbn. + exact (tt ,, r₁). + exact (tt ,, r₂). + intros ( x₃ & y₃ ). intros ( ( _ & s₁ ) & ( _ & s₂ ) ) ; cbn in s₁, s₂. exact (r₃ _ (s₁ ,, s₂)). - use hdisj_in2. revert H₁. use factor_through_squash_hProp. intros ( P₁ & P₂ & r₁ & r₂ & r₃ ). refine (hinhpr _). refine (prod_scott_open P₁ (true_scott_open_set _) ,, _). refine (prod_scott_open P₂ (true_scott_open_set _) ,, _ ,, _ ,, _) ; cbn. + exact (r₁ ,, tt). + exact (r₂ ,, tt). + intros ( x₃ & y₃ ). intros ( ( s₁ & _ ) & ( s₂ & _ ) ) ; cbn in s₁, s₂. exact (r₃ _ (s₁ ,, s₂)). - use hdisj_in2. revert H₁. use factor_through_squash_hProp. intros ( P₁ & P₂ & r₁ & r₂ & r₃ ). refine (hinhpr _). refine (prod_scott_open P₁ (true_scott_open_set _) ,, _). refine (prod_scott_open P₂ (true_scott_open_set _) ,, _ ,, _ ,, _) ; cbn. + exact (r₁ ,, tt). + exact (r₂ ,, tt). + intros ( x₃ & y₃ ). intros ( ( s₁ & _ ) & ( s₂ & _ ) ) ; cbn in s₁, s₂. exact (r₃ _ (s₁ ,, s₂)). 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.