equivPUnit

Mathlib.CategoryTheory.Closed.Zero

URI: https://scilib.ai/kg/mathlib#CategoryTheory.equivPUnit

Lean4

/-- A Cartesian-closed category with a zero object is equivalent to the category with one object and
one morphism.
-/
def equivPUnit [HasZeroObject C] : C ≌ Discrete PUnit.{w + 1}
    where
  functor := Functor.star C
  inverse := Functor.fromPUnit 0
  unitIso :=
    NatIso.ofComponents
      (fun X =>
        { hom := default
          inv := default })
      fun _ => Subsingleton.elim _ _
  counitIso := Functor.punitExt _ _

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

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

Разделы

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

Аффилиация

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