All Outputs (2)

Connecting Constructive Notions of Ordinals in Homotopy Type Theory (2021)
Conference Proceeding
Kraus, N., Nordvall Forsberg, F., & Xu, C. (2021). Connecting Constructive Notions of Ordinals in Homotopy Type Theory.

In classical set theory, there are many equivalent ways to introduce ordinals. In a constructive setting, however, the different notions split apart, with different advantages and disadvantages for each. We consider three different notions of ordinal... Read More about Connecting Constructive Notions of Ordinals in Homotopy Type Theory.

Internal ∞-Categorical Models of Dependent Type Theory : Towards 2LTT Eating HoTT (2021)
Conference Proceeding
Kraus, N. (2021). Internal ∞-Categorical Models of Dependent Type Theory : Towards 2LTT Eating HoTT. In 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (1-14). https://doi.org/10.1109/LICS52264.2021.9470667

Using dependent type theory to formalise the syntax of dependent type theory is a very active topic of study and goes under the name of "type theory eating itself" or "type theory in type theory." Most approaches are at least loosely based on Dybjer'... Read More about Internal ∞-Categorical Models of Dependent Type Theory : Towards 2LTT Eating HoTT.