15 Search Results for "van der Weide, Niels"

Document
DOI: 10.4230/LIPIcs.CSL.2026.40
The Groupoid-Syntax of Type Theory Is a Set

Authors: Thorsten Altenkirch, Ambrus Kaposi, and Szumi Xie

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the traditional notion of CwFs is the requirement to set-truncate types, which excludes models based on univalent categories, such as the standard set model. To address this limitation, we introduce the concept of a Groupoid Category with Families (GCwF). This framework truncates types at the groupoid level and incorporates coherence equations, providing a natural extension of the CwF framework when starting from a 1-category. We demonstrate that the initial GCwF for a type theory with a base family of sets and Π-types (groupoid-syntax) is set-truncated. Consequently, this allows us to utilize the conventional intrinsic syntax of type theory while enabling interpretations in semantically richer and more natural models. All constructions in this paper were formalised in Cubical Agda.
Cite as

Thorsten Altenkirch, Ambrus Kaposi, and Szumi Xie. The Groupoid-Syntax of Type Theory Is a Set. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 40:1-40:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{altenkirch_et_al:LIPIcs.CSL.2026.40,
  author =	{Altenkirch, Thorsten and Kaposi, Ambrus and Xie, Szumi},
  title =	{{The Groupoid-Syntax of Type Theory Is a Set}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{40:1--40:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.40},
  URN =		{urn:nbn:de:0030-drops-254650},
  doi =		{10.4230/LIPIcs.CSL.2026.40},
  annote =	{Keywords: Categorical models of type theory, category with families, groupoids, coherence, homotopy type theory}
}
Document
DOI: 10.4230/LIPIcs.CSL.2026.38
The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories

Authors: Daniël Otten and Matteo Spadetto

Published in: LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026)

Abstract
The semantics of extensional type theory has an elegant categorical description: models of extensional =-types, 𝟙-types, and Σ-types are biequivalent to finitely complete categories, while adding Π-types yields locally Cartesian closed categories. We establish parallel results for axiomatic type theory, which includes systems like cubical type theory, where the computation rule of the =-types only holds as a propositional axiom instead of a definitional reduction. In particular, we prove that models of axiomatic =-types, and standard 𝟙- and Σ-types are biequivalent to certain path categories, while adding axiomatic Π-types yields dependent homotopy exponents. This biequivalence simplifies axiomatic =-types, which are more intricate than extensional ones since they permit higher dimensional structure. Specifically, path categories use a primitive notion of equivalence instead of a direct reproduction of the syntactic elimination rules and computation axioms. We apply our correspondence to prove a coherence theorem: we show that these weak homotopical models can be turned into equivalent strict models of axiomatic type theory. In addition, we introduce a more modular notion, that of a display map path category, which only models axiomatic =-types by default, while leaving room to add other axiomatic type formers such as 𝟙-, Σ-, and Π-types.
Cite as

