agda-unimath
agda-unimath copied to clipboard
UniMath
Update metric spaces table
Some upcoming PRs (#1378, #1402, #1398, #1417, etc.) introduce new metric spaces so we should update tables/metric-spaces.md accordingly. However, since some of these PRs are already quite ready, I think it's better to merge them and update the table in some separate PR(s).
This could also be the place for people to add which metric spaces they wish in the library, so other people could fill the blanks.
- [ ] metric space of sequences in a metric space (#1378)
- [ ] metric space of convergent sequences in a metric space (#1378)
- [ ] metric space of Cauchy approximations in a complete metric space (#1402)
- [ ] metric space of Cauchy approximations in a saturated complete metric space (#1402)
- [ ] metric space of functions into a metric space (#1398)
- [ ] metric space of isometries between metric spaces (#1398)
- [ ] metric space of short maps between metric spaces (#1398)
- [ ] metric space of Lipschitz maps between metric spaces (#1417)
Maybe we could also add some new columns to the table, to mark which metric spaces are saturated and/or complete, or under which circumstances.
The table is already quite wide with its two columns, so I don't think it is well-advised to add more. However, what you might want to do is have another table of saturated metric spaces, and one for complete metric spaces, that you can feature on the appropriate pages.
The table is already quite wide with its two columns, so I don't think it is well-advised to add more. However, what you might want to do is have another table of saturated metric spaces, and one for complete metric spaces, that you can feature on the appropriate pages.
OK, I'll see how I can do it. For the moment I'll just try to keep track of new metric spaces here, and when I have a clearer idea, I'll update the metric-spaces table and possibly create new ones for saturated/complete spaces.
Actually, we could also consider reformatting the table. What comes to mind is merging the two current columns and separating the name and link by a newline instead. Then there's room for listing important properties
yeah, the current formatting seems a bit redundant. Let's see how many new metric spaces we need to add, and which property we'd like to list. See if some new format emerges.