Proposition way_below_ideal_completion_eq (I J : rounded_ideal_completion) : I ≪ J ≃ ∃ b₁, b₁ ∈ J ∧ I ⊑ principal_ideal b₁. Proof. use weqimplimpl. - apply from_way_below_ideal_completion. - use factor_through_squash. { apply propproperty. } intros [b [HJ HI]]. apply (to_way_below_ideal_completion b HJ HI). - apply propproperty. - apply propproperty. Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.Posets. 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.WayBelow. Require Import UniMath.OrderTheory.DCPOs.Basis.Continuous. Require Import UniMath.OrderTheory.DCPOs.Basis.Algebraic. Require Import UniMath.OrderTheory.DCPOs.Basis.Basis. Require Import UniMath.OrderTheory.DCPOs.Basis.CompactBasis. Require Import UniMath.OrderTheory.DCPOs.Elements.Maximal. Require Import UniMath.OrderTheory.DCPOs.Examples.Products. Require Import UniMath.OrderTheory.DCPOs.Examples.SubDCPO. Require Import UniMath.OrderTheory.DCPOs.Examples.Propositions.