4 ms·
I saw some other comments mentioning the need for context, and I think the notion of structure captures this. The context for an equality is the kind of structu
by black_knight 4y ago
I saw some other comments mentioning the need for context, and I think the notion of structure captures this. The context for an equality is the kind of structures we are considering at the moment. As types ℕ and ℤ are equal, but structured as addition semirings in the conventional way they are different.
- Koshkin 4y agoWell, the "modern" way to speak about structure is in category theory terms, specifically in terms of morphisms and universal properties; similarly, the fuzzy idea of a context, in the article, is replaced with a restriction on the set of assertions you allow as making sense to begin with.
- black_knight 4y agoOne of the cool features of HoTT is that you can look at types and compute what "isomorphism" should mean even before you put a category structure on it. For instance for groups, you can see what as isomorphism of groups is just by looking at the type of groups as the type of tuples with carrier, operation, neutral element and laws. Some times you can even chose two different category structures for the same types, as long as the two agree on what the isomorphism are. This happens with graphs for instance, where there are several coherent notions of maps of graphs.
- k0k0r0 4y agoAny recommendation for a (short) introduction to HoTT for a working mathematician?
- Koshkin 4y agoThis comes to mind: https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pdf https://math.uchicago.edu/~may/REU2015/REUPapers/Macor.pdf
- k0k0r0 4y agoThank you very much!
- black_knight 4y agoAwodey has a shortish introduction here: https://arxiv.org/abs/1701.02024 https://arxiv.org/abs/1701.02024