arXiv subjects

Niels van der Weide

Publications and source records attributed to Niels van der Weide.

16 recordsLinked to original sources

arXiv2026

The internal languages of univalent categories

Internal language theorems are fundamental in categorical logic, since they express an equivalence between syntax and semantics. One such theorem was proven by Clairambault and Dybjer, who corrected the result originally by Seely. More specifically, they constructed a biequivalence between the bicategory of locally Cartesian closed categories and the bicategory of democratic categories with families with extensional identity types, $Σ$-types, and $Π$-types. This theorem expresses that the internal language of locally Cartesian closed categories is extensional Martin-Löf type theory with dependent sums and products. In this paper, we study the theorem by Clairambault and Dybjer for univalent categories, and we extend it to various classes of toposes, among which are $Π$-pretoposes, elementary toposes, and elementary toposes with a universe. The results in this paper have been formalized using the proof assistant Rocq and the UniMath library.

math.CT↗

arXiv2026

Univalent Enriched Categories and the Enriched Rezk Completion

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.

cs.LO↗

arXiv2026

Initial Algebras of Domains via Quotient Inductive-Inductive Types

Domain theory has been developed as a mathematical theory of computation and to give a denotational semantics to programming languages. It helps us to fix the meaning of language concepts, to understand how programs behave and to reason about programs. At the same time it serves as a great theory to model various algebraic effects such as non-determinism, partial functions, side effects and numerous other forms of computation. In the present paper, we present a general framework to construct algebraic effects in domain theory, where our domains are DCPOs: directed complete partial orders. We first describe so called DCPO algebras for a signature, where the signature specifies the operations on the DCPO and the inequational theory they obey. This provides a method to represent various algebraic effects, like partiality. We then show that initial DCPO algebras exist by defining them as so called Quotient Inductive-Inductive Types (QIITs), known from homotopy type theory. A quotient inductive-inductive type allows one to simultaneously define an inductive type and an inductive relation on that type, together with equations on the type. We illustrate our approach by showing that several well-known constructions of DCPOs fit our framework: coalesced sums, smash products and free DCPOs (partiality and power domains). Our work makes use of various features of homotopy type theory and is formalized in Cubical Agda.

cs.LO↗

arXiv2026

Impredicativity in Linear Dependent Type Theory

We construct a realizability model of linear dependent type theory from a linear combinatory algebra. Our model motivates a number of additions to the type theory. In particular, we add a universe with two decoding operations: one takes codes to cartesian types and the other takes codes to linear types. The universe is impredicative in the sense that it is closed under both large cartesian dependent products and large linear dependent products. We also add a rule for injectivity of the modality turning linear terms into cartesian terms. With all of the additions, we are able to encode (linear) inductive types. As a case study, we consider the type of lists over a linear type, and demonstrate that our encoding has the relevant uniqueness principle. The construction of the realizability model is fully formalized in the proof assistant Rocq.

cs.LO↗

arXiv2026

The Rezk Completion for Elementary Topoi

The development of category theory in univalent foundations and the formalization thereof is an active field of research. Categories in that setting are often assumed to be univalent which means that identities and isomorphisms of objects coincide. One consequence hereof is that equivalences and identities coincide for univalent categories and that structure on univalent categories transfers along equivalences. However, constructions such as the Kleisli category, the Karoubi envelope, and the tripos-to-topos construction, do not necessarily give univalent categories. To deal with that problem, one uses the Rezk completion, which completes a category into a univalent one. However, to use the Rezk completion when considering categories with structure, one also needs to show that the Rezk completion inherits the structure from the original category. In this work, we present a modular framework for lifting the Rezk completion from categories to categories with structure. We demonstrate the modularity of our framework by lifting the Rezk completion from categories to elementary topoi in manageable steps.

cs.LO↗

arXiv2025

From Semantics to Syntax: A Type Theory for Comprehension Categories

