I can’t remember the entire proof, and maybe I misstated it, but IIRC part of the logic goes as follows:
With exponentials, you can prove that 0 x A ≈ 0, because any morphism 0 x A → B curries into 0 → B^A, of which by the universal property of 0, there’s only one.
Similarly, with coexponentials, you can prove that 1 + A ≈ 1, because any morphism A → B+1 cocurries into A-B → 1, of which there is only one.
So this at least proves that all the objects built out of 0, 1, x and + are trivial. I think there was something funky where you made use of the fact that A → B can be expressed as 1-(B^A) → 0 and 1 → 0^(B-A) to further prove all morphisms trivial, but I can’t remember it exactly.
First, each morphism f : A → 0 induces a unique morphism f . pr1 : A x 0 → 0. Proof: suppose f . pr1 = g . pr1. Then we have f = f . pr1 . (id, f) = g . pr1 . (id, f) = g.
Corollary: if you have exponential objects, then if you have any f : A → 0, then A ≈ 0, because there’s only one morphism 0 → 0^A.
But, if you have coexponential objects, any hom set A → B can instead be expressed as a hom set A-B → 0. This shows A-B ≈ 0, and also all homs are equal.
I can’t remember the entire proof, and maybe I misstated it, but IIRC part of the logic goes as follows:
With exponentials, you can prove that 0 x A ≈ 0, because any morphism 0 x A → B curries into 0 → B^A, of which by the universal property of 0, there’s only one.
Similarly, with coexponentials, you can prove that 1 + A ≈ 1, because any morphism A → B+1 cocurries into A-B → 1, of which there is only one.
So this at least proves that all the objects built out of 0, 1, x and + are trivial. I think there was something funky where you made use of the fact that A → B can be expressed as 1-(B^A) → 0 and 1 → 0^(B-A) to further prove all morphisms trivial, but I can’t remember it exactly.
Ahh, now I’ve got it:
First, each morphism f : A → 0 induces a unique morphism f . pr1 : A x 0 → 0. Proof: suppose f . pr1 = g . pr1. Then we have f = f . pr1 . (id, f) = g . pr1 . (id, f) = g.
Corollary: if you have exponential objects, then if you have any f : A → 0, then A ≈ 0, because there’s only one morphism 0 → 0^A.
But, if you have coexponential objects, any hom set A → B can instead be expressed as a hom set A-B → 0. This shows A-B ≈ 0, and also all homs are equal.