HEXAGONbeta

The Grothendieck construction between the telescope monad and contextads

A mix of human-written and AI-generated textHuman understanding: some partsmath.CT — Category Theorycs.MS — Mathematical Software

Contributed by Kotaro Kamiya ↗

Version 1 / Oct 17, 2026 / CC BY 4.0

Abstract

A telescope is a list of stages in which each stage is a family indexed over the Grothendieck construction of the previous ones. The telescope monad stacks stages as the free-monoid 2-monad on spans, whereas a contextad collapses two stages into one by a dependent sum. This paper derives both from the span of single stages, and thereby explains why the strict algebras of the telescope monad are contextads. The link is the Grothendieck extension of a span. Because it is monoidal and preserves coproducts, it turns the telescopes into the free monad on the extension of the span of stages and the stage contextad into the Grothendieck monad, whose Kleisli arrows are the contextful arrows. The main theorem identifies the stage contextad with the pseudo-algebra of the telescope monad transported from the display contextad. Its structure map is the dependent sum, which the extension turns into the iterated multiplication of the Grothendieck monad.

Provenance statement

This work was produced by the author with an AI agent based on a large language model. The author set the research direction, posed the questions and made the decisions on scope, structure and notation. The agent wrote drafts of the text, proofs and figures, and the author directed their revision through repeated rounds of close reading. The final text therefore results from the author's corrections to sentences, notation and figures. The agent also checked the drafts against the cited literature and kept notation, cross-references and the build consistent. Independent instances of the agent reviewed the drafts and tried to refute proofs, and the gaps they found were fixed.

