Fat Cell Structures and Generalized Algebraic Theories

Reference. Fat Cell Structures and Generalized Algebraic Theories

Xu Huang, Carlo Angiuli · LICS · 2026 · type-theory · DOI

We give a new syntax-independent account of finitely-presented generalized algebraic theories (GATs) as finite cell complexes in the category of categories with families (CwFs), in which GATs are constructed by successive pushouts along the CwF morphisms generically postulating a sort, an operation, or an equation. Inspired by the fat small object argument of Makkai, Rosický, and Vokřínek, we introduce fat GAT presentations, thereby allowing infinite presentations with non-linear dependency structure. Then, motivated by wanting our GATs to self-describe, we extend presentations to admit infinitary arities, including infinitely deep dependency chains. Finally, we verify that these generalized GATs satisfy expected semantic properties including Frey’s Gabriel–Ulmer duality.

Cite

Cite as @huang-2026-fat (helia, typst) · \cite{huang-2026-fat} (LaTeX)

BibTeX

bibtex · 14 lines

@inproceedings{huang-2026-fat,
  doi = {10.4230/LIPICS.LICS.2026.58},
  url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.58},
  author = {Huang, Xu and Angiuli, Carlo},
  keywords = {Generalized algebraic theories, quotient inductive-inductive types, categories with families, cell complexes, logical frameworks, Gabriel-Ulmer duality, Theory of computation → Categorical semantics, Theory of computation → Type theory},
  language = {en},
  title = {Fat Cell Structures and Generalized Algebraic Theories},
  volume = {380},
  pages = {58:1-58:27},
  publisher = {Schloss Dagstuhl – Leibniz-Zentrum für Informatik},
  year = {2026},
  copyright = {Creative Commons Attribution 4.0 International license},
  booktitle = {41st Annual Symposium on Logic in Computer Science (LICS 2026)}
}

hayagriva YAML (typst)

yaml · 16 lines

huang-2026-fat:
  type: article
  title: Fat Cell Structures and Generalized Algebraic Theories
  author:
  - Huang, Xu
  - Angiuli, Carlo
  date: 2026
  page-range: 58:1-58:27
  url: https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.58
  serial-number:
    doi: 10.4230/LIPICS.LICS.2026.58
  parent:
    type: proceedings
    title: 41st Annual Symposium on Logic in Computer Science (LICS 2026)
    publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
    volume: 380

Download: huang-2026-fat.bib · huang-2026-fat.yml

Cites 52 works (3 here)

With notes (3)

The Univalence Principle ahrens-2021-theMem. AMS · 2025

The Univalence Principle is the statement that equivalent mathematical structures are indistinguishable. We prove a general version of this principle that applies to all set-based, categorical, and higher-categorical structures defined in a non-algebraic and space-based style, as well as models of higher-order theories such as topological spaces. In particular, we formulate a general definition of indiscernibility for objects of any such structure, and a corresponding univalence condition that generalizes Rezk’s completeness condition for Segal spaces and ensures that all equivalences of structures are levelwise equivalences. Our work builds on Makkai’s First-Order Logic with Dependent Sorts, but is expressed in Voevodsky’s Univalent Foundations (UF), extending previous work on the Structure Identity Principle and univalent categories in UF. This enables indistinguishability to be expressed simply as identification, and yields a formal theory that is interpretable in classical homotopy theory, but also in other higher topos models. It follows that Univalent Foundations is a fully equivalence-invariant foundation for higher-categorical mathematics, as intended by Voevodsky.

DOI · arXiv

Syntax and semantics of dependent types Hofmann_1997Semantics and Logics of Computation · 1997

DOI

Functorial Semantics of Algebraic Theories lawvere_19631963

Web

External (49)

Comparing semantic frameworks for dependently-sorted algebraic theories (2025)
Duality for clans: an extension of Gabriel–Ulmer duality (2025)
Homotopy languages (2025)
∞-type theories (2025)
The shape of contexts (2024)
Second-order generalised algebraic theories: Signatures and first-order semantics (2024)
A general framework for the semantics of type theory (2023)
Univalent monoidal categories (2023)
On generalized algebraic theories and categories with families (2021)
Categories with Families: Unityped, Simply Typed, and Dependently Typed (2021)
An equational logical framework for type theories (2021)
Effective Metatheory for Type Theory (2021)
Homotopical inverse diagrams in categories with attributes (2021)
From dependent type theory to higher algebraic structures (2021)
A proof and formalization of the initiality conjecture of dependent type theory (2020)
Large and infinitary quotient inductive-inductive types (2020)
What are we thinking when we present a type theory? (2020)
A model 2-category of enriched combinatorial premodel categories (2019)
Building on the diamonds between theories: Theory presentation combinators (2019)
Constructing quotient inductive-inductive types (2019)
Natural models of homotopy type theory (2018)
The generalised algebraic theory of contextual categories (2018)
Model structures on categories of models of type theories (2018)
The homotopy theory of type theories (2018)
Undecidability of equality in the free locally cartesian closed category (extended version) (2017)
Notes on clans and tribes (2017)
Type theory in type theory using quotient inductive types (2016)
Subsystems and regular quotients of C-systems (2016)
Combinatorial structure of type dependency (2015)
Univalence for inverse diagrams and homotopy canonicity (2015)
On a fat small object argument (2014)
The theory and practice of Reedy categories (2014)
A classification of accessible categories (2002)
Model categories (1999)
Practical Foundations of Mathematics (1999)
Internal type theory (1996)
Formal objects in type theory using very dependent types (1996)
On the meanings of the logical constants and the justifications of the logical laws (1996)
First order logic with dependent sorts, with applications to category theory (1995)
Locally Presentable and Accessible Categories (1994)
A framework for defining logics (1993)
Cellular Structures in Topology (1990)
Programming in Martin-Löf’s Type Theory (1990)
The finiteness obstruction of C. T. C. Wall (1989)
Generalised algebraic theories and contextual categories (1986)
Intuitionistic type theory (1984)
Generalised algebraic theories and contextual categories (1978)
An intuitionistic theory of types: Predicative part (1975)
Lokal präsentierbare Kategorien (1971)