What question did this study set out to answer?

The aim is to show how homotopy type theory can effectively describe diagrams of infinity-logoses and improve logical reasoning.

March 16, 2026Open Access

Homotopy type theory as a language for diagrams of -logoses

Key Points

The aim is to show how homotopy type theory can effectively describe diagrams of infinity-logoses and improve logical reasoning.
Extended homotopy type theory is employed using lex and accessible modalities.
Diagrams of infinity-logoses are analyzed within this theoretical framework.
The study illustrates a connection to Sterling's synthetic Tait computability.
Homotopy type theory successfully reconstructs certain diagrams of infinity-logoses.
A higher dimensional version of logical relations is established through this framework.

Abstract

We show that certain diagrams of -logoses are reconstructed in homotopy type theory extended with some lex, accessible modalities, which enables us to use plain homotopy type theory to reason about not only a single -logos but also a diagram of -logoses. This also provides a higher dimensional version of Sterling's synthetic Tait computability -- a type theory for higher dimensional logical relations.

Bookmark

View Full Paper