×
Author ID: kraus.nicolai Recent zbMATH articles by "Kraus, Nicolai"
Published as: Kraus, Nicolai
Homepage: http://www.cs.nott.ac.uk/~psznk/
External Links: ORCID · Google Scholar · dblp

Publications by Year

Citations contained in zbMATH Open

13 Publications have been cited 59 times in 37 Documents Cited by Year
Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002
The Univalent Foundations Program
129
2013
Partiality, revisited. The partiality monad as a quotient inductive-inductive type. Zbl 1486.68036
Altenkirch, Thorsten; Danielsson, Nils Anders; Kraus, Nicolai
12
2017
Quotient inductive-inductive types. Zbl 1506.03063
Altenkirch, Thorsten; Capriotti, Paolo; Dijkstra, Gabe; Kraus, Nicolai; Nordvall Forsberg, Fredrik
11
2018
Extending homotopy type theory with strict equality. Zbl 1370.03014
Altenkirch, Thorsten; Capriotti, Paolo; Kraus, Nicolai
7
2016
Constructions with non-recursive higher inductive types. Zbl 1394.03010
Kraus, Nicolai
5
2016
Notions of anonymous existence in Martin-Löf type theory. Zbl 1377.03005
Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten
5
2017
Higher homotopies in a hierarchy of univalent universes. Zbl 1354.03100
Kraus, Nicolai; Sattler, Christian
4
2015
Generalizations of Hedberg’s theorem. Zbl 1433.03032
Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten
4
2013
Free higher groups in homotopy type theory. Zbl 1453.03003
Kraus, Nicolai; Altenkirch, Thorsten
4
2018
The general universal property of the propositional truncation. Zbl 1434.03150
Kraus, Nicolai
3
2015
Coherence via well-foundedness. Taming set-quotients in homotopy type theory. Zbl 1498.03033
Kraus, Nicolai; von Raumer, Jakob
2
2020
Functions out of higher truncations. Zbl 1373.03011
Capriotti, Paolo; Kraus, Nicolai; Vezzosi, Andrea
1
2015
Connecting constructive notions of ordinals in homotopy type theory. Zbl 07724243
Kraus, Nicolai; Nordvall, Forsberg Fredrik; Xu, Chuangjie
1
2021
Connecting constructive notions of ordinals in homotopy type theory. Zbl 07724243
Kraus, Nicolai; Nordvall, Forsberg Fredrik; Xu, Chuangjie
1
2021
Coherence via well-foundedness. Taming set-quotients in homotopy type theory. Zbl 1498.03033
Kraus, Nicolai; von Raumer, Jakob
2
2020
Quotient inductive-inductive types. Zbl 1506.03063
Altenkirch, Thorsten; Capriotti, Paolo; Dijkstra, Gabe; Kraus, Nicolai; Nordvall Forsberg, Fredrik
11
2018
Free higher groups in homotopy type theory. Zbl 1453.03003
Kraus, Nicolai; Altenkirch, Thorsten
4
2018
Partiality, revisited. The partiality monad as a quotient inductive-inductive type. Zbl 1486.68036
Altenkirch, Thorsten; Danielsson, Nils Anders; Kraus, Nicolai
12
2017
Notions of anonymous existence in Martin-Löf type theory. Zbl 1377.03005
Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten
5
2017
Extending homotopy type theory with strict equality. Zbl 1370.03014
Altenkirch, Thorsten; Capriotti, Paolo; Kraus, Nicolai
7
2016
Constructions with non-recursive higher inductive types. Zbl 1394.03010
Kraus, Nicolai
5
2016
Higher homotopies in a hierarchy of univalent universes. Zbl 1354.03100
Kraus, Nicolai; Sattler, Christian
4
2015
The general universal property of the propositional truncation. Zbl 1434.03150
Kraus, Nicolai
3
2015
Functions out of higher truncations. Zbl 1373.03011
Capriotti, Paolo; Kraus, Nicolai; Vezzosi, Andrea
1
2015
Homotopy type theory. Univalent foundations of mathematics. Zbl 1298.03002
The Univalent Foundations Program
129
2013
Generalizations of Hedberg’s theorem. Zbl 1433.03032
Kraus, Nicolai; Escardó, Martín; Coquand, Thierry; Altenkirch, Thorsten
4
2013

Citations by Year