Timeline for What notions of universe does predicative type theory admit?
Current License: CC BY-SA 2.5
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 11, 2010 at 19:05 | history | edited | François G. Dorais | CC BY-SA 2.5 |
fixed grammar and clarity
|
| Jan 11, 2010 at 18:56 | comment | added | François G. Dorais | I should have made it clearer which part of your question I was addressing. I conveniently ignored the induction part of your question, and I really don't know what happens there. Thanks for pointing out the issue in Setzer's work. I don't remember such issues in RGP, but the context is very different. | |
| Jan 11, 2010 at 13:57 | comment | added | Charles Stewart | Thanks. Palmgren kicked off the field with his PhD, which described the kind of constructions on universes need to make LUAs. IIRC, Setzer distinguishes between strong and weak Mahlo universes, where only the weak construction gives an induction principle. | |
| Jan 11, 2010 at 13:28 | history | answered | François G. Dorais | CC BY-SA 2.5 |