SU\G(𝔸)/K·U

Anthony Bordg

Follow

Generating author description...

All published works
Action Title Year Authors
+ PDF Chat Simple Type Theory is not too Simple: Grothendieck’s Schemes Without Dependent Types 2022 Anthony Bordg
Lawrence C. Paulson
Wenda Li
+ The Interpretation Lifting Theorem for C-Systems. 2021 Anthony Bordg
+ Elements of Differential Geometry in Lean: A Report for Mathematicians 2021 Anthony Bordg
Nicolò Cavalleri
+ PDF Chat A Replication Crisis in Mathematics? 2021 Anthony Bordg
+ Grothendieck's Schemes in Algebraic Geometry. 2021 Anthony Bordg
Lawrence C. Paulson
Wenda Li
+ Elements of Differential Geometry in Lean: A Report for Mathematicians 2021 Anthony Bordg
Nicolò Cavalleri
+ Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types 2021 Anthony Bordg
Lawrence C. Paulson
Wenda Li
+ PDF Chat Certified Quantum Computation in Isabelle/HOL 2020 Anthony Bordg
Hanna Lachnitt
Yijun He
+ PDF Chat On a Model Invariance Problem in Homotopy Type Theory 2019 Anthony Bordg
+ PDF Chat Univalent Foundations and the UniMath Library 2019 Anthony Bordg
+ Comment on "Quantum Games and Quantum Strategies" 2019 Anthony Bordg
Yijun He
+ The Localization of a Commutative Ring. 2018 Anthony Bordg
+ On a model invariance problem in Homotopy Type Theory 2017 Anthony Bordg
+ On the Inadequacy of the Projective Structure with Respect to the Univalence Axiom 2017 Anthony Bordg
+ From functors between categories to homomorphisms of C-systems 2017 Anthony Bordg
+ On a model invariance problem in Homotopy Type Theory 2017 Anthony Bordg
+ On the Inadequacy of the Projective Structure with Respect to the Univalence Axiom 2017 Anthony Bordg
+ The Interpretation Lifting Theorem for C-Systems 2017 Anthony Bordg
+ Modèles de l'univalence dans le cadre équivariant 2015 Anthony Bordg
+ On lifting univalence to the equivariant setting 2015 Anthony Bordg
+ 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
Common Coauthors
Coauthor Papers Together
Wenda Li 3
Lawrence C. Paulson 3
Nicolò Cavalleri 2
Yijun He 2
Per Martin‐Löf 1
Benedikt Ahrens 1
Hanna Lachnitt 1
Marc Bezem 1
Daniel R. Licata 1
Daniel R. Grayson 1
Yves Bertot 1
Nicolai Kraus 1
Peter LeFanu Lumsdaine 1
Emily Riehl 1
Robert Harper 1
Pieter Hofstra 1
Joachim Koch 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
Martı́n Hötzel Escardó 1
Peter Aczel 1
Peter Dybjer 1
Thorsten Altenkirch 1
Michael Nahas 1
Vladimir Voevodsky 1
Hugo Herbelin 1
Philip Scott 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
Egbert Rijke 1
Thierry Coquand 1
Zhaohui Luo 1
Nuo Li 1
Martin Hofmann 1
Michael A. Warren 1
Robert L. Constable 1
Commonly Cited References
Action Title Year Authors # of times referenced
+ PDF Chat Univalence for inverse diagrams and homotopy canonicity 2014 Michael Shulman
 4
+ PDF Chat The univalence axiom for elegant Reedy presheaves 2015 Michael Shulman
 4
+ On lifting univalence to the equivariant setting 2015 Anthony Bordg
 3
+ 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
 2
+ PDF Chat K(N)-local duality for finite groups and groupoids 2000 Neil Strickland
 2
+ PDF Chat AN INTRODUCTION TO QUANTUM GAME THEORY 2002 Adrian P. Flitney
Derek Abbott
 2
+ PDF Chat Comment on “Quantum Games and Quantum Strategies'' 2001 Simon C. Benjamin
Patrick Hayden
 2
