MigMit migmit at gmail.com
Sun Jan 10 21:25:36 UTC 2021

```Damn, you're right, my mistake.

So, in short, there doesn't seem to be a good representation for (X^Y). But even if it was, we can be certain that

#(X^Y) = (#X + 1) * (#X + 1)^(#Y) * (#X + 1)^(#Y) - 1 = (#X + 1)^(2 * #Y + 1) - 1

That makes it possible to calculate both #(Z -> Maybe X^Y) and #(OneOrBoth Z Y -> Maybe X):

#(Z -> Maybe X^Y) = #(Maybe X^Y)^#Z = (#X + 1)^(2 * #Y * #Z + #Z)
#(OneOrBoth Z Y -> Maybe X) = #(Maybe X)^#(OneOrBoth Z Y) = (#X + 1)^(#Y * #Z + #Y + #Z)

and we still see that they are different, unless X is empty or Z ~ ().

Thanks!

> On 10 Jan 2021, at 22:10, Olaf Klinke <olf at aatal-apotheke.de> wrote:
>
> 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.
>
> 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
>

```