Author: tomr Format: TextIs there category of HoTT theorie (category of category of contexts, where the particular category of contexts is the categorical counterpart of particular HoTT theory)? Has someone specified it and are there some theorems about it?
There are similar notions in the boundary fields already:
* Instituion in the logics and computer science (https://en.wikipedia.org/wiki/Institution_(computer_science))
* category of First order theories and subcategory of geometrical theories as defined by Olivia Caramell (in her book https://global.oup.com/academic/product/theories-sites-toposes-9780198758914?cc=it&lang=en&, while I wonder that she mentions that there is some controversy around it http://www.oliviacaramello.com/Unification/Controversy.html)
So - are there some results or maybe it is not possible or it is not interesting to pursue building such category. I have my goals of using such category in the formalization of deep learning and I wonder what is the status of its research?
Is there category of HoTT theorie (category of category of contexts, where the particular category of contexts is the categorical counterpart of particular HoTT theory)? Has someone specified it and are there some theorems about it?
There are similar notions in the boundary fields already: * Instituion in the logics and computer science (https://en.wikipedia.org/wiki/Institution_(computer_science)) * category of First order theories and subcategory of geometrical theories as defined by Olivia Caramell (in her book https://global.oup.com/academic/product/theories-sites-toposes-9780198758914?cc=it&lang=en&, while I wonder that she mentions that there is some controversy around it http://www.oliviacaramello.com/Unification/Controversy.html)
So - are there some results or maybe it is not possible or it is not interesting to pursue building such category. I have my goals of using such category in the formalization of deep learning and I wonder what is the status of its research?
Author: tomr Format: TextOK, this https://www.sciencedirect.com/science/article/pii/S0001870818303062 "The homotopy theory of type theories" seems to be the answer and the right point to start exploration. Thx.
OK, this https://www.sciencedirect.com/science/article/pii/S0001870818303062 "The homotopy theory of type theories" seems to be the answer and the right point to start exploration. Thx.