+ THE SIMPLICIAL MODEL OF UNIVALENT FOUNDATIONS 2014 Krzysztof Kapulkin
Peter LeFanu Lumsdaine
Vladimir Voevodsky
 2
+ Univalence for inverse EI diagrams 2015 Michael Shulman
 2
+ The Simplicial Model of Univalent Foundations (after Voevodsky) 2012 Chris Kapulkin
Peter LeFanu Lumsdaine
 2
+ PDF Chat Lawvere theories and C-systems 2020 Marcelo Fiore
Vladimir Voevodsky
 2
+ PDF Chat Quantum Games and Quantum Strategies 1999 Jens Eisert
Martin Wilkens
Maciej Lewenstein
 2
+ A model for the homotopy theory of homotopy theory 2000 Charles Rezk
 1
+ Linear Programs for the Kepler Conjecture 2010 Thomas Hales
 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
+ PDF Chat The Mathematical Work of the 2002 Fields Medalists 2003 Eric M. Friedlander
Michael Rapoport
Andrei Suslin
 1
+ PDF Chat Axiom of choice and complementation 1975 Radu Diaconescu
 1
+ Weak ω-Categories from Intensional Type Theory 2009 Peter LeFanu Lumsdaine
 1
+ PDF Chat On proof and progress in mathematics 1994 William P. Thurston
 1
+ Metric spaces, generalized logic, and closed categories 1973 F. William Lawvere
 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
+ Homotopy Theoretic Aspects of Constructive Type Theory 2008 Michael A. Warren
 1
+ PDF Chat Extensional equality in intensional type theory 2003 Thorsten Altenkirch
 1
+ PDF Chat Advantage of a quantum player over a classical one in 2 × 2 quantum games 2003 Adrian P. Flitney
Derek Abbott
 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
+ PDF Chat An experimental library of formalized Mathematics based on the univalent foundations 2015 Vladimir Voevodsky
 1
+ PDF Chat On the strength of dependent products in the type theory of Martin-Löf 2009 Richard Garner
 1
+ PDF Chat Formalization of Quantum Protocols using Coq 2015 Jaap Boender
Florian Kammüller
Rajagopal Nagarajan
 1
+ A C-system defined by a universe category 2014 Vladimir Voevodsky
 1
+ PDF Chat Twenty-Five Years with Nicolas Bourbaki, 1949-1973 1998 Armand Borel
 1
+ Higher Topos Theory (AM-170) 2009 Jacob Lurie
 1
+ PDF Chat Congruence Closure in Intensional Type Theory 2016 Daniel Selsam
Leonardo de Moura
 1
+ ALGEBRA: (Graduate Texts in Mathematics, 73) 1982 Dan Segal
 1
+ C-systems defined by universe categories: presheaves 2017 Vladimir Voevodsky
 1
+ Stack completions and Morita equivalence for categories in a topos 1979 Marta Bunge
 1
+ PDF Chat Univalent Foundations and the UniMath Library 2019 Anthony Bordg
 1
+ On the Inadequacy of the Projective Structure with Respect to the Univalence Axiom 2017 Anthony Bordg
 1
+ PDF Chat QWIRE Practice: Formal Verification of Quantum Circuits in Coq 2018 Robert W. Rand
Jennifer Paykin
Steve Zdancewic
 1
+ PDF Chat Hilbert Meets Isabelle: Formalisation of the DPRM Theorem in Isabelle 2018 Benedikt Stock
Abhik Pal
Maria Antonia Oprea
Yufei Liu
Malte S. Haßler
Simon Dubischar
Prabhat Devkota
Yiping Deng
Marco David
Bogdan Ciurezu
 1
+ Constructivist and Structuralist Foundations: Bishop's and Lawvere's Theories of Sets 2012 Erik Palmgren
 1
+ PDF Chat Univalence for inverse EI diagrams 2017 Michael Shulman
 1
+ PDF Chat On a Model Invariance Problem in Homotopy Type Theory 2019 Anthony Bordg
 1
+ Nine Chapters of Analytic Number Theory in Isabelle/HOL. 2019 Manuel Eberl
 1
+ PDF Chat Quantum Strategies 1999 David Meyer
 1