{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : Cᵒᵖ} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          [h : CategoryTheory.Limits.HasPullback f g] →
            CategoryTheory.Limits.pullback f g ≅ Opposite.op (CategoryTheory.Limits.pushout f.unop g.unop)