isCocartesian_of_isStronglyCocartesian

English

If p is strongly cocartesian for f φ, then p is cocartesian for f φ.

Русский

Если p является сильно кокартезианской для f φ, то она является кокартезианской для f φ.

LaTeX

$$[IsStronglyCocartesian p f φ] ⇒ [IsCocartesian p f φ]$$

Lean4

instance isCocartesian_of_isStronglyCocartesian [p.IsStronglyCocartesian f φ] : p.IsCocartesian f φ where
  universal_property := fun φ' => universal_property p f φ (𝟙 S) f (comp_id f).symm φ'

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