Now taking name suggestions for a type theory with Agda-ish sized types (except the stuff that make it inconsistent), Coq-ish conversion, N, W, and wonky cumulative universes
Conversation
I thought you already had a name?
Typey McType Theory
1
1
20
If this gets more than 5 likes you legally have to name your type theory that
2
7
There's probably a loophole where the theory gets named something else and then a component of the tool gets named Typey McType Theory "so the internet isn't disappointed".
2
6
gotta call it something serious and sensible like “Sir David Attenborough Type Theory” or something