English
There is an equivalence between SmallHom sets across different universes; up to isomorphism the type does not depend on the universe index.
Русский
Существуют эквивалентности между множеставми SmallHom в разных вселенных; по существованию, тип не зависит от индекса вселенной.
LaTeX
$$$\mathrm{SmallHom}^w W X Y \simeq \mathrm{SmallHom}^{w''} W X Y$$$
Lean4
/-- Up to an equivalence, the type `SmallHom.{w} W X Y n` does not depend on the universe `w`. -/
noncomputable def chgUniv {X Y : C} [HasSmallLocalizedHom.{w} W X Y] [HasSmallLocalizedHom.{w''} W X Y] :
SmallHom.{w} W X Y ≃ SmallHom.{w''} W X Y :=
(equiv.{w} W W.Q).trans (equiv.{w''} W W.Q).symm