comonEquiv

Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_

URI: https://scilib.ai/kg/mathlib#comonEquiv

Lean4

/-- The category of comonoid objects in a Cartesian monoidal category is equivalent
to the category itself, via the forgetful functor.
-/
@[simps]
def comonEquiv : Comon C ≌ C where
  functor := Comon.forget C
  inverse := cartesianComon C
  unitIso := NatIso.ofComponents isoCartesianComon
  counitIso := NatIso.ofComponents (fun _ => .refl _)

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

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

Разделы

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

Аффилиация

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