Currently we only support fixed universes `Set`, `Set1`, `Set2`, to cover more of Agda we should expand this to include universe-polymorphic functions.