[00PP] Univalence in locally cartesian closed infinity-categories

Chapter 3121 · Reference depth 1

Author TeX is available. HTML chapter conversion is pending.

Cited by Braiding on type A Soergel bimodules: semistrictness and naturality, The ∞-Categorical Eckmann-Hilton Argument

Original source PDF · 1208.1749v5

Preserved original PDF pages

References in this collection

1. Arndt-Kapulkin:1208.5683 · Homotopy-theoretic models of type theory Depth 2
2. oberwolfach2011 · Mathematisches Forschungsinstitut Oberwolfach Report No. 11/2011. Available from http://hottheory.files.wordpress.com/2011/06/report-11_2011.pdf Depth 2
3. Awodey-Warren:0709.0248 · Homotopy theoretic models of identity types Depth 2
4. Barr-Wells · Toposes, triples and theories Depth 2
5. Carboni-Janelidze-Kelly-Pare · On localization and stabilization for factorization systems Depth 2
6. Cassidy-Hebert-Kelly · Reflective subcategories, localizations and factorization systems Depth 2
7. Cisinski:THT · Théories homotopiques dans les topos Depth 2
8. Cisinski:1406.0058 · Cisinski D.-C., Univalent universes for elegant models of homotopy types, preprint 2014, https://arxiv.org/abs/1406.0058. Depth 2
9. Cisinski:blogpost · D.-C. Cisinski and M. Shulman, entry at the n-Category Caf\'e, \\ http://golem.ph.utexas.edu/category/2012/05/the_mysterious_nature_of_right.html#c041306. Depth 2
10. DS · Mapping spaces in Quasi-categories Depth 2
11. DK84 · Homotopy theory and simplicial groupoids Depth 2
12. Gambino-Garner:0803.4349 · The identity type weak factorisation system Depth 2
13. Garner-Lack:1106.5331 · Grothendieck quasitoposes Depth 2
14. Gepner-Haugseng:1312 · Enriched ∞-categories via non-symmetric ∞-operads Depth 1
15. Hofmann-Streicher:98 · The groupoid interpretation of type theory Depth 2
16. Joyal:CRM · The theory of quasi-categories Depth 2
17. Kapulkin-Lumsdaine:1211.2851 · Kapulkin K. and Lumsdaine P. L., The simplicial model of univalent foundations (after Voevodsky), preprint 2012, https://arxiv.org/abs/1211.2851. Depth 2
18. Kapulkin-Lumsdaine-Voevodsky:1203.2553 · Kapulkin K., Lumsdaine P. L. and Voevodsky V., Univalence in simplicial sets, preprint 2012, http://arxiv.org/abs/1203.2553. Depth 2
19. Lumsdaine:0812.0409 · Weak -categories from intensional type theory Depth 2
20. Lumsdaine-Warren:1411.1736 · The local universes model: an overlooked coherence construction for dependent type theories Depth 2
21. MacLane-Moerdijk · Sheaves in Geometry and Logic: a first introduction to topos theory Depth 2
22. Morel-Voevodsky:IHES · A^1-homotopy theory of schemes Depth 2
23. nLab: · nLab entry, Model of type theory in an (infinity,1)-topos. http://ncatlab.org/homotopytypetheory/show/model+of+type+theory+in+an+ Depth 2
24. Rezk:MR1804411 · A model for the homotopy theory of homotopy theory Depth 1
25. Shulman:1203.3253 · The univalence axiom for inverse diagrams and homotopy canonicity Depth 2
26. Shulman:1307.6248 · The univalence axiom for elegant Reedy presheaves Depth 2
27. SO · Motivic twisted K-theory Depth 2
28. Streicher:MR3166196 · A model of type theory in simplicial sets: a brief introduction to Voevodsky's homotopy type theory Depth 2
29. HoTT-book · Homotopy type theory---univalent foundations of mathematics Depth 2
30. vdBerg-Garner:0812.0298 · Types are weak -groupoids Depth 2
31. VoevodskyV:notts · Notes on type systems Depth 2
32. Lurie:HTT · Higher Topos Theory Depth 1
33. Lurie:HA · Higher algebra Depth 1