Lawvere theories and C-systems
HTML articles powered by AMS MathViewer
- by Marcelo Fiore and Vladimir Voevodsky PDF
- Proc. Amer. Math. Soc. 148 (2020), 2297-2315 Request permission
Abstract:
In this paper we consider the class of $\ell$-bijective C-systems, i.e., C-systems for which the length function is a bijection. The main result of the paper is a construction of an isomorphism between two categories: the category of $\ell$-bijective C-systems and the category of Lawvere theories.References
- John Cartmell, Generalised algebraic theories and contextual categories, Ph.D. Thesis, Oxford University, 1978.
- John Cartmell, Generalised algebraic theories and contextual categories, Ann. Pure Appl. Logic 32 (1986), no. 3, 209–243. MR 865990, DOI 10.1016/0168-0072(86)90053-9
- Peter Dybjer, Internal type theory, Types for proofs and programs (Torino, 1995) Lecture Notes in Comput. Sci., vol. 1158, Springer, Berlin, 1996, pp. 120–134. MR 1474535, DOI 10.1007/3-540-61780-9_{6}6
- Marcelo Fiore, Algebraic type theory, Note, 2008, http://www.cl.cam.ac.uk/~mpf23/Notes/att.pdf
- Eric M. Friedlander, In memoriam: Vladimir Voevodsky, Bull. Amer. Math. Soc. (N.S.) 55 (2018), no. 4, 403–404. MR 3854070, DOI 10.1090/bull/1636
- F. William Lawvere, Functorial semantics of algebraic theories and some algebraic problems in the context of functorial semantics of algebraic theories, Repr. Theory Appl. Categ. 5 (2004), 1–121. Reprinted from Proc. Nat. Acad. Sci. U.S.A. 50 (1963), 869–872 [MR0158921] and Reports of the Midwest Category Seminar. II, 41–61, Springer, Berlin, 1968 [MR0231882]. MR 2118935
- Vladimir Voevodsky, A C-system defined by a universe category, Theory Appl. Categ. 30 (2015), Paper No. 37, 1181–1215. MR 3402489
- Vladimir Voevodsky, An experimental library of formalized mathematics based on the univalent foundations, Math. Structures Comput. Sci. 25 (2015), no. 5, 1278–1294. MR 3340542, DOI 10.1017/S0960129514000577
- Vladimir Voevodsky, Subsystems and regular quotients of C-systems, A panorama of mathematics: pure and applied, Contemp. Math., vol. 658, Amer. Math. Soc., Providence, RI, 2016, pp. 127–137. MR 3475277, DOI 10.1090/conm/658/13124
- Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson et al., UniMath - A library of formalized mathematics. Available at https://github.com/UniMath.
Additional Information
- Marcelo Fiore
- Affiliation: Department of Computer Science and Technology, University of Cambridge, Cambridge, CB3 0FD, United Kingdom
- MR Author ID: 341275
- Email: marcelo.fiore@cl.cam.ac.uk
- Vladimir Voevodsky
- Affiliation: School of Mathematics, Institute for Advanced Study, Princeton, New Jersey 08540
- Received by editor(s): January 21, 2016
- Received by editor(s) in revised form: June 30, 2017, and April 4, 2019
- Published electronically: February 26, 2020
- Additional Notes: The following is the acknowledgement for the support of the second author by a USAFR grant managed from the Carnegie Mellon University: This material is based on research sponsored by the United States Air Force Research Laboratory under agreement number FA9550-15-1-0053. The US Government is authorized to reproduce and distribute reprints for governmental purposes notwithstanding any copyright notation thereon.
The views and conclusions contained herein are those of the author and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of the United States Air Force Research Laboratory, the U.S. Government, or Carnegie Mellon University. - Communicated by: Mirna Džamonja
- © Copyright 2020 American Mathematical Society
- Journal: Proc. Amer. Math. Soc. 148 (2020), 2297-2315
- MSC (2010): Primary primary, 18C10, 18C50, 08C99, 03F50
- DOI: https://doi.org/10.1090/proc/14660
- MathSciNet review: 4080876