The slides from the talk “Spartan type theory”, given at the School and Workshop on Univalent Mathematics.

**Download slides with speaker notes: Spartan Type Theory [PDF]**

The slides from the talk “Spartan type theory”, given at the School and Workshop on Univalent Mathematics.

**Download slides with speaker notes: Spartan Type Theory [PDF]**

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)

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

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).

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.