ULift
creates small (co)limits #
This file shows that uliftFunctor.{v, u}
creates (and hence preserves) limits and colimits indexed
by J
with [Category.{u, u} J]
.
It also shows that uliftFunctor.{v, u}
preserves "all" limits (i.e. of size max u v
,
potentially too big to exist in Type u
).
The equivalence between the ulift of the explicit limit cone of a functor K
and the explicit limit
cone of K ⋙ uliftFunctor
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The functor uliftFunctor : Type u ⥤ Type (max u v)
creates u
-small limits.
Equations
- CategoryTheory.Limits.Types.instCreatesLimitsOfSizeTypeTypesTypeTypesUliftFunctor = CategoryTheory.CreatesLimitsOfSize.mk
The equivalence between K.sections
and (K ⋙ uliftFunctor.{v, u}).sections
. This is used to show
that uliftFunctor
preserves limits that are too possibly too large to exist in the source
category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The functor uliftFunctor : Type u ⥤ Type (max u v)
preserves limits.
Equations
- CategoryTheory.Limits.Types.instPreservesLimitsTypeTypesTypeTypesUliftFunctor = CategoryTheory.Limits.PreservesLimitsOfSize.mk
The equivalence between the ulift of the explicit colimit cocone of a functor K
and the explicit
colimit cocone of K ⋙ uliftFunctor
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The functor uliftFunctor : Type u ⥤ Type (max u v)
creates u
-small colimits.
Equations
- CategoryTheory.Limits.Types.instCreatesColimitsOfSizeTypeTypesTypeTypesUliftFunctor = CategoryTheory.CreatesColimitsOfSize.mk