Skip to main content
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