SU\G(𝔸)/K·U

Author Description

Login to generate an author description

Ask a Question About This Mathematician

All published works (21)

Action Title Date Authors
+ PDF Ask
The Formal Theory of Monads, Univalently 2025-02-19 Niels van der Weide
+ PDF Ask
Intrinsically Correct Sorting in Cubical Agda 2025-01-10 Cass Alexandru Vikraman Choudhury Jurriaan Rot Niels van der Weide
+ PDF Ask
The internal languages of univalent categories 2024-11-10 Niels van der Weide
+ PDF Ask
Insights From Univalent Foundations: A Case Study Using Double Categories 2024-02-07 Nima Rasekh Niels van der Weide Benedikt Ahrens Paige Randall North
+ PDF Ask
Univalent Double Categories 2024-01-09 Niels van der Weide Nima Rasekh Benedikt Ahrens Paige Randall North
+ PDF Ask
Univalent Enriched Categories and the Enriched Rezk Completion 2024-01-01 Niels van der Weide
+
The Interval Domain in Homotopy Type Theory 2024-01-01 Niels van der Weide Dan Frumin
+ PDF Ask
Bicategorical type theory: semantics and syntax 2023-10-17 Benedikt Ahrens Paige Randall North Niels van der Weide
+ PDF Ask
Certifying Higher-Order Polynomial Interpretations 2023-02-23 Niels van der Weide Deivid Vale Cynthia Kop
+ PDF Ask
Certifying Higher-Order Polynomial Interpretations 2023-01-01 Niels van der Weide Deivid Vale Cynthia Kop
+ PDF Ask
Univalent Double Categories 2023-01-01 Niels van der Weide Nima Rasekh Benedikt Ahrens Paige Randall North
+ PDF Ask
Semantics for two-dimensional type theory 2022-08-02 Benedikt Ahrens Paige Randall North Niels van der Weide
+ PDF Ask
The Formal Theory of Monads, Univalently 2022-01-01 Niels van der Weide
+ PDF Ask
Bicategories in univalent foundations 2021-11-01 Benedikt Ahrens Dan Frumin Marco Maggesi Niccolò Veltri Niels van der Weide
+ PDF Ask
Constructing Higher Inductive Types as Groupoid Quotients 2021-04-22 Niccolò Veltri Niels van der Weide
+
Constructing Higher Inductive Types as Groupoid Quotients 2021-01-01 Niccolò Veltri Niels van der Weide
+ PDF Ask
Formalizing Higher-Order Termination in Coq 2021-01-01 Deivid Vale Niels van der Weide
+ PDF Ask
Constructing Higher Inductive Types as Groupoid Quotients 2020-05-26 Niels van der Weide
+ PDF Ask
Bicategories in Univalent Foundations 2019-03-04 Benedikt Ahrens Dan Frumin Marco Maggesi Niccolò Veltri Niels van der Weide
+ PDF Ask
Finite sets in homotopy type theory 2018-01-08 Dan Frumin Herman Geuvers LĂ©on Gondelman Niels van der Weide
+ PDF Ask
Finite sets in homotopy type theory 2017-12-22 Dan Frumin Herman Geuvers LĂ©on Gondelman Niels van der Weide

Common Coauthors

Coauthor Papers Together
Benedikt Ahrens 7
Dan Frumin 5
Paige Randall North 5
Niccolò Veltri 4
Deivid Vale 3
Nima Rasekh 3
Cynthia Kop 2
Marco Maggesi 2
LĂ©on Gondelman 2
Herman Geuvers 2
Vikraman Choudhury 1
Jurriaan Rot 1
Cass Alexandru 1

Commonly Cited References

