open import Cat.Displayed.Total
open import Cat.Functor.Adjoint
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 AA is a DCPO. To see this, note that every semi-directed family f:I→Af : I \to A in a discrete poset is constant. Furthermore, ff 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 Sets\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 Sets\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 AA; IE a pointed DCPO AβŠ₯A_{\bot} with the property that for all pointed DCPOs BB, functions Aβ†’BA \to B correspond with strictly Scott-continuous maps AβŠ₯β†’BA_{\bot} \to B.

To start, we define a type of partial elements of AA as a pair of a proposition Ο†\varphi, along with a function Ο†β†’A\varphi \to A.

record Part {β„“} (A : Type β„“) : Type β„“ where
  no-eta-equality
  field
    def : Ξ©
    elt : ∣ def ∣ β†’ A

open Part

We say that a partial element xx is defined when the associated proposition is true, and write x↓yx \downarrow y to denote that xx is defined, and it’s value is yy.

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 yy refines xx if yy is defined whenever xx is, and their values are equal whenever xx 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 AA 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β†’As : I \to A be a semidirected family, IE: for every i,j:Ii, j : I, there merely exists some k:Ik : I such that s(i)βŠ‘s(k)s(i) \sqsubseteq s(k) and s(j)βŠ‘s(k)s(j) \sqsubseteq s(k). The least upper bound of ss shall be defined whenever there merely exists some i:Ii : I such that s(i)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 AA under the assumption that there exists such an ii. The obvious move is to use the value of s(i)s(i), though this is hindered by the fact that there only merely exists an ii. However, as AA is a set, it suffices to show that the map (i,Ο†i)↦s(i)(Ο†i)(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 ss is semidirected to obtain a kk such that s(i),s(j)βŠ‘s(k)s(i), s(j) \sqsubseteq s(k). We can then use the fact that s(k)s(k) refines both s(i)s(i) and s(j)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 Sets\mathbf{Sets} to the category of pointed DCPOs that maps a set AA to the pointed DCPO of partial elements of AA.

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 Sets\mathbf{Sets}. We start by constructing the unit of the adjunction, which takes an element a:Aa : A to ⊀,λtt.a\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 xx be a partial element of a pointed DCPO DD. We can define an element of DD that approximates xx by taking a directed join over the proposition associated with xx.

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 xx is defined, then the counit simply extracts the value of xx.

  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 xx 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