daniel gratzer

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

Public Key

npub1p6adh0fwyx6303tm7amv3sjv2nzn9ak0umwtd7n39lvq0rqhdj7slkevjm

NIP-05 Address

danielgratzer@mathstodon-xyz.mostr.pub

Profile Code

nprofile1qqsqawkmh5hzrdghc4alwakgcfx9f3fj7m87dh9klfcjlkq83stke0gpz3mhxue69uhhyetvv9ujuerpd46hxtnfduqs6amnwvaz7tmwdaejumr0dsm5vkv5

Publishing to

relay.damus.io

nos.lol

Author Public Key

npub1p6adh0fwyx6303tm7amv3sjv2nzn9ak0umwtd7n39lvq0rqhdj7slkevjm

Show more details

Last Notes

2026-01-26 14:35:12 UTC

First CfC for HoTT/UF is out! The relevant material is also on the website (https://hott-uf.github.io/2026/)
Deadline for submissions is March 27, and I hope to see some of you in Aarhus this June! :)

2025-12-23 12:27:58 UTC

- reply

@nprofile…rrqe Yes, this got revised at some point if I recall... I think it's basically because he needs this case sooner for various lifting arguments if I recall.

2025-12-23 12:24:37 UTC

- reply

@nprofile…rrqe Oh yeah that sucks. Also Lurie for some reason _never_ uses the right adjoint to pullback explicitly. No clue why 🤷

2025-12-23 12:23:51 UTC

- reply

@nprofile…rrqe It gets better as you go---later arguments are more abstract than earlier ones, but generally because they refer to those earlier chapters :)
[PS: What part are you at?]

2025-12-15 16:15:14 UTC

- reply

@nprofile…rrqe which unfortunately this toot is too small to contain.

2025-12-09 12:38:43 UTC

Controlling unfolding in type theory has now been published 🎉
https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/article/controlling-unfolding-in-type-theory/A2865261D18E29153AB7B0F2E89BA8C8

2025-12-08 21:17:20 UTC

- reply

@nprofile…dand Still a bit more polishing before releasing it I think... the topic is sort of subtle enough that we want to avoid confusing things further with an incoherent first draft :D
However, soon, I hope!

2025-12-08 18:11:07 UTC

First draft of the LF/GATs appendix is done! Stitches together some of the wonderful work done by
1. Kaposi, Kovacs, and Altenkirch (POPL, 2019)
2. Castellan, Clairambault, and Dybjer (LMCS, 2017)
3. Bezem, Coquand, Dybjer, and Escardo (2022)
The story is both more complex than I had initially thought, but cleaner than I had feared. It ended up being 22p in draft form; not a bad outcome overall.

2025-12-03 12:55:38 UTC

Sigma.
https://media.mathstodon.xyz/media_attachments/files/115/655/737/765/909/626/original/6cb88a3472ab38fc.png

2025-11-27 13:22:43 UTC

- reply

@nprofile…dand OK, well a moment's glance more: they acknowledge the use of AI (good! though not in writing, which I'm still suspicious of). However, they just straight up postulate univalence which is inconsistent in Lean. So uh. yeah, this is indeed going to be a very powerful framework for homotopy theory. Perhaps a smidge too powerful.
https://github.com/Arthur742Ramos/ComputationalPathsLean/blob/324ecc421fab12978e913e583135b7d8d9e470b3/ComputationalPaths/Path/Basic/Univalence.lean#L24

2025-11-27 13:09:17 UTC

- reply

@nprofile…dand Very suspicious of the fact that (1) the report has these extremely regular hierarchical sections, often with no filler text between Sec N and subsec N.1 (2) it is very unclear what novel thing they're doing and (3) all the commits in the repo are by an OpenAI code writing agent.
Signs point to maybe this is AI written, bluntly.

2025-11-25 20:46:53 UTC

- reply

@nprofile…rrqe My most extreme example (though with SML) was a student who only compiled/tested their code by submitting to the autograder. Witnessing this in office hours hurt my soul a bit.

2025-11-18 09:50:01 UTC

- reply

@nprofile…rrqe @nprofile…9l0g This should work I think; you are essentially taking the free coproduct completion and then forcing the adjoined initial object to be the existing one. So y : C --> C+ should be universal among categories D with finite coproducts and a map F : C --> D which preserves the initial object. At least, that's a sensible universal property to describe what Reed asked for I think.

2025-11-12 14:27:32 UTC

- reply

@nprofile…rrqe @nprofile…8pq6 I also think there's something to be said for making mathematical precise claims and explicitly stating they will not be proven. However, I think it's also very frustrating to have (1) an imprecise claim (2) no hope of a proof.
For instance, pausing to point out open problems or recent results can be very inspiring, especially since you can say "see, now you can actually glimpse the frontier of research".

2025-11-12 14:13:34 UTC

Time to update my bibtex entry for @nprofile…356e's book! Wonderful to see this in print!

2025-11-11 17:52:48 UTC

- reply

@nprofile…ral2 Dumb question but... how often does Grothendieck completion occurs vs Grothendieck construction? Given that both occur in this screenshot I wonder if it's just a typo?

2025-11-10 12:38:22 UTC

- reply

@nprofile…w8t5 @nprofile…kag9 I suspected that it must be somewhere in TypeTopology! I also like that your version does not require impredicativity by allowing the sets one chooses from to belong to a different universe than the universe of propositions the predicate draws from.

2025-11-10 12:22:33 UTC

In a conversation with @nprofile…kag9, we had occasion to go through Diaconescu's argument that choice implies excluded middle and translate it to type theory. It's quite a subtle argument!
Let us work within type theory with an impredicative universe of propositions \(\Omega\) which satisfies proposition univalence/propositional extensionality. We wish to show that \(P \lor \neg P\) holds for some \(P : \Omega\). To this end, let us fix two predicates \(U,V : 2 \to \Omega\) given by \(- = 0 \lor P\) and \(- = 1 \lor P\) respectively. Consider now the type
\(
X = \sum_{\phi : 2 \to \Omega} (\phi = U \lor \phi = V)
\)
We can prove that for all \(\phi : X\) that there exists \(b : 2\) such that \(\phi(b)\) holds. Consequently, using choice, we have a function \(f : X \to 2\) such that for all \(\phi : X\), we have \(\phi(f(\phi))\). Since \(2\) admits decidable equality, we have \(\phi(U) = \phi(V) \lor \phi(U) \neq \phi(V)\). If the first branch holds, then \(P\) holds: \(U\) and \(V\) only have a common element when \(P\) is true. Moreover, if \(\phi(U) \neq \phi(V)\) holds, then we must have \(U \neq V\) (functions respect equality) and so, by propositional univalence, we must know that \(U\) and \(V\) are not interprovable and so \(P\) must not hold. Thus, \(P \lor \neg P\).

2025-11-03 16:36:41 UTC

- reply

@nprofile…w8t5 @nprofile…n7dy HOAS is perfectly compatible with funext provided one works in the correct setting, akin to how one may use nominal sets to reason about binding via exponentiation by the type of names.

2025-10-26 11:44:57 UTC

Ah, the fun week where clocks in Europe have changed, but not in the US. This will make every research meeting this week totally impossible to plan properly in my experience.

2025-10-22 20:50:09 UTC

- reply

@nprofile…dand Ooph... didn't know about this one. That's... a bit painful.

2025-10-15 21:01:09 UTC

- reply

@nprofile…w8t5 Indeed... I think a measure of how closely a foundation matches our idealized mathematics/reasoning is how large a ratio one can have of users of system : scholars of system.
Proof assistants for various type theories are certainly increasing this number for MLTT... The alternative approach to maximizing this number seems to be to carry out a decades-long program to convince mathematicians they are secretly using your foundation already :)

2025-09-29 22:01:22 UTC

Oh god, Lurie reversed the definition of twisted arrow category between Kerodon and Higher Algebra...
In HA it's the right fibration version and in Kerodon it's the left fibration version. One is sent to the other by the op functor on simplicial sets. Well uh... that explains why all of my computations were yielding results backwards from what I expected.
This one hurts more than the fact that Kerodon vs Higher Algebra also switches the meanings of left and right cofinal.

2025-06-20 10:10:56 UTC

- reply

