module Order.DCPO.Free where
private variable o o' β : Level A B C : Type β open is-directed-family open Lub open Functor open _=>_ open _β£_
Free DCPOsπ
The discrete poset on a set is a DCPO. To see this, note that every semi-directed family in a discrete poset is constant. Furthermore, is directed, so it is merely inhabited.
Disc-is-dcpo : β {β} {A : Set β} β is-dcpo (Disc A) Disc-is-dcpo {A = A} .is-dcpo.directed-lubs {Ix = Ix} f dir = const-inhabited-famβlub (Disc A) disc-fam-const (dir .elt) where disc-fam-const : β i j β f i β‘ f j disc-fam-const i j = β₯-β₯-rec! (Ξ» (k , p , q) β p β sym q) (dir .semidirected i j) Disc-dcpo : (A : Set β) β DCPO β β Disc-dcpo A = Disc A , Disc-is-dcpo
This extends to a functor from to the category of DCPOs.
Free-DCPO : β {β} β Functor (Sets β) (DCPOs β β) Free-DCPO .Fβ = Disc-dcpo Free-DCPO .Fβ f = to-scott-directed f Ξ» s dir x x-lub β const-inhabited-famβis-lub (Disc _) (Ξ» ix β ap f (disc-is-lubβconst x-lub ix)) (dir .elt) Free-DCPO .F-id = scott-path (Ξ» _ β refl) Free-DCPO .F-β _ _ = scott-path (Ξ» _ β refl)
Furthermore, this functor is left adjoint to the forgetful functor to .
Free-DCPOβ£Forget-DCPO : β {β} β Free-DCPO {β} β£ Forget-DCPO Free-DCPOβ£Forget-DCPO .unit .Ξ· _ x = x Free-DCPOβ£Forget-DCPO .unit .is-natural _ _ _ = refl Free-DCPOβ£Forget-DCPO .counit .Ξ· D = to-scott-directed (Ξ» x β x) Ξ» s dir x x-lub β Ξ» where .is-lub.famβ€lub i β pathββ€ (disc-is-lubβconst x-lub i) .is-lub.least y le β β₯-β₯-rec β€-thin (Ξ» i β x =Λβ¨ disc-is-lubβconst x-lub i β©=Λ s i β€β¨ le i β©β€ y β€β) (dir .elt) where open DCPO D Free-DCPOβ£Forget-DCPO .counit .is-natural x y f = scott-path (Ξ» _ β refl) Free-DCPOβ£Forget-DCPO .zig = scott-path (Ξ» _ β refl) Free-DCPOβ£Forget-DCPO .zag = refl
Free Pointed DCPOsπ
We construct the free pointed DCPO on a set ; IE a pointed DCPO with the property that for all pointed DCPOs , functions correspond with strictly Scott-continuous maps .
To start, we define a type of partial elements of as a pair of a proposition , along with a function .
record Part {β} (A : Type β) : Type β where no-eta-equality field def : Ξ© elt : β£ def β£ β A open Part
We say that a partial element is defined when the associated proposition is true, and write to denote that is defined, and itβs value is .
is-defined : Part A β Type is-defined x? = β£ x? .def β£ _β_ : Part A β A β Type _ x β y = Ξ£[ d β is-defined x ] (x .elt d β‘ y)
Paths between partial elements are given by bi-implications of their propositions, along with a path between their values, assuming that both elements are defined.
Part-pathp : {x : Part A} {y : Part B} β (p : A β‘ B) β (q : x .def β‘ y .def) β PathP (Ξ» i β β£ q i β£ β p i) (x .elt) (y .elt) β PathP (Ξ» i β Part (p i)) x y Part-pathp {x = x} {y = y} p q r i .def = q i Part-pathp {x = x} {y = y} p q r i .elt = r i part-ext : β {x y : Part A} β (to : is-defined x β is-defined y) β (from : is-defined y β is-defined x) β (β (x-def : is-defined x) (y-def : is-defined y) β x .elt x-def β‘ y .elt y-def) β x β‘ y part-ext to from p = Part-pathp refl (Ξ©-ua to from) (funext-dep (Ξ» _ β p _ _))
Part-is-hlevel : β {A : Type β} β β n β is-hlevel A (2 + n) β is-hlevel (Part A) (2 + n) Part-is-hlevel n hl = Isoβis-hlevel (2 + n) eqv $ Ξ£-is-hlevel (2 + n) hlevel! Ξ» _ β Ξ -is-hlevel (2 + n) Ξ» _ β hl where unquoteDecl eqv = declare-record-iso eqv (quote Part) Part-is-set : is-set A β is-set (Part A) Part-is-set = Part-is-hlevel 0
We say that a partial element refines if is defined whenever is, and their values are equal whenever is defined.
record _β_ {β} {A : Type β} (x y : Part A) : Type β where no-eta-equality field implies : is-defined x β is-defined y refines : (x-def : is-defined x) β (y .elt (implies x-def) β‘ x .elt x-def) open _β_
β-is-hlevel : β {x y : Part A} β β n β is-hlevel A (2 + n) β is-hlevel (x β y) (suc n) β-is-hlevel {x = x} {y = y} n hl = Isoβis-hlevel (suc n) eqv $ Ξ£-is-hlevel (suc n) (Ξ -is-hlevel (suc n) Ξ» _ β is-propβis-hlevel-suc (y .def .is-tr)) Ξ» _ β Ξ -is-hlevel (suc n) Ξ» _ β hl _ _ where unquoteDecl eqv = declare-record-iso eqv (quote _β_)
This ordering is reflexive, transitive, and anti-symmetric, so the type of partial elements forms a poset whenever is a set.
β-refl : β {x : Part A} β x β x β-refl .implies x-def = x-def β-refl .refines _ = refl β-thin : β {x y : Part A} β is-set A β is-prop (x β y) β-thin A-set = β-is-hlevel 0 A-set β-trans : β {x y z : Part A} β x β y β y β z β x β z β-trans p q .implies x-def = q .implies (p .implies x-def) β-trans p q .refines x-def = q .refines (p .implies x-def) β p .refines x-def β-antisym : β {x y : Part A} β x β y β y β x β x β‘ y β-antisym {x = x} {y = y} p q = part-ext (p .implies) (q .implies) Ξ» x-def y-def β ap (x .elt) (x .def .is-tr _ _) β q .refines y-def Parts : (A : Set β) β Poset β β Parts A = to-poset (Part β£ A β£) mk-parts where mk-parts : make-poset _ (Part β£ A β£) mk-parts .make-poset.rel = _β_ mk-parts .make-poset.id = β-refl mk-parts .make-poset.thin = β-thin (A .is-tr) mk-parts .make-poset.trans = β-trans mk-parts .make-poset.antisym = β-antisym
Furthermore, the poset of partial elements has least upper bounds of all semidirected families.
β-lub : β {Ix : Type β} β is-set A β (s : Ix β Part A) β (β i j β β[ k β Ix ] (s i β s k Γ s j β s k)) β Part A
Let be a semidirected family, IE: for every , there merely exists some such that and . The least upper bound of shall be defined whenever there merely exists some such that is defined.
β-lub {Ix = Ix} set s dir .def = elΞ© (Ξ£[ i β Ix ] is-defined (s i))
Next, we need to construct an element of under the assumption that there exists such an . The obvious move is to use the value of , though this is hindered by the fact that there only merely exists an . However, as is a set, it suffices to show that the map is constant.
β-lub {Ix = Ix} set s dir .elt = β‘-rec-set (Ξ» pi β s (fst pi) .elt (snd pi)) (Ξ» p q i β is-const p q i .elt $ is-propβpathp (Ξ» i β (is-const p q i) .def .is-tr) (p .snd) (q .snd) i) set where abstract
To see this, we use the fact that is semidirected to obtain a such that . We can then use the fact that refines both and to obtain the desired path.
is-const : β (p q : Ξ£[ i β Ix ] is-defined (s i)) β s (p .fst) β‘ s (q .fst) is-const (i , si) (j , sj) = β₯-β₯-proj {ap = Part-is-set set _ _} $ do (k , p , q) β dir i j pure $ part-ext (Ξ» _ β sj) (Ξ» _ β si) Ξ» si sj β s i .elt si β‘Λβ¨ p .refines si β©β‘Λ s k .elt (p .implies si) β‘β¨ ap (s k .elt) (s k .def .is-tr _ _) β©β‘ s k .elt (q .implies sj) β‘β¨ q .refines sj β©β‘ s j .elt sj β
Next, we show that this actually defines a least upper bound. This is pretty straightforward, so we do not dwell on it too deeply.
β-lub-le : β {Ix : Type β} β {set : is-set A} β {s : Ix β Part A} β {dir : β i j β β[ k β Ix ] (s i β s k Γ s j β s k)} β β i β s i β β-lub set s dir β-lub-le i .implies si = inc (i , si) β-lub-le i .refines si = refl β-lub-least : β {Ix : Type β} β {set : is-set A} β {s : Ix β Part A} β {dir : β i j β β[ k β Ix ] (s i β s k Γ s j β s k)} β β x β (β i β s i β x) β β-lub set s dir β x β-lub-least {Ix = Ix} {set = set} {s = s} {dir = dir} x le .implies = β‘-rec! Ξ» si β le (si .fst) .implies (si .snd) β-lub-least {Ix = Ix} {set = set} {s = s} {dir = dir} x le .refines = β‘-elim (Ξ» _ β set _ _) Ξ» (i , si) β le i .refines si
Therefore, the type of partial elements forms a DCPO.
Parts-is-dcpo : β {A : Set β} β is-dcpo (Parts A) Parts-is-dcpo {A = A} .is-dcpo.directed-lubs s dir .Lub.lub = β-lub (A .is-tr) s (dir .semidirected) Parts-is-dcpo {A = A} .is-dcpo.directed-lubs s dir .Lub.has-lub .is-lub.famβ€lub = β-lub-le Parts-is-dcpo {A = A} .is-dcpo.directed-lubs s dir .Lub.has-lub .is-lub.least = β-lub-least Parts-dcpo : (A : Set β) β DCPO β β Parts-dcpo A = Parts A , Parts-is-dcpo
Furthermore, it forms a pointed DCPO, as it has least upper bounds of all semidirected families. However, we opt to explicitly construct a bottom for computational reasons.
never : Part A never .def = el β₯ (hlevel 1) never-β : β {x : Part A} β never β x never-β .implies () never-β .refines () Parts-is-pointed-dcpo : β {A : Set β} β is-pointed-dcpo (Parts-dcpo A) Parts-is-pointed-dcpo .Bottom.bot = never Parts-is-pointed-dcpo .Bottom.has-bottom _ = never-β Parts-pointed-dcpo : β (A : Set β) β Pointed-dcpo β β Parts-pointed-dcpo A = Parts-dcpo A , Parts-is-pointed-dcpo
Next, we shall construct a functor from to the category of pointed DCPOs that maps a set to the pointed DCPO of partial elements of .
part-map : (A β B) β Part A β Part B part-map f x .def = x .def part-map f x .elt px = f (x .elt px) part-map-β : β {f : A β B} {x y : Part A} β x β y β part-map f x β part-map f y part-map-β p .implies = p .implies part-map-β {f = f} p .refines d = ap f (p .refines d) part-map-id : β (x : Part A) β part-map (Ξ» a β a) x β‘ x part-map-id x = part-ext (Ξ» p β p) (Ξ» p β p) (Ξ» _ _ β ap (x .elt) (x .def .is-tr _ _)) part-map-β : β (f : B β C) (g : A β B) β β (x : Part A) β part-map (f β g) x β‘ part-map f (part-map g x) part-map-β f g x = part-ext (Ξ» p β p) (Ξ» p β p) (Ξ» _ _ β ap (f β g β x .elt) (x .def .is-tr _ _))
The mapping we just defined also preserves least upper bounds and bottom elements, and thus defines a functor.
part-map-lub : β {Ix : Type β} β {A : Set o} {B : Set o'} β {s : Ix β Part β£ A β£} β {dir : β i j β β[ k β Ix ] (s i β s k Γ s j β s k)} β (f : β£ A β£ β β£ B β£) β is-lub (Parts B) (part-map f β s) (part-map f (β-lub (A .is-tr) s dir)) part-map-lub f .is-lub.famβ€lub i = part-map-β (β-lub-le i) part-map-lub f .is-lub.least y le .implies = β‘-rec! Ξ» si β le (si .fst) .implies (si .snd) part-map-lub {B = B} f .is-lub.least y le .refines = β‘-elim (Ξ» _ β B .is-tr _ _) Ξ» si β le (si .fst) .refines (si .snd) part-map-never : β {f : A β B} {x} β part-map f never β x part-map-never .implies () part-map-never .refines () Free-Pointed-dcpo : Functor (Sets β) (Pointed-DCPOs β β) Free-Pointed-dcpo .Fβ A = Parts-pointed-dcpo A Free-Pointed-dcpo .Fβ {x = A} f = to-strict-scott-bottom (part-map f) (Ξ» _ _ β part-map-β) (Ξ» _ _ β part-map-lub {A = A} f) (Ξ» _ β part-map-never) Free-Pointed-dcpo .F-id = strict-scott-path part-map-id Free-Pointed-dcpo .F-β f g = strict-scott-path (part-map-β f g)
Finally, we shall show that this functor is left-adjoint to the forgetful functor into . We start by constructing the unit of the adjunction, which takes an element to .
always : A β Part A always a .def = el β€ (hlevel 1) always a .elt _ = a always-inj : β {x y : Type β} β always x β‘ always y β x β‘ y always-inj {x = x} p = J (Ξ» y p β (d : is-defined y) β x β‘ y .elt d) (Ξ» _ β refl) p tt
Next, we characterize refinements of always
, and note that it is
natural.
always-β : β {x : Part A} {y : A} β (β (d : is-defined x) β x .elt d β‘ y) β x β always y always-β p .implies _ = tt always-β p .refines d = sym (p d) always-β : β {x : A} {y : Part A} β (p : is-defined y) β x β‘ y .elt p β always x β y always-β p q .implies _ = p always-β p q .refines _ = sym q always-natural : β {x : A} β (f : A β B) β part-map f (always x) β‘ always (f x) always-natural f = part-ext (Ξ» _ β tt) (Ξ» _ β tt) Ξ» _ _ β refl
With that out of the way, we proceed to define the counit of the adjunction. Let be a partial element of a pointed DCPO . We can define an element of that approximates by taking a directed join over the proposition associated with .
part-counit : Part Ob β Ob part-counit x = β-prop (x .elt β Lift.lower) def-prop where abstract def-prop : is-prop (Lift o (is-defined x)) def-prop = hlevel!
If is defined, then the counit simply extracts the value of .
part-counit-elt : (x : Part Ob) β (p : is-defined x) β part-counit x β‘ x .elt p part-counit-elt x p = β€-antisym (β-prop-least _ _ _ Ξ» (lift p') β pathββ€ (ap (x .elt) (x .def .is-tr _ _))) (β-prop-le _ _ (lift p))
Furthermore, if is not defined, then the counit return the bottom element.
part-counit-Β¬elt : (x : Part Ob) β (is-defined x β β₯) β part-counit x β‘ bottom part-counit-Β¬elt x Β¬def = β€-antisym (β-prop-least _ _ _ (Ξ» p β absurd (Β¬def (Lift.lower p)))) (bottomβ€x _)
We also note that the counit preserves refinements, least upper bounds, and bottom elements.
part-counit-β : (x y : Part Ob) β x β y β part-counit x β€ part-counit y part-counit-β x y p = β-prop-least _ _ (part-counit y) Ξ» (lift i) β x .elt i =Λβ¨ p .refines i β©=Λ y .elt (p .implies i) β€β¨ β-prop-le _ _ (lift (p .implies i)) β©β€ β-prop (y .elt β Lift.lower) _ β€β part-counit-lub : {Ix : Type o} β (s : Ix β Part Ob) β (sdir : is-semidirected-family (Parts set) s) β is-lub poset (part-counit β s) (part-counit (β-lub (set .is-tr) s sdir)) part-counit-lub s sdir .is-lub.famβ€lub i = β-prop-least _ _ _ Ξ» (lift p) β β-prop-le _ _ (lift (inc (i , p))) part-counit-lub {Ix = Ix} s sdir .is-lub.least y le = β-prop-least _ _ _ $ Ξ» (lift p) β β‘-elim (Ξ» p β β€-thin {x = β-lub _ s sdir .elt p}) (Ξ» where (i , si) β s i .elt si β€β¨ β-prop-le _ _ (lift si) β©β€ β-prop _ _ β€β¨ le i β©β€ y β€β) p part-counit-never : β x β part-counit never β€ x part-counit-never x = β-prop-least _ _ x (absurd β Lift.lower)
We can tie this all together to obtain the desired adjunction.
Free-Pointed-dcpoβ£Forget-Pointed-dcpo : β {β} β Free-Pointed-dcpo {β} β£ Forget-Pointed-dcpo Free-Pointed-dcpoβ£Forget-Pointed-dcpo .unit .Ξ· A x = always x Free-Pointed-dcpoβ£Forget-Pointed-dcpo .unit .is-natural x y f = funext Ξ» _ β sym (always-natural f) Free-Pointed-dcpoβ£Forget-Pointed-dcpo .counit .Ξ· D = to-strict-scott-bottom (part-counit D) (part-counit-β D) (Ξ» s dir β part-counit-lub D s (dir .semidirected)) (part-counit-never D) Free-Pointed-dcpoβ£Forget-Pointed-dcpo .counit .is-natural D E f = strict-scott-path Ξ» x β sym $ Strict-scott.pres-β-prop f _ _ _ Free-Pointed-dcpoβ£Forget-Pointed-dcpo .zig {A} = strict-scott-path Ξ» x β part-ext (A?.β-prop-least _ _ x (Ξ» p β always-β (Lift.lower p) refl) .implies) (Ξ» p β A?.β-prop-le _ _ (lift p) .implies tt) (Ξ» p q β sym (A?.β-prop-least _ _ x (Ξ» p β always-β (Lift.lower p) refl) .refines p) β ap (x .elt) (x .def .is-tr _ _)) where module A? = Pointed-dcpo (Parts-pointed-dcpo A) Free-Pointed-dcpoβ£Forget-Pointed-dcpo .zag {B} = funext Ξ» x β sym $ lub-of-const-fam B.poset (Ξ» _ _ β refl) (B.β-prop-lub _ _ ) (lift tt) where module B = Pointed-dcpo B
Monad Structureπ
The adjunction from the previous section yields a monad on the category of sets, but we opt to define it by hand to get better computational behaviour.
part-ap : Part (A β B) β Part A β Part B part-ap f x .def = el (is-defined f Γ is-defined x) hlevel! part-ap f x .elt (pf , px) = f .elt pf (x .elt px) part-bind : Part A β (A β Part B) β Part B part-bind x f .def = el (Ξ£[ px β is-defined x ] is-defined (f (x .elt px))) hlevel! part-bind x f .elt (px , pfx) = f (x .elt px) .elt pfx
instance Part-Map : Map (eff Part) Part-Map .Map._<$>_ = part-map Part-Idiom : Idiom (eff Part) Part-Idiom .Idiom.Map-idiom = Part-Map Part-Idiom .Idiom.pure = always Part-Idiom .Idiom._<*>_ = part-ap Part-Bind : Bind (eff Part) Part-Bind .Bind._>>=_ = part-bind Part-Bind .Bind.Idiom-bind = Part-Idiom