Table of Contents
Fetching ...

Homotopy Languages

César Bardomiano Martínez, Simon Henry

TL;DR

This work develops a homotopy-invariant first-order language attached to the fibrant objects of (weak) model categories, generalizing the Blanc-Freyd categorical language to higher-categorical and diagrammatic contexts. It constructs two complementary viewpoints—the syntactic approach via generalized $\kappa$-algebraic theories and the category/clan approach using $\kappa$-clans and their boolean-algebra languages—and proves fundamental invariance theorems ensuring formulas are preserved under homotopy, weak equivalence, and Quillen equivalence. The framework is illustrated across a wide array of models (categories, 2-categories, chain complexes, topological spaces, Kan complexes, Segal spaces, and Segal-type structures), showing how to express homotopical properties without equality. A central technical development is a Brown-style path-object construction and Barton trivial fibrations, enabling invariance results to extend along diagrams and along Quillen equivalences. Overall, the paper provides a unifying logic for homotopy-theoretic structures, with potential applications to semantic interpretation, language-invariant reasoning, and higher-categorical model theory.

Abstract

We attach to each weak model category $\mathcal{M}$ a class of first order formulas about the fibrant objects of $\mathcal{M}$ whose validity is invariant under homotopies and weak equivalences. This is a generalization of the classical Blanc-Freyd Language of categories -- which involves formula avoiding equality on objects and which are invariant under isomorphism and equivalences of categories. In particular, we obtain similar homotopy invariant languages for $2$-categories, bicategories, chain complexes, Kan complexes, quasi-categories, Segal spaces, and so on...

Homotopy Languages

TL;DR

This work develops a homotopy-invariant first-order language attached to the fibrant objects of (weak) model categories, generalizing the Blanc-Freyd categorical language to higher-categorical and diagrammatic contexts. It constructs two complementary viewpoints—the syntactic approach via generalized -algebraic theories and the category/clan approach using -clans and their boolean-algebra languages—and proves fundamental invariance theorems ensuring formulas are preserved under homotopy, weak equivalence, and Quillen equivalence. The framework is illustrated across a wide array of models (categories, 2-categories, chain complexes, topological spaces, Kan complexes, Segal spaces, and Segal-type structures), showing how to express homotopical properties without equality. A central technical development is a Brown-style path-object construction and Barton trivial fibrations, enabling invariance results to extend along diagrams and along Quillen equivalences. Overall, the paper provides a unifying logic for homotopy-theoretic structures, with potential applications to semantic interpretation, language-invariant reasoning, and higher-categorical model theory.

Abstract

We attach to each weak model category a class of first order formulas about the fibrant objects of whose validity is invariant under homotopies and weak equivalences. This is a generalization of the classical Blanc-Freyd Language of categories -- which involves formula avoiding equality on objects and which are invariant under isomorphism and equivalences of categories. In particular, we obtain similar homotopy invariant languages for -categories, bicategories, chain complexes, Kan complexes, quasi-categories, Segal spaces, and so on...

Paper Structure

This paper contains 43 sections, 127 theorems, 182 equations.

Key Result

Theorem 1

If $X$ is fibrant and $v:C \to X$ is homotopic to $v':C \to X$ then $M \vdash \phi(v) \Leftrightarrow M \vdash \phi(v')$.

Theorems & Definitions (317)

  • Theorem : $1^{st}$ Invariance
  • Theorem : $2^{nd}$ Invariance
  • Theorem : $3^{rd}$ Invariance
  • Theorem : $4^{th}$ Invariance
  • Definition 2.1
  • Remark 2.2
  • Example 2.3
  • Example 2.4
  • Definition 2.6
  • Proposition 2.7
  • ...and 307 more