Document Open Access Logo

Wild omega-Categories for the Homotopy Hypothesis in Type Theory

Authors André Hirschowitz, Tom Hirschowitz, Nicolas Tabareau

PDF
Thumbnail PDF

File

LIPIcs.TLCA.2015.226.pdf
  • Filesize: 499 kB
  • 15 pages

Document Identifiers

Author Details

André Hirschowitz
Tom Hirschowitz
Nicolas Tabareau

Cite As Get BibTex

André Hirschowitz, Tom Hirschowitz, and Nicolas Tabareau. Wild omega-Categories for the Homotopy Hypothesis in Type Theory. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 226-240, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TLCA.2015.226

Abstract

In classical homotopy theory, the homotopy hypothesis asserts that the fundamental varpi-groupoid construction induces an equivalence between topological spaces and weak varpi-groupoids. In the light of Voevodsky's univalent foundations program, which puts forward an interpretation of types as topological spaces, we consider the question of transposing the homotopy hypothesis to type theory. Indeed such a transposition could stand as a new approach to specifying higher inductive types. Since the formalisation of general weak varpi-groupoids in type theory is a difficult task, we only take a first step towards this goal, which consists in exploring a shortcut through strict varpi-categories.
The first outcome is a satisfactory type-theoretic notion of strict varpi-category, which has hsets of cells in all dimensions. For this notion, defining the 'fundamental strict varpi-category' of a type seems out of reach. The second outcome is an 'incoherently strict' notion of type-theoretic varpi-category, which admits arbitrary types of cells in all dimensions. These are the 'wild' varpi-categories of the title. They allow the definition of a 'fundamental wild varpi-category' map, which leads to our (partial) homotopy hypothesis for type theory (stating an adjunction, not an equivalence).
All of our results have been formalised in the Coq proof assistant. Our formalisation makes systematic use of the machinery of coinductive types.

Subject Classification

Keywords
  • Homotopy Type theory; Omega-categories; Coinduction; Homotopy hypothesis

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. B. Ahrens, K. Kapulkin, and M. Shulman. Univalent categories and the Rezk completion. Mathematical Structures in Computer Science, 2015. Google Scholar
  2. T. Altenkirch, N. Li, and O. Rypáček. Some constructions on ω-groupoids. In LFMTP '14, pages 4:1-4:8. ACM, 2014. Google Scholar
  3. B. \swapBerg van den and R. Garner. Types are weak ω-groupoids. Proceedings of the London Mathematical Society, 102(2):370-394, 2011. Google Scholar
  4. R. Brown and P. Higgins. The equivalence of ∞-groupoids and crossed complexes. Cahiers de Topologie et Géométrie Différentielle Catégoriques, 22, 1981. Google Scholar
  5. A. Burroni. Higher-dimensional word problems with applications to equational logic. Theoretical Computer Science, 115(1):43-62, 1993. Google Scholar
  6. E. Cheng. An ω-category with all duals is an ω-groupoid. Applied Categorical Structures, 15:439-453, 2007. Google Scholar
  7. E. Cheng and T. Leinster. Weak ω-categories via terminal coalgebras. ArXiv e-prints, December 2012. Google Scholar
  8. A. Chlipala. Certified Programming with Dependent Types. MIT Press, 2014. Google Scholar
  9. A. Hirschowitz, T. Hirschowitz, and N. Tabareau. Formalisation of strict omega-categories and the homotopy hypothesis in type theory, using coinduction. Coq code, https://github.com/tabareau/omega_categories, 2015.
  10. M. Hofmann and T. Streicher. The groupoid model refutes uniqueness of identity proofs. In LICS, pages 208-212. IEEE Computer Society, 1994. Google Scholar
  11. M. Hovey. Model Categories, volume 63 of Mathematical Surveys and Monographs. American Mathematical Society, 1999. Google Scholar
  12. M. M. Kapranov and V. A. Voevodsky. ∞-groupoids and homotopy types. Cahiers de Topologie et Géométrie Différentielle Catégoriques, 32(1):29-46, 1991. Google Scholar
  13. C. Kapulkin, P. LeFanu Lumsdaine, and V. Voevodsky. The simplicial model of univalent foundations. ArXiv e-prints, November 2012. Google Scholar
  14. S. Kasangian, G. Metere, and E. Vitale. Weak inverses for strict n-categories. Preprint, 2009. Google Scholar
  15. Y. Lafont, F. Métayer, and K. Worytkiewicz. A folk model structure on omega-cat. Advances in Mathematics, 224(3):1183 - 1231, 2010. Google Scholar
  16. P. LeFanu Lumsdaine. Weak omega-categories from intensional type theory. Logical Methods in Computer Science, 6(3), 2010. Google Scholar
  17. P. LeFanu Lumsdaine and M. Shulman. Semantics of higher inductive types. Preprint, 2012. Google Scholar
  18. C. Simpson. Homotopy types of strict 3-groupoids. ArXiv e-prints, 1998. Google Scholar
  19. K. Sojakova. Higher inductive types as homotopy-initial algebras. In POPL, pages 31-42. ACM, 2015. Google Scholar
  20. R. Street. The algebra of oriented simplexes. Journal of Pure and Applied Algebra, 49(3):283-335, 1987. Google Scholar
  21. The Coq development team. Coq 8.4 Reference Manual. Inria, 2012. Google Scholar
  22. The NLab. Homotopy hypothesis. Accessed April 2015. Google Scholar
  23. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  24. M. A. Warren. The strict ω-groupoid interpretation of type theory. CRM Proceedings and Lecture Notes, 53:291-340, 2011. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact