Bicartesian closed categories and Heyting algebras - MathOverflow most recent 30 from http://mathoverflow.net 2013-05-24T07:02:03Z http://mathoverflow.net/feeds/question/31091 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/31091/bicartesian-closed-categories-and-heyting-algebras Bicartesian closed categories and Heyting algebras Matthew Wampler-Doty 2010-07-08T18:04:55Z 2010-07-09T14:49:54Z <p>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.</p> <p>On the other hand, fixing a bicartesian closed category, and using $A \cong B$ to denote that morphisms<sup>1</sup> exists between $A$ and $B$, we can see that every bicartesian closed category exhibits the <a href="http://en.wikipedia.org/wiki/Heyting_algebra#Characterization_using_the_axioms_of_intuitionistic_logic" rel="nofollow">intuitionistic equational axiomatization</a> of a Heyting algebra. Specifically, we can observe that:</p> <ol> <li>If $X \to Y \cong 1$ and $Y \to X \cong 1$ then $X \cong Y$</li> <li>If $1 \to X \cong 1$ then $X \cong 1$</li> <li>$X \to (Y \to X) \cong 1$</li> <li>$(X \to (Y \to Z)) \to (X \to Y) \to (X \to Z) \cong 1$</li> <li>$X \times Y \to X \cong 1$</li> <li>$X \times Y \to Y \cong 1$</li> <li>$X \to Y \to X \times Y \cong 1$</li> <li>$X \to X + Y \cong 1$</li> <li>$Y \to X + Y \cong 1$</li> <li>$(X \to Z) \to (Y \to Z) \to (X + Y \to Z) \cong 1$</li> <li>$0 \to X \cong 1$</li> </ol> <p>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. </p> <p>I cannot find the statement of this in Lambek &amp; Scott, however. So I have two questions:</p> <p>(A) Does this follow from some general theorem regarding bicartesian closed categories?<br/> (B) Is this a folk theorem, or is there a place in the literature where this is established?</p> <hr> <p>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 <em>equimorphic</em>.</p> http://mathoverflow.net/questions/31091/bicartesian-closed-categories-and-heyting-algebras/31192#31192 Answer by François G. Dorais for Bicartesian closed categories and Heyting algebras François G. Dorais 2010-07-09T14:12:44Z 2010-07-09T14:12:44Z <p>As Andreas Blass observed, those identities do not hold in all bicartesian closed categories. However, they are true if "isomorphism" is replaced by "equimorphism." In a poset category, equimorphism and isomorphism are the same and thus these equations do verify that a bicartesian closed poset category is a Heyting algebra.</p> <p>That said, I suppose that the answer to your underlying question is the <a href="http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="nofollow">Curry&ndash;Howard isomorphism</a>. 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$.</p>