1. 6
  1. 1

    I brought this up a couple of weeks ago, so I might as well repeat myself: I would really like to see a “toy” implementation of type theory which is consistent (i.e. doesn’t have Type : Type), so I can throw some symbol-manipulating “exploration” AI algorithms at it and see what happens.

    1. 2

      I don’t know of any, but I’m still learning this stuff. When I start fiddling around with these small type theories I’ll try adding infinite universes and do a write up of it.