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