{C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            {L : CategoryTheory.Functor C D} →
              {F₁ F₂ : CategoryTheory.Functor C H} →
                (α₁ : L.RightExtension F₁) →
                  (α₂ : L.RightExtension F₂) →
                    (e : F₁ ≅ F₂) →
                      (e' : α₁.left ≅ α₂.left) →
                        CategoryTheory.CategoryStruct.comp (L.whiskerLeft e'.hom) α₂.hom =
                            CategoryTheory.CategoryStruct.comp α₁.hom e.hom →
                          CategoryTheory.CostructuredArrow.IsUniversal α₁ ≃
                            CategoryTheory.CostructuredArrow.IsUniversal α₂