References

  1. N. Arkor, P. Saville, A. Slattery. Bicategories of algebras for relative pseudomonads. Preprint, arXiv:2501.12510 (https://arxiv.org/abs/2501.12510), 2025.arXiv
  2. S. Awodey. Natural models of homotopy type theory. Math. Struct. Comput. Sci. 28(2):241--286, 2018. arXiv:1406.3219 (https://arxiv.org/abs/1406.3219).arXiv
  3. B. Ahrens, P. LeFanu Lumsdaine, P. R. North. Comparing semantic frameworks for dependently-sorted algebraic theories. Preprint, arXiv:2412.19946 (https://arxiv.org/abs/2412.19946), 2024.arXiv
  4. S. Awodey, C. Newstead. Polynomial pseudomonads and dependent type theory. Preprint, arXiv:1802.00997 (https://arxiv.org/abs/1802.00997), 2018.arXiv
  5. R. Blackwell, G. M. Kelly, A. J. Power. Two-dimensional monad theory. J. Pure Appl. Algebra 59(1), 1--41, 1989.
  6. R. Bocquet. Strictification of weakly stable type-theoretic structures using generic contexts. Preprint, arXiv:2111.10862 (https://arxiv.org/abs/2111.10862), 2021.arXiv
  7. J. Cartmell. Generalised algebraic theories and contextual categories. Ann. Pure Appl. Logic 32, 209--243, 1986.
  8. G. Coraglia, J. Emmenegger. A 2-categorical analysis of context comprehension. Preprint, arXiv:2403.03085 (https://arxiv.org/abs/2403.03085), 2024.arXiv
  9. G. S. H. Cruttwell, M. J. Lambert, D. A. Pronk, M. Szyld. Double fibrations. Theory Appl. Categ. 38(35), 1326--1394, 2022. Numbers refer to the journal version. Its Definition 2.25 is Definition 2.23 of arXiv:2205.15240 (https://arxiv.org/abs/2205.15240).arXiv
  10. M. Capucci, D. J. Myers. Contextads as wreaths; Kleisli, Para, and Span constructions as wreath products. Preprint, arXiv:2410.21889 (https://arxiv.org/abs/2410.21889), 2024.arXiv
Show all 31 referencesShow fewer references
  1. N. G. de Bruijn. Telescopic mappings in typed lambda calculus. Inform. and Comput. 91(2), 189--204, 1991.
  2. N. Gambino, J. Kock. Polynomial functors and polynomial monads. Math. Proc. Cambridge Philos. Soc. 154(1):153--192, 2013. arXiv:0906.4931 (https://arxiv.org/abs/0906.4931).arXiv
  3. B. Jacobs. Categorical Logic and Type Theory . Stud. Logic Found. Math. 141, North-Holland, 1999.
  4. B. Jacobs. Comprehension categories and the semantics of type dependency. Theoret. Comput. Sci. 107(2), 169--207, 1993.
  5. K. Kamiya. The contextad of double telescopes. Preprint, 2026.
  6. G. M. Kelly. A unified treatment of transfinite constructions for free algebras, free monoids, colimits, associated sheaves, and so on. Bull. Austral. Math. Soc. 22(1), 1--83, 1980.
  7. G. M. Kelly, S. Lack. Monoidal functors generated by adjunctions, with applications to transport of structure. In Galois Theory, Hopf Algebras, and Semiabelian Categories , Fields Inst. Commun. 43, 319--340. Amer. Math. Soc., 2004.
  8. S. Lack. A coherent approach to pseudomonads. Adv. Math. 152(2), 179--202, 2000.
  9. A. Joyal and R. Street. The geometry of tensor calculus, I. Adv. Math. 88(1):55--112, 1991.
  10. N. Johnson and D. Yau. 2-Dimensional Categories . Oxford University Press, 2021. arXiv:2002.06055 (https://arxiv.org/abs/2002.06055).arXiv
  11. A. Joyal and R. Street. Pullbacks equivalent to pseudopullbacks. Cahiers Topologie Géom. Différentielle Catég. 34(2):153--156, 1993.
  12. T. Leinster. Higher Operads, Higher Categories . London Math. Soc. Lecture Note Ser. 298. Cambridge University Press, 2004. arXiv:math/0305049 (https://arxiv.org/abs/math/0305049).arXiv
  13. F. Lucatelli Nunes. Pseudoalgebras and non-canonical isomorphisms. Appl. Categ. Structures 27(1):55--63, 2019.
  14. M. B. McCurdy. Graphical methods for T annaka duality of weak bialgebras and weak H opf algebras. Theory Appl. Categ. , 26(9):233--280, 2012.
  15. F. Loregian, E. Riehl. Categorical notions of fibration. Expo. Math. 38(4), 496--514, 2020.
  16. C. Newstead. Algebraic Models of Dependent Type Theory . PhD thesis, Carnegie Mellon University, 2018. arXiv:2103.06155 (https://arxiv.org/abs/2103.06155).arXiv
  17. E. Palmgren. The Grothendieck construction and models for dependent types. Notes, 2013, revised 2016, https://staff.math.su.se/palmgren/iterated_presheaves_and_dependent_types_v8.pdf.link
  18. P. Selinger. A survey of graphical languages for monoidal categories. In New Structures for Physics , Lecture Notes in Phys. 813, 289--355. Springer, 2011. arXiv:0908.3347 (https://arxiv.org/abs/0908.3347).arXiv
  19. T. Streicher. Fibered categories à la Jean Bénabou. Preprint, arXiv:1801.02927 (https://arxiv.org/abs/1801.02927), version 20, 2023.arXiv
  20. M. Weber. Polynomials in categories with pullbacks. Theory Appl. Categ. 30(16):533--598, 2015.
  21. J. Zucker. Formalization of classical mathematics in Automath. In Colloques Internationaux du CNRS 249, 135--145, 1975. Reprinted in Selected Papers on Automath , Stud. Logic Found. Math. 133, North-Holland, 1994, 127--139, doi:10.1016/S0049-237X(08)70202-7 (https://doi.org/10.1016/S0049-237X(08)70202-7).DOI

Version history

  1. v1Submitted by Kotaro KamiyaInitial depositCurrentOct 17, 2026