4 papers
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…
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…
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…