Exponential.idr

An interesting fact about functor categories is that we can use them to define currying and uncurrying operation on them.

That is, from a functor $\mathcal{C}\to [\mathcal{D},\mathcal{E}]$ we can obtain the functor $\mathcal{C}\ast \mathcal{D}\to \mathcal{E}$. The proof is quite large so it is left in appendix.

curryFunctor : {0 o : Type} -> {c : Category o} ->
               a ->> (FunctorCat b c) -> (a × b) ->> c

Similarly, we can uncurry bifunctors $\mathcal{C}\ast \mathcal{D}\to \mathcal{E}$ as a functor $\mathcal{C}\to [\mathcal{D},\mathcal{E}]$. Again, the implementation is quite large so it is left in appendix.

uncurryFunctor :
    {0 o, p, q : Type} ->
    {a : Category p} -> {b : Category q} -> {c : Category o} ->
    (a × b) ->> c -> a ->> (FunctorCat b c)
    -- Proof in appendix