2026-07-20T10:39:52Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26845 2026-07-09T11:31:10Z ddc:004 open_access

Fat Cell Structures and Generalized Algebraic Theories Huang, Xu Angiuli, Carlo Generalized algebraic theories quotient inductive-inductive types categories with families cell complexes logical frameworks Gabriel-Ulmer duality 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Xu Huang and Carlo Angiuli 2026 Is Part Of LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.LICS.2026.58 urn:nbn:de:0030-drops-268451 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.58 eng https://creativecommons.org/licenses/by/4.0/legalcode