inverseAssociatorIsEquivalence — Mathlib

English

Similarly, the inverse associator functor for C, D, E is an equivalence of categories.

Русский

Аналогично, обратный ассоциатор является эквивалентностью категорий.

LaTeX

$$$$ \mathrm{inverseAssociator}_{C D E} : C \oplus (D \oplus E) \stackrel{\sim}{\to} (C \oplus D) \oplus E \text{ is an equivalence.} $$$$

Lean4

instance inverseAssociatorIsEquivalence : (inverseAssociator C D E).IsEquivalence :=
  (by infer_instance : (associativity C D E).inverse.IsEquivalence)
    -- TODO unitors?
    -- TODO pentagon natural transformation? ...satisfying?

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