@nprofile…6kk0 The first chapter in particular is very nice... the later chapters kind of go in a specific direction which I haven't found as useful.

2025-06-10 11:45:41 UTC

- reply

@nprofile…6kk0 "when the paragraph is not perfectly rectangular"

2025-06-04 10:17:24 UTC

- reply

@nprofile…6kk0 Honestly... not a bad endorsement in terms of not worrying about it a bunch...

2025-06-04 10:07:48 UTC

My left wrist has been bugging me more and more lately and I'm starting to lay some of the blame at emacs's feet.
What's it like using vim or vscode for editing latex nowadays? Do people have other cool editors that are worth investigating?

2025-05-26 15:19:09 UTC

- reply

@nprofile…6kk0 @nprofile…aym3 Similar but with Wells Fargo. However, I have the advantage of branches near family members with linked accounts.

2025-05-26 14:54:06 UTC

- reply

@nprofile…6kk0 @nprofile…aym3 There are already banks without physical locations!! In those cases, I'd assume that one can call a phone number etc etc but already the solution of "I will go to physical location and talk to a human being" is not viable for many people

2025-05-26 12:29:45 UTC

- reply

@nprofile…6kk0 Was just discussing with a friend: if I lost my phone while traveling, I'd be unable to access my bank account or to make purchases online, as both require mitid authentication. Same with booking a doctor, viewing government communication, or dealing with essentially any government website

2025-05-26 12:27:25 UTC

- reply

@nprofile…6kk0 C.f., "bespoke hardware for this auth app" :/ The documentation for mitid is also insane from this perspective:
> Make sure you have a backup device with mitid installed in case you lose your main device.
> Don't have access to a spare phone? Consider using (1) your work phone or (2) your family member's spare phone

2025-05-26 12:16:58 UTC

- reply

@nprofile…6kk0 that went away several years ago... I loved that approach honestly.

2025-05-26 11:45:54 UTC

Mild vent: I just received a mail that after August I won't be able to use mitid (Danish auth app) on my phone, as apparently it's too old. The advice is "get a new phone" or "switch to bespoke device that does not work".
Frustrating that for this (and a few other instances of the same situation) I'm very strongly considering replacing my perfectly functional phone a newer one.

2025-05-01 09:51:22 UTC

