English
For a localization setting with a universe parameter w and another universe w'', the type SmallShiftedHom^{w} W X Y m is canonically equivalent to SmallShiftedHom^{w''} W X Y m; in particular, the construction does not depend on the chosen universe.
Русский
Для локализации с параметром множества вселенных w и другой множества w'', тип SmallShiftedHom^{w} W X Y m канонически эквивалентен SmallShiftedHom^{w''} W X Y m; построение не зависит от выбранной вселенной.
LaTeX
$$$SmallShiftedHom^{w} W\; X\; Y\; m\cong SmallShiftedHom^{w''} W\; X\; Y\; m$$$
Lean4
/-- Up to an equivalence, the type `SmallShiftedHom.{w} W X Y m` does
not depend on the universe `w`. -/
noncomputable def chgUniv {X Y : C} {m : M} [HasSmallLocalizedShiftedHom.{w} W M X Y]
[HasSmallLocalizedShiftedHom.{w''} W M X Y] : SmallShiftedHom.{w} W X Y m ≃ SmallShiftedHom.{w''} W X Y m :=
SmallHom.chgUniv
