naturality_id

Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence

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

Lean4

theorem naturality_id {p : a ⟶ b} {f : b ⟶ c} {pf : a ⟶ c} (η_f : p ≫ f ≅ pf) : p ◁ Iso.refl f ≪≫ η_f = η_f :=
  Iso.ext (by simp)

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

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

Разделы

Аффилиация

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