Daniël Otten and Matteo Spadetto. The Biequivalence of Path Categories and Axiomatic Martin-Löf Type Theories. In 34th EACSL Annual Conference on Computer Science Logic (CSL 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 363, pp. 38:1-38:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{otten_et_al:LIPIcs.CSL.2026.38,
  author =	{Otten, Dani\"{e}l and Spadetto, Matteo},
  title =	{{The Biequivalence of Path Categories and Axiomatic Martin-L\"{o}f Type Theories}},
  booktitle =	{34th EACSL Annual Conference on Computer Science Logic (CSL 2026)},
  pages =	{38:1--38:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-411-6},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{363},
  editor =	{Guerrini, Stefano and K\"{o}nig, Barbara},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.38},
  URN =		{urn:nbn:de:0030-drops-254633},
  doi =		{10.4230/LIPIcs.CSL.2026.38},
  annote =	{Keywords: Axiomatic type theory, cubical type theory, propositional equality, biequivalence, display map categories, path categories, homotopy theory, coherence}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.36
Verifying Datalog Reasoning with Lean

Authors: Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Datalog is an essential logical rule language with many applications, and modern rule engines compute logical consequences for Datalog with high performance and scalability. While Datalog is rather simple and, in principle, explainable by design, such sophisticated implementations and optimizations are hard to verify. We therefore propose a certificate-based approach to validate results of Datalog reasoners in a formally verified checker for Datalog proofs. Using the proof assistant Lean, we implement such a checker and verify its correctness against direct formalizations of the Datalog semantics. We propose two JSON encodings for Datalog proofs: one using the widely supported Datalog proof trees, and one using directed acyclic graphs for succinctness. To evaluate the practical feasibility and performance of our approach, we validate proofs that we obtain by converting derivation traces of an existing Datalog reasoner into our tool-independent format.
Cite as

Johannes Tantow, Lukas Gerlach, Stephan Mennicke, and Markus Krötzsch. Verifying Datalog Reasoning with Lean. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 36:1-36:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{tantow_et_al:LIPIcs.ITP.2025.36,
  author =	{Tantow, Johannes and Gerlach, Lukas and Mennicke, Stephan and Kr\"{o}tzsch, Markus},
  title =	{{Verifying Datalog Reasoning with Lean}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{36:1--36:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.36},
  URN =		{urn:nbn:de:0030-drops-246342},
  doi =		{10.4230/LIPIcs.ITP.2025.36},
  annote =	{Keywords: Certifying Algorithms, Datalog, Formal Verification}
}
Document
DOI: 10.4230/LIPIcs.ITP.2025.33
Scott’s Representation Theorem and the Univalent Karoubi Envelope

Authors: Arnoud van der Leer, Kobe Wullaert, and Benedikt Ahrens

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
Lambek and Scott constructed a correspondence between simply-typed lambda calculi and Cartesian closed categories. Scott’s Representation Theorem is a cousin to this result for untyped lambda calculi. It states that every untyped lambda calculus arises from a reflexive object in some category. We present a formalization of Scott’s Representation Theorem in univalent foundations, in the (Rocq-)UniMath library. Specifically, we implement two proofs of that theorem, one by Scott and one by Hyland. We also explain the role of the Karoubi envelope - a categorical construction - in the proofs and the impact the chosen foundation has on this construction. Finally, we report on some automation we have implemented for the reduction of λ-terms.
Cite as

Arnoud van der Leer, Kobe Wullaert, and Benedikt Ahrens. Scott’s Representation Theorem and the Univalent Karoubi Envelope. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 33:1-33:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{vanderleer_et_al:LIPIcs.ITP.2025.33,
  author =	{van der Leer, Arnoud and Wullaert, Kobe and Ahrens, Benedikt},
  title =	{{Scott’s Representation Theorem and the Univalent Karoubi Envelope}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{33:1--33:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.33},
  URN =		{urn:nbn:de:0030-drops-246318},
  doi =		{10.4230/LIPIcs.ITP.2025.33},
  annote =	{Keywords: Lambda calculi, algebraic theories, categorical semantics, Karoubi envelope, formalization, Rocq-UniMath, univalent foundations}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2025.11
Impredicative Encodings of Inductive and Coinductive Types

Authors: Steven Bronsveld, Herman Geuvers, and Niels van der Weide

Published in: LIPIcs, Volume 337, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)

Abstract
In impredicative type theory (System F, also known as λ2), it is possible to define inductive data types, such as natural numbers and lists. It is also possible to define coinductive data types such as streams. They work well in the sense that their (co)recursion principles obey the expected computation rules (the β-rules). Unfortunately, they do not yield a (co)induction principle [Herman Geuvers, 2001; Ivar Rummelhoff, 2004], because the necessary uniqueness principles are missing (the η-rules). Awodey, Frey, and Speight [Steve Awodey et al., 2018] used an extension of the Calculus of Constructions [Thierry Coquand and Gérard P. Huet, 1988] (λ C) with Σ-types, identity-types, and functional extensionality to define System F style inductive types with an induction principle, by encoding them as a well-chosen subtype, making them initial algebras. In this paper, we extend their results to coinductive data types, and we detail the example of the stream data type with the desired coinduction principle (also called bisimulation). To do that, we first define quotient types (with the desired η-rules) and we also need a stronger form of the definable existential types. We also show that we can use the original method by Awodey, Frey and Speight for general inductive types by defining W-types with an induction principle. The dual approach for streams can be extended to M-types, the generic notion of coinductive types, and the dual of W-types.
Cite as

Steven Bronsveld, Herman Geuvers, and Niels van der Weide. Impredicative Encodings of Inductive and Coinductive Types. In 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 337, pp. 11:1-11:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{bronsveld_et_al:LIPIcs.FSCD.2025.11,
  author =	{Bronsveld, Steven and Geuvers, Herman and van der Weide, Niels},
  title =	{{Impredicative Encodings of Inductive and Coinductive Types}},
  booktitle =	{10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)},
  pages =	{11:1--11:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-374-4},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{337},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2025.11},
  URN =		{urn:nbn:de:0030-drops-236263},
  doi =		{10.4230/LIPIcs.FSCD.2025.11},
  annote =	{Keywords: Formulas-as-types, impredicativity, inductive types, coinductive types}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2024.3
A Foundation for Synthetic Stone Duality

Authors: Felix Cherubini, Thierry Coquand, Freek Geerligs, and Hugo Moeneclaey

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

Abstract
The language of homotopy type theory has proved to be an appropriate internal language for various higher toposes, for example for the Zariski topos in Synthetic Algebraic Geometry. This paper aims to do the same for the higher topos of light condensed anima of Dustin Clausen and Peter Scholze. This seems to be an appropriate setting for synthetic topology in the style of Martín Escardó. We use homotopy type theory extended with 4 axioms. We prove Markov’s principle, LLPO and the negation of WLPO. Then we define a type of open propositions, inducing a topology on any type such that any map is continuous. We give a synthetic definition of second countable Stone and compact Hausdorff spaces, and show that their induced topologies are as expected. This means that any map from e.g. the unit interval 𝕀 to itself is continuous in the usual epsilon-delta sense. With the usual definition of cohomology in homotopy type theory, we show that H¹(S,ℤ) = 0 for S Stone and that H¹(X,ℤ) for X compact Hausdorff can be computed using Čech cohomology. We use this to prove H¹(𝕀¹,ℤ) = 0 and H¹(𝕊¹,ℤ) = ℤ where 𝕊¹ is the set ℝ/ℤ. As an application, we give a synthetic proof of Brouwer’s fixed-point theorem.
Cite as

Felix Cherubini, Thierry Coquand, Freek Geerligs, and Hugo Moeneclaey. A Foundation for Synthetic Stone Duality. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 3:1-3:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{cherubini_et_al:LIPIcs.TYPES.2024.3,
  author =	{Cherubini, Felix and Coquand, Thierry and Geerligs, Freek and Moeneclaey, Hugo},
  title =	{{A Foundation for Synthetic Stone Duality}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{3:1--3: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.3},
  URN =		{urn:nbn:de:0030-drops-233659},
  doi =		{10.4230/LIPIcs.TYPES.2024.3},
  annote =	{Keywords: Homotopy Type Theory, Synthetic Topology, Cohomology}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2024.6
Data Types with Symmetries via Action Containers

Authors: Philipp Joram and Niccolò Veltri

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

Abstract
We study two kinds of containers for data types with symmetries in homotopy type theory, and clarify their relationship by introducing the intermediate notion of action containers. Quotient containers are set-valued containers with groups of permissible permutations of positions, interpreted as (possibly non-finitary) analytic functors on the category of sets. Symmetric containers encode symmetries in a groupoid of shapes, and are interpreted accordingly as polynomial functors on the 2-category of groupoids. Action containers are endowed with groups that act on their positions, with morphisms preserving the actions. We show that, as a category, action containers are equivalent to the free coproduct completion of a category of group actions. We derive that they model non-inductive single-variable strictly positive types in the sense of Abbott et al.: The category of action containers is closed under arbitrary (co)products and exponentiation with constants. We equip this category with the structure of a locally groupoidal 2-category, and prove that it locally embeds into the 2-category of symmetric containers. This follows from the embedding of a 2-category of groups into the 2-category of groupoids, extending the delooping construction.
Cite as

Philipp Joram and Niccolò Veltri. Data Types with Symmetries via Action Containers. In 30th International Conference on Types for Proofs and Programs (TYPES 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 336, pp. 6:1-6:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{joram_et_al:LIPIcs.TYPES.2024.6,
  author =	{Joram, Philipp and Veltri, Niccol\`{o}},
  title =	{{Data Types with Symmetries via Action Containers}},
  booktitle =	{30th International Conference on Types for Proofs and Programs (TYPES 2024)},
  pages =	{6:1--6:21},
  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.6},
  URN =		{urn:nbn:de:0030-drops-233681},
  doi =		{10.4230/LIPIcs.TYPES.2024.6},
  annote =	{Keywords: Containers, Homotopy Type Theory, Agda, 2-categories}
}
Document
DOI: 10.4230/LIPIcs.CSL.2025.45
Insights from Univalent Foundations: A Case Study Using Double Categories

Authors: Nima Rasekh, Niels van der Weide, Benedikt Ahrens, and Paige Randall North

Published in: LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)

Abstract
Category theory unifies mathematical concepts, aiding comparisons across structures by incorporating not just objects, but also morphisms capturing interactions between objects. Of particular importance in some applications are double categories, which are categories with two classes of morphisms, axiomatizing two different kinds of interactions between objects. These have found applications in many areas of mathematics and theoretical computer science, for instance, the study of lenses, open systems, and rewriting. However, double categories come with a wide variety of equivalences, which makes it challenging to transport structure along equivalences. To deal with this challenge, we propose the univalence maxim: each notion of equivalence of categorical structures has a corresponding notion of univalent categorical structure which induces that notion of equivalence. We also prove corresponding univalence principles, which allow us to transport structure and properties along equivalences. In this way, the usually informal practice of reasoning modulo equivalence becomes grounded in an entirely formal logical principle. We apply this perspective to various double categorical structures, such as (pseudo) double categories and double bicategories. Concretely, we characterize and formalize their definitions in Coq UniMath up to chosen equivalences, which we achieve by establishing their univalence principles.
Cite as

Nima Rasekh, Niels van der Weide, Benedikt Ahrens, and Paige Randall North. Insights from Univalent Foundations: A Case Study Using Double Categories. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 45:1-45:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{rasekh_et_al:LIPIcs.CSL.2025.45,
  author =	{Rasekh, Nima and van der Weide, Niels and Ahrens, Benedikt and North, Paige Randall},
  title =	{{Insights from Univalent Foundations: A Case Study Using Double Categories}},
  booktitle =	{33rd EACSL Annual Conference on Computer Science Logic (CSL 2025)},
  pages =	{45:1--45:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-362-1},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{326},
  editor =	{Endrullis, J\"{o}rg and Schmitz, Sylvain},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.45},
  URN =		{urn:nbn:de:0030-drops-228024},
  doi =		{10.4230/LIPIcs.CSL.2025.45},
  annote =	{Keywords: formalization of mathematics, category theory, double categories, univalent foundations}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.4
Univalent Enriched Categories and the Enriched Rezk Completion

Authors: Niels van der Weide

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Enriched categories are categories whose sets of morphisms are enriched with extra structure. Such categories play a prominent role in the study of higher categories, homotopy theory, and the semantics of programming languages. In this paper, we study univalent enriched categories. We prove that all essentially surjective and fully faithful functors between univalent enriched categories are equivalences, and we show that every enriched category admits a Rezk completion. Finally, we use the Rezk completion for enriched categories to construct univalent enriched Kleisli categories.
Cite as

Niels van der Weide. Univalent Enriched Categories and the Enriched Rezk Completion. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 4:1-4:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{vanderweide:LIPIcs.FSCD.2024.4,
  author =	{van der Weide, Niels},
  title =	{{Univalent Enriched Categories and the Enriched Rezk Completion}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{4:1--4:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.4},
  URN =		{urn:nbn:de:0030-drops-203337},
  doi =		{10.4230/LIPIcs.FSCD.2024.4},
  annote =	{Keywords: enriched categories, univalent categories, homotopy type theory, univalent foundations, Rezk completion}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2022.15
Univalent Monoidal Categories

Authors: Kobe Wullaert, Ralph Matthes, and Benedikt Ahrens

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
Univalent categories constitute a well-behaved and useful notion of category in univalent foundations. The notion of univalence has subsequently been generalized to bicategories and other structures in (higher) category theory. Here, we zoom in on monoidal categories and study them in a univalent setting. Specifically, we show that the bicategory of univalent monoidal categories is univalent. Furthermore, we construct a Rezk completion for monoidal categories: we show how any monoidal category is weakly equivalent to a univalent monoidal category, universally. We have fully formalized these results in UniMath, a library of univalent mathematics in the Coq proof assistant.
Cite as

Kobe Wullaert, Ralph Matthes, and Benedikt Ahrens. Univalent Monoidal Categories. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 15:1-15:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{wullaert_et_al:LIPIcs.TYPES.2022.15,
  author =	{Wullaert, Kobe and Matthes, Ralph and Ahrens, Benedikt},
  title =	{{Univalent Monoidal Categories}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{15:1--15:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.15},
  URN =		{urn:nbn:de:0030-drops-184580},
  doi =		{10.4230/LIPIcs.TYPES.2022.15},
  annote =	{Keywords: Univalence, Monoidal categories, Rezk completion, Displayed (bi)categories, Proof assistant Coq, UniMath library}
}
Document
DOI: 10.4230/LIPIcs.ITP.2023.30
Certifying Higher-Order Polynomial Interpretations

Authors: Niels van der Weide, Deivid Vale, and Cynthia Kop

Published in: LIPIcs, Volume 268, 14th International Conference on Interactive Theorem Proving (ITP 2023)

Abstract
Higher-order rewriting is a framework in which one can write higher-order programs and study their properties. One such property is termination: the situation that for all inputs, the program eventually halts its execution and produces an output. Several tools have been developed to check whether higher-order rewriting systems are terminating. However, developing such tools is difficult and can be error-prone. In this paper, we present a way of certifying termination proofs of higher-order term rewriting systems. We formalize a specific method that is used to prove termination, namely the polynomial interpretation method. In addition, we give a program that processes proof traces containing a high-level description of a termination proof into a formal Coq proof script that can be checked by Coq. We demonstrate the usability of this approach by certifying higher-order polynomial interpretation proofs produced by Wanda, a termination analysis tool for higher-order rewriting.
Cite as

Niels van der Weide, Deivid Vale, and Cynthia Kop. Certifying Higher-Order Polynomial Interpretations. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 30:1-30:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{vanderweide_et_al:LIPIcs.ITP.2023.30,
  author =	{van der Weide, Niels and Vale, Deivid and Kop, Cynthia},
  title =	{{Certifying Higher-Order Polynomial Interpretations}},
  booktitle =	{14th International Conference on Interactive Theorem Proving (ITP 2023)},
  pages =	{30:1--30:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-284-6},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{268},
  editor =	{Naumowicz, Adam and Thiemann, Ren\'{e}},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2023.30},
  URN =		{urn:nbn:de:0030-drops-184051},
  doi =		{10.4230/LIPIcs.ITP.2023.30},
  annote =	{Keywords: higher-order rewriting, Coq, termination, formalization}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2023.6
The Formal Theory of Monads, Univalently

Authors: Niels van der Weide

Published in: LIPIcs, Volume 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)

Abstract
We develop the formal theory of monads, as established by Street, in univalent foundations. This allows us to formally reason about various kinds of monads on the right level of abstraction. In particular, we define the bicategory of monads internal to a bicategory, and prove that it is univalent. We also define Eilenberg-Moore objects, and we show that both Eilenberg-Moore categories and Kleisli categories give rise to Eilenberg-Moore objects. Finally, we relate monads and adjunctions in arbitrary bicategories. Our work is formalized in Coq using the https://github.com/UniMath/UniMath library.
Cite as

Niels van der Weide. The Formal Theory of Monads, Univalently. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 6:1-6:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{vanderweide:LIPIcs.FSCD.2023.6,
  author =	{van der Weide, Niels},
  title =	{{The Formal Theory of Monads, Univalently}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{6:1--6:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2023.6},
  URN =		{urn:nbn:de:0030-drops-179904},
  doi =		{10.4230/LIPIcs.FSCD.2023.6},
  annote =	{Keywords: bicategory theory, univalent foundations, formalization, monads, Coq}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2021.22
Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor

Authors: Niccolò Veltri

Published in: LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)

Abstract
The finite powerset functor is a construct frequently employed for the specification of nondeterministic transition systems as coalgebras. The final coalgebra of the finite powerset functor, whose elements characterize the dynamical behavior of transition systems, is a well-understood object which enjoys many equivalent presentations in set-theoretic foundations based on classical logic. In this paper, we discuss various constructions of the final coalgebra of the finite powerset functor in constructive type theory, and we formalize our results in the Cubical Agda proof assistant. Using setoids, the final coalgebra of the finite powerset functor can be defined from the final coalgebra of the list functor. Using types instead of setoids, as it is common in homotopy type theory, one can specify the finite powerset datatype as a higher inductive type and define its final coalgebra as a coinductive type. Another construction is obtained by quotienting the final coalgebra of the list functor, but the proof of finality requires the assumption of the axiom of choice. We conclude the paper with an analysis of a classical construction by James Worrell, and show that its adaptation to our constructive setting requires the presence of classical axioms such as countable choice and the lesser limited principle of omniscience.
Cite as

Niccolò Veltri. Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor. In 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 195, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{veltri:LIPIcs.FSCD.2021.22,
  author =	{Veltri, Niccol\`{o}},
  title =	{{Type-Theoretic Constructions of the Final Coalgebra of the Finite Powerset Functor}},
  booktitle =	{6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
  pages =	{22:1--22:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-191-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{195},
  editor =	{Kobayashi, Naoki},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.22},
  URN =		{urn:nbn:de:0030-drops-142601},
  doi =		{10.4230/LIPIcs.FSCD.2021.22},
  annote =	{Keywords: type theory, finite powerset, final coalgebra, Cubical Agda}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.5
Bicategories in Univalent Foundations

Authors: Benedikt Ahrens, Dan Frumin, Marco Maggesi, and Niels van der Weide

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
We develop bicategory theory in univalent foundations. Guided by the notion of univalence for (1-)categories studied by Ahrens, Kapulkin, and Shulman, we define and study univalent bicategories. To construct examples of those, we develop the notion of "displayed bicategories", an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. Displayed bicategories allow us to construct univalent bicategories in a modular fashion. To demonstrate the applicability of this notion, we prove several bicategories are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Our work is formalized in the UniMath library of univalent mathematics.
Cite as

Benedikt Ahrens, Dan Frumin, Marco Maggesi, and Niels van der Weide. Bicategories in Univalent Foundations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 5:1-5:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{ahrens_et_al:LIPIcs.FSCD.2019.5,
  author =	{Ahrens, Benedikt and Frumin, Dan and Maggesi, Marco and van der Weide, Niels},
  title =	{{Bicategories in Univalent Foundations}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{5:1--5:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.5},
  URN =		{urn:nbn:de:0030-drops-105124},
  doi =		{10.4230/LIPIcs.FSCD.2019.5},
  annote =	{Keywords: bicategory theory, univalent mathematics, dependent type theory, Coq}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.32
Guarded Recursion in Agda via Sized Types

Authors: Niccolò Veltri and Niels van der Weide

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
In type theory, programming and reasoning with possibly non-terminating programs and potentially infinite objects is achieved using coinductive types. Recursively defined programs of these types need to be productive to guarantee the consistency of the type system. Proof assistants such as Agda and Coq traditionally employ strict syntactic productivity checks, which often make programming with coinductive types convoluted. One way to overcome this issue is by encoding productivity at the level of types so that the type system forbids the implementation of non-productive corecursive programs. In this paper we compare two different approaches to type-based productivity: guarded recursion and sized types. More specifically, we show how to simulate guarded recursion in Agda using sized types. We formalize the syntax of a simple type theory for guarded recursion, which is a variant of Atkey and McBride’s calculus for productive coprogramming. Then we give a denotational semantics using presheaves over the preorder of sizes. Sized types are fundamentally used to interpret the characteristic features of guarded recursion, notably the fixpoint combinator.
Cite as

Niccolò Veltri and Niels van der Weide. Guarded Recursion in Agda via Sized Types. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{veltri_et_al:LIPIcs.FSCD.2019.32,
  author =	{Veltri, Niccol\`{o} and van der Weide, Niels},
  title =	{{Guarded Recursion in Agda via Sized Types}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{32:1--32:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.32},
  URN =		{urn:nbn:de:0030-drops-105391},
  doi =		{10.4230/LIPIcs.FSCD.2019.32},
  annote =	{Keywords: guarded recursion, type theory, semantics, coinduction, sized types}
}
  • Refine by Type
  • 15 Document/PDF
  • 6 Document/HTML

  • Refine by Publication Year
  • 2 2026
  • 6 2025
  • 1 2024
  • 3 2023
  • 1 2021
  • Show More...

  • Refine by Author
  • 7 van der Weide, Niels
  • 4 Ahrens, Benedikt
  • 3 Veltri, Niccolò
  • 2 Wullaert, Kobe
  • 1 Altenkirch, Thorsten
  • Show More...

  • Refine by Series/Journal
  • 15 LIPIcs

  • Refine by Classification
  • 12 Theory of computation → Type theory
  • 6 Theory of computation → Logic and verification
  • 3 Theory of computation → Categorical semantics
  • 1 Computing methodologies → Theorem proving algorithms
  • 1 Mathematics of computing → Topology
  • Show More...

  • Refine by Keyword
  • 4 univalent foundations
  • 3 Coq
  • 3 formalization
  • 2 Homotopy Type Theory
  • 2 Rezk completion
  • Show More...

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