module Order.DCPO.Free where

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:

  ⊑-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
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 $_)

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