Timeline for Two interpretations of implication in categorical logic?
Current License: CC BY-SA 4.0
10 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 9, 2021 at 18:16 | comment | added | Mike Shulman | Yes, they do coincide. | |
| Jan 9, 2021 at 11:40 | comment | added | YKY | Sorry for slow response. In the topos, subsets of a sub-object form a Heyting algebra, from which we get an implication arrow (Heyting implication, intuitionistic). On the other hand, the "internal language" of this topos is a type theory (are you familiar with this terminology?) and this logic has an implication arrow also. Do these two implication arrows actually coincide? | |
| Dec 23, 2020 at 21:30 | comment | added | Mike Shulman | The (dependent) type corresponding to $\phi:A\to \Omega$ is the monomorphism $J \rightarrowtail A$ that it classifies, according to the universal property of $\Omega$. Substituting ${\rm John}:1\to A$ pulls this monomorphism back, yielding a subterminal object (a mere-proposition type). In the usual internal logic of a topos, not all types are regarded as propositions, only the monomorphisms (for dependent types) / subterminals (for non-dependent ones). | |
| Dec 23, 2020 at 10:03 | comment | added | YKY | Moreover, this whole way of interpreting logic in the form $\phi: A \rightarrow \Omega$ entirely ignores the Curry-Howard view (propositions-as-types). How can this be reconciled? Yet in Bart Jacobs' book Ch.10 is described a way to treat dependent types à la Martin-Lof type theory, which respects the Curry-Howard view. I just don't understand how the two approaches are unified. | |
| Dec 23, 2020 at 9:50 | comment | added | YKY | Sorry that I needed some time to read the books, but now I can rephrase my question: Suppose we have $\phi: A \rightarrow \Omega$ in a topos $\mathcal{C}$. This corresponds to a logic formula in the internal language of $\mathcal{C}$. For instance, A could be the sort of persons, and $\phi$ tells us if the person is male or not. $\phi$(John) maps to $\top$ as John is male. However, the Curry-Howard view (proposition-as-types) would require that $\phi$(John) be a type. Here we have A as a type but it does not correspond to any proposition in the Curry-Howard sense. | |
| Dec 7, 2020 at 3:24 | comment | added | Mike Shulman | I can't really parse that sentence. Maybe this requires a longer discussion in a different forum. | |
| Dec 7, 2020 at 3:07 | comment | added | YKY | Oh... I guess I should be looking into the 'internal language" of the topos which ensures that Curry-Howard correspondence is satisfied? I was wondering about the type-theoretic interpretation of the Boolean / Heyting algebra in the sub-objects, because there doesn't seem to be a counterpart of that in type theory.... | |
| Dec 6, 2020 at 1:37 | comment | added | Mike Shulman | Essentially by definition, if I understand correctly. In the fibration constructed from a topos, the base category is the topos, while the fiber over an object $X$ is the poset of subobjects of $X$ (i.e. monomorphisms into $X$). So if there is an arrow $A\to B$ in the fiber, that means by definition that $A$ and $B$ are objects equipped with a monomorphism into $X$, and the former factors through the latter by a morphism $A\to B$. | |
| Dec 5, 2020 at 17:00 | comment | added | YKY | Thanks, my question is actually more related to your answer... specifically I don't know how the topos logic is related to the type theory via Curry-Howard. If there is an arrow $A \Rightarrow B$ in the fiber, how does one assure that there is a corresponding type or term in the base? | |
| Dec 5, 2020 at 1:30 | history | answered | Mike Shulman | CC BY-SA 4.0 |