Flexible.agda

module Flexible where

-- Exploring flexible graded monads, based on the work of Katsumata, McDermott, Uustalu and Wu
-- https://dylanm.org/drafts/flexibly-graded-presentations.pdf

open import Function

_⇒_ : {E : Set} -> (E -> Set) -> (E -> Set) -> Set
_⇒_ {E} X Y = forall (e : E) -> X e -> Y e

record Flexible (E : Set) : Set₁ where
  field
   T : (E -> Set) -> E -> Set

   _*_ : E -> E -> E
   
   unit : {X : E -> Set} -> X ⇒ T X
   bind :  {X : E -> Set} {Y : E -> Set}
        -> (e : E)
        -> (X   ⇒ \f -> T Y (f * e))
        -> (T X ⇒ \f -> T Y (f * e))

open Flexible

record Graded (E : Set) : Set₁ where
  field
    G    : E -> Set -> Set
    I    : E
    _·_  : E -> E -> E
    unit : {A : Set} -> A -> G I A
    bind : {A B : Set} {e f : E}
        -> (A -> G e B)
        -> (G f A -> G (f · e) B)
  
open Graded


into : {E : Set} -> (g : Graded E) -> Flexible E
into g =
  record { T = \X -> \e -> G g (I g) (X e) 
        ; _*_ = _·_ g
        ; unit = λ e x → let y = unit g x in unit g x
        ; bind = {!!} }

-- Surely not?
outo : {E : Set} -> (f : Flexible E) -> Graded E
outo f =
  record { G = λ e A → T f (\_ -> A) e
         ; I = {!!}
         ; _·_ = {!!}
         ; unit = λ a → unit {{!!}} {!!}
         ; bind = {!!} }