Martin Escardo

@EscardoMartin

@jonmsterling @agdakx @JulesJacobs5 @andrejbauer (I don't want an implicit coersion. I want x to be an element of a group, rather than an element of a type.)

14/10/2022, 18:24:48

Favs: 5

Retweets: 0

Martin Escardo

@EscardoMartin

@jonmsterling @agdakx @JulesJacobs5 @andrejbauer (Foundations currently emphasize precision and consistency. But there is scope for "practical foundations" that additionally address how mathematicians (of all kinds!) actually do and write mathematics. In particular, this matters regarding how structures are organized.)

14/10/2022, 18:32:57

Favs: 6

Retweets: 0