Definition strongly_maximal_prod_weq (a : A) (b : B) : @is_strongly_maximal (A × B)%dcpo (a ,, b) ≃ (is_strongly_maximal a ∧ is_strongly_maximal b). Proof. use logeqweq. - exact (λ p, strongly_maximal_pr1 p ,, strongly_maximal_pr2 p). - exact (λ p, strongly_maximal_pair (pr1 p) (pr2 p)). Defined.
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.