normalizeEquiv

Mathlib.CategoryTheory.Bicategory.Coherence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.FreeBicategory.normalizeEquiv

Lean4

/-- Normalization as an equivalence of categories. -/
def normalizeEquiv (a b : B) : Hom a b ≌ Discrete (Path.{v + 1} a b) :=
  Equivalence.mk ((normalize _).mapFunctor a b) (inclusionPath a b) (normalizeUnitIso a b)
    (Discrete.natIso fun f =>
      eqToIso
        (by
          obtain ⟨f⟩ := f
          induction f with
          | nil => rfl
          | cons _ _
            ih =>
            ext1 -- Porting note: `tidy` closes the goal in mathlib3 but `aesop` doesn't here.

            injection ih with ih
            conv_rhs => rw [← ih]
            rfl))

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru