module Cat.Diagram.Monad.Relative where

Relative extension systemsπŸ”—

By definition, monads must be endofunctors. For most applications, this is sufficient, and the theory of monads is quite rich. However, this restriction can become problematic. As an example, let be a monad on interpreted as an algebraic theory, where each fibre is interpreted as the syntax of with variables. In this situation, the unit interprets a variable as a term, and the multiplication performs substitution.

However, we might wish to give a more refined treatment of variables1, then we immediately run into issues: We want to restrict domain away from being an endofunctor but we can’t make it into an endofunctor on either! In all but the most trivial situations, the collection of syntax trees on even a single variable is infinite.

So, if we want to work in a scenario like this, we will need to generalise the notion of monad. The fundamental impediment is that we can not take iterated composites of a functor so the unit-and-multiplication presentation of monads will not do. However, we can consider an alternative starting point: extension systems, where the problematic multiplication is replaced with an extension operation, written

Since the type of the extension operation does not mention iterated composites of we have cleared the main obstruction. It remains to see that we can actually achieve something. Following (Altenkirch, Chapman, and Uustalu 2015), we define a relative extension system, over a functor as:

  1. A mapping of objects, and

  2. A family of unit morphisms, and

  3. An extension operation,

Like their non-relative counterparts, we do not require any functoriality or naturality.

  record Relative-extension-system : Type (oj βŠ” oc βŠ” β„“c) where
    no-eta-equality
    field
      Mβ‚€ : J.Ob β†’ C.Ob
      unit : βˆ€ {x} β†’ C.Hom (F.β‚€ x) (Mβ‚€ x)
      bind : βˆ€ {x y} β†’ C.Hom (F.β‚€ x) (Mβ‚€ y) β†’ C.Hom (Mβ‚€ x) (Mβ‚€ y)

The equations for a relative extension system are similar to the non-relative case.

      bind-unit-id : βˆ€ {x} β†’ bind (unit {x}) ≑ C.id
      bind-unit-∘ : βˆ€ {x y} (f : C.Hom (F.β‚€ x) (Mβ‚€ y)) β†’ bind f C.∘ unit ≑ f
      bind-∘
        : βˆ€ {x y z}
        β†’ (f : C.Hom (F.β‚€ y) (Mβ‚€ z)) (g : C.Hom (F.β‚€ x) (Mβ‚€ y))
        β†’ bind f C.∘ bind g ≑ bind (bind f C.∘ g)

The functorial action of on can be recovered by extending

    M₁ : βˆ€ {x y} β†’ J.Hom x y β†’ C.Hom (Mβ‚€ x) (Mβ‚€ y)
    M₁ f = bind (unit C.∘ F.₁ f)

Furthermore, the latter two equations ensure naturality of the unit and extension, respectively.

    unit-natural
      : βˆ€ {x y} (f : J.Hom x y)
      β†’ unit C.∘ F.₁ f ≑ M₁ f C.∘ unit
    unit-natural f =
      unit C.∘ F.₁ f                 β‰‘Λ˜βŸ¨ bind-unit-∘ (unit C.∘ F.₁ f) βŸ©β‰‘Λ˜
      bind (unit C.∘ F.₁ f) C.∘ unit ∎

    bind-naturall
      : βˆ€ {x y z} (f : J.Hom y z) (g : C.Hom (F.β‚€ x) (Mβ‚€ y))
      β†’ M₁ f C.∘ bind g ≑ bind (M₁ f C.∘ g)
    bind-naturall f g =
      bind (unit C.∘ F.₁ f) C.∘ bind g   β‰‘βŸ¨ bind-∘ (unit C.∘ (F.₁ f)) g βŸ©β‰‘
      bind (bind (unit C.∘ F.₁ f) C.∘ g) ∎

    bind-naturalr
      : βˆ€ {x y z} (f : C.Hom (F.β‚€ y) (Mβ‚€ z)) (g : J.Hom x y)
      β†’ bind f C.∘ M₁ g ≑ bind (f C.∘ F.₁ g)
    bind-naturalr f g =
      bind f C.∘ bind (unit C.∘ F.₁ g)   β‰‘βŸ¨ bind-∘ f (unit C.∘ F.₁ g) βŸ©β‰‘
      bind (bind f C.∘ unit C.∘ (F.₁ g)) β‰‘βŸ¨ ap bind (C.pulll (bind-unit-∘ f)) βŸ©β‰‘
      bind (f C.∘ F.₁ g) ∎

