1. 5

The repository for this video is at https://github.com/andrejbauer/spartan-type-theory

  1. 2

    I like these “mini” type systems (e.g. also LambdaPi) but they always assume Type : Type. That’s reasonable for human experimenters (i.e. don’t do Russell’s paradox and you should be fine), but I’d like to use them as a playground for AI algorithms, and I fear that this inconsistency would cause the whole thing to collapse :(

    My currently preferred solution is cumulative universes, but that requires extra checks (like how Coq checks universe constraints). I’ve not seen a “toy” example of this anywhere, and fear I’d mess it up if I tried myself ;)