kmill
commented
2 years ago Thanks, nice to hear that diagram has been useful.
Terminology history note for maintainers: "degree" comes from Automath, where universes/types/terms respectively have degrees 1, 2, and 3. (One complication, though, is that there was a version of Automath with proof irrelevance where, effectively, Prop/propositions/proofs respectively had degrees 2, 3, and 4, so it's not a perfect correspondence, but this degree shift might have been more of an implementation hack.)
@kmill drew a very nice little diagram that was basically this for someone on Zulip a while ago, and people seemed to get a lot out of it. It crossed my mind earlier today and I thought it might be helpful here as well.