open import Cat.Displayed.Univalence.Thin
open import Cat.Functor.Subcategory
open import Cat.Displayed.Total
open import Cat.Prelude

open import Data.Partial.Properties
open import Data.Partial.Base
open import Data.Sum

open import Order.Instances.Discrete
open import Order.Diagram.Bottom
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 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-fam-const (dir .elt)
where
disc-fam-const : β i j β f i β‘ f j
disc-fam-const i j = case dir .semidirected i j of Ξ» k p q β p β sym q

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
(Ξ» ix β ap f (disc-is-lubβconst x-lub ix))
(dir .elt)
Free-DCPO .F-id = trivial!
Free-DCPO .F-β _ _ = trivial!


Furthermore, this functor is left adjoint to the forgetful functor to

Free-DCPOβ£Forget-DCPO : β {β} β Free-DCPO {β} β£ DCPOsβͺSets
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 β β€-refl' (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 = trivial!
Free-DCPOβ£Forget-DCPO .zig = trivial!
Free-DCPOβ£Forget-DCPO .zag = refl


# Free pointed DCPOsπ

The purpose of this section is to establish that the free pointed DCPO on a set is given by its partial elements We have already constructed the order we will use, the information ordering, and established some of its basic order-theoretic properties, so that we immediately get a poset of partial elements:

Parts : (A : Set β) β Poset β β
Parts A .Poset.Ob        = β― β£ A β£
Parts A .Poset._β€_       = _β_
Parts A .Poset.β€-thin    = hlevel 1
Parts A .Poset.β€-refl    = β-refl
Parts A .Poset.β€-trans   = β-trans
Parts A .Poset.β€-antisym = β-antisym


Unfortunately, the hardest two parts of the construction remain:

1. We must show that has least upper bounds for all semidirected families, i.e., that it is actually a DCPO;

2. We must show that this construction is actually free, meaning that every map to a pointed DCPO extends uniquely to a strictly Scott-continuous

We will proceed in this order.

## Directed joins of partial elementsπ

β-lub
: {Ix : Type β} β¦ _ : H-Level A 2 β¦ (s : Ix β β― A)
β (semi : β i j β β[ k β Ix ] (s i β s k Γ s j β s k))
β β― A


Suppose that is a semidirected family of partial elements β which, recall, means that for each we can merely find satisfying and We decree that the join is defined whenever there exists such that is defined.

β-lub {Ix = Ix} s dir .def = elΞ© (Ξ£[ i β Ix ] β 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 itself. However, we only merely have such an and weβre not mapping into a proposition β weβre mapping into a set. But thatβs not a major impediment: weβre allowed to make this choice, as long as we show that the function is constant.

β-lub {Ix = Ix} s dir .elt =
β‘-rec-set (hlevel 2) (Ξ» (ix , def) β s ix .elt def) (Ξ» 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) where abstract  So imagine that we have two indices with and both defined. We must show that Since is semidirected, and weβre showing a proposition, we may assume that there is some satisfying and We then compute:  is-const : β (p q : Ξ£[ i β Ix ] β s i β) β s (p .fst) β‘ s (q .fst) is-const (i , si) (j , sj) = β₯-β₯-out! do (k , p , q) β dir i j pure$ part-ext (Ξ» _ β sj) (Ξ» _ β si) Ξ» si sj β
s i .elt _   β‘Λβ¨ p .refines si β©β‘Λ
s k .elt _   β‘β¨ β―-indep (s k) β©β‘
s k .elt _   β‘β¨ q .refines sj β©β‘
s j .elt _   β


After having constructed the element, weβre still left with proving that this is actually a least upper bound. This turns out to be pretty straightforward, so we present the solution without further comments:

module
_ {Ix : Type β} β¦ set : H-Level A 2 β¦ {s : Ix β β― A}
{dir : β i j β β[ k β Ix ] (s i β s k Γ s j β s k)}
where

  β-lub-le : β i β s i β β-lub s dir
β-lub-le i .implies si = inc (i , si)
β-lub-le i .refines si = refl

β-lub-least
: β x β (β i β s i β x) β β-lub s dir β x
β-lub-least x le .implies = rec! Ξ» i si β le i .implies si
β-lub-least x le .refines = elim! Ξ» i si β le i .refines si

open is-dcpo
open is-lub
open Bottom
open Lub

Parts-is-dcpo : β {A : Set β} β is-dcpo (Parts A)
Parts-is-dcpo {A = A} .directed-lubs s dir .lub =
β-lub s (dir .semidirected)
Parts-is-dcpo {A = A} .directed-lubs s dir .has-lub .famβ€lub = β-lub-le
Parts-is-dcpo {A = A} .directed-lubs s dir .has-lub .least = β-lub-least

Parts-dcpo : (A : Set β) β DCPO β β
Parts-dcpo A = Parts A , Parts-is-dcpo


Furthermore, itβs a pointed DCPO, since we additionally have a bottom element.

Parts-is-pointed-dcpo : β {A : Set β} β is-pointed-dcpo (Parts-dcpo A)
Parts-is-pointed-dcpo .bot          = never
Parts-is-pointed-dcpo .has-bottom _ = never-β

Parts-pointed-dcpo : β (A : Set β) β Pointed-dcpo β β
Parts-pointed-dcpo A = Parts-dcpo A , Parts-is-pointed-dcpo


Finally, we note that the functorial action of the partiality monad preserves these directed joins. Since itβs valued in strict Scott-continuous maps, this action extends to a proper functor from the category to the category of pointed dcpos.

part-map-lub
: {Ix : Type β} {A : Set o} {B : Set o'} {s : Ix β β― β£ 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 s dir))
part-map-lub f .famβ€lub i = part-map-β (β-lub-le i)
part-map-lub f .least y le .implies = rec! Ξ» i si β le i .implies si
part-map-lub {B = B} f .least y le .refines = elim! Ξ» i si β le i .refines si

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 = ext (part-map-id $_) Free-Pointed-dcpo .F-β f g = ext (part-map-β f g$_)

module _ (D : Pointed-dcpo o β) where
open Pointed-dcpo D


## The universal propertyπ

It remains to show that this functor is actually a left adjoint. We have already constructed the adjunction unit: it is the map always which embeds into We turn to defining the counit. Since every pointed dcpo admits joins indexed by propositions, given a we can define to be the join

  part-counit : β― Ob β Ob
part-counit x = β-prop (x .elt β Lift.lower) def-prop where abstract
def-prop : is-prop (Lift o β x β)
def-prop = hlevel 1


We can characterise the behaviour of this definition as though it were defined by cases: if is defined, then this simply yields its value. And if is undefined, then this is the bottom element.

  part-counit-elt : (x : β― Ob) (p : β x β) β part-counit x β‘ x .elt p
part-counit-elt x p = β€-antisym
(β-prop-least _ _ _ Ξ» (lift p') β β€-refl' (β―-indep x))
(β-prop-le _ _ (lift p))

part-counit-Β¬elt : (x : β― Ob) β (β x β β β₯) β part-counit x β‘ bottom
part-counit-Β¬elt x Β¬def = β€-antisym
(β-prop-least _ _ _ (Ξ» p β absurd (Β¬def (Lift.lower p))))
(bottomβ€x _)


The following three properties are fundamental: the counit

1. preserves the information order; and
2. preserves directed joins; and
3. preserves the bottom element.
  part-counit-β : β {x y} β x β y β part-counit x β€ part-counit y
part-counit-lub
: β {Ix} s (sdir : is-semidirected-family (Parts set) {Ix} s)
β is-lub poset (part-counit β s) (part-counit (β-lub s sdir))
part-counit-never : β x β part-counit never β€ x

The proofs here are simply calculations. We leave them for the curious reader.
  part-counit-β {x = x} {y = 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 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}) (Ξ» (i , si) β s i .elt si β€β¨ β-prop-le _ _ (lift si) β©β€ β-prop _ _ β€β¨ le i β©β€ y β€β) p part-counit-never x = β-prop-least _ _ x (Ξ» ())  We can tie this all together to obtain the desired adjunction. Free-Pointed-dcpoβ£Forget-Pointed-dcpo : β {β} β Free-Pointed-dcpo {β} β£ Pointed-DCPOsβͺSets Free-Pointed-dcpoβ£Forget-Pointed-dcpo .unit .Ξ· A x = always x Free-Pointed-dcpoβ£Forget-Pointed-dcpo .unit .is-natural x y f = ext Ξ» _ β 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 = ext Ξ» x β sym$ Strict-scott.pres-β-prop f _ _ _

Free-Pointed-dcpoβ£Forget-Pointed-dcpo .zig {A} = ext Ξ» 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)
β β―-indep x)
where module A? = Pointed-dcpo (Parts-pointed-dcpo A)

Free-Pointed-dcpoβ£Forget-Pointed-dcpo .zag {B} = ext Ξ» x β
sym \$ lub-of-const-fam (Ξ» _ _ β refl) (B.β-prop-lub _ _ ) (lift tt)
where module B = Pointed-dcpo B