# Does the category of functors possess a coexponential?

Suppose I have maps

lam : (u -> u) -> u
app : u -> (u -> u)


One sort of dual concept would be

lam : (u -< u) -> u
app : u -> (u -< u)


What would it mean to map to and from a coexponential?

lamMap : ? -> hom (lam f) (lam g)
appMap : hom a b -> ? (app f) (app g)


My intuition is one would encode a sort of coexponential via negation.

lamMap : hom a b -> (forall x. void (f x) (g x)) -> hom (lam a f) (lam b g)


But this doesn't seem to really work to me.

I think you could also try switching around variance but that also gets rapidly confusing.