nLab Daniel Gratzer

• personal page

Selected works

On the principles of dependent type theory

• Carlo Angiuli, Daniel Gratzer, Principles of Dependent Type Theory (pdf)

On categorical models of dependent types via locally Cartesian closed categories:

• Daniel Gratzer, Jonathan Sterling, Syntactic categories for dependent type theory: sketching and adequacy [arXiv:2012.10783]

On modal type theory:

• Daniel Gratzer, G. Alex Kavvos, Andreas Nuyts, Lars Birkedal: Multimodal Dependent Type Theory, Logical Methods in Computer Science 17 3 (2021) lmcs:7713 [arXiv:2011.15021, doi:10.46298/lmcs-17(3:11)2021]

• Daniel Gratzer, Implementing Modal Dependent Type Theory, talk at ICFP 19 (slides pdf)

• Daniel Gratzer, Syntax and semantics of modal type theory, PhD Aarhus (2023) [pdf]

On XTT:

• Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, Cubical syntax for reflection-free extensional equality. In Herman Geuvers (ed.), 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:25. (arXiv:1904.08562, doi:10.4230/LIPIcs.FCSD.2019.31)

• Jonathan Sterling, Carlo Angiuli, Daniel Gratzer, A Cubical Language for Bishop Sets, Logical Methods in Computer Science, 18 (1), 2022. (arXiv:2003.01491).

On the independence of the continuum hypothesis from ZFC via forcing in topos theory:

• Daniel Gratzer: On The Independence of the Continuum Hypothesis (2019) [pdf, pdf]

On simplicial type theory:

• Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, Directed univalence in simplicial homotopy type theory (arXiv:2407.09146)

• Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz, The Yoneda embedding in simplicial type theory (arXiv:2501.13229)

On the category of Peter Aczel‘s iterative sets in homotopy type theory:

• Daniel Gratzer, Håkon Gylterud, Anders Mörtberg, Elisabeth Stenholm, The Category of Iterative Sets in Homotopy Type Theory and Univalent Foundations, Mathematical Structures in Computer Science 34 Special Issue 9: Advances in Homotopy type theory (2024) 945-970 [doi:10.1017/S0960129524000288, arXiv:2402.04893]

category: people