Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Taichi Uemura

TL;DR

The paper addresses how to internalize diagrams of $\infty$-logoses within plain $\infty$-HoTT by developing mode sketches—structures encoding lex, accessible modalities arranged in finite posets. It introduces two equivalent axiom systems (modalities vs lattice propositions) and shows that models of a mode sketch are equivalent to diagrams of $\infty$-logoses indexed by the sketch, via oplax limits (Artin gluing generalization). This establishes a higher-dimensional synthetic framework for logical relations and promises applications to higher type theories and normalization results. The approach unifies internal diagram reasoning with higher category theory, enabling a uniform, proof-assistant-friendly language for diagrams of $\infty$-logoses and their morphisms, including oplax transformations and mates.

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.

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

TL;DR

The paper addresses how to internalize diagrams of -logoses within plain -HoTT by developing mode sketches—structures encoding lex, accessible modalities arranged in finite posets. It introduces two equivalent axiom systems (modalities vs lattice propositions) and shows that models of a mode sketch are equivalent to diagrams of -logoses indexed by the sketch, via oplax limits (Artin gluing generalization). This establishes a higher-dimensional synthetic framework for logical relations and promises applications to higher type theories and normalization results. The approach unifies internal diagram reasoning with higher category theory, enabling a uniform, proof-assistant-friendly language for diagrams of -logoses and their morphisms, including oplax transformations and mates.

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.
Paper Structure (26 sections, 52 theorems, 38 equations, 1 figure)

This paper contains 26 sections, 52 theorems, 38 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Modalities in homotopy type theory
  3. Synthetic Tait computability
  4. Oplax limits of $(\infty, 1)$-categories
  5. Organization
  6. Related work
  7. Modalities in homotopy type theory
  8. The poset of lex, accessible modalities
  9. Accessibility of the canonical join
  10. Open and closed modalities
  11. Mode sketches
  12. Internal diagrams induced by modalities
  13. Mode sketches
  14. Intended models, internally
  15. Mode sketches and synthetic Tait computability
  16. ...and 11 more sections

Key Result

proposition 1

Let $\mathfrak{m}$ and $\mathfrak{n}$ be LAMs such that $\mathfrak{m}\leq {}^{\mathord{\mathrel{\bot}}}\mathfrak{n}$. In the special case when $\mathfrak{m}= {}^{\mathord{\mathrel{\bot}}} \mathfrak{n}$, we have $\mathfrak{m}\lor \mathfrak{n}= \mathfrak{Top}$.

Theorems & Definitions (127)

  • definition 1
  • definition 2
  • definition 3
  • definition 4
  • definition 5
  • definition 6
  • definition 7
  • definition 8: rijke2020modalities
  • definition 9
  • proposition 1: Fracture and gluing theorem
  • ...and 117 more