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

This paper demonstrates that homotopy type theory extended with specific lex, accessible modalities can reconstruct diagrams of $\infty$-logoses, thereby enabling reasoning about multiple $\infty$-logoses simultaneously and providing a higher-dimensional generalization of Sterling's synthetic Tait computability.

The Gist

Here is an explanation of the paper "Homotopy Type Theory as a Language for Diagrams of $\infty$-Logoses" using simple language and creative analogies.

The Big Picture: Building a Universal Translator

Imagine you are a master architect who designs universes. In this paper, the author, Taichi Uemura, is working with two very different tools:

1. $\infty$-Logoses (The Universes): Think of these as massive, complex, self-contained worlds where mathematics happens. They are like "super-cities" where you can do advanced geometry and topology.
2. Homotopy Type Theory (The Language): This is a very precise, logical language (like a super-advanced version of English or Python) used to describe shapes, spaces, and how things connect.

The Problem:
Usually, this language is great at describing one universe at a time. But in real mathematics, these universes don't live in isolation. They are connected by bridges (functors) and tunnels (natural transformations). They form diagrams—complex networks of worlds.

The problem is that the language (Homotopy Type Theory) wasn't built to talk about the connections between worlds. It's like having a dictionary that can describe a single city perfectly, but if you try to describe a subway map connecting ten cities, the dictionary gets confused. It can't easily handle the "traffic" between the cities.

The Solution:
Uemura has invented a new way to use this language. He created a set of rules (called Mode Sketches) that allow the language to describe not just one world, but an entire network of worlds and the bridges between them, all from the inside.

---

The Core Concepts (With Analogies)

1. The "Fracture and Glue" Technique

Imagine you have a giant, messy puzzle. You want to understand the whole picture, but it's too big.

• The Old Way: You try to look at the whole thing at once and get overwhelmed.
• The New Way (Fracture and Glue): You break the puzzle into two manageable pieces:
  • Piece A (The Open Part): A section that is easy to see and flexible.
  • Piece B (The Closed Part): A section that is rigid and fixed.
• The Magic: You study Piece A and Piece B separately. Then, you use a special "glue" to snap them back together. The paper proves that if you know how to glue these two pieces, you can reconstruct the entire complex universe.

In the paper, this "glue" is a mathematical operation that takes two different types of logical rules and combines them into a new, bigger rule.

2. Mode Sketches (The Blueprint)

Think of a Mode Sketch as a blueprint or a flowchart for a network of universes.

• It's a simple drawing with dots (representing different universes) and arrows (representing the bridges between them).
• Some arrows are "one-way" (you can go from Universe A to B, but not back).
• Some triangles of arrows are "thin" (meaning the path going around the triangle is the same as going straight through; it's a perfect loop).

Uemura shows that for any blueprint you draw (as long as it follows certain simple rules), you can write a set of instructions in Homotopy Type Theory that perfectly recreates that entire network of universes.

3. Synthetic Tait Computability (The "Logical Relation" Superpower)

This is a fancy term for a technique used to prove that computer programs behave correctly.

• The Analogy: Imagine you want to prove that two different recipes for a cake will always taste the same. You don't just bake them; you look at the relationship between the ingredients.
• The Innovation: Uemura shows that his new "Mode Sketch" method is actually a super-powered, 3D version of this technique. Instead of just checking if two recipes are related, his method can check if entire networks of recipes are related in complex, multi-dimensional ways. This is crucial for proving that advanced computer languages (like those used in AI or quantum computing) are safe and reliable.

---

Why Does This Matter?

1. It Simplifies the Complex
Before this, mathematicians had to use very complicated, custom-built languages to talk about networks of universes. Uemura's method lets them use the standard, well-understood language (Homotopy Type Theory) to do the same job. It's like realizing you can build a skyscraper using standard Lego bricks instead of needing custom-molded plastic.

2. It Helps Computer Science
This isn't just abstract math. These "universes" are models for how computer programs work. By being able to describe complex networks of logic rules, we can build better tools to verify that software is bug-free. The paper mentions "normalization," which is essentially ensuring that a computer program will eventually finish its task and not get stuck in an infinite loop.

3. It Unifies Math and Code
The paper bridges the gap between pure geometry (shapes and spaces) and logic (computer code). It shows that the way we organize logical rules is mathematically identical to the way we organize geometric shapes in higher dimensions.

The Takeaway

Taichi Uemura has discovered a universal translator. He found a way to take a complex map of interconnected mathematical worlds and translate it into a single, coherent sentence in a logical language.

• Before: "I can describe World A. I can describe World B. But describing how they talk to each other is a nightmare."
• After: "I can describe the whole conversation between World A and World B using the same simple rules I use for a single world."

This opens the door to solving harder problems in both mathematics and computer science, allowing us to reason about complex systems with the same ease as simple ones.

Technical Summary

Here is a detailed technical summary of the paper "Homotopy Type Theory as a Language for Diagrams of $\infty$-Logoses" by Taichi Uemura.

1. Problem Statement

The paper addresses a fundamental limitation in Homotopy Type Theory (HoTT): while HoTT is a powerful internal language for reasoning about a single $\infty$-logos (or $\infty$-topos), it struggles to reason about diagrams of $\infty$-logoses (collections of $\infty$-logoses connected by functors and natural transformations).

• The Challenge: Naive internalization of such diagrams fails. For instance, internalizing arbitrary adjunctions leads to contradictions, and internalizing idempotent comonads often results in triviality.
• The Gap: Existing methods, such as "cohesive HoTT," require extending the type theory with new layers of context or modal operators, complicating the system. There is a need for a method to internalize diagrams of $\infty$-logoses using plain HoTT extended only by standard modalities, allowing for the study of higher-dimensional logical relations and normalization of complex type theories.

2. Methodology

The author introduces a framework called Mode Sketches to define specific shapes of diagrams that can be internalized within HoTT using Lex, Accessible Modalities (LAMs).

Core Concepts:

• Lex, Accessible Modalities (LAMs): These are modalities in HoTT that correspond to sub-$\infty$-toposes or localizations of an $\infty$-logos. They are "lex" (preserving finite limits) and "accessible" (presented by small data).
• Mode Sketches ($M$): A combinatorial structure defined as a finite decidable poset $I_M$ with a subset of "thin" triangles $T_M$.
  • Axiom A: For any $j \not\leq i$ in the poset, the modality $m(i)$ is "strongly disjoint" from $m(j)$ (denoted $m(i) \leq^\perp m(j)$). This effectively cuts off functors in one direction, leaving a directed diagram.
  • Axiom B: For "thin" triangles $(i_0 < i_1 < i_2)$, the canonical natural transformation between functors is invertible (making the triangle commute).
  • Axiom C: The top modality is the canonical join of all modalities in the sketch, ensuring the universe is reconstructed from the diagram.
• Synthetic Tait Computability: The paper reformulates Sterling's "Synthetic Tait Computability" (a technique for logical relations) purely in terms of modalities. It shows that a mode sketch is equivalent to postulating a lattice of propositions, where types are "fractured" into open and closed parts, behaving like logical relations.

Technical Tools:

• Fracture and Gluing Theorem: The paper improves the existing theorem by Rijke, Shulman, and Spitters, proving that the join of two lex modalities preserves accessibility (Proposition 2.17). This is crucial for constructing the internal universe.
• Oplax Limits: The semantics of these diagrams are interpreted as oplax limits of $\infty$-logoses. The paper establishes that the oplax limit of a diagram of $\infty$-logoses and lex, accessible functors is itself an $\infty$-logos (Theorem 5.43).
• Higher Category Theory: The paper utilizes $(\infty, 2)$-category theory, specifically the correspondence between oplax natural transformations and functors between $(\infty, 2)$-categories of elements (Corollary 5.55).

3. Key Contributions

1. Definition of Mode Sketches: A new class of diagram shapes definable internally in HoTT using LAMs. This allows the internal reconstruction of diagrams of $\infty$-logoses without extending the base type theory with new context layers.
2. Equivalence of Axioms (Theorem 4.4): The paper proves that the axioms defining a mode sketch (postulating LAMs) are equivalent to postulating a lattice of propositions. This generalizes Synthetic Tait Computability, showing that "logical relations as types" can be formulated purely via modalities.
3. Accessibility of Joins (Proposition 2.17): A technical proof that the join of two lex, accessible modalities (under the disjointness condition) remains accessible. This fills a gap in previous literature and ensures the resulting internal universe is well-behaved.
4. Main Semantic Theorem (Theorem 6.4): The central result establishing an equivalence between:
   • The $(\infty, 1)$-category of models of a mode sketch (an $\infty$-logos equipped with LAMs satisfying the axioms).
   • The $(\infty, 1)$-category of diagrams of $\infty$-logoses indexed over the mode sketch (interpreted as an $(\infty, 2)$-category).
   • The reconstruction of the model is achieved via oplax limits, generalizing Artin gluing.
5. Higher-Dimensional Logical Relations: By working in HoTT, the framework naturally yields higher-dimensional logical relations, extending Sterling's work to $\infty$-type theories.

4. Results

• Internal Reconstruction: For any mode sketch $M$, one can construct a diagram of $\infty$-logoses internally in HoTT. The universe of the internal $\infty$-logos is equivalent to the oplax limit of the diagram.
• Generalization of Artin Gluing: The classic Artin gluing (gluing two logoses along a functor) is shown to be the specific case of a mode sketch with two elements. The paper generalizes this to arbitrary finite diagrams defined by mode sketches.
• Mate Correspondence: The paper establishes a new result in $(\infty, 2)$-category theory: an equivalence between the spaces of oplax and lax natural transformations for diagrams indexed over an arbitrary $(\infty, 2)$-category (Proposition 5.58).
• Normalization Applications: The framework is designed to support the normalization of $\infty$-type theories (introduced by Nguyen and Uemura), providing a synthetic method to prove properties of complex type theories via logical relations.

5. Significance

• Simplicity and Formalizability: Unlike "cohesive HoTT" which requires complex extensions, this approach uses plain HoTT with standard modalities. This makes the results immediately formalizable in existing proof assistants (like Agda or Coq) and easier to use informally.
• Unified Framework for Logical Relations: It provides a synthetic, higher-dimensional generalization of logical relations. Instead of manually constructing relations for each type theory, one can define a mode sketch, and the type theory automatically generates the appropriate "fractured" types representing these relations.
• Bridging Type Theory and Higher Category Theory: The paper rigorously connects the internal language of type theory (modalities) with external categorical structures (oplax limits of $\infty$-logoses). It demonstrates that the semantics of type theory can naturally encompass diagrams of $\infty$-toposes, not just single ones.
• Future Directions: This work lays the groundwork for analyzing $\infty$-type theories and proving meta-theoretic properties (like normalization) for them using synthetic methods, moving beyond the limitations of set-level or single-topos reasoning.

In summary, Uemura successfully demonstrates that Homotopy Type Theory, when augmented with specific lex, accessible modalities, serves as a robust and synthetic language for reasoning about diagrams of $\infty$-logoses, effectively internalizing higher-dimensional logical relations and generalizing Artin gluing.