instCategory

Mathlib.CategoryTheory.Join.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Join.instCategory

Lean4

instance : Category.{max v₁ v₂} (C ⋆ D) where
  Hom X Y := Hom X Y
  id _ := id _
  comp := comp
  assoc {a b c d} f g
    h := by cases a <;> cases b <;> cases c <;> cases d <;> simp only [Hom, comp, Category.assoc] <;> tauto
  id_comp {x y} f := by cases x <;> cases y <;> simp only [Hom, id, comp, Category.id_comp] <;> tauto
  comp_id {x y} f := by cases x <;> cases y <;> simp only [Hom, id, comp, Category.comp_id] <;> tauto

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

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

Разделы

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

Аффилиация

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