Universe inequalities and essential surjectivity of uliftFunctor.

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

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

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

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

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

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

Equations

• UnivLE.witness = CategoryTheory.uliftFunctor.{?u.18, ?u.19}.comp CategoryTheory.uliftFunctor.{?u.19, ?u.18}.inv

instance instFaithfulWitness [UnivLE.{max u v, v}] : UnivLE.witness.Faithful

instance instFullWitness [UnivLE.{max u v, v}] : UnivLE.witness.Full