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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.