Theorems · Theorem · category theory

CategoryTheory.Limits.Bicone.category_id_hom

∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F),
  (CategoryTheory.CategoryStruct.id B).hom = CategoryTheory.CategoryStruct.id B.pt

Defined in

Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Cited by

0 results in Mathlib

Foundations

Depth 13 from the axioms · uses propext, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphisms