Theorems · Theorem · category theory

CategoryTheory.Arrow.RightHomotopy.compLeftId_hom

∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] [inst_1 : CategoryTheory.Preadditive V]
  {u v : CategoryTheory.Arrow V} {f : v ⟶ v}
  (h : CategoryTheory.Arrow.RightHomotopy f (CategoryTheory.CategoryStruct.id v)) (g : u ⟶ v),
  (h.compLeftId g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right g) h.hom

Defined in

Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Cited by

0 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive