Article
Full entry |
PDF
(1.1 MB)
Feedback
PDF
(1.1 MB)
Feedback
Keywords:
homotopy type theory; $\infty$-categories; Segal spaces; Rezk spaces
homotopy type theory; $\infty$-categories; Segal spaces; Rezk spaces
Summary:
We propose foundations for a synthetic theory of $(\infty,1)$-categories within homotopy type theory. We axiomatize a directed interval type, then define higher simplices from it and use them to probe the internal categorical structures of arbitrary types. We define {\it Segal types}, in which binary composites exist uniquely up to homotopy; this automatically ensures composition is coherently associative and unital at all dimensions. We define {\it Rezk types}, in which the categorical isomorphisms are additionally equivalent to the type-theoretic identities — a “local univalence” condition. And we define {\it covariant fibrations}, which are type families varying functorially over a Segal type, and prove a “dependent Yoneda lemma” that can be viewed as a directed form of the usual elimination rule for identity types. We conclude by studying homotopically correct adjunctions between Segal types, and showing that for a functor between Rezk types to have an adjoint is a mere proposition. To make the bookkeeping in such proofs manageable, we use a three-layered type theory with shapes, whose contexts are extended by polytopes within directed cubes, which can be abstracted over using “extension types” that generalize the path-types of cubical type theory. In an appendix, we describe the motivating semantics in the Reedy model structure on bisimplicial sets, in which our Segal and Rezk types correspond to Segal spaces and complete Segal spaces.
References:
[1] Ahrens, Benedikt, Kapulkin, Krzysztof, Shulman, Michael: Univalent categories and the Rezk completion. Mathematical Structures in Computer Science, 25:1010–1039, 6 2015. arXiv:1303.0584
[2] Annenkov, Danil, Capriotti, Paolo, Kraus, Nicolai: Two-level type theory and applications. arXiv:1705.03307
[3] Ayala, David, Francis, John: Fibrations of ∞-categories. arXiv:1702.02681
[4] Bergner, Julia E., Rezk, Charles: Reedy categories and the 𝛩-construction. Math. Z., 274(1-2):499–514, 2013. arXiv:1110.1066
[5] Cohen, Cyril, Coquand, Thierry, Huber, Simon, Mörtberg, Anders: Cubical type theory: a constructive interpretation of the univalence axiom. arXiv:1611.02108
[6] de Brito, Pedro Boavida: Segal objects and the Grothendieck construction. arXiv:1605.00706
[7] Jacobs, Bart: Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam
[8] Johnstone, Peter T.: On a topological topos. Proc. London Math. Soc. (3), 38(2):237–271
[9] Joyal, A.: Quasi-categories and Kan complexes. Journal of Pure and Applied Algebra, 175:207–222
[10] Joyal, André: Disks, duality, and θ-categories. Draft available at https://ncatlab.org/nlab/files/JoyalThetaCategories.pdf
[11] Joyal, André, Tierney, Myles: Quasi-categories vs Segal spaces. In Categories in Algebra, Geometry and Mathematical Physics, pages 277–326. American Mathematical Society, 2006. arXiv:math/0607820
[12] Kapulkin, Chris, Lumsdaine, Peter LeFanu: The simplicial model of univalent foundations (after Voevodsky). arXiv:1211.2851
[13] Kazhdan, David, Varshavsky, Yakov: Yoneda lemma for complete segal spaces. arXiv:1401.5656
[14] Lawvere, F. William: Equality in hyperdoctrines and comprehension schema as an adjoint functor. In Applications of Categorical Algebra (Proc. Sympos. Pure Math., Vol. XVII, New York, 1968), pages 1–14. Amer. Math. Soc., Providence, R.I
[15] Lawvere, F. William: Axiomatic cohesion. Theory and Applications of Categories, 19(3):41–49
[16] Licata, Dan, Harper, Robert: 2-dimensional directed dependent type theory. MFPS. http://www.cs.cmu.edu/~drl/pubs/lh102dtt/lh102dtt.pdf
[17] Lumsdaine, Peter LeFanu: Weak omega-categories from intensional type theory. Typed lambda calculi and applications, 6:1–19. arXiv:0812.0409
[18] Lumsdaine, Peter LeFanu, Warren, Michael A.: The local universes model: An overlooked coherence construction for dependent type theories. ACM Trans. Comput. Logic, 16(3):23:1–23:31, July 2015. arXiv:1411.1736
[19] Lurie, Jacob: Higher topos theory. Number 170 in Annals of Mathematics Studies. Princeton University Press, 2009. arXiv:math.CT/0608040
[20] Lane, Saunders Mac, Moerdijk, Ieke: Sheaves in geometry and logic: a first introduction to topos theory. Universitext. Springer-Verlag, New York. Corrected reprint of the 1992 edition
[21] Rasekh, Nima: Yoneda lemma for simplicial spaces. arXiv:1711.03160
[22] Rezk, Charles: A model for the homotopy theory of homotopy theory. Trans. Amer. Math. Soc., 353(3):973–1007 (electronic), 2001. arXiv:math.AT/9811037
[23] Rezk, Charles: A cartesian presentation of weak n-categories. Geometry & Topology, 14, 2010. arXiv:0901.3602
[24] Riehl, Emily, Verity, Dominic: Homotopy coherent adjunctions and the formal theory of monads. Advances in Mathematics, 286(2):802–888, January 2016
[25] Riehl, Emily, Verity, Dominic: Fibrations and yoneda’s lemma in an ∞-cosmos. J. Pure Appl. Algebra, 221(3):499–564, 2017. arXiv:1506.05500
[26] Schreiber, Urs: Differential cohomology in a cohesive ∞-topos. arXiv:1310.7930
[27] Shulman, Michael: The univalence axiom for elegant Reedy presheaves. Homology, Homotopy, and Applications, 17(2):81–106, 2015. arXiv:1307.6248
[28] Shulman, Michael: Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. To appear in MSCS. arXiv:1509.07584
[29] Program, Univalent Foundations: Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book/, first edition
[30] Berg, Benno van den, Garner, Richard: Types are weak ω-groupoids. Proceedings of the London Mathematical Society, 102(2):370–394
[31] Voevodsky, Vladimir: A simple type system with two identity types. Draft available at https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/HTS.pdf, ee also https://ncatlab.org/homotopytypetheory/show/Homotopy+Type+System
Search
Partner of
