Coden.agda

{-# OPTIONS --type-in-type #-}
module Coden (m : Set → Set) where

open import Category.Functor
open RawFunctor {{...}}

Ran : (K : Set → Set) → Set → Set
Ran K a = (c : Set) → (a → K c) → m c

α : ∀ {a}{K} → Ran K (K a) → m a
α m = m _ (\ x → x)

-- universal map
intro : ∀ {H : Set → Set}{{_ : RawFunctor H}}{K} → (∀ a → H (K a) → m a) → ∀ a → H a → Ran K a
intro t a r = λ c x → t c (x <$> r)

Cod : Set → Set
Cod a = Ran m a

instance
  codF : RawFunctor Cod
  RawFunctor._<$>_ codF f m = λ c x → m c λ x₁ → x (f x₁)
  cod2 : RawFunctor (\ x → Cod (Cod x))
  RawFunctor._<$>_ cod2 f m = _<$>_ {F = Cod} f <$> m

join join' : ∀ a → Cod (Cod a) → Cod a

-- definition from the diagram
join = intro (\ a x → α (α <$> x))

-- normal form of the above
join' = λ a codcod c k → codcod c (λ cod → cod c k)

bind : ∀ {a b} → Cod a → (a → Cod b) → Cod b
bind m f c k = m c (λ z → f z c k)