Mathematics and Computation

A blog about mathematics for computers

Spartan type theory

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]

Comments

Anonymous

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)

Arnaud Spiwack

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

Peter Hancock

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.

Kram1032

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.

Post a comment:
Write your comment using Markdown. Use $⋯$ for inline and $$⋯$$ for display LaTeX formulas, and <pre>⋯</pre> for display code. Your E-mail address is only used to compute your Gravatar and is not stored anywhere. Comments are moderated through pull requests.

Name

E-mail

Website

Comment