Timeline for Free models of finitely presented essentially algebraic theories in elementary toposes?
Current License: CC BY-SA 4.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 18, 2020 at 9:02 | vote | accept | Peter LeFanu Lumsdaine | ||
| Nov 30, 2019 at 0:04 | history | edited | YCor | CC BY-SA 4.0 |
unabbreviated in title, and removed ref-request which is already in tags
|
| Nov 23, 2019 at 14:30 | answer | added | Simon Henry | timeline score: 11 | |
| Nov 23, 2019 at 11:10 | comment | added | Peter LeFanu Lumsdaine | @SimonHenry: Thankyou, excellent suggestion/reference — I’d forgotten they make the metatheoretic requirements so clear. Could you make it an answer, and if I don’t get anything more explicit, I’ll accept it? | |
| Nov 22, 2019 at 22:49 | comment | added | Simon Henry | I guess Vickers and Palmgreen "Partial Horn logic ..." core.ac.uk/download/pdf/82110032.pdf qualifies. It gives a completely constructive (and even predicative) proof of the existence of the free model for essentially algebraic theory. Their work clearly applies in every exact locally cartesian closed category with a NNO (in particular elementary toposes with NNO). According to the authors, it also apply within an arithmetic universe (=Pretopos with parametrized list objects) but this is not as clear. But the paper do not develop these internal application explicitly. | |
| Nov 22, 2019 at 22:14 | history | edited | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |
clarified assumption of a natural numbers object
|
| Nov 22, 2019 at 22:13 | comment | added | Peter LeFanu Lumsdaine | @IvanDiLiberti: Sorry, yes, of course an NNO is needed. I’m too used to hanging out in circles where one takes “elementary topos” to always include an NNO. But I certainly don’t want to assume a Grothendieck topos (where this can be done off-the-shelf by adjoint functor theorems). | |
| Nov 22, 2019 at 19:53 | comment | added | Ivan Di Liberti | This is very much compatible with the additional request of a NNO. | |
| Nov 22, 2019 at 19:27 | comment | added | Dmitri Pavlov | The theory of rings is finitely presented, but does not have an initial object in the elementary topos of finite sets. In fact, existence of such initial objects immediately implies that the elementary topos under consideration is a W-topos. | |
| Nov 22, 2019 at 18:28 | comment | added | Ivan Di Liberti | Are you sure that you do not need at least a Grothendieck topos or a NNO? | |
| Nov 22, 2019 at 15:47 | history | asked | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |