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.
