Theorems · Theorem · category theory

CategoryTheory.RetractArrow.i_w

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left h.i) g =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Arrow.Hom.right h.i)

Defined in

Mathlib.CategoryTheory.Retract

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category