Underlying Type Theory
It’s not entirely sustainable to claim that Epigram’s underlying theory is exactly Luo’s UTT, what with funny η-rules popping out of the woodwork. Perhaps we need a new name. Being naturally hostile to acronyms, but enjoying suggestive combinations of sounds, I propose ‘Grut’.