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
link← @EscardoMartin Twitter archive
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
linkMartin 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
linkMartin Escardo
@EscardoMartin
@jonmsterling @agdakx @JulesJacobs5 @andrejbauer Here I summarize what I want. But very imprecisely. The problem is to make my question precise and answer it precisely:
https://twitter.com/EscardoMartin/status/1580982517263642625
14/10/2022, 19:20:45
Favs: 1
Retweets: 0
link