daniel gratzer

assistant professor at Aarhus University interested in (higher) category theory and (modal) type theory. he/him 🏳️‍🌈

Website: https://danielgratzer.com

Last Notes

2026-09-23 17:55:06 UTC

- reply

Chapter 3 deals with this stuff a bit! C-f for injectivity there (and see Theorem 3.5.19 for a proof that ETT lacks injective pi types)

2026-09-23 17:53:01 UTC

- reply

The lack of injective type-constructors is also pretty rough (related but distinct from lack of decidable equality). It means that a hypothetical type-checker will not only be at best a semi-decision procedure, but also require a lot of annotations if it's to be robust at all.
That said, I use ETT all the time in my work, just limited to pen-and-paper work rather than formalized in a proof assistant.

2026-04-09 11:01:15 UTC

Registration is now open for HoTT/UF 2026! Hope to see some of you in Aarhus soon 😃
See https://hott-uf.github.io/2026/ for registration details.

2026-03-15 16:32:50 UTC

Some news: the first summer school on Programming Languages, Logic, and Software Security, will be held August 10–14, 2026 in Aarhus, Denmark.
The summer school offers intensive courses by leading researchers covering foundational and applied topics at the intersection of programming languages, formal methods, and software security. It is aimed at PhD students and advanced B.Sc./M.Sc. students active in the areas of programming languages, logic, semantics, and software security.
Dates: August 10–14, 2026
Venue: Aarhus University, Aarhus, Denmark
Webpage: https://conferences.au.dk/pls
Courses and Speakers:
Bas Spitters: The Rocq proof assistant and Gen-AI Tools for Formalization of Mathematics
Lars Birkedal and Amin Timany: Higher-Order Concurrent Separation Logic
Daniel Gratzer: Introduction to Type theory
Aslan Askarov: Language-Based Security
Anders Møller: Program Analysis

2025-09-12 12:44:25 UTC

Gonna see if I can get students to read my notes carefully this way...
https://media.mathstodon.xyz/media_attachments/files/115/191/360/931/329/517/original/561da13737399428.png

2025-01-08 21:22:46 UTC

I tried to buy a new tube of toothpaste while traveling in Belgium and (not looking closely enough) bought a similarly packaged tube of denture adhesive cream.
I... lack the words to describe the emotional turmoil that resulted from me trying to brush my teeth with this.

2024-10-11 11:00:50 UTC

A preprint:
Title: Idempotent Resources in Separation Logic
Authors: myself, Mathias Adam Møller, and Lars Birkedal
An attempt to understand better what's going on with Iris' notion of "abstract resource" from a slightly more categorical/algebraic point of view. Also known as "attempt number 103458 to explain Iris to @npub1tr9…hca0".
https://www.danielgratzer.com/papers/idempotent-resources-in-separation-logic.pdf