Timeline for Recursively dependent types?
Current License: CC BY-SA 2.5
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 1, 2010 at 14:07 | history | edited | Paul Taylor | CC BY-SA 2.5 |
rewritten
|
| Dec 30, 2009 at 6:46 | comment | added | Mike Shulman | Yes, certainly. I was just using "display map" to mean "the projection from a dependent type to its context," but I can see that that might give the wrong impression. I don't think the point or the question depends on whether the whole category is lcc or not. (Also, just as an MO usage point, I think this would have been more appropriate as a "comment" than as an "answer.") | |
| Dec 29, 2009 at 23:00 | history | answered | Paul Taylor | CC BY-SA 2.5 |