naturality_inv

Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Bicategory.naturality_inv

Lean4

theorem naturality_inv {p : a ⟶ b} {f g : b ⟶ c} {pf : a ⟶ c} {η : f ≅ g} (η_f : p ≫ f ≅ pf) (η_g : p ≫ g ≅ pf)
    (ih : p ◁ η ≪≫ η_g = η_f) : p ◁ η.symm ≪≫ η_f = η_g :=
  by
  rw [← ih]
  apply Iso.ext (by simp)

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

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

Разделы

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

Аффилиация

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