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.EssSurj CategoryTheory.uliftFunctor.{u, v} ) : UnivLE.{max u v, v}

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

Equations

• ⋯ = ⋯

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

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

Equations

• instIsEquivalenceTypeTypesTypeTypesUliftFunctor = CategoryTheory.Equivalence.ofFullyFaithfullyEssSurj CategoryTheory.uliftFunctor.{u, v}

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

Equations

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

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

Equations

• ⋯ = ⋯

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

Equations

• One or more equations did not get rendered due to their size.