open import Cat.Displayed.Univalence.Thin
open import Cat.Functor.Subcategory
open import Cat.Displayed.Total
open import Cat.Functor.Adjoint
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 βŠ™ 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 (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 βŠ™ 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-βŠ’ (lower p , refl)) .implies)
  (Ξ» p β†’ A?.⋃-prop-le _ _ (lift p) .implies tt)
  (Ξ» p q β†’
    sym (A?.⋃-prop-least _ _ x (Ξ» p β†’ always-βŠ’ (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