0
$\begingroup$

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.

$\endgroup$

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.