Functoriality also follows.

    M-id : βˆ€ {x} β†’ M₁ (J.id {x}) ≑ C.id
    M-id =
      bind (unit C.∘ F.₁ J.id) β‰‘βŸ¨ ap bind (C.elimr F.F-id) βŸ©β‰‘
      bind unit                β‰‘βŸ¨ bind-unit-id βŸ©β‰‘
      C.id                     ∎

    M-∘ : βˆ€ {x y z} β†’ (f : J.Hom y z) (g : J.Hom x y) β†’ M₁ (f J.∘ g) ≑ M₁ f C.∘ M₁ g
    M-∘ f g =
      bind (unit C.∘ F.₁ (f J.∘ g))  β‰‘βŸ¨ ap bind (F.shufflel (unit-natural f)) βŸ©β‰‘
      bind (M₁ f C.∘ unit C.∘ F.₁ g) β‰‘Λ˜βŸ¨ bind-∘ (unit C.∘ F.₁ f) (unit C.∘ F.₁ g) βŸ©β‰‘Λ˜
      M₁ f C.∘ M₁ g                  ∎

However, note that we do not have a multiplication operation, as we cannot iterate

module _
  {oj β„“j oc β„“c}
  {J : Precategory oj β„“j}
  {C : Precategory oc β„“c}
  {F : Functor J C}
  {E E' : Relative-extension-system F} where
  private
    module J = Cat.Reasoning J
    module C = Cat.Reasoning C
    module F = Cat.Functor.Reasoning F
    module E = Relative-extension-system E
    module E' = Relative-extension-system E'
    open Relative-extension-system

  Relative-extension-system-path
    : (p0 : βˆ€ x β†’ E.Mβ‚€ x ≑ E'.Mβ‚€ x)
    β†’ (βˆ€ x β†’ PathP (Ξ» i β†’ C.Hom (F.β‚€ x) (p0 x i)) E.unit E'.unit)
    β†’ (βˆ€ {x y} (f : βˆ€ i β†’ C.Hom (F.β‚€ x) (p0 y i)) β†’ PathP (Ξ» i β†’ C.Hom (p0 x i) (p0 y i)) (E.bind (f i0)) (E'.bind (f i1)))
    β†’ E ≑ E'
  Relative-extension-system-path p0 punit pbind = sys where
    coe-pbind
      : βˆ€ i
      β†’ {x y : J.Ob}
      β†’ (f : C.Hom (F.β‚€ x) (p0 y i))
      β†’ C.Hom (p0 x i) (p0 y i)
    coe-pbind i {x} {y} f = pbind (Ξ» j β†’ coe (Ξ» i β†’ C.Hom (F.β‚€ x) (p0 y i)) i j f) i

    sys : E ≑ E'
    sys i .Mβ‚€ x = p0 x i
    sys i .unit {x} = punit x i
    sys i .bind f = coe-pbind i f
    sys i .bind-unit-id {x} =
      is-prop→pathp (λ i → C.Hom-set (p0 x i) (p0 x i) (coe-pbind i (punit x i)) C.id)
        E.bind-unit-id
        E'.bind-unit-id i
    sys i .bind-unit-∘ {x} {y} f =
      hcomp (βˆ‚ i) Ξ» where
        j (i = i0) β†’ C.Hom-set _ _ _ _ base (E.bind-unit-∘ f) j
        j (i = i1) β†’ C.Hom-set _ _ _ _ base (E'.bind-unit-∘ f) j
        j (j = i0) β†’ base
      where
        base =
          coe0β†’i (Ξ» i β†’ (f : C.Hom (F.β‚€ x) (p0 y i)) β†’ coe-pbind i f C.∘ punit x i ≑ f)
            i
            (Ξ» f β†’ E.bind-unit-∘ {x} {y} f) f
    sys i .bind-∘ {x} {y} {z} f g =
      hcomp (βˆ‚ i) Ξ» where
        j (i = i0) β†’ C.Hom-set _ _ _ _ base (E.bind-∘ f g) j
        j (i = i1) β†’ C.Hom-set _ _ _ _ base (E'.bind-∘ f g) j
        j (j = i0) β†’ base
      where
        base =
          coe0β†’i (Ξ» i β†’ (f : C.Hom (F.β‚€ y) (p0 z i)) (g : C.Hom (F.β‚€ x) (p0 y i)) β†’ coe-pbind i f C.∘ coe-pbind i g ≑ coe-pbind i (coe-pbind i f C.∘ g))
            i
            (Ξ» f g β†’ E.bind-∘ {x} {y} f g) f g

Algebras over a relative extension systemπŸ”—

A relative extension algebra over is the relative extension system analog of an algebra over a monad. Following the general theme of extension operations, a relative extension algebra on is given by an operation Intuitively, this operation lets us β€œevaluate” any so long as the codomain of the evaluation is

  record Relative-algebra-on (x : C.Ob) : Type (oj βŠ” β„“c) where
    no-eta-equality
    field
      Ξ½ : βˆ€ {a} (f : C.Hom (F.β‚€ a) x) β†’ C.Hom (Mβ‚€ a) x

This operation must satisfy a pair of equations:

  1. For every we must have

  2. For every and we must have

      Ξ½-unit : βˆ€ {a} (f : C.Hom (F.β‚€ a) x) β†’ Ξ½ f C.∘ unit ≑ f
      Ξ½-bind
        : βˆ€ {a b} (f : C.Hom (F.β‚€ b) x) (g : C.Hom (F.β‚€ a) (Mβ‚€ b))
        β†’ Ξ½ f C.∘ bind g ≑ Ξ½ (Ξ½ f C.∘ g)

From these, we can deduce a sort of naturality principle for

    Ξ½-natural
      : βˆ€ {a b} (f : C.Hom (F.β‚€ b) x) (g : J.Hom a b)
      β†’ Ξ½ f C.∘ M₁ g ≑ Ξ½ (f C.∘ F.₁ g)
    Ξ½-natural f g =
      Ξ½ f C.∘ bind (unit C.∘ F.₁ g) β‰‘βŸ¨ Ξ½-bind f (unit C.∘ F.₁ g) βŸ©β‰‘
      Ξ½ (Ξ½ f C.∘ unit C.∘ F.₁ g)    β‰‘βŸ¨ ap Ξ½ (C.pulll (Ξ½-unit f)) βŸ©β‰‘
      Ξ½ (f C.∘ F.₁ g)  ∎
module _
  {oj β„“j oc β„“c}
  {J : Precategory oj β„“j}
  {C : Precategory oc β„“c}
  {F : Functor J C}
  {E : Relative-extension-system F}
  where
  private
    module J = Cat.Reasoning J
    module C = Cat.Reasoning C
    module F = Cat.Functor.Reasoning F
    open Relative-extension-system E
    open Relative-algebra-on

  Relative-algebra-on-pathp
    : βˆ€ {x y}
    β†’ (p : x ≑ y)
    β†’ {Ξ± : Relative-algebra-on E x}
    β†’ {Ξ² : Relative-algebra-on E y}
    β†’ (βˆ€ {a} β†’ (f : βˆ€ i β†’ C.Hom (F.β‚€ a) (p i)) β†’ PathP (Ξ» i β†’ C.Hom (Mβ‚€ a) (p i)) (Ξ± .Ξ½ (f i0)) (Ξ² .Ξ½ (f i1)))
    β†’ PathP (Ξ» i β†’ Relative-algebra-on E (p i)) Ξ± Ξ²
  Relative-algebra-on-pathp {x} {y} p {Ξ±} {Ξ²} pΞ½ = sys where
    coe-Ξ½ : βˆ€ i β†’ {a : J.Ob} β†’ (f : C.Hom (F.β‚€ a) (p i)) β†’ C.Hom (Mβ‚€ a) (p i)
    coe-Ξ½ i {a} f = pΞ½ (Ξ» j β†’ coe (Ξ» i β†’ C.Hom (F.β‚€ a) (p i)) i j f) i

    sys : PathP (Ξ» i β†’ Relative-algebra-on E (p i)) Ξ± Ξ²
    sys i .Ξ½ f = coe-Ξ½ i f
    sys i .Ξ½-unit {a} f =
      hcomp (βˆ‚ i) Ξ» where
        j (i = i0) β†’ C.Hom-set _ _ _ _ base (Ξ± .Ξ½-unit f) j
        j (i = i1) β†’ C.Hom-set _ _ _ _ base (Ξ² .Ξ½-unit f) j
        j (j = i0) β†’ base
      where
        base =
          coe0β†’i (Ξ» i β†’ (f : C.Hom (F.β‚€ a) (p i)) β†’ coe-Ξ½ i f C.∘ unit ≑ f)
            i
            (Ξ± .Ξ½-unit) f
    sys i .Ξ½-bind {a} {b} f g =
      hcomp (βˆ‚ i) Ξ» where
        j (i = i0) β†’ C.Hom-set _ _ _ _ base (Ξ± .Ξ½-bind f g) j
        j (i = i1) β†’ C.Hom-set _ _ _ _ base (Ξ² .Ξ½-bind f g) j
        j (j = i0) β†’ base
      where
        base =
          coe0β†’i (Ξ» i β†’ (f : C.Hom (F.β‚€ b) (p i)) β†’ coe-Ξ½ i f C.∘ bind g ≑ coe-Ξ½ i (coe-Ξ½ i f C.∘ g))
            i
            (Ξ» f β†’ Ξ± .Ξ½-bind f g) f

The relative Eilenberg-Moore categoryπŸ”—

We can also relativize the Eilenberg-Moore category to obtain the relative Eilenberg-Moore category.

  Relative-Eilenberg-Moore : Displayed C (oj βŠ” β„“c) (oj βŠ” β„“c)

Objects over are given by relative extension algebras over and maps over between algebras and are relative extension algebra morphisms when, for every we have

  Relative-Eilenberg-Moore .Ob[_] = Relative-algebra-on E
  Relative-Eilenberg-Moore .Hom[_] {x} {y} f Ξ± Ξ² =
    βˆ€ {a} (g : C.Hom (F.β‚€ a) x) β†’ f C.∘ Ξ± .Ξ½ g ≑ Ξ² .Ξ½ (f C.∘ g)

It is straightforward to show that relative extension algebra morphisms are closed under identities and composites.

  Relative-Eilenberg-Moore .id' {x = Ξ±} g =
    C.id C.∘ Ξ± .Ξ½ g   β‰‘βŸ¨ C.idl _ βŸ©β‰‘
    Ξ± .Ξ½ g            β‰‘Λ˜βŸ¨ ap (Ξ± .Ξ½) (C.idl _) βŸ©β‰‘Λ˜
    α .ν (C.id C.∘ g) ∎
  Relative-Eilenberg-Moore ._∘'_ {x = α} {y = β} {z = γ} {f = f} {g = g} p q h =
    (f C.∘ g) C.∘ Ξ± .Ξ½ h   β‰‘βŸ¨ C.pullr (q h) βŸ©β‰‘
    f C.∘ Ξ² .Ξ½ (g C.∘ h)   β‰‘βŸ¨ p (g C.∘ h) βŸ©β‰‘
    Ξ³ .Ξ½ (f C.∘ g C.∘ h)   β‰‘βŸ¨ ap (Ξ³ .Ξ½) (C.assoc _ _ _) βŸ©β‰‘
    γ .ν ((f C.∘ g) C.∘ h) ∎
All of the equations are trivial.
  Relative-Eilenberg-Moore .Hom[_]-set = hlevel!
  Relative-Eilenberg-Moore .idr' _ =
    is-prop→pathp (λ i → Π-is-hlevel' 1 λ _ → Π-is-hlevel 1 λ _ → C.Hom-set _ _ _ _) _ _
  Relative-Eilenberg-Moore .idl' _ =
    is-prop→pathp (λ i → Π-is-hlevel' 1 λ _ → Π-is-hlevel 1 λ _ → C.Hom-set _ _ _ _) _ _
  Relative-Eilenberg-Moore .assoc' _ _ _ =
    is-prop→pathp (λ i → Π-is-hlevel' 1 λ _ → Π-is-hlevel 1 λ _ → C.Hom-set _ _ _ _) _ _

  1. For instance, if we want to model a syntax where terms can only have finitely many variables.β†©οΈŽ


References

  • Altenkirch, Thosten, James Chapman, and Tarmo Uustalu. 2015. β€œMonads Need Not Be Endofunctors.” Logical Methods in Computer Science Volume 11, Issue 1 (March): 928. https://doi.org/10.2168/LMCS-11(1:3)2015.