Hello, thank you for posting these interesting slides.

Is there a typo on page 30? Should the last equation read:

ind_nat P e f (S n) = f n (ind_nat P e f n)

What's spartan about all this? I'm kind of curious now.

You'll have to ask Benedikt Ahrens. I think he was looking for a word that meant "no bells and whistles" (such as univalence, propositional resizing and other fancy stuff).

Yes, thank you, I fixed it (as well as a couple of other typos).

If "bells and whistles" is replaced by "smells and bells" (as in incense), then one would have a non-catholic type theory. There is something reminiscent of transubstantiation about the identity type.

Of course one could have Austerity Type Theory, the competition to which is the Magic Axiom Tree type theory.

I see you changed your tobacco for something more potent.

Nice. Are any of the other talks available? Either in PDF form like here, or as a video or something? Just bare slides work too but I love that you included what you actually said along with the slides. Makes them far more penetrable.

Also, I tried out Lean in the past and at least roughly got the hang of it. Its tutorial really helped with that. Is there anything similar for Coq? - It looks somewhat similar but not quite similar enough to jump right in from just knowing (very basic) Lean. Lean's tutorial was basically learning by doing style, walking you through super simple basic logical constructions, giving you various simple things to prove while introducing new syntax as it becomes necessary, first showing a few examples for each, which you could also modify interactively and quickly see how the type system responds to each change.