{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) →
                CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g →
                  (Z ⟶ CompHausLike.pullback f g)