Timeline for Existence of internal toposes/inner models in a topos
Current License: CC BY-SA 3.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 18, 2014 at 23:26 | comment | added | David Roberts♦ | @MichalR.Przybylek - I've gotten my hands on some lecture notes of Joyal from 1974. His definition of arithmetic universe at that point is a pretopos such that there are free internal categories on internal graphs. Maietti's definition (pretopos with parameterised list objects) implies Joyal's definition. | |
| Dec 16, 2014 at 4:03 | comment | added | David Roberts♦ | @Michal fair enough, I know the history of these ideas is convoluted... | |
| Dec 15, 2014 at 22:41 | comment | added | Michal R. Przybylek | Thanks, David, I'll take a look into the paper. But, anyway, I think it was Jean Benabou who first introduced the notion of an internal topos (BTW: I meant JEAN Benabou, of course. I can't believe I've written John. Shame on me...) | |
| Dec 15, 2014 at 22:35 | comment | added | David Roberts♦ | @Michal Joyal's definition has never been published or even circulated, so I can only point to work of Maietti (published in Theory and Appl. of Categories) and Paul (see link in his answer below). An internal topos is a model of the finite limit theory of toposes (I take the axioms to be pullbacks, Cartesian closed, subobject classifier, NNO, all given by specified operations). This is probably the same as what is in Problemes dans les topos, I don't have it in front of me. | |
| Dec 15, 2014 at 12:59 | comment | added | Michal R. Przybylek | David, what do you mean by "arithmetic universe" defined by Joyal? And what is your definition of an "internal topos"? Are your definitions of arithmetic universe and internal topos the same as given by John Benabou (and later described in "Problemes dans les topos")? | |
| Dec 15, 2014 at 8:38 | answer | added | Paul Taylor | timeline score: 8 | |
| Dec 15, 2014 at 8:36 | comment | added | François G. Dorais | An (elementary) boolean topos with nno is certainly able to construct the initial model of an essentially algebraic theory. Note that this model may be degenerate (equal to the terminal model) even if this is not true for the same theory in the real world. Booleanness shouldn't be that essential. Some parts of the classical theory rely on symbols of languages being distinguishable from each other but I don't think that's essential in this case. | |
| Dec 15, 2014 at 5:42 | history | edited | David Roberts♦ | CC BY-SA 3.0 |
added 259 characters in body; edited tags; edited title
|
| Dec 15, 2014 at 5:34 | history | asked | David Roberts♦ | CC BY-SA 3.0 |