chgUniv — Mathlib

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

Похожие утверждения