Various universe constructions in Agda
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