Homotopy type theory as a language for diagrams of $\infty$-logoses

TL;DR

This paper demonstrates how homotopy type theory extended with modalities can model diagrams of $ abla$-logoses, enabling reasoning about complex higher-dimensional logical structures within a unified type-theoretic framework.

Contribution

It introduces a method to reconstruct diagrams of $ abla$-logoses in homotopy type theory with modalities, extending the scope of synthetic reasoning to higher dimensions.

Findings

Diagrams of $ abla$-logoses can be reconstructed in extended homotopy type theory.

Enables reasoning about multiple $ abla$-logoses simultaneously.

Provides a higher-dimensional version of synthetic Tait computability.

Abstract

We show that certain diagrams of $\infty$-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 $\infty$-logos but also a diagram of $\infty$-logoses. This also provides a higher dimensional version of Sterling's synthetic Tait computability -- a type theory for higher dimensional logical relations.