7 papers
Univalent Enriched Categories and the Enriched Rezk Completion
Niels van der Weide
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 theo…
Initial Algebras of Domains via Quotient Inductive-Inductive Types
Simcha van Collem, Niels van der Weide, Herman Geuvers
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 c…
Impredicativity in Linear Dependent Type Theory
Sam Speight, Niels van der Weide
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, w…
The Rezk Completion for Elementary Topoi
Kobe Wullaert, Niels van der Weide
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 univale…
The internal languages of univalent categories
Niels van der Weide
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 Dyb…
Master Thesis Impredicative Encodings of Inductive and Coinductive Types
Steven Bronsveld, Herman Geuvers, Niels van der Weide
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…