# Bicartesian closed categories and Heyting algebras

In Lambek and Scott's "Introduction to higher order categorical logic" (1988), they state that every Heyting Algebra can be understood as a bicartesian closed category.

On the other hand, fixing a bicartesian closed category, and using $A \cong B$ to denote that morphisms1 exists between $A$ and $B$, we can see that every bicartesian closed category exhibits the intuitionistic equational axiomatization of a Heyting algebra. Specifically, we can observe that:

1. If $X \to Y \cong 1$ and $Y \to X \cong 1$ then $X \cong Y$
2. If $1 \to X \cong 1$ then $X \cong 1$
3. $X \to (Y \to X) \cong 1$
4. $(X \to (Y \to Z)) \to (X \to Y) \to (X \to Z) \cong 1$
5. $X \times Y \to X \cong 1$
6. $X \times Y \to Y \cong 1$
7. $X \to Y \to X \times Y \cong 1$
8. $X \to X + Y \cong 1$
9. $Y \to X + Y \cong 1$
10. $(X \to Z) \to (Y \to Z) \to (X + Y \to Z) \cong 1$
11. $0 \to X \cong 1$

Here $\to$ is an exponential, $\times$ is a product, and $+$ is a co-product, $1$ is a final object and $0$ is an initial object.

I cannot find the statement of this in Lambek & Scott, however. So I have two questions:

(A) Does this follow from some general theorem regarding bicartesian closed categories?
(B) Is this a folk theorem, or is there a place in the literature where this is established?

I originally wrote isomorphism here, but as Andreas Blass notes this is not true (for instance, in the category of sets). However, as noted below, this is true if we weaken the statement to equimorphic.

-
Can you clarify your second paragraph. Which equational axiomatization do you have in mind? Are $\wedge$, $\vee$, $\to$ products, coproducts, and exponentials? –  François G. Dorais Jul 8 '10 at 19:02
I suppose you mean equimorphism. I think the answer to your question is that the internal logic is intuitionistic. –  François G. Dorais Jul 8 '10 at 23:00
You seem to be using a different definition of "bicartesian closed" than the one I'm familiar with, which requires only finite products, finite coproducts and exponential. (This definition fits with your comment about Heyting algebras being bicartesian closed categories.) In particular, I would consider the category of sets to be bicartesian closed. But items 3 through 10 on your list fail in the category of sets. So, what definition of "bicartesian closed" are you referring to? (I don't have the Lambek-Scott book immediately available, so I can't look up their definition.) –  Andreas Blass Jul 9 '10 at 6:14
@Andreas: L&S use finite products and coproducts, as fits with their general discipline of specifying categorical constructions using only equations. –  Charles Stewart Jul 9 '10 at 12:54
That said, I suppose that the answer to your underlying question is the Curry–Howard isomorphism. Under this interpretation, an intuitionistic proof of a proposition like $X \land Y \to X$ can be interpreted as a morphism $X \times Y \to X$ or $1 \to X^{X \times Y}$. In this particular case, the obvious proof gives the projection $\pi_1:X \times Y \to X$ but this is by no means the only possible morphism $X \times Y \to X$.