Reduce universe variables in a number of places#1721

Merged

jdchristensen merged 10 commits intoHoTT:masterfrom jdchristensen:universevars

Feb 26, 2023

+94-91

Commits on Feb 21, 2023

Define and use const_tt to eliminate unneeded universe variables in many places
jdchristensen
committed

Commits on Feb 24, 2023

Commits on Feb 26, 2023

ReflectiveSubuniverse: get rid of a couple more universe variables and adapt other files
jdchristensen
committed