4 added 232 characters in body

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 an isomorphism 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.

3 Add equational axiomatization regarding 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 an isomorphism 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 (ie, Y \to X) \cong 1$
4. $A (X \to B (Y \to A Z)) \to (X \to Y) \to (X \to Z) \cong 1$
5. $X \top$, times Y \to X \cong 1$6.$A X \wedge B times Y \to A Y \cong 1$7.$X \top$, 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 so on)$+$ 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?

2 downcase

1