Search Results

Documents authored by Pujet, Loïc

Artifact
Software
DOI: 10.4230/artifacts.26875
Cellular Methods in Homotopy Type Theory (accompanying formalisation)

Authors: Axel Ljungström and Loïc Pujet

Abstract
Cite as

Axel Ljungström, Loïc Pujet. Cellular Methods in Homotopy Type Theory (accompanying formalisation) (Software). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-26875,
   title = {{Cellular Methods in Homotopy Type Theory (accompanying formalisation)}}, 
   author = {Ljungstr\"{o}m, Axel and Pujet, Lo\"{i}c},
   note = {Software, Knut and Alice Wallenberg Foundation Postdoctoral Scholarship: Program in Mathematics for researchers with a Swedish doctor’s degree, swhId: \href{https://archive.softwareheritage.org/swh:1:dir:7904cf81046d351ce2a27f778d8b96f71186035d;origin=https://github.com/agda/cubical;visit=swh:1:snp:82843e2d41d4b8b6a9013ffeadeb01fbcbb23e53;anchor=swh:1:rev:8a45d739ad0b75f4773874be4a5e42dbd46c9cd6}{\texttt{swh:1:dir:7904cf81046d351ce2a27f778d8b96f71186035d}} (visited on 2026-07-09)},
   url = {https://github.com/agda/cubical/blob/master/Cubical/Papers/CellularMethods.agda},
   doi = {10.4230/artifacts.26875},
}
Document
DOI: 10.4230/LIPIcs.LICS.2026.41
Definitional Proof Irrelevance Made Accessible

Authors: Thiago Felicissimo, Yann Leray, Loïc Pujet, Nicolas Tabareau, Éric Tanter, and Théo Winterhalter

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
A universe of propositions equipped with definitional proof irrelevance constitutes a convenient medium to express properties and proofs in type-theoretic proof assistants such as Lean, Rocq, and Agda. However, allowing accessibility predicates - used to establish semantic termination arguments - to inhabit such a universe yields undecidable typechecking, hampering the predictability and foundational bases of a proof assistant. To effectively reconcile definitional proof irrelevance and accessibility predicates with both theoretical foundations and practicality in mind, we describe a type theory that extends the Calculus of Inductive Constructions featuring observational equality in a universe of strict propositions, with two variants for handling the elimination principle of accessibility predicates: one variant safeguards decidability by sticking to propositional unfolding, and the other variant favors flexibility with definitional unfolding, at the expense of a potentially diverging typechecking procedure. Crucially, the metatheory of this dual approach establishes that any proof made in the definitional variant of the theory can be translated into a proof of the same statement in the propositional variant, all while preserving the decidability of the latter. Moreover, we prove the two variants to be consistent and to satisfy forms of canonicity, ensuring that programs can indeed be properly evaluated. We present an implementation in Rocq and compare it with existing approaches. Overall, this work introduces an effective technique that informs the design of proof assistants with strict propositions, enabling local computation with accessibility predicates without compromising the ambient type theory.
Cite as

Thiago Felicissimo, Yann Leray, Loïc Pujet, Nicolas Tabareau, Éric Tanter, and Théo Winterhalter. Definitional Proof Irrelevance Made Accessible. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 41:1-41:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{felicissimo_et_al:LIPIcs.LICS.2026.41,
  author =	{Felicissimo, Thiago and Leray, Yann and Pujet, Lo\"{i}c and Tabareau, Nicolas and Tanter, \'{E}ric and Winterhalter, Th\'{e}o},
  title =	{{Definitional Proof Irrelevance Made Accessible}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{41:1--41:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.41},
  URN =		{urn:nbn:de:0030-drops-268289},
  doi =		{10.4230/LIPIcs.LICS.2026.41},
  annote =	{Keywords: Dependent type theory, proof assistants, Rocq, proof irrelevance, accessibility predicates, observational equality, canonicity, set-theoretic models}
}
Document
DOI: 10.4230/LIPIcs.LICS.2026.66
Cellular Methods in Homotopy Type Theory

Authors: Axel Ljungström and Loïc Pujet

Published in: LIPIcs, Volume 380, 41st Annual Symposium on Logic in Computer Science (LICS 2026)

Abstract
In classical mathematics, a CW complex is a topological space which can be built up inductively by gluing together cells of increasing dimension. Thanks to their excellent categorical properties, CW complexes have become one of the main objects of interest in algebraic topology. Although their quasi-combinatorial nature suggests that a constructive treatment is possible, there seems to be little literature on the subject - perhaps because of the important role played by the axiom of choice in the classical theory of CW complexes. In this paper, we present a synthetic and constructive account of the theory of CW complexes in homotopy type theory. Our first main result is a finitary version of the cellular approximation theorem which, among other things, allows us to construct a cellular homology functor without needing the axiom of choice or relying on a pre-existing notion of homology. Our second main result, which we call the "Hurewicz approximation theorem", shows that the CW complexes that are n-connected types are precisely the ones that can be presented by a CW structure with no nontrivial cells up to dimension n. This theorem is standard in the classical treatment of CW complexes, but it is far from being obvious in a constructive setting. As a corollary, we give a new proof of the Hurewicz theorem for CW complexes, which relates the first non-vanishing homotopy group of a CW complex with the corresponding homology group. All key theorems presented in this paper have been mechanised in Cubical Agda.
Cite as

Axel Ljungström and Loïc Pujet. Cellular Methods in Homotopy Type Theory. In 41st Annual Symposium on Logic in Computer Science (LICS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 380, pp. 66:1-66:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ljungstrom_et_al:LIPIcs.LICS.2026.66,
  author =	{Ljungstr\"{o}m, Axel and Pujet, Lo\"{i}c},
  title =	{{Cellular Methods in Homotopy Type Theory}},
  booktitle =	{41st Annual Symposium on Logic in Computer Science (LICS 2026)},
  pages =	{66:1--66:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-434-5},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{380},
  editor =	{Faggian, Claudia and Katoen, Joost-Pieter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.LICS.2026.66},
  URN =		{urn:nbn:de:0030-drops-268536},
  doi =		{10.4230/LIPIcs.LICS.2026.66},
  annote =	{Keywords: Homotopy type theory, Univalent foundations, constructive mathematics, synthetic homotopy theory, CW complexes, cellular homology, Hurewicz theorem}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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