nLab Niels van der Weide

• website

 Publications

On higher inductive types in homotopy type theory:

• Henning Basold, Herman Geuvers, Niels van der Weide, Higher Inductive Types in Programming, Journal of Universal Computer Science 23 1 (2017) 63-88 [pdf, slides pdf]

• Niccolò Veltri, Niels van der Weide, Constructing Higher Inductive Types as Groupoid Quotients, Logical Methods in Computer Science 17 2 (2021) [arXiv:2002.08150, doi:10.23638/LMCS-17(2:8)2021]

• Niels van der Weide, Constructing 1-Truncated Finitary Higher Inductive Types as Groupoid Quotients, Homotopy Type Theory Electronic Seminar Talks, 6 February 2020 (video, slides)

On finite sets in homotopy type theory/univalent foundations of mathematics:

• Dan Frumin, Herman Geuvers, Léon Gondelman, Niels van der Weide, Finite Sets in Homotopy Type Theory, in CPP 2018: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (2018) 201–214 [doi:10.1145/3167085, pdf]

On 2-dimensional type theory:

• Benedikt Ahrens, Paige Randall North, Niels van der Weide, Semantics for two-dimensional type theory, LICS ‘22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, 12 (2022) 1–14, [doi:10.1145/3531130.3533334]

On univalent bicategories in homotopy type theory:

• Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niels van der Weide, Bicategories in Univalent Foundations, Mathematical Structures in Computer Science 31 10 (2022) 1232-1269 [arXiv:1903.01152, doi:10.1017/S0960129522000032&rbrack

An internal language for comprehension categories is developed in:

• Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens, Paige Randall North, A Type Theory for Comprehension Categories with Applications to Subtyping (arXiv:2503.10868)

Related entries

• univalent foundations of mathematics

• UniMath project

category: people