Theorems · Theorem · category theory

CompHausLike.pullback.lift_snd_assoc

∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [inst : CompHausLike.HasExplicitPullback f g]
  {Z : CompHausLike P} (a : Z ⟶ X) (b : Z ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g) {Z_1 : CompHausLike P}
  (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.lift f g a b w)
      (CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.snd f g) h) =
    CategoryTheory.CategoryStruct.comp b h

Defined in

Mathlib.Topology.Category.CompHausLike.Limits

Cited by

0 results in Mathlib

Foundations

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

Assumes

CompHausLike.HasExplicitPullback