dginev
commented
5 years ago The second link did get lost, copying first one verbatim:
Unfortunately, many of their (presumably automatically) added
hyperlinks are wrong. E.g.
"universe" -> http://planetmath.org/universe or
http://planetmath.org/universeofdiscourse
"equivalent" -> http://planetmath.org/filterbasis or
http://planetmath.org/equivalenceofforcingnotions or
http://planetmath.org/equivalentmachines or
http://planetmath.org/equivalencerelation
"contraction" -> http://planetmath.org/sequent
"connotations" -> http://planetmath.org/signrelation
"quasi-inverse" -> http://planetmath.org/quasiinverseofafunction
and this only from a random sampling of a couple of sections.
However, more internal hyperlinking is an interesting idea:
https://github.com/HoTT/book/issues/598
Just putting these here so they don't get lost - I imagine they will be resolved in the course of current work on link accuracy.
https://groups.google.com/forum/#!topic/homotopytypetheory/tZMQEa7y35k
http://nforum.mathforge.org/discussion/5025/homotopy-type-theory-univalent-foundations-of-mathematics/?Focus=44415#Comment_44415