Could someone point me to some formal presentation of Agda's universe polymorphism, ideally an article somewhere with soundness proof or something like that. Stefan