Univalent higher categories via complete Semi-Segal types

Abstract

Category theory in homotopy type theory is intricate as categorical laws can only be stated "up to homotopy", and thus require coherences. The established notion of a univalent category (as introduced by Ahrens et al.) solves this by considering only truncated types, roughly corresponding to an ordinary category. This fails to capture many naturally occurring structures, stemming from the fact that the naturally occurring structures in homotopy type theory are not ordinary, but rather higher categories.

Out of the large variety of approaches to higher category theory that mathematicians have proposed, we believe that, for type theory, the simplicial strategy is best suited. Work by Lurie and Harpaz motivates the following definition. Given the first (n+3) levels of a semisimplicial type S, we can equip S with three properties: first, contractibility of the types of certain horn fillers; second, a completeness property; and third, a truncation condition. We call this a complete semi-Segal n-type. This is very similar to an earlier suggestion by Schreiber.

The definition of a univalent (1-) category by Ahrens et al. can easily be extended or restricted to the definition of a univalent n-category (more precisely, (n,1)-category) for n ∈ {0,1,2}, and we show that the type of complete semi-Segal n-types is equivalent to the type of univalent n-categories in these cases. Thus, we believe that the notion of a complete semi-Segal n-type can be taken as the definition of a univalent n-category.

We provide a formalisation in the proof assistant Agda using a completely explicit representation of semi-simplicial types for levels up to 4.

References

1. Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman. 2015. Univalent Categories and the Rezk Completion. Mathematical Structures in Computer Science (MSCS) (Jan 2015), 1–30.
2. Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. 2016. Extending Homotopy Type Theory with Strict Equality. In 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), Jean-Marc Talbot and Laurent Regnier (Eds.), Vol. 62. Dagstuhl, Germany, 21:1–21:17.
3. Danil Annenkov, Paolo Capriotti, and Nicolai Kraus. 2017. Two-Level Type Theory and Applications. Arxiv e-prints (2017). http://arxiv.org/abs/1705.03307
4. Steve Awodey and Michael A. Warren. 2008. Homotopy theoretic models of identity types. Mathematical Proceedings of the Cambridge Philosophical Society 146, 01 (Jul 2008), 45.
5. John C. Baez and James Dolan. 1998. Higher-Dimensional Algebra III: n-Categories and the Algebra of Opetopes. Advances in Mathematics 135, 145–206.
6. Michael Batanin. 1998. Monoidal Globular Categories As a Natural Environment for the Theory of Weakn-Categories. Advances in Mathematics 136, 1 (1998), 39 – 103.
7. Julia E. Bergner. 2010. A Survey of (∞, 1)-Categories. Springer New York, New York, NY, 69–83.
8. Yves Bertot and Pierre Castéran. 2004. Interactive Theorem Proving and Program Development. Coq’Art: The Calculus of Inductive Constructions. Springer Verlag.
9. J. M. Boardman and R. M. Vogt. 1973. Homotopy invariant algebraic structures on topological spaces. Springer-Verlag, Berlin. 257 pages.
10. Paolo Capriotti. 2016. Models of Type Theory with Strict Equality. Ph.D. Dissertation. School of Computer Science, University of Nottingham, Nottingham, UK. Available online at https://arxiv.org/abs/1702.04912 .
11. Paolo Capriotti and Nicolai Kraus. 2017. Univalent Higher Categories via Complete Semi-Segal Types. ArXiv e-prints (2017). arXiv: 1707.03693 https://arxiv.org/abs/1707.03693 Version with full proofs.
12. James Cranch. 2013. Concrete Categories in Homotopy Type Theory. (Nov 2013). http://arxiv.org/abs/1311.1852
13. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover. In Automated Deduction - CADE-25, 25th International Conference on Automated Deduction.
14. Eric Finster and Samuel Mimram. 2017. A type-theoretical definition of weak ω-categories. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. 1–12.
15. Nick Gurski. 2007. An algebraic theory of tricategories. Ph.D. Dissertation. University of Chicago. Available online at http://www.math.yale.edu/~mg622/tricats.pdf .
16. Yonatan Harpaz. 2015. Quasi-unital ∞–categories. Algebraic & Geometric Topology 15, 4 (2015), 2303–2381.
17. André Joyal. 1997. Disks, duality and Θ-categories. (1997). Unpublished note, available online at https://ncatlab.org/nlab/ files/JoyalThetaCategories.pdf .
18. André Joyal. 2002. Quasi-categories and Kan complexes. Journal of Pure and Applied Algebra 175, 1 (2002), 207–222.
19. André Joyal. 2008. The theory of quasi-categories and its applications, from "Advanced course on simplicial methods in higher categories". Quaderns 45 (2008).
20. Nicolai Kraus and Christian Sattler. 2017. Space-Valued Diagrams, Type-Theoretically (Extended Abstract). ArXiv e-prints (2017). arXiv: 1704.04543v1 https://arxiv.org/abs/1704.04543v1
21. Tom Leinster. 2004. Higher Operads, Higher Categories. Cambridge University Press. Also available online at http: //arxiv.org/abs/math.CT/0305049 .
22. Daniel R. Licata and Robert Harper. 2011. 2-Dimensional Directed Type Theory. Electronic Notes in Theoretical Computer Science 276 (2011), 263 – 289.
23. Jacob Lurie. 2009a. Higher Topos Theory. Princeton University Press, Princeton. Also avaialabe online at http://arxiv.org/ abs/math/0608040 .
24. Jacob Lurie. 2009b. On the classification of topological field theories. Current developments in mathematics 2008 (2009), 129–280.
25. Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph.D. Dissertation. Department of Computer Science and Engineering, Chalmers University of Technology and Göteborg University, Göteborg, Sweden. http://www.cs.chalmers.se/~ulfn/papers/thesis.html
26. Andreas Nuyts. 2015. Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance. (2015). Master thesis, available online at https://distrinet.cs.kuleuven.be/people/andreasn .
27. Christopher Reedy. 1974. Homotopy theory of model categories. (1974).
28. Emily Riehl and Michael Shulman. 2017. A type theory for synthetic ∞-categories. Arxiv e-prints (2017). https://arxiv.org/ abs/1705.07442
29. Urs Schreiber. 2012. Category object in an (infinity,1)-category, Revision 20. nLab entry, https://ncatlab.org/nlab/revision/ category+object+in+an+%28infinity%2C1%29- category/20 ; newest version available at https://ncatlab.org/nlab/show/ category+object+in+an+%28infinity%2C1%29- category .
30. Michael Shulman. 2015. Univalence for Inverse Diagrams and Homotopy Canonicity. Mathematical Structures in Computer Science (Jan 2015), 1–75.
31. Ross Street. 1987. The algebra of oriented simplexes. Journal of Pure and Applied Algebra 49, 3 (1987), 283 – 335.
32. Zouhair Tamsamani. 1999. Sur des notions de n-catégorie et n-groupoïde non strictes via des ensembles multi-simpliciaux. Ph.D. Dissertation.
33. Dimitris Tsementzis. 2016. First-Order Logic with Isomorphism. ArXiv e-prints (2016). arXiv: 1603.03092 https://arxiv.org/ abs/1603.03092
34. The Univalent Foundations Program. 2013a. Homotopy Type Theory: Univalent Foundations of Mathematics. http: //homotopytypetheory.org/book/ , Institute for Advanced Study.
35. The Univalent Foundations Program. 2013b. Semi-simplicial types. Wiki page of the Univalent Foundations project at the Institute for Advanced Studies, https://uf- ias- 2012.wikispaces.com/Semi- simplicial+types .
36. Dominic Verity. 2006. Weak complicial sets, a simplicial weak omega-category theory. Part I: basic homotopy theory. (April 2006). https://arxiv.org/abs/math/0604414
37. Vladimir Voevodsky. 2013. A simple type system with two identity types. Unpublished note.

Index Terms

• Theory of computation

  • Logic

    • Type theory