proposition: Proposition preorder_to_abstract_basis_laws : abstract_basis_laws preorder_to_abstract_basis_data.
proof: Proof. repeat split. - apply istrans_po. - intros a. refine (hinhpr (a ,, _)). apply isrefl_po. - intros a₁ a₂ b p q. refine (hinhpr (b ,, _ ,, p ,, q)). apply isrefl_po. Qed.
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