Recent models of intensional type theory have been constructed in algebraic weak factorization systems (AWFSs). AWFSs give rise to comprehension categories that feature non-trivial morphisms between types; these morphisms are not used in the standard interpretation of Martin-Löf type theory in comprehension categories. We develop a type theory that internalizes morphisms between types, reflecting this semantic feature back into syntax. Our type theory comes with $Π$-, $Σ$-, and identity types. We discuss how it can be viewed as an extension of Martin-Löf type theory with coercive subtyping, as sketched by Coraglia and Emmenegger. We furthermore define semantic structure that interprets our type theory and prove a soundness result. Finally, we exhibit many examples of the semantic structure, yielding a plethora of interpretations.

cs.PL↗

arXiv2025

Master Thesis Impredicative Encodings of Inductive and Coinductive Types

In the impredicative type theory of System F (λ2), it is possible to create inductive data types, such as natural numbers and lists. It is also possible to create coinductive data types such as streams. They work well in the sense that their (co)recursion principles obey the expected computation rules (the \b{eta}-rules). Unfortunately, they do not yield a (co)induction principle, because the necessary uniqueness principles are missing (the η-rules). Awodey, Frey, and Speight (2018) used an extension of λC with sigma-types, equality-types, and functional extensionality to provide System F style inductive types with an induction principle by encoding them as a well-chosen subtype, making them initial algebras. In this thesis, we extend their results. We create a list and quotient type that have the desired induction principles. We show that we can use the technique for general inductive types by defining W-types with an induction principle. We also take the dual notion of their technique and create a coinductive stream type with the desired coinduction principle (also called bisimulation). We finish by showing that this dual approach can be extended to M-types, the generic notion of coinductive types, and the dual of W-types.

cs.LO↗

arXiv2025

The Formal Theory of Monads, Univalently

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 UniMath library.

cs.LO↗

arXiv2024

Intrinsically Correct Sorting in Cubical Agda

The paper "Sorting with Bialgebras and Distributive Laws" by Hinze et al. uses the framework of bialgebraic semantics to define sorting algorithms. From distributive laws between functors they construct pairs of sorting algorithms using both folds and unfolds. Pairs of sorting algorithms arising this way include insertion/selection sort and quick/tree sort. We extend this work to define intrinsically correct variants in cubical Agda. Our key idea is to index our data types by multisets, which concisely captures that a sorting algorithm terminates with an ordered permutation of its input list. By lifting bialgebraic semantics to the indexed setting, we obtain the correctness of sorting algorithms purely from the distributive law.

cs.LO↗

arXiv2024

Insights From Univalent Foundations: A Case Study Using Double Categories

Category theory unifies mathematical concepts, aiding comparisons across structures by incorporating objects and morphisms, which capture their interactions. It has influenced areas of computer science such as automata theory, functional programming, and semantics. Certain objects naturally exhibit two classes of morphisms, leading to the concept of a double category, which has found applications in computing science (e.g., ornaments, profunctor optics, denotational semantics). The emergence of diverse categorical structures motivated a unified framework for category theory. However, unlike other mathematical objects, classification of categorical structures faces challenges due to various relevant equivalences. This poses significant challenges when pursuing the formalization of categories and restricts the applicability of powerful techniques, such as transport along equivalences. This work contends that univalent foundations offers a suitable framework for classifying different categorical structures based on desired notions of equivalences, and remedy the challenges when formalizing categories. The richer notion of equality in univalent foundations makes the equivalence of a categorical structure an inherent part of its structure. We concretely apply this analysis to double categorical structures. We characterize and formalize various definitions in Coq UniMath, including (pseudo) double categories and double bicategories, up to chosen equivalences. We also establish univalence principles, making chosen equivalences part of the double categorical structure, analyzing strict double setcategories (invariant under isomorphisms), pseudo double setcategories (invariant under isomorphisms), univalent pseudo double categories (invariant under vertical equivalences) and univalent double bicategories (invariant under gregarious equivalences).

math.CT↗

arXiv2023

Univalent Double Categories

