Theorems · Theorem · category theory

CategoryTheory.IsKernelPair.lift_fst_assoc

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {R X Y : C} {f : X ⟶ Y} {a b : R ⟶ X} {S : C}
  (k : CategoryTheory.IsKernelPair f a b) (p q : S ⟶ X)
  (w : CategoryTheory.CategoryStruct.comp p f = CategoryTheory.CategoryStruct.comp q f) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (k.lift p q w) (CategoryTheory.CategoryStruct.comp a h) =
    CategoryTheory.CategoryStruct.comp p h

Defined in

Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category