Hostname: page-component-6898cfcb55-kwdml Total loading time: 0 Render date: 2026-11-11T08:17:41.870Z Has data issue: false hasContentIssue false
  • English
  • Français

Elementary fibrations of enriched groupoids

Published online by Cambridge University Press:  19 November 2021

Jacopo Emmenegger,
Fabio Pasquali and
Giuseppe RosoliniOpen the ORCID record for Giuseppe Rosolini[Opens in a new window]
Jacopo Emmenegger
Affiliation:
School of Computer Science, University of Birmingham, Birmingham, UK
Fabio Pasquali
Affiliation:
DIMA, Università di Genova, Genova, Italy
Giuseppe Rosolini*
Affiliation:
DIMA, Università di Genova, Genova, Italy
*
*Corresponding author. Email: rosolini@unige.it
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

The present paper aims at stressing the importance of the Hofmann–Streicher groupoid model for Martin Löf Type Theory as a link with the first-order equality and its semantics via adjunctions. The groupoid model was introduced by Martin Hofmann in his Ph.D. thesis and later analysed in collaboration with Thomas Streicher. In this paper, after describing an algebraic weak factorisation system $$\mathsf {L, R}$$ on the category $${\cal C}-{\cal Gpd}$$ of $${\cal C}$$-enriched groupoids, we prove that its fibration of algebras is elementary (in the sense of Lawvere) and use this fact to produce the factorisation of diagonals for $$\mathsf {L, R}$$ needed to interpret identity types.

Keywords

Elementary fibrationsalgebraic weak factorisation systemgroupoid model

Information

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 31 , Special Issue 9: In Homage to Martin Hofmann , October 2021, pp. 958 - 978
Check for updates
Creative Commons
Creative Common License - CCCreative Common License - BY
This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.
Copyright
© The Author(s), 2021. Published by Cambridge University Press

References

Borceux, F. (1994). Handbook of Categorical Algebra, vol. II. Cambridge University Press.Google Scholar
Bourke, J. and Garner, R. (2016). Algebraic weak factorisation systems I: Accessible AWFS. Journal of Pure and Applied Algebra 220 (1) 108–147.10.1016/j.jpaa.2015.06.002CrossRefGoogle Scholar
Emmenegger, J., Pasquali, F. and Rosolini, G. (2020). Elementary doctrines as coalgebras. Journal of Pure and Applied Algebra 224 (12) 106445, 16.10.1016/j.jpaa.2020.106445CrossRefGoogle Scholar
Emmenegger, J., Pasquali, F. and Rosolini, G. (2021). A characterization of elementary fibrations. Available as arXiv:2007.16180.Google Scholar
Gambino, N. and Larrea, M. F. (2021). Models of Martin-Löf type theory from algebraic weak factorisation systems. Journal of Symbolic Logic (In Press). Preprint version available as arXiv:1906.01491.Google Scholar
Garner, R. (2008). Understanding the small object argument. Applied Categorical Structures 17 (3) 247–285.10.1007/s10485-008-9137-4CrossRefGoogle Scholar
Grandis, M. and Tholen, W. (2006). Natural weak factorization systems. Archiv der Mathematik (Brno) 42(4) 397–408.Google Scholar
Hermida, C. (1994). On fibred adjunctions and completeness for fibred categories. In: Recent Trends in Data Type Specification (Caldes de Malavella, 1992), vol. 785. Lecture Notes in Computer Science. Springer, 235–251.10.1007/3-540-57867-6_14CrossRefGoogle Scholar
Hofmann, M. (1997). Extensional Constructs in Intensional Type Theory . CPHC/BCS Distinguished Dissertations. Springer-Verlag London Ltd.Google Scholar
Hofmann, M. and Streicher, T. (1994). The groupoid model refutes uniqueness of identity proofs. In: Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society, 208–212.10.1109/LICS.1994.316071CrossRefGoogle Scholar
Hofmann, M. and Streicher, T. (1998). The groupoid interpretation of type theory. In: Twenty-Five Years of Constructive Type Theory (Venice, 1995), vol. 36. Oxford Logic Guides. Oxford Univ. Press, 83–111.10.1093/oso/9780198501275.003.0008CrossRefGoogle Scholar
Jacobs, B. (1999). Categorical Logic and Type Theory, vol. 141. Studies in Logic and the Foundations of Mathematics. North Holland Publishing Company.Google Scholar
Kelly, G. (1982). Basic Concepts of Enriched Category Theory, vol. 64. London Mathematical Society Lecture Note Series. Cambridge University Press.Google Scholar
Lawvere, F. (1970). Equality in hyperdoctrines and comprehension schema as an adjoint functor. In: Heller, A. (ed.) Proc. New York Symposium on Application of Categorical Algebra. American Mathematical Society, 1–14.10.1090/pspum/017/0257175CrossRefGoogle Scholar
Maietti, M. and Rosolini, G. (2013a). Elementary quotient completion. Theory and Applications of Categories 27 445–463.Google Scholar
Maietti, M. and Rosolini, G. (2013b). Quotient completion for the foundation of constructive mathematics. Logica Universalis 7(3) 371–402.10.1007/s11787-013-0080-2CrossRefGoogle Scholar
Maietti, M. and Rosolini, G. (2015). Unifying exact completions. Applied Categorical Structures 23 43–52.10.1007/s10485-013-9360-5CrossRefGoogle Scholar
Streicher, T. 2020. Fibred Categories à la Jean Bénabou. Available at arXiv:1801.02927v7.Google Scholar
The Univalent Foundations Program (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study.Google Scholar
van den Berg, B. and Garner, R. (2012). Topological and simplicial models of identity types. ACM Transactions on Computational Logic 13(1) 1–44.10.1145/2071368.2071371CrossRefGoogle Scholar
van Woerkom, W. (2021). Algebraic models of type theory. Master’s thesis, Universiteit van Amsterdam.Google Scholar
Vasilakopoulou, C. (2018). On enriched fibrations. Cahiers de Topologie et Géométrie Différentielle Catégoriques LIX(4) 354–387.Google Scholar
Warren, M. (2008). Homotopy Theoretic Aspects of Constructive Type Theory. PhD thesis, Carnegie Mellon University.Google Scholar
Warren, M. (2011). The strict ω-groupoid interpretation of type theory. In: B. Hart, et al. (eds.) Models, Logics and Higher-Dimensional Categories, CRM Proceedings and Lecture Notes, vol. 53, American Mathematical Society, 291–34010.1090/crmp/053/16CrossRefGoogle Scholar