{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : Cᵒᵖ} →
      {f : X ⟶ Y} →
        [inst_1 : CategoryTheory.Limits.HasPullback f f] →
          [inst_2 : CategoryTheory.Limits.HasPushout f.unop f.unop] →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ f ⋯) ≃
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Fork.ofι f.unop ⋯)