Peter Dybjer

Generating author description...

All published works

Action	Title	Year	Authors
+	Type Theory with Explicit Universe Polymorphism	2022	Marc Bezem Thierry Coquand Peter Dybjer Martı́n Hötzel Escardó
+ PDF Chat	Categories with Families: Unityped, Simply Typed, and Dependently Typed	2021	Simon Castellan Pierre Clairambault Peter Dybjer
+	A Note on Generalized Algebraic Theories and Categories with Families	2020	Marc Bezem Thierry Coquand Peter Dybjer Martı́n Hötzel Escardó
+	Categories with Families: Unityped, Simply Typed, and Dependently Typed	2019	Simon Castellan Pierre Clairambault Peter Dybjer
+	Categories with Families: Unityped, Simply Typed, and Dependently Typed	2019	Simon Castellan Pierre Clairambault Peter Dybjer
+	Finitary Higher Inductive Types in the Groupoid Model	2018	Peter Dybjer Hugo Moeneclaey
+	Undecidability of Equality in the Free Locally Cartesian Closed Category	2015	Simon Castellan Pierre Clairambault Peter Dybjer
+	Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)	2015	Simon Castellan Pierre Clairambault Peter Dybjer
+ PDF Chat	The biequivalence of locally cartesian closed categories and Martin-Löf type theories	2014	Pierre Clairambault Peter Dybjer
+	Homotopy Type Theory: Univalent Foundations of Mathematics	2013	Peter Aczel Benedikt Ahrens Thorsten Altenkirch Steve Awodey Bruno Barras Andrej Bauer Yves Bertot Marc Bezem Thierry Coquand Eric Finster
+ PDF Chat	The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories	2011	Pierre Clairambault Peter Dybjer
+	Normalization by Evaluation for Martin-Löf Type Theory with One Universe	2007	Andreas Abel Klaus Aehlig Peter Dybjer
+	Normalization and the Yoneda embedding	1998	Djordje Čubrić Peter Dybjer Philip Scott
+	Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids	1996	Ilya Beylin Peter Dybjer
+	Internal type theory	1996	Peter Dybjer
+	Extracting a proof of coherence for monoidal categories from a formal proof of normalization for monoids	1996	Peter Dybjer Ilya Beylin

Common Coauthors

Coauthor	Papers Together
Pierre Clairambault	7
Simon Castellan	5
Martı́n Hötzel Escardó	3
Marc Bezem	3
Thierry Coquand	3
Ilya Beylin	2
Philip Scott	2
Daniel R. Licata	1
Daniel R. Grayson	1
Yves Bertot	1
Hugo Moeneclaey	1
Nicolai Kraus	1
Peter LeFanu Lumsdaine	1
Emily Riehl	1
Robert Harper	1
Pieter Hofstra	1
Joachim Koch	1
Anthony Bordg	1
Andrew Polonsky	1
Sergey A. Melikhov	1
Benno van den Berg	1
Bas Spitters	1
Erik Palmgren	1
Richard Garner	1
Steve Awodey	1
Nicola Gambino	1
Peter Aczel	1
Klaus Aehlig	1
Thorsten Altenkirch	1
Michael Nahas	1
Vladimir Voevodsky	1
Hugo Herbelin	1
Kuen-Bang Hou	1
Matthieu Sozeau	1
Michael Shulman	1
Álvaro Pelayo	1
Andrej Bauer	1
André Joyal	1
Georges Gonthier	1
Guillaume Brunerie	1
Carlo Angiuli	1
Kristina Sojakova	1
Djordje Čubrić	1
Egbert Rijke	1
Zhaohui Luo	1
Nuo Li	1
Martin Hofmann	1
Michael A. Warren	1
Robert L. Constable	1
Cyril Cohen	1

Commonly Cited References

Action	Title	Year	Authors	# of times referenced
+	On the interpretation of type theory in locally cartesian closed categories	1995	Martin Hofmann	5
+	Internal type theory	1996	Peter Dybjer	4
+	Locally cartesian closed categories and type theory	1984	R. A. G. Seely	4
+	Fibered categories and the foundations of naive category theory	1985	Jean Bénabou	3
+	Extensional concepts in intensional type theory	1995	Martin Hofmann	3
+	Basic Bicategories	1998	Tom Leinster	2
+	Coherence for tricategories	1995	Robert J. Gordon John Power Ross Street	2
+	Undecidability of Equality in the Free Locally Cartesian Closed Category (Extended version)	2015	Simon Castellan Pierre Clairambault Peter Dybjer	2
+ PDF Chat	The biequivalence of locally cartesian closed categories and Martin-Löf type theories	2014	Pierre Clairambault Peter Dybjer	2
+ PDF Chat	Categories for the Working Mathematician	1971	Saunders Mac Lane	2
+ PDF Chat	The Local Universes Model: An Overlooked Coherence Construction for Dependent Type Theories	2015	Peter LeFanu Lumsdaine Michael A. Warren	1
+	A model for the homotopy theory of homotopy theory	2000	Charles Rezk	1
+	Partial Horn logic and cartesian categories	2006	Erik Palmgren Steve Vickers	1
+ PDF Chat	Inductive Types in Homotopy Type Theory	2012	Steve Awodey Nicola Gambino Kristina Sojakova	1
+	Wellfounded trees in categories	2000	Ieke Moerdijk Erik Palmgren	1
+	Semi-abelian categories	2002	George Janelidze L. Márki Walter Tholen	1
+ PDF Chat	Axiom of choice and complementation	1975	Radu Diaconescu	1
+	Weak ω-Categories from Intensional Type Theory	2009	Peter LeFanu Lumsdaine	1
+	Metric spaces, generalized logic, and closed categories	1973	F. William Lawvere	1
+	Braided Tensor Categories	1993	André Joyal Ross Street	1
+	On the Structure of Abstract Algebras	1935	Garrett Birkhoff	1
+ PDF Chat	Higher Inductive Types as Homotopy-Initial Algebras	2014	Kristina Sojakova	1
+ PDF Chat	Calculating the Fundamental Group of the Circle in Homotopy Type Theory	2013	Daniel R. Licata Michael Shulman	1
+	Real numbers and other completions	2008	Fred Richman	1
+ PDF Chat	The fundamental theorem of algebra: a constructive development without choice	2000	Fred Richman	1
+	Some free constructions in realizability and proof theory	1995	A. Carboni	1
+	A constructive and functorial embedding of locally compact metric spaces into locales	2007	Erik Palmgren	1
+	Embedding of a free cartesian-closed category into the category of sets	1998	Djordje Čubrić	1
+	Homotopy Theoretic Aspects of Constructive Type Theory	2008	Michael A. Warren	1
+ PDF Chat	Extensional equality in intensional type theory	2003	Thorsten Altenkirch	1
+	Revisiting the categorical interpretation of dependent type theory	2014	Pierre-Louis Curien Richard Garner Martin Hofmann	1
+ PDF Chat	Type theories, toposes and constructive set theory: predicative aspects of AST	2002	Ieke Moerdijk Erik Palmgren	1
+	Setoids and universes	2010	Olov Wilander	1
+	THE SIMPLICIAL MODEL OF UNIVALENT FOUNDATIONS	2014	Krzysztof Kapulkin Peter LeFanu Lumsdaine Vladimir Voevodsky	1
+	A general coherence result	1989	John Power	1
+ PDF Chat	On the strength of dependent products in the type theory of Martin-Löf	2009	Richard Garner	1
+	Extracting a proof of coherence for monoidal categories from a formal proof of normalization for monoids	1996	Peter Dybjer Ilya Beylin	1
+	Stack completions and Morita equivalence for categories in a topos	1979	Marta Bunge	1
+ PDF Chat	Constructing quotient inductive-inductive types	2019	Ambrus Kaposi András Kovács Thorsten Altenkirch	1
+	Algebraic Models of Dependent Type Theory	2018	Clive Newstead	1
+	Categorical structures for type theory in univalent foundations	2017	Benedikt Ahrens Peter LeFanu Lumsdaine Vladimir Voevodsky	1
+	Constructivist and Structuralist Foundations: Bishop's and Lawvere's Theories of Sets	2012	Erik Palmgren	1
+ PDF Chat	Natural models of homotopy type theory	2016	Steve Awodey	1
+	Impredicative Encodings of (Higher) Inductive Types	2018	Steve Awodey Jonas Frey Sam Speight	1
+	POLYNOMIALS IN CATEGORIES WITH PULLBACKS	2015	Mark Weber	1
+	Algebraic topology	2001	Allen Hatcher	1
+ PDF Chat	Types are weak <i>ω</i> -groupoids	2010	Benno van den Berg Richard Garner	1
+ PDF Chat	Homotopy theoretic models of identity types	2008	Steve Awodey Michael A. Warren	1
+	An intuitionistic theory of types	1998	Per Martin‐Löf	1
+ PDF Chat	Quantum Gauge Field Theory in Cohesive Homotopy Type Theory	2014	Urs Schreiber Michael Shulman	1