Theorems · Theorem · category theory

CategoryTheory.Arrow.RightHomotopy.compRight_hom

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

Defined in

Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Preadditive