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

Equations

• ⋯ = ⋯

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

Equations

• instIsEquivalenceUliftFunctorOfUnivLE = CategoryTheory.Functor.IsEquivalence.ofFullyFaithfullyEssSurj CategoryTheory.uliftFunctor.{u, v}

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

Equations

• UnivLE.witness = CategoryTheory.uliftFunctor.{v, u} .comp CategoryTheory.uliftFunctor.{u, v} .inv

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