beckEqualizer_lift

Mathlib.CategoryTheory.Monad.Equalizer

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Comonad.beckEqualizer_lift

Lean4

@[simp]
theorem beckEqualizer_lift (s : Fork (T.toFunctor.map X.a) (T.δ.app X.A)) :
    (beckEqualizer X).lift s = s.ι ≫ T.ε.app _ :=
  rfl

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

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

Разделы

Аффилиация

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