Indexed monad demonstration

imonad.agda

module imonad where

postulate
  -- Whatever the monad is indexed over
  Ix : Set₁
  
infixr 3 _:→_
_:→_ : (Ix -> Set) -> (Ix -> Set) -> Set₁
a :→ b = ∀{x : Ix} -> a x -> b x


ifun = (Ix → Set) → Ix → Set
cfun = Ix → Ix → Set → Set

record IFunctor (f : ifun) : Set₁ where
  field
    imap : ∀{s t} → (s :→ t) → (f s :→ f t)

infixr 20 _≔_
data _≔_ (x : Set) : Ix → Ix → Set where
  V : ∀{i} → x → (x ≔ i) i

constr-≔ : ∀{x t} i → (x ≔ i) :→ t → x → t i
constr-≔ _ f a = f (V a)

destr-≔ : ∀{x t} i → (x → t i) → (x ≔ i) :→ t
destr-≔ _ f (V x) = f x

record IMonad (m : ifun) {{_ : IFunctor m}} : Set₁ where
  field
    iskip : ∀{p} → p :→ m p
    iextend : ∀{p q} → (p :→ m q) → (m p :→ m q)
  ret-atkey : ∀{x i} → x → m (x ≔ i) i
  ret-atkey x = iskip (V x)

const : ∀{l}{A B : Set l} → A → B → A
const a b = a

record CatMonad (f : cfun) : Set₁ where
  field
    -- cofmap and fmap of first args aren't expressible since we
    -- don't assume Ix to be a category 
    fmap-value : ∀{i j x y} → (x → y) → f i j x → f i j y
    return : ∀{i x} → x → f i i x
    bind : ∀{i j k x y} → f i j x → (x → f j k y) → f i k y


module _ (m : ifun){{FM : IFunctor m}}{{MM : IMonad m}} where
  open IFunctor FM 
  open IMonad MM 

  cmf : cfun
  cmf i j x = m (x ≔ j) i 

  fmap-value-cmf : ∀{i j x y} → (x → y) → cmf i j x → cmf i j y
  fmap-value-cmf f m = iextend (λ { (V x) → ret-atkey (f x) }) m

  return-cmf : ∀{i x} → x → cmf i i x
  return-cmf x = iskip (V x)

  bind-cmf : ∀{i j k x y} → cmf i j x → (x → cmf j k y) → cmf i k y
  bind-cmf m f = iextend (λ { (V x) → f x }) m