Document Open Access Logo

The General Universal Property of the Propositional Truncation

Author Nicolai Kraus

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2014.111.pdf
  • Filesize: 0.67 MB
  • 35 pages

Document Identifiers

Subject Classification

Keywords
  • coherence conditions
  • propositional truncation
  • Reedy limits
  • universal property
  • well-behaved constancy

Metrics

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

Abstract

In a type-theoretic fibration category in the sense of Shulman (representing a dependent type theory with at least unit, sigma, pi, and identity types), we define the type of coherently constant functions from A to B. This involves an infinite tower of coherence conditions, and we therefore need the category to have Reedy limits of diagrams over omega^op. Our main result is that, if the category further has propositional truncations and satisfies function extensionality, the type of coherently constant function is equivalent to the type ||A|| -> B. If B is an n-type for a given finite n, the tower of coherence conditions becomes finite and the requirement of nontrivial Reedy limits vanishes. The whole construction can then be carried out in standard syntactical homotopy type theory and generalises the universal property of the truncation. This provides a way to define functions ||A|| -> B if B is not known to be propositional, and it streamlines the common approach of finding a propositional type Q with A -> Q and Q -> B.

Cite As Get BibTex

Nicolai Kraus. The General Universal Property of the Propositional Truncation. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 111-145, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TYPES.2014.111

Author Details

Nicolai Kraus

References

  1. Benedikt Ahrens, Paolo Capriotti, and Régis Spadotti. Non-wellfounded trees in homotopy type theory. In Typed Lambda Calculi and Applications (TLCA), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pages 17-30. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2015. Google Scholar
  2. Thorsten Altenkirch, Paolo Capriotti, and Nicolai Kraus. Infinite structures in type theory: Problems and approaches. Presented at TYPES, Tallinn, Estonia, 20 May 2015. Work in progress, working title. Google Scholar
  3. Steve Awodey. Natural models of homotopy type theory. arXiv preprints, arXiv:1406.3219, Jun 2014. Google Scholar
  4. Steve Awodey and Andrej Bauer. Propositions as [types]. Journal of Logic and Computation, 14(4):447-471, 2004. Google Scholar
  5. Michael Batanin. Monoidal globular categories as a natural environment for the theory of weak n-categories. Advances in Mathematics, 136(1):39-103, 1998. Google Scholar
  6. Paolo Capriotti, Nicolai Kraus, and Andrea Vezzosi. Functions out of higher truncations, 2015. In preparation, to appear in Computer Science Logic (CSL). Google Scholar
  7. R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, NJ, 1986. Google Scholar
  8. Nicola Gambino and Richard Garner. The identity type weak factorisation system. Theoretical Computer Science, 409:94-109, Dec 2008. Google Scholar
  9. Hugo Herbelin. A dependently-typed construction of semi-simplicial types. Mathematical Structures in Computer Science, pages 1-16, Mar 2015. Google Scholar
  10. Jason J. Hickey. Formal objects in type theory using very dependent types. In Foundations of Object Oriented Languages 3, 1996. Google Scholar
  11. André Hirschowitz, Tom Hirschowitz, and Nicolas Tabareau. Wild omega-categories for the homotopy hypothesis in type theory. In Typed Lambda Calculi and Applications (TLCA), volume 38 of Leibniz International Proceedings in Informatics (LIPIcs), pages 226-240. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2015. Google Scholar
  12. Mark Hovey. Model Categories. Number 63 in Mathematical surveys and monographs. American Mathematical Society, 2007. Google Scholar
  13. Nicolai Kraus. Truncation Levels in Homotopy Type Theory. PhD thesis, School of Computer Science, University of Nottingham, Nottingham, UK, 2015. Google Scholar
  14. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. Notions of anonymous existence in Martin-Löf type theory, 2014. Submitted to the special issue of TLCA'13. Google Scholar
  15. Tom Leinster. A survey of definitions of n-category. Theory and applications of Categories, 10(1):1-70, 2002. Google Scholar
  16. Peter LeFanu Lumsdaine. Weak omega-categories from intensional type theory. In Typed Lambda Calculi and Applications (TLCA), pages 172-187. Springer-Verlag, 2009. Google Scholar
  17. Peter LeFanu Lumsdaine and Michael A. Warren. The local universes model: an overlooked coherence construction for dependent type theories. Transactions on Computational Logic (TOCL), 16(3), 2015. To appear. Google Scholar
  18. Jacob Lurie. Higher topos theory, volume 170 of Annals of Mathematics Studies. Princeton University Press, Princeton, NJ, 2009. Google Scholar
  19. James E. McClure. On semisimplicial sets satisfying the Kan condition. Homology, Homotopy and Applications, 15(1):73-82, 2013. Google Scholar
  20. Matt Oliveri. A formalized interpreter. Blog post, URL: http://homotopytypetheory.org/2014/08/19/a-formalized-interpreter/.
  21. Colin Patrick Rourke and Brian Joseph Sanderson. Δ-sets I: Homotopy theory. The Quarterly Journal of Mathematics, 22(3):321-338, 1971. Google Scholar
  22. Graeme Segal. Classifying spaces and spectral sequences. Publications Mathématiques de l'Institut des Hautes Études Scientifiques, 34(1):105-112, 1968. Google Scholar
  23. Michael Shulman. Homotopy type theory should eat itself (but so far, it’s too big to swallow). Blog post, URL: http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/.
  24. Michael Shulman. Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science, pages 1-75, Jan 2015. Google Scholar
  25. Ross Street. The algebra of oriented simplexes. Journal of Pure and Applied Algebra, 49(3):283-335, 1987. Google Scholar
  26. The HoTT and UF community. Homotopy type theory mailing list, since 2011. URL: https://groups.google.com/forum/#!aboutgroup/homotopytypetheory.
  27. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book/, Institute for Advanced Study, first edition, 2013.
  28. Benno van den Berg and Richard Garner. Types are weak ω-groupoids. Proceedings of the London Mathematical Society, 102(2):370-394, 2011. Google Scholar
  29. Vladimir Voevodsky. A simple type system with two identity types, 2013. Unpublished note. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact