Re: Grothendieck toposes

[Patrik Eklund <peklund@cs.umu.se>]

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/ ]