Various universe constructions in Agda
root
This repository contains definitions of several sorts of type theoretic universes, with explanations and some references. It's unlikely to be useful directly for anything practical, but it may serve as a reference for people trying to understand some of the theory behind universes.
To proceed as far as complexity goes, the recommended reading order would be:
Universe.Simple
Universe.Grothendieck
Universe.Super
Universe.Mahlo
Universe.Super.Autonomous