comp_assoc — Mathlib

English

Composition of strictly unitary lax functors is strictly associative: (F ∘ G) ∘ H = F ∘ (G ∘ H).

Русский

Состояние строгой ассоциативности композиции строго унитарных lax-функторов: (F ∘ G) ∘ H = F ∘ (G ∘ H).

LaTeX

$$$ (F\\, .\\, G)\\, .\\, H = F\\, .\\, (G\\, .\\, H)$$$

Lean4

/-- Composition of `StrictlyUnitaryLaxFunctor` is strictly associative -/
theorem comp_assoc {E : Type u₄} [Bicategory.{w₄, v₄} E] (F : StrictlyUnitaryLaxFunctor B C)
    (G : StrictlyUnitaryLaxFunctor C D) (H : StrictlyUnitaryLaxFunctor D E) : (F.comp G).comp H = F.comp (G.comp H) :=
  by
  ext
  · simp
  all_goals
    · rw [heq_iff_eq]
      ext
      simp

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