Skip to main content
4 events
when toggle format what by license comment
Feb 6, 2014 at 20:24 history edited Urs Schreiber CC BY-SA 3.0
added an addendum pointing to notes that further develop the theme of the comment
Apr 24, 2013 at 19:58 comment added Urs Schreiber @Margaret, right, so Heyting algebras are to toposes as logic is to type theory (ncatlab.org/nlab/show/type%20theory): the latter includes the former. So what I said above involves not just intuitionistic logic, but also intuitionistic type theory (ncatlab.org/nlab/show/intuitionistic%20type%20theory). But that's only natural.
Apr 24, 2013 at 19:43 comment added Margaret Friedland @Urs: thanks for elaboration. However, Heyting algebras are not a mere analogy (or non-analogy) here. There is a connection to topos theory, which I could not articulate, not being conversant in the theory. I found useful information on this under the following link (to a project which you co-authored): ncatlab.org/nlab/show/Heyting+algebra#to_toposes_35
Apr 24, 2013 at 18:04 history answered Urs Schreiber CC BY-SA 3.0