Action Title Date Authors # of times referenced
+
Finitary Higher Inductive Types in the Groupoid Model 2018-04-01 Peter Dybjer Hugo Moeneclaey 6
+ PDF Ask
Univalent categories and the Rezk completion 2015-01-19 Benedikt Ahrens Krzysztof Kapulkin Michael Shulman 6
+ PDF Ask
The simplicial model of Univalent Foundations (after Voevodsky) 2021-03-08 Krzysztof Kapulkin Peter LeFanu Lumsdaine 5
+
Introduction to bicategories 1967-01-01 Jean BĂ©nabou 5
+ PDF Ask
Inductive Types in Homotopy Type Theory 2012-06-01 Steve Awodey Nicola Gambino Kristina Sojakova 4
+ PDF Ask
Univalent higher categories via complete Semi-Segal types 2017-12-27 Paolo Capriotti Nicolai Kraus 4
+ PDF Ask
Constructing the propositional truncation using non-recursive HITs 2016-01-12 Floris van Doorn 4
+ PDF Ask
Higher Inductive Types as Homotopy-Initial Algebras 2014-12-19 Kristina Sojakova 4
+ PDF Ask
Types are weak <i>ω</i> -groupoids 2010-10-12 Benno van den Berg Richard Garner 4
+ PDF Ask
Constructions with Non-Recursive Higher Inductive Types 2016-07-05 Nicolai Kraus 4
+ PDF Ask
Bicategories in univalent foundations 2021-11-01 Benedikt Ahrens Dan Frumin Marco Maggesi Niccolò Veltri Niels van der Weide 4
+ PDF Ask
Homotopy Type Theory: Univalent Foundations of Mathematics 2013-01-01 Peter Aczel Benedikt Ahrens Thorsten Altenkirch Steve Awodey Bruno Barras Andrej Bauer Yves Bertot Marc Bezem Thierry Coquand Eric Finster 3
+ PDF Ask
Biequivalences in tricategories 2011-01-01 Nick Gurski 3
+
A Coherent Approach to Pseudomonads 2000-06-01 Stephen Lack 3
+ PDF Ask
Towards a Directed Homotopy Type Theory 2019-11-01 Paige Randall North 3
+
Two-dimensional monad theory 1989-07-01 Robert Blackwell G. M. Kelly John Power 3
+ PDF Ask
Weak omega-categories from intensional type theory 2010-09-17 Peter LeFanu Lumsdaine 3
+ PDF Ask
Calculating the Fundamental Group of the Circle in Homotopy Type Theory 2013-06-01 Daniel R. Licata Michael Shulman 3
+ PDF Ask
Higher inductive types in cubical computational type theory 2019-01-02 Evan Cavallo Robert Harper 3
+ PDF Ask
Eilenberg-MacLane spaces in homotopy type theory 2014-07-14 Daniel R. Licata Eric Finster 3
+
Fibrations and partial products in a 2-category 1993-01-01 Peter Johnstone 2
+ PDF Ask
Constructing Higher Inductive Types as Groupoid Quotients 2021-04-22 Niccolò Veltri Niels van der Weide 2
+ PDF Ask
The Integers as a Higher Inductive Type 2020-05-26 Thorsten Altenkirch Luis Scoccola 2
+
Some properties of Fib as a fibred 2-category 1999-01-01 Claudio Hermida 2
+ PDF Ask
Displayed Categories 2017-01-01 Benedikt Ahrens Peter LeFanu Lumsdaine 2
+
Internal type theory 1996-01-01 Peter Dybjer 2
+ PDF Ask
Fibred 2-categories and bicategories 2013-11-25 Mitchell Buckley 2
+
Characterization of bicategories of stacks 1982-01-01 Ross Street 2
+ PDF Ask
Homotopy Type Theory in Lean 2017-01-01 Floris van Doorn Jakob von Raumer Ulrik Buchholtz 2
+ PDF Ask
Ramsey's Theorem and the Pigeonhole Principle in Intuitionistic Mathematics 1993-04-01 Wim Veldman Marc Bezem 2
+
Finiteness and rational sequences, constructively 2017-01-01 Tarmo Uustalu Niccolò Veltri 2
+ PDF Ask
A type theory for cartesian closed bicategories (Extended Abstract) 2019-06-01 Marcelo Fiore Philip Saville 2
+ PDF Ask
Impredicative Encodings of (Higher) Inductive Types 2018-06-27 Steve Awodey Jonas Frey Sam Speight 2
+ PDF Ask
A Cubical Approach to Synthetic Homotopy Theory 2015-07-01 Daniel R. Licata Guillaume Brunerie 2
+ PDF Ask
On Higher Inductive Types in Cubical Type Theory 2018-06-27 Thierry Coquand Simon Huber Anders Mörtberg 2
+ PDF Ask
Cubical Type Theory: a constructive interpretation of the univalence axiom 2016-01-01 Cyril Cohen Thierry Coquand Simon Huber Anders Mörtberg 2
+ PDF Ask
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type 2016-10-28 Thorsten Altenkirch Nils Anders Danielsson Nicolai Kraus 2
+ PDF Ask
Categorical structures for type theory in univalent foundations 2017-01-01 Benedikt Ahrens Peter LeFanu Lumsdaine Vladimir Voevodsky 2
+ PDF Ask
An induction principle and pigeonhole principles for K-finite sets 1995-12-01 Andreas Blass 2
+ PDF Ask
Quotient Inductive-Inductive Types 2018-01-01 Thorsten Altenkirch Paolo Capriotti Gabe Dijkstra Nicolai Kraus Fredrik Nordvall Forsberg 2
+
Univalent Higher Categories via Complete Semi-Segal Types 2018-01-07 Paolo Capriotti Nicolai Kraus 2
+ PDF Ask
Stack semantics of type theory 2017-06-01 Thierry Coquand Bassel Mannaa Fabian Ruch 2
+
Discrete Generalised Polynomial Functors 2012-01-01 Marcelo Fiore 2
+ PDF Ask
The real projective spaces in homotopy type theory 2017-06-01 Ulrik Buchholtz Egbert Rijke 2
+ PDF Ask
Constructing quotient inductive-inductive types 2019-01-02 Ambrus Kaposi András Kovács Thorsten Altenkirch 2
+ PDF Ask
Finite sets in homotopy type theory 2018-01-08 Dan Frumin Herman Geuvers LĂ©on Gondelman Niels van der Weide 2
+ PDF Ask
Variations on Noetherianness 2016-04-01 Denis Firsov Tarmo Uustalu Niccolò Veltri 2
+ PDF Ask
Two-dimensional models of type theory 2009-07-02 Richard Garner 2
+
Fibred and Cofibred Categories 1966-01-01 John W. Gray 2
+ PDF Ask
Natural models of homotopy type theory 2016-11-17 Steve Awodey 2