Document Open Access Logo

Fat Cell Structures and Generalized Algebraic Theories

Authors Xu Huang , Carlo Angiuli

PDF

File

Thumbnail PDF
PDF
LIPIcs.LICS.2026.58.pdf
  • Filesize: 1.33 MB
  • 27 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Type theory
Keywords
  • Generalized algebraic theories
  • quotient inductive-inductive types
  • categories with families
  • cell complexes
  • logical frameworks
  • Gabriel-Ulmer duality

Metrics

Abstract

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 As Get BibTex

Xu Huang and Carlo Angiuli. Fat Cell Structures and Generalized Algebraic Theories. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 58:1-58:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.LICS.2026.58

Author Details

Xu Huang
  • Indiana University, Bloomington, IN, USA
Carlo Angiuli
  • Indiana University, Bloomington, IN, USA

Funding

This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-24-1-0350. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the United States Air Force.

Acknowledgements

We are especially grateful to Chaitanya Leena Subramaniam for many early conversations with the second author that inspired this line of inquiry. We also thank Jonas Frey and Daniel Gratzer for helpful discussions about this work.

References

  1. Jiří Adámek, Francis Borceux, Stephen Lack, and Jiří Rosický. A classification of accessible categories. Journal of Pure and Applied Algebra, 175(1):7-30, 2002. Special Volume celebrating the 70th birthday of Professor Max Kelly. URL: https://doi.org/10.1016/S0022-4049(02)00126-3.
  2. Jiří Adámek and Jiří Rosický. Locally Presentable and Accessible Categories, volume 189 of London Mathematical Society Lecture Note Series. Cambridge University Press, 1994. URL: https://doi.org/10.1017/CBO9780511600579.
  3. Benedikt Ahrens, Peter Lefanu Lumsdaine, and Paige Randall North. Comparing semantic frameworks for dependently-sorted algebraic theories. In Lecture Notes in Computer Science, Lecture Notes in Computer Science, pages 3-22. Springer Nature Singapore, Singapore, 2025. URL: https://doi.org/10.1007/978-981-97-8943-6_1.
  4. Benedikt Ahrens, Paige Randall North, Michael Shulman, and Dimitris Tsementzis. The Univalence Principle, volume 305 of Memoirs of the American Mathematical Society. American Mathematical Society, 2025. URL: https://doi.org/10.1090/memo/1541.
  5. Thorsten Altenkirch and Ambrus Kaposi. Type theory in type theory using quotient inductive types. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, pages 18-29, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2837614.2837638.
  6. Steve Awodey. Natural models of homotopy type theory. Mathematical Structures in Computer Science, 28(2):241-286, 2018. URL: https://doi.org/10.1017/S0960129516000268.
  7. Reid William Barton. A model 2-category of enriched combinatorial premodel categories. PhD thesis, Harvard University, 2019. URL: http://nrs.harvard.edu/urn-3:HUL.InstRepos:42013127.
  8. Marc Bezem, Thierry Coquand, Peter Dybjer, and Martín Escardó. On generalized algebraic theories and categories with families. Mathematical Structures in Computer Science, 31(9):1006-1023, 2021. Special issue in homage to Martin Hofmann. URL: https://doi.org/10.1017/S0960129521000268.
  9. Jacques Carette, Russell O'Connor, and Yasmine Sharoda. Building on the diamonds between theories: Theory presentation combinators, 2019. Preprint. URL: https://arxiv.org/abs/1812.08079.
  10. John Cartmell. Generalised algebraic theories and contextual categories. PhD thesis, Oxford University, 1978. URL: https://ncatlab.org/nlab/files/Cartmell-Thesis.pdf.
  11. John Cartmell. Generalised algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209-243, 1986. URL: https://doi.org/10.1016/0168-0072(86)90053-9.
  12. John Cartmell. The generalised algebraic theory of contextual categories, 2018. Unpublished note. URL: http://entitymodelling.org/downloads/theGATofCCs_10Jan2018.pdf.
  13. Simon Castellan, Pierre Clairambault, and Peter Dybjer. Undecidability of equality in the free locally cartesian closed category (extended version). Logical Methods in Computer Science, 13(4), November 2017. URL: https://doi.org/10.23638/LMCS-13(4:22)2017.
  14. Simon Castellan, Pierre Clairambault, and Peter Dybjer. Categories with Families: Unityped, Simply Typed, and Dependently Typed, pages 135-180. Springer International Publishing, Cham, 2021. URL: https://doi.org/10.1007/978-3-030-66545-6_5.
  15. Menno de Boer. A proof and formalization of the initiality conjecture of dependent type theory, 2020. Licentiate thesis, Stockholm University. URL: https://urn.kb.se/resolve?urn=urn:nbn:se:su:diva-181640.
  16. Peter Dybjer. Internal type theory. In Stefano Berardi and Mario Coppo, editors, Types for Proofs and Programs (TYPES 1995), volume 1158 of Lecture Notes in Computer Science, pages 120-134, Berlin, Heidelberg, 1996. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-61780-9_66.
  17. Jonas Frey. The shape of contexts. Presentation at COST WG6 meeting, April 2024. URL: https://europroofnet.github.io/_pages/WG6/Leuven/slides/frey.pdf.
  18. Jonas Frey. Duality for clans: an extension of Gabriel-Ulmer duality. The Journal of Symbolic Logic, pages 1-38, 2025. URL: https://doi.org/10.1017/jsl.2024.79.
  19. Rudolf Fritsch and Renzo Piccinini. Cellular Structures in Topology. Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1990. URL: https://doi.org/10.1017/CBO9780511983948.
  20. Peter Gabriel and Friedrich Ulmer. Lokal präsentierbare Kategorien. Lecture Notes in Mathematics. Springer, Berlin, Germany, January 1971. URL: https://doi.org/10.1007/BFb0059396.
  21. Richard Garner. Combinatorial structure of type dependency. Journal of Pure and Applied Algebra, 219(6):1885-1914, 2015. URL: https://doi.org/10.1016/j.jpaa.2014.07.015.
  22. Robert Harper. An equational logical framework for type theories, June 2021. Preprint. URL: https://arxiv.org/abs/2106.01484.
  23. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, January 1993. URL: https://doi.org/10.1145/138027.138060.
  24. Philipp Haselwarter. Effective Metatheory for Type Theory. PhD thesis, University of Ljubljana, 2021. URL: https://repozitorij.uni-lj.si/IzpisGradiva.php?id=134439.
  25. Allen Hatcher. Algebraic Topology. Cambridge University Press, 2001. URL: https://pi.math.cornell.edu/~hatcher/AT/ATpage.html.
  26. Jason Hickey. Formal objects in type theory using very dependent types. In The Third International Workshop on Foundations of Object-Oriented Languages, FOOL 3, 1996. URL: https://www.cs.cornell.edu/jyh/papers/fool3/.
  27. Martin Hofmann. Syntax and Semantics of Dependent Types, pages 79-130. Publications of the Newton Institute. Cambridge University Press, 1997. URL: https://doi.org/10.1017/CBO9780511526619.004.
  28. Mark Hovey. Model categories, volume 63 of Mathematical Surveys and Monographs. American Mathematical Society, Providence, RI, 1999. URL: https://doi.org/10.1090/surv/063.
  29. Valery Isaev. Model structures on categories of models of type theories. Mathematical Structures in Computer Science, 28(10):1695-1722, November 2018. URL: https://doi.org/10.1017/S0960129517000202.
  30. André Joyal. Notes on clans and tribes, October 2017. Preprint. URL: https://arxiv.org/abs/1710.10238.
  31. Ambrus Kaposi, András Kovács, and Thorsten Altenkirch. Constructing quotient inductive-inductive types. Proceedings of the ACM on Programming Languages, 3(POPL):2:1-2:24, January 2019. URL: https://doi.org/10.1145/3290315.
  32. Ambrus Kaposi and Szumi Xie. Second-order generalised algebraic theories: Signatures and first-order semantics. In International Conference on Formal Structures for Computation and Deduction, 2024. URL: https://doi.org/10.4230/LIPIcs.FSCD.2024.10.
  33. Krzysztof Kapulkin and Peter LeFanu Lumsdaine. The homotopy theory of type theories. Advances in Mathematics, 337:1-38, 2018. URL: https://doi.org/10.1016/j.aim.2018.08.003.
  34. Krzysztof Kapulkin and Peter LeFanu Lumsdaine. Homotopical inverse diagrams in categories with attributes. Journal of Pure and Applied Algebra, 225(4):106563, 2021. URL: https://doi.org/10.1016/j.jpaa.2020.106563.
  35. András Kovács and Ambrus Kaposi. Large and infinitary quotient inductive-inductive types. In Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 648-661, 2020. URL: https://doi.org/10.1145/3373718.3394770.
  36. Francis William Lawvere. Functorial semantics of algebraic theories. Proceedings of the National Academy of Sciences, 50(5):869-872, 1963. URL: https://doi.org/10.1073/pnas.50.5.869.
  37. Peter LeFanu Lumsdaine, Andrej Bauer, and Philipp Haselwarter. What are we thinking when we present a type theory? Presentation at HoTTEST, June 2020. URL: https://youtu.be/kQe0knDuZqg.
  38. M. Makkai, J. Rosický, and L. Vokřínek. On a fat small object argument. Advances in Mathematics, 254:49-68, 2014. URL: https://doi.org/10.1016/j.aim.2013.12.012.
  39. Michael Makkai. First order logic with dependent sorts, with applications to category theory, 1995. Unpublished note. URL: https://www.math.mcgill.ca/makkai/.
  40. Per Martin-Löf. An intuitionistic theory of types: Predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium '73, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. North-Holland, 1975. URL: https://doi.org/10.1016/S0049-237X(08)71945-1.
  41. Per Martin-Löf. Intuitionistic type theory, volume 1 of Studies in Proof Theory. Bibliopolis, 1984. URL: https://archive-pml.github.io/martin-lof/pdfs/Bibliopolis-Book-1984.pdf.
  42. Per Martin-Löf. On the meanings of the logical constants and the justifications of the logical laws. Nordic Journal of Philosophical Logic, 1(1):11-60, May 1996. URL: https://www.hf.uio.no/ifikk/english/research/publications/journals/njpl/files/vol1no1/meaning.pdf.
  43. César Bardomiano Martínez and Simon Henry. Homotopy languages, 2025. Preprint. URL: https://arxiv.org/abs/2510.02607.
  44. Hoang Kim Nguyen and Taichi Uemura. ∞-type theories. Higher Structures, 9(1):179-226, 2025. URL: https://doi.org/10.21136/HS.2025.04.
  45. Bengt Nordström, Kent Petersson, and Jan Smith. Programming in Martin-Löf’s Type Theory. Oxford University Press, 1990. URL: http://www.cse.chalmers.se/research/group/logic/book/.
  46. Emily Riehl and Dominic Verity. The theory and practice of Reedy categories. Theory and Applications of Categories, 29(9):256-301, 2014. URL: http://www.tac.mta.ca/tac/volumes/29/9/29-09.pdf.
  47. Michael Shulman. Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science, 25(5):1203-1277, 2015. URL: https://doi.org/10.1017/S0960129514000565.
  48. Chaitanya Leena Subramaniam. From dependent type theory to higher algebraic structures. PhD thesis, Université de Paris, 2021. URL: https://arxiv.org/abs/2110.02804.
  49. Paul Taylor. Practical Foundations of Mathematics, volume 59 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1999. URL: https://www.paultaylor.eu/~pt/prafm/.
  50. Taichi Uemura. A general framework for the semantics of type theory. Mathematical Structures in Computer Science, 33(3):134-179, 2023. Special issue: Homotopy Type Theory 2019. URL: https://doi.org/10.1017/S0960129523000208.
  51. Kalathoor Varadarajan. The finiteness obstruction of C. T. C. Wall. Canadian Mathematical Society Series of Monographs and Advanced Texts. John Wiley & Sons, Inc., New York, 1989. A Wiley-Interscience Publication. Google Scholar
  52. Vladimir Voevodsky. Subsystems and regular quotients of C-systems. In A Panorama of Mathematics: Pure and Applied, volume 658 of Contemporary Mathematics, pages 127-137. American Mathematical Society, 2016. URL: https://doi.org/10.1090/conm/658/13124.
  53. Kobe Wullaert, Ralph Matthes, and Benedikt Ahrens. Univalent monoidal categories. In Delia Kesner and Pierre-Marie Pédrot, editors, 28th International Conference on Types for Proofs and Programs (TYPES 2022), volume 269 of Leibniz International Proceedings in Informatics (LIPIcs), pages 15:1-15:21, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.TYPES.2022.15.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact