∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [inst : CompHausLike.HasExplicitPullback f g],
  CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.fst f g) f =
    CategoryTheory.CategoryStruct.comp (CompHausLike.pullback.snd f g) g