Theorems · Theorem · category theory

CompHausLike.pullback.condition_assoc

∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [inst : CompHausLike.HasExplicitPullback f g]
  {Z : CompHausLike P} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.fst f g) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.snd f g) (CategoryTheory.CategoryStruct.comp g 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