On 2016-11-03 12:17, Steve Vickers wrote:
Actually, maths is _strong_ on types.
Yes, and I would say mathematics in particular as used within theoretical computer science (my chair is in that area), and how it focuses on types and type constructors, but the
... way "HoTTematics" doesn't comply with mathematics.
to me is a concern, e.g., since 'type constructors' are brought in from the outside, so as to say, and this is a bit of that "doesn't comply", isn't it, Steve? We've tried out something to keep those constructors "inside", not (yet) for that empty type, but some small pieces can be found following the links under GLIOC. It shows e.g. how we try to relate things back to Sch??nfinkel, Church and Curry and their G??ttingen times. Church's 'o' type in his 1940 paper is still not well understood, I think. His 'iota' is Martin-L??f's 'type', and we know how things went wrong when they started to say "type is a type". It was fixed but that fixing indeed "doesn't comply", does it? Best, Patrik [For admin and other information see: http://www.mta.ca/~cat-dist/ ]