Universe inequalities and essential surjectivity of uliftFunctor.

We show UnivLE.{u, v} ↔ EssSurj (uliftFunctor.{u, v} : Type v ⥤ Type max u v).

theorem UnivLE.ofEssSurj (w : CategoryTheory.EssSurj CategoryTheory.uliftFunctor.{u, v} ) : UnivLE.{u, v}

instance instEssSurjTypeTypeTypesTypesUliftFunctor [UnivLE.{u, v} ] : CategoryTheory.EssSurj CategoryTheory.uliftFunctor.{u, v}

theorem UnivLE_iff_essSurj : UnivLE.{u, v} ↔ CategoryTheory.EssSurj CategoryTheory.uliftFunctor.{u, v}

instance instIsEquivalenceTypeTypesTypeTypesUliftFunctor [UnivLE.{u, v} ] : CategoryTheory.IsEquivalence CategoryTheory.uliftFunctor.{u, v}

def UnivLE.witness [UnivLE.{u, v} ] : CategoryTheory.Functor (Type u) (Type v)

instance instFaithfulTypeTypesTypeTypesWitnessType [UnivLE.{u, v} ] : CategoryTheory.Faithful UnivLE.witness

instance instFullTypeTypesTypeTypesWitnessType [UnivLE.{u, v} ] : CategoryTheory.Full UnivLE.witness