Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
There is a question at Math Overflow that I don't have time to answer now, but it would be a shame if Mike Shulman didn’t get a chance to notice it: http://mathoverflow.net/questions/172980/what-is-semantics-of-type-do-types-of-type-theory-semantically-differ-fro
(It might get moved to Math Stackexchange.)
Well, I don’t really have time to write a long answer, and I’m not sure whether anything I’ve already written is exactly what this guy seems to be looking for.
There were at least some useful comments to the question at Math Overflow, but now that it's been migrated, these seem to be inaccessible!
1 to 3 of 3