comapEq

Mathlib.CategoryTheory.GradedObject

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GradedObject.comapEq

Lean4

/-- The natural isomorphism comparing between
pulling back along two propositionally equal functions.
-/
@[simps]
def comapEq {β γ : Type w} {f g : β → γ} (h : f = g) : comap C f ≅ comap C g
    where
  hom := { app := fun X b => eqToHom (by dsimp; simp only [h]) }
  inv := { app := fun X b => eqToHom (by dsimp; simp only [h]) }

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

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

Разделы

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

Аффилиация

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