open import Cat.Displayed.Total
open import Cat.Prelude

open import Data.Sum

open import Order.Instances.Discrete
open import Order.DCPO.Pointed
open import Order.Diagram.Lub
open import Order.Base
open import Order.DCPO

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 $A$ is a DCPO. To see this, note that every semi-directed family $f : I \to A$ in a discrete poset is constant. Furthermore, $f$ 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 $\mathbf{Sets}$ 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 $\mathbf{Sets}$.

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 $A$; IE a pointed DCPO $A_{\bot}$ with the property that for all pointed DCPOs $B$, functions $A \to B$ correspond with strictly Scott-continuous maps $A_{\bot} \to B$.

To start, we define a type of partial elements of $A$ as a pair of a proposition $\varphi$, along with a function $\varphi \to A$.

record Part {β} (A : Type β) : Type β where
no-eta-equality
field
elt : β£ def β£ β A

open Part


We say that a partial element $x$ is defined when the associated proposition is true, and write $x \downarrow y$ to denote that $x$ is defined, and itβs value is $y$.

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
(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 $y$ refines $x$ if $y$ is defined whenever $x$ is, and their values are equal whenever $x$ 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 $A$ 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 $s : I \to A$ be a semidirected family, IE: for every $i, j : I$, there merely exists some $k : I$ such that $s(i) \sqsubseteq s(k)$ and $s(j) \sqsubseteq s(k)$. The least upper bound of $s$ shall be defined whenever there merely exists some $i : I$ such that $s(i)$ is defined.

β-lub {Ix = Ix} set s dir .def = elΞ© (Ξ£[ i β Ix ] is-defined (s i))


Next, we need to construct an element of $A$ under the assumption that there exists such an $i$. The obvious move is to use the value of $s(i)$, though this is hindered by the fact that there only merely exists an $i$. However, as $A$ is a set, it suffices to show that the map $(i , \varphi_i) \mapsto s(i)(\varphi_i)$ 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 $s$ is semidirected to obtain a $k$ such that $s(i), s(j) \sqsubseteq s(k)$. We can then use the fact that $s(k)$ refines both $s(i)$ and $s(j)$ 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 $\mathbf{Sets}$ to the category of pointed DCPOs that maps a set $A$ to the pointed DCPO of partial elements of $A$. 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 $\mathbf{Sets}$. We start by constructing the unit of the adjunction, which takes an element $a : A$ to $\top, \lambda tt. a$. 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 $x$ be a partial element of a pointed DCPO $D$. We can define an element of $D$ that approximates $x$ by taking a directed join over the proposition associated with $x$. module _ (D : Pointed-dcpo o β) where open Pointed-dcpo D   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 $x$ is defined, then the counit simply extracts the value of $x$.  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 $x$ 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


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