UnivLE and cardinals

theorem univLE_iff_cardinal_le : UnivLE.{u, v} ↔ Cardinal.univ.{u, v + 1} ≤ Cardinal.univ.{v, u + 1}

theorem univLE_total : UnivLE.{u, v} ∨ UnivLE.{v, u}

Together with transitivity, this shows UnivLE "IsTotalPreorder".