Document Open Access Logo

Effective Kan Fibrations for W-Types in Homotopy Type Theory

Author Shinichiro Tanaka

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2024.8.pdf
  • Filesize: 1.72 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • Homotopy Type Theory
  • Effective Kan Fibrations
  • W-types

Metrics

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

Abstract

We investigate effective Kan fibrations in the context of the semantics of Homotopy Type Theory (HoTT). Effective Kan fibrations were proposed by Benno van den Berg and Eric Faber as constructive alternatives to classical Kan fibrations for modeling HoTT. Our work specifically explores their interaction with W-types in HoTT, which are inductive types representing well-founded trees, and extends this exploration to variants such as M-types. By using the categorical properties of W-types, we show that effective Kan fibrations model them. Additionally, we examine the behavior of quotient maps and discuss that certain cases can also be classified as effective Kan fibrations.

Cite As Get BibTex

Shinichiro Tanaka. Effective Kan Fibrations for W-Types in Homotopy Type Theory. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 8:1-8:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.TYPES.2024.8

Author Details

Shinichiro Tanaka
  • Institute for Logic, Language and Computation, University of Amsterdam, The Netherlands

Acknowledgements

I would like to thank Dr. Benno van den Berg for his insightful advice and support.

References

  1. Steve Awodey and Michael A. Warren. Homotopy theoretic models of identity types. Math. Proc. Cambridge Philos. Soc., 146(1): pp. 45-55, 2009. URL: https://doi.org/10.1017/S0305004108001783.
  2. Benno van den Berg and Eric Faber. Effective Kan Fibrations in Simplicial Sets. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-18900-5.
  3. Benno van den Berg and Ieke Moerdijk. W-types in homotopy type theory. Mathematical Structures in Computer Science, 25(5): pp. 1100-1115, 2015. URL: https://doi.org/10.1017/S0960129514000516.
  4. Thierry Coquand, Henri Lombardi, and Stefan Neuwirth. Constructive theory of ordinals. arXiv, 2022. arXiv preprint arXiv:2201.04352. URL: https://doi.org/10.48550/arXiv.2201.04352.
  5. Storm Diephuis. Effective kan fibrations for simplicial groupoids, semisimplicial sets and ex^∞, 2023. https://eprints.illc.uva.nl/id/eprint/2247/1/MoL-2023-06.text.pdf. Google Scholar
  6. Nicola Gambino and Christian Sattler. The Frobenius Condition, Right Properness, and Uniform Fibrations. Journal of Pure and Applied Algebra, 221(12): pp. 3027-3068, 2017. URL: https://doi.org/10.1016/j.jpaa.2017.02.013.
  7. Freek Geerligs. Symmetric effective and degenerate-preferring kan complexes, 2023. https://studenttheses.uu.nl/handle/20.500.12932/43910. Google Scholar
  8. Paul Goerss and John F. Jardine. Simplicial homotopy theory. Birkhäuser, 1999. URL: https://doi.org/10.1007/978-3-0348-8707-6.
  9. Per Martin-Löf. Notes on constructive mathematics. Almqvist & Wiksell, Stockholm, 1970. URL: https://worldcat.org/oclc/472257944.
  10. Per Martin-Löf. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science VI, volume VI, pages pp. 153-175. Elsevier, 1982. URL: https://doi.org/10.1016/S0049-237X(09)70189-2.
  11. Egbert Rijke. Introduction to homotopy type theory. Cambridge University Press, 2022. URL: https://doi.org/10.48550/arXiv.2212.11082.
  12. Univalent Foundations Project. Homotopy type theory -– univalent foundations of mathematics, 2013. Accessed: 2025-05-02. URL: https://homotopytypetheory.org/book/.
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