You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Valery Isaev (Aug 22 2021 at 18:35):Let's say we want to formalize semantics of type theory in HoTT. It is a famous problem to formalize semantics of HoTT in HoTT, but I thought it should be straightforward to formalize TT+K in HoTT since we can model it in sets, so the coherence problems shouldn't be an issues. But now after some thought I'm not actually sure it is possible. It seems we still run into the same problems. Did anyone try to do this?
Valery Isaev (Aug 22 2021 at 18:43):To clarify, the problem is that the type of sets (if we want to model it in sets) is not a set, so if we want to use CwA for example, it should be based on (pre)categories and the type of types in a context cannot be a set, it should be at least a 1-type. Since everything is truncated, it seems we should be able to deal with coherence problems, but I'm not sure. So, I'd like to know if it was done already.
Mike Shulman (Aug 22 2021 at 19:45):Yes, that's a problem! I don't think anyone has solved it yet.
Steve Awodey (Aug 23 2021 at 03:21):The HoTT Zulip is probably a better place for this question.