On Sat, 2021-01-09 at 23:45 +0100, MigMit wrote: But it won't be cartesian closed. If it were, then for any finite
X and Y we should have
Maybe (X^Y) ~ () -> Maybe (X^Y) ~ OneOrBoth () Y -> Maybe X ~ (() -> Maybe X, Y -> Maybe X, ((), Y) -> Maybe X) ~ (Maybe X, Y -> Maybe X, Y -> Maybe X)
so
X^Y ~ (X, Y -> Maybe X, Y -> Maybe X)
No, my arrows and isomorphisms are all in the original category, not the Kleisli one — although the "X^Y" is the exponent in the Kleisli category.
I don't follow your argument. I still must be misinterpreting something. Maybe (X^Y) ~ () -> Maybe (X^Y) -- because () is terminal in Hask ~ OneOrBoth () Y -> Maybe X -- OneOrBoth is the product in Kleisli Maybe ~ (Maybe X, Y -> Maybe X, Y -> Maybe X) -- universal property of coproduct But how did you get to the next step: X^Y ~ (X, Y -> Maybe X, Y -> Maybe X) I think this can not hold for cardinality reasons: 1+X*((1+X)^Y)^2 /= (1+X)*((1+X)^Y)^2 Olaf