e_assoc' — Mathlib

English

An Enriched category in Type is equivalent to an ordinary category.

Русский

Обогащенная категория в Type эквивалентна обычной категории.

LaTeX

$$$\mathrm{EnrichedCategory}(Type(v),C) \simeq \mathrm{Category}(C)$$$

Lean4

@[reassoc]
theorem e_assoc' (W X Y Z : C) :
    (α_ _ _ _).hom ≫ _ ◁ eComp V X Y Z ≫ eComp V W X Z = eComp V W X Y ▷ _ ≫ eComp V W Y Z := by
  rw [← e_assoc V W X Y Z, Iso.hom_inv_id_assoc]

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