Timeline for Free models of finitely presented essentially algebraic theories in elementary toposes?
Current License: CC BY-SA 4.0
8 events
when toggle format | what | by | license | comment | |
---|---|---|---|---|---|
Mar 18, 2020 at 9:02 | vote | accept | Peter LeFanu Lumsdaine | ||
Nov 30, 2019 at 14:38 | comment | added | David Roberts♦ | @Simon ah, thanks. I thought it uncharacteristic of you to make such a bold and false statement; I apologise! | |
Nov 30, 2019 at 14:24 | comment | added | Simon Henry | @DavidRoberts : we are only talking about finitary theories here. The type of problems you are referring too is for infinitary theories. | |
Nov 30, 2019 at 11:34 | comment | added | David Roberts♦ | "predicative toposes" of Moerdijk and Palmgren, and this includes elementary toposes with NNO. really? I think you probably need WISC or even M&P's "strong AMC" (as van den Berg calls it) to get the result. vdB says ZF is not enough to prove free algebras of algebraic theories exist. | |
Nov 30, 2019 at 8:27 | comment | added | Andrej Bauer | Steve and Erik's paper is my favorite presentation of this topic. | |
Nov 29, 2019 at 16:11 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 146 characters in body
|
Nov 23, 2019 at 18:01 | comment | added | Peter LeFanu Lumsdaine | An external/categorical argument is what I was really hoping for, but in lieu of that, this paper seems the next best thing: they give a clean, self-contained, and foundationally economical presentation of the construction, which makes its internalisability much easier to check. I’ll accept this answer in a day or two, unless anyone finds a better answer in that time. | |
Nov 23, 2019 at 14:30 | history | answered | Simon Henry | CC BY-SA 4.0 |