instIsHomLiftObjPIdObj — Mathlib

English

For a based functor F and an object a, there is a lifting structure IsHomLift 𝒴.p (𝟙 (𝒳.p.obj a)) (F.obj a).

Русский

Для основанного функторa F и объекта a существует поднятие IsHomLift 𝒴.p (𝟙 (𝒳.p.obj a)) (F.obj a).

LaTeX

$$$\\text{instance } (F : 𝒳 ⥤ᵇ 𝒴) (a : 𝒳.obj) : IsHomLift 𝒴.p (𝟙 (𝒳.p.obj a)) (F.obj a)$$$

Lean4

instance (F : 𝒳 ⥤ᵇ 𝒴) (a : 𝒳.obj) : IsHomLift 𝒴.p (𝟙 (𝒳.p.obj a)) (𝟙 (F.obj a)) :=
  IsHomLift.id (w_obj F a)

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