<div dir='auto'>Consider, for example, the Agda type <div dir="auto"><br></div><div dir="auto">   (I j : Level) -> Set i -> Set j -> Set(i\/j)</div><div dir="auto"><br></div><div dir="auto">e.g. for the sum of two types.</div><div dir="auto"><br></div><div dir="auto">I would like to, alternatively, write this type as follows:</div><div dir="auto"><br></div><div dir="auto">  (U V : Universe) -> U -> V -> U \/ V</div><div dir="auto"><br></div><div dir="auto">Instead of thinking of universe levels, I am thinking of universes themselves.</div><div dir="auto"><br></div><div dir="auto">So then U \/ V is the least universe containing both U and V.</div><div dir="auto"><br></div><div dir="auto">In particular, this notation works well with for example univalent type theory as in the HoTT book.</div><div dir="auto"><br></div><div dir="auto">This should not only make some definitions more concise and readable, but also mathematically more intuitive.</div><div dir="auto"><br></div><div dir="auto">There are two pieces of notation missing in this proposal, for the first universe and for the successor of a universe. </div><div dir="auto"><br></div><div dir="auto">I would like Agda to allow me to think and write in this way.</div><div dir="auto"><br></div><div dir="auto">Best, Martin</div></div>