Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
Happened to notice a question at bicartesian closed category.
Question: don’t you need distributive bicartesian closed categories to interpret intuitionistic propositional logic? Consider the or-elimination rule
$\frac{\Gamma, A \vdash C \qquad \Gamma,B \vdash C} {\Gamma, A + B \vdash C}$The intepretations of the two premises will be maps of type $\Gamma \times A \to C$ and $\Gamma \times B \to C$. Then the universal property of coproducts gets us to $(\Gamma \times A) + (\Gamma \times B) \to C$, but we can’t get any farther – we need a distributivity law to get $\Gamma \times (A+B) \to C$.
I’ve added a short paragraph to address this.
Does this need a more thorough answer?
If not, should I remove the question block?
The anonymous questioner acknowledged that the edit was to satisfactory, so I removed the question block.
Incidentally, when replying to questions like this that are written directly on the nLab, it’s probably worth (briefly) pointing out that they’d get a better chance of an answer if they posted it at the nForum (which can be done anonymously). I only happened across this question by chance.
Hi Andrew and Ulrik:
I asked that question. It didn’t occur to me to ask it here, since the average level of discussion is quite a bit more sophisticated than my rather elementary question. If you think it won’t bring down the tone, I’m happy to ask similar questions here in the future. :)
Neel, please feel free to ask any questions at any level. There are plenty of elementary questions that get asked here.
http://www.math.ntnu.no/~stacey/Mathforge/nForum/comments.php?DiscussionID=2932 being a case in point!
1 to 7 of 7