Author: tomr Format: TextJust quick question - are there some theorems, results than connect some concrete HoTT theory (collection of types and terms) with the topological invariants of the nerve of the category of contexts for this theory, e.g. https://arxiv.org/abs/1703.03007 details how such category can be constructed for particular theory, of course, one can take nerve of it and then compute some topological invariants for this nerve. Maybe invariants can say something interesting about theory and maybe they can be used to classify such theories. E.g. book https://global.oup.com/academic/product/theories-sites-toposes-9780198758914?cc=it&lang=en& has some very general classification of theories (e.g. geometric theories), but this classification is for classical (not HoTT) theories.
Just quick question - are there some theorems, results than connect some concrete HoTT theory (collection of types and terms) with the topological invariants of the nerve of the category of contexts for this theory, e.g. https://arxiv.org/abs/1703.03007 details how such category can be constructed for particular theory, of course, one can take nerve of it and then compute some topological invariants for this nerve. Maybe invariants can say something interesting about theory and maybe they can be used to classify such theories. E.g. book https://global.oup.com/academic/product/theories-sites-toposes-9780198758914?cc=it&lang=en& has some very general classification of theories (e.g. geometric theories), but this classification is for classical (not HoTT) theories.
Author: tomr Format: TextI am thinking about HoTT as knowledge representation formalism which is good or is not good according to https://link.springer.com/chapter/10.1007/978-3-030-93758-4_19
I am thinking about HoTT as knowledge representation formalism which is good or is not good according to https://link.springer.com/chapter/10.1007/978-3-030-93758-4_19
Author: tomr Format: TextSurprisingly, this morning Arxiv announced article along these lines https://arxiv.org/abs/2306.12011 "Non-trivial higher homotopy of first-order theories". So, people are thinking about this. Of course, this article is about FOL theories only.
Surprisingly, this morning Arxiv announced article along these lines https://arxiv.org/abs/2306.12011 "Non-trivial higher homotopy of first-order theories". So, people are thinking about this. Of course, this article is about FOL theories only.