{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {FC : C → C → Type u_1} →
      {CC : C → Type v} →
        [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory C FC] →
            {X₁ X₂ S : C} →
              (f₁ : X₁ ⟶ S) →
                (f₂ : X₂ ⟶ S) →
                  [inst_3 : CategoryTheory.Limits.HasPullback f₁ f₂] →
                    [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f₁ f₂)
                          (CategoryTheory.forget C)] →
                      CategoryTheory.ToType (CategoryTheory.Limits.pullback f₁ f₂) ≃
                        { p //
                          (CategoryTheory.ConcreteCategory.hom f₁) p.1 = (CategoryTheory.ConcreteCategory.hom f₂) p.2 }