@nprofile…tphs and I just pushed an update to "Principles of Dependent Type Theory" (https://www.danielgratzer.com/papers/type-theory-book.pdf).
Summary:
- Draft of first 5 sections of Chapter 6 dealing with models of type theory
- Improvements to 2.8 (Propositions in ETT)
- Numerous typo fixes/small improvements
The approach in Chapter 6 is still very provisional and subject to change, but the current plan is roughly to develop the model theory of type theory as discussed in Chapter 3 categorically and to give some indications as to its use.
As always, comments welcome!

2025-04-29 12:10:38 UTC

Preparing for a new update on the book draft and I think I have now rewritten Section 5.3 four separate times and Carlo and I have now "rewritten" it out of existence and into a short remark in Chapter 6.
I know this is how writing progresses but ugh, wasted effort.

2025-04-24 16:18:45 UTC

- reply

Sorry I miscounted: the expected number of people tomorrow (again, to watch kayak/drink-racing across a pond <1.5m deep) is 30,000 people.
(Also, you might think this is an age-old tradition that has carried forwards for 200 years. Nope, it's from the 90s.)

2025-04-24 16:11:15 UTC

Tomorrow is the day of the year where literally thousands of people pile into the university park and consume ungodly amounts of alcohol. This is ostensibly to watch people paddle across a small pond in a kayak, drink a beer, spin around ten times, then paddle back.
This is the main day where I remember that I really enjoy living in Denmark but oh my god I am not a Dane.

2025-04-14 11:21:00 UTC

Small observation to share: in the context of simplicial type theory, I was wondering about the h-level of the various axioms we impose. In particular, while assuming "some bounded-distributive lattice 𝕀" is clearly not an hprop, what about the rest?
It turns out that the duality axiom (called synthetic quasicoherence by Blechschmidt) actually implies that a number of a priori non-hprop axioms are actually props!
Take, for instance, the axiom stating roughly that \(\mathbb{I} \cong \mathbb{I}^{\mathsf{op}}\). A priori, there could be many such equivalences \(\mathbb{I}\) is an set. However, since by duality we know that \(\mathbb{I}\) has no non-trivial automorphisms, we can actually argue that there can only be at most one such isomorphism (if we are given two \(\alpha_0,\alpha_1\) then we can argue that \(\alpha_1^{-1} \circ \alpha_0 = \mathsf{id}\)).
Why does this matter? Well, it tells us that our axioms can (and do) miss a lot of the peculiarities of simplicial spaces, but at least they don't accidentally miss out on coherences.

2025-04-12 13:32:50 UTC

- reply

@nprofile…6kk0 Better term: I shall refer to the colimit-y ones as "cool" and the limit-y ones as "sick"

2025-04-12 13:30:31 UTC

- reply

@nprofile…6kk0 Yeah, this is the HTT approach. It's not totally great (it's weird seeing statements in proofs that deal only with f that discuss "f^op being cofinal") but it's easy to remember and matches my expectations from order theory.

2025-04-12 13:27:07 UTC

- reply

@nprofile…6kk0 I would be inclined to agree but it's really used *all the time* in oo-categorical proofs. It's so frequent that terminology for at least one direction is necessary (in the paper I'm reading now, something like 8 proofs in a row use various reductions of colimits using cofinal functors)

2025-04-12 13:23:31 UTC

- reply

@nprofile…6kk0 This is a worthy goal... I've sort of given up on this hope for terminology with oo-categories 😅
This thought process is brought, however, by revisiting what we should call these things in our LICS paper. Currently we use the Kerodon terminology, but 2 reviewers independently suggested Joyal's terminology.

2025-04-12 13:20:18 UTC

- reply

@nprofile…6kk0 final/initial are usually pretty easy to remember by reminding oneself that "the inclusion of the terminal object is final" and "the inclusion of the initial object is initial". One then can do a quick sanity check to see how these ought to behave with respect to (co)limits by considering the (co)limit of F : {0 -> 1} --> C.

2025-04-12 13:09:43 UTC

Terminology I've encountered for "functors f : C -> D such that colim{D} = colim{C} o f^*" or the dual condition with limits (as of today):
Source: colimits/limits
- HTT: cofinal/no explicit terms
- HA: left cofinal/right cofinal
- Kerodon: right cofinal/left cofinal
- Cisinski: final/cofinal
- Joyal: final/initial
- Harpaz: coinitial/initial
- Borceux: no explicit terminology (?)/final

2025-04-09 14:43:34 UTC

- reply

@nprofile…l9jz @nprofile…6kk0 Arxiv frequently hurts my feelings by noticing I've tagged my submission with `cs.LO` or something and going "Did you mean to tag this with `math.CT`".
I can't believe they've captured the soul of Reviewer 2 on my papers with this algorithm..

2025-04-09 09:12:33 UTC

Happy the paper
The Yoneda embedding in simplicial type theory
has been accepted for LICS 2025. Joint work with Jonathan Weinberger & @nprofile…unwh
A preprint is available here (https://arxiv.org/abs/2501.13229), but stay tuned for a forthcoming update with slicker proofs!

2025-04-08 16:00:38 UTC

- reply

@nprofile…6kk0 I was just revisiting this book recently for pedagogy reasons actually! There are a few chapters which I think are Pretty Much Fine. IV, V, VI cover stuff in a way I am mostly happy with. Some of the proofs are a bit tedious, but not unreasonably so. but notably the later chapters which deal with the category Topos are very brutal proofwise and the proof of Diaconescu's theorem is particularly painful

2025-03-19 14:10:10 UTC

Some nice (WIP) notes introducing infinity category theory by Rune Haugseng: https://runegha.folk.ntnu.no/naivecat_web.pdf
Notably, this integrates @nprofile…4vq9 and Christian Sattler's recent lovely proof that filtered (in fact, confluent) colimits commute with finite limits.

2025-01-29 15:54:20 UTC

- reply

@nprofile…6kk0 Perhaps something can be rigged up.

2025-01-29 15:52:58 UTC

- reply

@nprofile…6kk0 Ah excellent. Next we need a learning group and perhaps a ring of collaborators.