univLE_total

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

This theorem states that the universal less-than-or-equal-to relation (`UnivLE`) is total on any two types `u` and `v`. In other words, for any two types `u` and `v`, either every element of `u` is less than or equal to every element of `v` (`UnivLE.{u, v}`), or every element of `v` is less than or equal to every element of `u` (`UnivLE.{v, u}`). Combined with transitivity, this makes `UnivLE` a total preorder.

More concisely: For any types `u` and `v`, the universal less-than-or-equality relation between `u` and `v` is a total preorder.