6 thoughts on “Spartan type theory

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

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

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

Leave a Reply to Arnaud Spiwack Cancel reply

Your email address will not be published. Required fields are marked *