Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

Atrium > Mathematics, Physics & Philosophy: Is there category of HoTT theories (category of category of contexts)?

Bottom of Page

1 to 2 of 2

  1.  
    • CommentRowNumber1.
    • CommentAuthortomr
    • CommentTimeJul 25th 2023
    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?
    • CommentRowNumber2.
    • CommentAuthortomr
    • CommentTimeJul 25th 2023
    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.

1 to 2 of 2

  1.