Lift.idr

Proposition

The $•$ operator forms a bifunctor $[\mathcal{S}et,\mathcal{S}et{]}^{op}\times \mathcal{C}ont\to \mathcal{C}ont$. The map on objects is the application of $(•)$ and the map on morphisms, the map on morphisms relies on the naturality square of the functors in $\mathcal{S}et$

FApplyBifunctor : Bifunctor (EndoCat Set).op Cont Cont
FApplyBifunctor = MkFunctor
    { mapObj = (\f => f.π1.mapObj • f.π2)
    , mapHom = mapHom
    , presId = presId
    , presComp = presComp
    } -- proofs in appendix

We can partially apply the above bifunctor to obtain endofunctors in $\mathcal{C}ont$ given any functor $M:\mathcal{S}et\to \mathcal{S}et$

Proposition

Given a functor $F:\mathcal{S}et\to \mathcal{S}et$ we obtain a functor $F{•}_{:}\mathcal{C}ont\to \mathcal{C}ont$

parameters (f : Endo Set)
  FApplyFunctor : Endo Cont
  FApplyFunctor = applyBifunctor {a = (EndoCat Set).op} f FApplyBifunctor

The inversion from $(•)$ means that every monad on $\mathcal{S}et$ becomes a comonad in $\mathcal{C}ont$ when applied with (•).

Proposition

Given a monad $m:\mathcal{S}et\to \mathcal{S}et$, the functor $m{•}_{:}\mathcal{C}ont\to \mathcal{C}ont$ is a comonad.

• finish transforming between monads in set to comonads in cont

ContComonad : (Monad Set e) -> Comonad Cont (FApplyFunctor e)

Additionally we are going to need the following property to run programs with IO: δ : m • (a ▷ b) ⇒ m • (a ▷ m • b)

Proposition

Functorial application distributes to the right of $(⊳)$ when m is a monad.

    δ : {a, b : _} -> m • (a ▷ b) =%> m • (a ▷ m • b)
    δ = id <! (\x, y => joinSnd {a = a.response x.ex1, b = b.response . x.ex2 } y )

Relation to Monadic lenses

Monadic lenses as defined by \ref{monadicLens} are lenses where the backward morphism is wrapped in a monad in set. We can reproduce the results from this paper but in $\mathcal{C}ont$ by using functorial application in the domain of any dependent lens.

Proposition

Lenses using the functor application in their domain are monadic lenses

The definition of a monadic lens is a lens MLens s t a b where the backward morphism end in f t instead of t.

We leave the proof to be done by observation, to help, here are the two definitions superimposed:

     a ->        (s * (t -> f b)) -- Monadic lenses
(_ : a) -> Σ (_ : s) | t -> f b   -- Dependent lenses f • (a, b) =&> (s, t)

Some helper functions to manipulate functorial applications

• find a better spot for that

%unbound_implicits on
export
counit : (0 m : Type -> Type) -> Monad m => m • a =%> a
counit _ = id <! \_ => pure
 
export
cojoin : (0 m : Type -> Type) -> Monad m => m • a =%> m • m • a
cojoin m = id <! \_ => join