comp_app_eq

Mathlib.CategoryTheory.Category.ReflQuiv

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ReflQuiv.adj.counit.comp_app_eq

Lean4

/-- The counit of `ReflQuiv.adj` is closely related to the counit of `Quiv.adj`. -/
@[simp]
theorem comp_app_eq (C : Type u) [Category C] :
    Cat.FreeRefl.quotientFunctor C ⋙ adj.counit.app C = pathComposition (Cat.of C) :=
  rfl

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

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

Разделы

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

Аффилиация

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