Universe inequalities and essential surjectivity of uliftFunctor
. #
We show UnivLE.{u, v} ↔ EssSurj (uliftFunctor.{u, v} : Type v ⥤ Type max u v)
.
instance
instFaithfulTypeTypesTypeTypesWitnessType
[UnivLE.{u, v} ]
:
CategoryTheory.Faithful UnivLE.witness