4 citations · 12 across the 8 of their papers we have counts for
6 papers · 1 filter
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…
Certifying Higher-Order Polynomial Interpretations
Niels van der Weide, Deivid Vale, Cynthia Kop
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 Formal Theory of Monads, Univalently
Niels van der Weide
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 ab…
Bicategorical type theory: semantics and syntax
Benedikt Ahrens, Paige Randall North, Niels van der Weide
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…
Formalizing Higher-Order Termination in Coq
Deivid Vale, Niels van der Weide
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…
Constructing Higher Inductive Types as Groupoid Quotients
Niccolò Veltri, Niels van der Weide
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 qu…