Category theory is a branch of mathematics that provides a formal framework for understanding the relationship between mathematical structures. To this end, a category not only incorporates the data of the desired objects, but also "morphisms", which capture how different objects interact with each other. Category theory has found many applications in mathematics and in computer science, for example in functional programming. Double categories are a natural generalization of categories which incorporate the data of two separate classes of morphisms, allowing a more nuanced representation of relationships and interactions between objects. Similar to category theory, double categories have been successfully applied to various situations in mathematics and computer science, in which objects naturally exhibit two types of morphisms. Examples include categories themselves, but also lenses, petri nets, and spans. While categories have already been formalized in a variety of proof assistants, double categories have received far less attention. In this paper we remedy this situation by presenting a formalization of double categories via the proof assistant Coq, relying on the Coq UniMath library. As part of this work we present two equivalent formalizations of the definition of a double category, an unfolded explicit definition and a second definition which exhibits excellent formal properties via 2-sided displayed categories. As an application of the formal approach we establish a notion of univalent double category along with a univalence principle: equivalences of univalent double categories coincide with their identities

math.CT↗

arXiv2023

Bicategorical type theory: semantics and syntax

We develop semantics and syntax for bicategorical type theory. Bicategorical type theory features contexts, types, terms, and directed reductions between terms. This type theory is naturally interpreted in a class of structured bicategories. We start by developing the semantics, in the form of comprehension bicategories. Examples of comprehension bicategories are plentiful; we study both specific examples as well as classes of examples constructed from other data. From the notion of comprehension bicategory, we extract the syntax of bicategorical type theory, that is, judgment forms and structural inference rules. We prove soundness of the rules by giving an interpretation in any comprehension bicategory. The semantic aspects of our work are fully checked in the Coq proof assistant, based on the UniMath library.

cs.LO↗

arXiv2023

Certifying Higher-Order Polynomial Interpretations

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, namely the polynomial interpretation method, that is used to prove termination. In addition, we give a program that turns the output of Wanda, a termination analysis tool for higher-order rewriting systems, into a Coq script, so that we can check whether the output is a valid proof of termination.

cs.LO↗

arXiv2022

Bicategories in Univalent Foundations

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 univalent bicategories in a modular fashion, we develop displayed bicategories, an analog of displayed 1-categories introduced by Ahrens and Lumsdaine. We demonstrate the applicability of this notion, and prove that several bicategories of interest are univalent. Among these are the bicategory of univalent categories with families and the bicategory of pseudofunctors between univalent bicategories. Furthermore, we show that every bicategory with univalent hom-categories is weakly equivalent to a univalent bicategory. All of our work is formalized in Coq as part of the UniMath library of univalent mathematics.

math.CT↗

arXiv2021

Formalizing Higher-Order Termination in Coq

We describe a formalization of higher-order rewriting theory and formally prove that an AFS is strongly normalizing if it can be interpreted in a well-founded domain. To do so, we use Coq, which is a proof assistant based on dependent type theory. Using this formalization, one can implement several termination techniques, like the interpretation method or dependency pairs, and prove their correctness. Those implementations can then be extracted to OCaml, which results in a verified termination checker.

cs.LO↗

arXiv2021

Constructing Higher Inductive Types as Groupoid Quotients

In this paper, we study finitary 1-truncated higher inductive types (HITs) in homotopy type theory. We start by showing that all these types can be constructed from the groupoid quotient. We define an internal notion of signatures for HITs, and for each signature, we construct a bicategory of algebras in 1-types and in groupoids. We continue by proving initial algebra semantics for our signatures. After that, we show that the groupoid quotient induces a biadjunction between the bicategories of algebras in 1-types and in groupoids. Then we construct a biinitial object in the bicategory of algebras in groupoids, which gives the desired algebra. From all this, we conclude that all finitary 1-truncated HITs can be constructed from the groupoid quotient. We present several examples of HITs which are definable using our notion of signature. In particular, we show that each signature gives rise to a HIT corresponding to the freely generated algebraic structure over it. We also start the development of universal algebra in 1-types. We show that the bicategory of algebras has PIE limits, i.e. products, inserters and equifiers, and we prove a version of the first isomorphism theorem for 1-types. Finally, we give an alternative characterization of the foundamental groups of some HITs, exploiting our construction of HITs via the groupoid quotient. All the results are formalized over the UniMath library of univalent mathematics in Coq.

cs.LO↗