Definition.idr

Functorial Application and Monadic Lenses

Functorial application combines a functor $F\in \mathcal{S}et\to \mathcal{S}et$ with a container by applying the functor to the the “response” part of the container.

Definition

Functor application of containers, read “app”.

(•) : (f : Type -> Type) -> Container -> Container
(•) f c = (x : c.req) !> f (c.res x)

The first thing to notice about this operator is that it flips the arrows between the functor category in $\mathcal{S}et$ and the functor category in $\mathcal{C}ont$. Formally this is described as a functor from the opposite category of endofunctors to the category of morphisms in $\mathcal{C}ont$. Or equivalently: