Elementary fibrations of enriched groupoids. (English) Zbl 07547338
Summary: 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 M. Hofmann in his PhD Thesis [Extensional constructs in intensional type theory. London: Springer; Edinburgh: Univ. Edinburgh (Diss. 1996) (1997; Zbl 1411.03001)] and later analysed in collaboration with T. Streicher [“The groupoid model refutes uniqueness of identity proofs”, LICS 1994, 208–212 (1994; doi:10.1109/LICS.1994.316071); “The groupoid interpretation of type theory”, in: G. Sambin (ed.) et al., Twenty-five years of constructive type theory. Oxford: Clarendon Press. 83–111 (1998; Zbl 0930.03089)]. In this paper, after describing an algebraic weak factorisation system (\(\mathsf{L, R}\)) on the category \(C\)-\(Gpd\) of \(C\)-enriched groupoids, we prove that its fibration of algebras is elementary (in the sense of W. Lawvere [in: A. Heller (ed.), Applications of categorical algebra. Providence, RI: AMS. 1–14 (1970; Zbl 0234.18002)]) and use this fact to produce the factorisation of diagonals for (\(\mathsf{L, R}\)) needed to interpret identity types.
MSC:
| 03B38 | Type theory |
| 03G30 | Categorical logic, topoi |
| 18B40 | Groupoids, semigroupoids, semigroups, groups (viewed as categories) |
| 18D20 | Enriched categories (over closed or monoidal categories) |
References:
| [1] | Borceux, F. (1994). Handbook of Categorical Algebra, vol. II. Cambridge University Press. · Zbl 0911.18001 |
| [2] | Bourke, J. and Garner, R. (2016). Algebraic weak factorisation systems I: Accessible AWFS. Journal of Pure and Applied Algebra220 (1) 108-147. · Zbl 1327.18004 |
| [3] | Emmenegger, J., Pasquali, F. and Rosolini, G. (2020). Elementary doctrines as coalgebras. Journal of Pure and Applied Algebra224 (12) 106445, 16. · Zbl 1469.18008 |
| [4] | Emmenegger, J., Pasquali, F. and Rosolini, G. (2021). A characterization of elementary fibrations. Available as arXiv:2007.16180. · Zbl 1492.18008 |
| [5] | 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. |
| [6] | Garner, R. (2008). Understanding the small object argument. Applied Categorical Structures17 (3) 247-285. · Zbl 1173.55009 |
| [7] | Grandis, M. and Tholen, W. (2006). Natural weak factorization systems. Archiv der Mathematik (Brno)42(4) 397-408. · Zbl 1164.18300 |
| [8] | 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. · Zbl 0941.18501 |
| [9] | Hofmann, M. (1997). Extensional Constructs in Intensional Type Theory. CPHC/BCS Distinguished Dissertations. Springer-Verlag London Ltd. · Zbl 1411.03001 |
| [10] | 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. |
| [11] | 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. · Zbl 0930.03089 |
| [12] | Jacobs, B. (1999). Categorical Logic and Type Theory, vol. 141. Studies in Logic and the Foundations of Mathematics. North Holland Publishing Company. · Zbl 0911.03001 |
| [13] | Kelly, G. (1982). Basic Concepts of Enriched Category Theory, vol. 64. London Mathematical Society Lecture Note Series. Cambridge University Press. · Zbl 0478.18005 |
| [14] | 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. · Zbl 0234.18002 |
| [15] | Maietti, M. and Rosolini, G. (2013a). Elementary quotient completion. Theory and Applications of Categories27445-463. · Zbl 1288.03048 |
| [16] | Maietti, M. and Rosolini, G. (2013b). Quotient completion for the foundation of constructive mathematics. Logica Universalis7(3) 371-402. · Zbl 1288.03049 |
| [17] | Maietti, M. and Rosolini, G. (2015). Unifying exact completions. Applied Categorical Structures2343-52. · Zbl 1386.03074 |
| [18] | Streicher, T.2020. Fibred Categories à la Jean Bénabou. Available at arXiv:1801.02927v7. |
| [19] | (2013). Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study. · Zbl 1298.03002 |
| [20] | Van Den Berg, B. and Garner, R. (2012). Topological and simplicial models of identity types. ACM Transactions on Computational Logic13(1) 1-44. · Zbl 1352.03012 |
| [21] | Van Woerkom, W. (2021). Algebraic models of type theory. Master’s thesis, Universiteit van Amsterdam. |
| [22] | Vasilakopoulou, C. (2018). On enriched fibrations. Cahiers de Topologie et Géométrie Différentielle Catégoriques LIX(4) 354-387. · Zbl 1419.18015 |
| [23] | Warren, M. (2008). Homotopy Theoretic Aspects of Constructive Type Theory. PhD thesis, Carnegie Mellon University. |
| [24] | 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-340 · Zbl 1243.03012 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
