proposition: Proposition way_below_ideal_completion_eq (I J : rounded_ideal_completion) : I ≪ J ≃ ∃ b₁, b₁ ∈ J ∧ I ⊑ principal_ideal b₁.
proof: 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.
imports: UniMath.MoreFoundations.All UniMath.OrderTheory.Posets UniMath.OrderTheory.DCPOs.Core.DirectedSets UniMath.OrderTheory.DCPOs.Core.Basics UniMath.OrderTheory.DCPOs.Core.ScottContinuous UniMath.OrderTheory.DCPOs.Core.WayBelow UniMath.OrderTheory.DCPOs.Basis.Continuous UniMath.OrderTheory.DCPOs.Basis.Algebraic UniMath.OrderTheory.DCPOs.Basis.Basis UniMath.OrderTheory.DCPOs.Basis.CompactBasis UniMath.OrderTheory.DCPOs.Elements.Maximal UniMath.OrderTheory.DCPOs.Examples.Products UniMath.OrderTheory.DCPOs.Examples.SubDCPO UniMath.OrderTheory.DCPOs.Examples.Propositions