instCategoryTotal

Mathlib.CategoryTheory.Presentable.ColimitPresentation

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.ColimitPresentation.instCategoryTotal

Lean4

@[simps! id_base id_hom comp_base comp_hom]
instance : Category (Total P) where
  Hom := Total.Hom
  id _ := { base := 𝟙 _, hom := 𝟙 _ }
  comp := Total.Hom.comp

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

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

Разделы

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

Аффилиация

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