Proposition compact_basis_laws_from_algebraic_struct {X : dcpo} (AX : algebraic_dcpo_struct X) : compact_basis_laws X (compact_basis_data_from_algebraic_struct AX). Proof. pose (CX := algebraic_dcpo_struct_to_continuous AX). simple refine (_ ,, _ ,, _). - intro b. exact (pr2 b). - intro x. pose (D := compact_approximating_family AX x). split. + assert (H := directed_set_el D). revert H. use factor_through_squash ; [ apply propproperty | ]. intro y. simple refine (hinhpr ((D y ,, _) ,, _)) ; cbn -[way_below]. * apply is_compact_approximating_family. * rewrite <- (compact_approximating_family_lub AX x). use (less_than_dcpo_lub D _ y). apply refl_dcpo. + intros y z. induction y as [ [ y Hy ] p ]. induction z as [ [ z Hz ] q ]. assert (Hxy : y ⊑ ⨆ D). { unfold D. rewrite (compact_approximating_family_lub AX x). exact p. } assert (Hxz : z ⊑ ⨆ D). { unfold D. rewrite (compact_approximating_family_lub AX x). exact q. } assert (H₁ := Hy D Hxy). revert H₁. use factor_through_squash ; [ apply propproperty | ]. intros i. induction i as [ i ri ]. assert (H₂ := Hz D Hxz). revert H₂. use factor_through_squash ; [ apply propproperty | ]. intros j. induction j as [ j rj ]. assert (H₃ := directed_set_top D i j). revert H₃. use factor_through_squash ; [ apply propproperty | ]. intros k. induction k as [ k [ s₁ s₂ ] ]. simple refine (hinhpr (((D k ,, _) ,, _) ,, (_ ,, _))). * apply is_compact_approximating_family. * cbn. rewrite <- (compact_approximating_family_lub AX x). use (less_than_dcpo_lub _ _ k). apply refl_dcpo. * exact (trans_dcpo ri s₁). * exact (trans_dcpo rj s₂). - intro x. split. + intros i. induction i as [ i p ]. exact p. + intros y Hy. rewrite <- (compact_approximating_family_lub AX x). use dcpo_lub_is_least. intro i. simple refine (Hy ((compact_approximating_family AX x i ,, _) ,, _)). * apply is_compact_approximating_family. * apply way_below_to_le. apply compact_approximating_family_way_below. Qed.
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.