I wonder if it is related to exponentials vs coexponentials, since categories with both exponentials and coexponentials are posetal. I don’t have any particular argument for how that’d work, though.
Do you have a reference for this statement?
I suppose it is related to Joyal’s result that a Boolean category is always a poset, preventing a naive categorical analysis of classical proof theory.
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.
Do you know programming? A coexponential A−B is intuitively roughly speaking an A together with a return position where you can place a B. It’s how function calls are implemented in computers, as morphisms A−B→0, corresponding to the fact that you have the parameters A and the call stack −B.
(More formally: given a coproduct (~disjoint union) +, a coexponential − is defined based on A→B+C being equivalent to A−B→C.)
I wonder if it is related to exponentials vs coexponentials, since categories with both exponentials and coexponentials are posetal. I don’t have any particular argument for how that’d work, though.
Do you have a reference for this statement? I suppose it is related to Joyal’s result that a Boolean category is always a poset, preventing a naive categorical analysis of classical proof theory.
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.
Not a category theorist, I only understood this post through set theory analogies, so I have no idea what you just said.
Do you know programming? A coexponential A−B is intuitively roughly speaking an A together with a return position where you can place a B. It’s how function calls are implemented in computers, as morphisms A−B→0, corresponding to the fact that you have the parameters A and the call stack −B.
(More formally: given a coproduct (~disjoint union) +, a coexponential − is defined based on A→B+C being equivalent to A−B→C.)
OK, that explanation helped me understand coexponentials a bit but I’m unsure how it’s relevant to the assymetry between the examples Alok gave.