DROPS

Document

DOI: 10.4230/LIPIcs.TYPES.2024.8

Effective Kan Fibrations for W-Types in Homotopy Type Theory

Authors: Shinichiro Tanaka

Published in: LIPIcs, Volume 336, 30th International Conference on Types for Proofs and Programs (TYPES 2024)

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

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)

Copy BibTex To Clipboard

@InProceedings{tanaka:LIPIcs.TYPES.2024.8,
  author =	{Tanaka, Shinichiro},
  title =	{{Effective Kan Fibrations for W-Types in Homotopy Type Theory}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{8:1--8:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-376-8},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{336},
  editor =	{M{\o}gelberg, Rasmus Ejlers and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.8},
  URN =		{urn:nbn:de:0030-drops-233707},
  doi =		{10.4230/LIPIcs.TYPES.2024.8},
  annote =	{Keywords: Homotopy Type Theory, Effective Kan Fibrations, W-types}
}

Search Results

Documents authored by Tanaka, Shinichiro

Effective Kan Fibrations for W-Types in Homotopy Type Theory

Abstract

Cite as

Thanks for your feedback!

Could not send message