natTransOfWhiskerLeftInlInr_id — Mathlib

English

The whiskered identity natural transformations compose to the identity transformation on F.

Русский

Уравнение для единичного преобразования под операции whiskerLeftInlInr дает тождественное преобразование на F.

LaTeX

$$natTransOfWhiskerLeftInlInr (𝟙 (Sum.inl_ A A' ⋙ F)) (𝟙 (Sum.inr_ A A' ⋙ F)) = 𝟙 F$$

Lean4

@[simp]
theorem natTransOfWhiskerLeftInlInr_id {F : A ⊕ A' ⥤ B} :
    natTransOfWhiskerLeftInlInr (𝟙 (Sum.inl_ A A' ⋙ F)) (𝟙 (Sum.inr_ A A' ⋙ F)) = 𝟙 F := by cat_disch

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