instIsStableUnderRetractsFunctorFunctorCategory

English

If W is stable under retracts, then so is W.functorCategory J, for any J.

Русский

Если W устойчиво к retracts, то и W.functorCategory J так же устойчиво к retracts для любой J.

LaTeX

$$[W.IsStableUnderRetracts] ⇒ [W.functorCategory J].IsStableUnderRetracts$$

Lean4

instance [W.IsStableUnderRetracts] (J : Type u'') [Category.{v''} J] : (W.functorCategory J).IsStableUnderRetracts where
  of_retract hfg hg j := W.of_retract (hfg.map ((evaluation _ _).obj j).mapArrow) (hg j)

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