{C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      {D' : Type u_5} →
        [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] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] →
                {L : CategoryTheory.Functor C D} →
                  {L' : CategoryTheory.Functor D D'} →
                    {F₀ : CategoryTheory.Functor C H} →
                      {F₁ : CategoryTheory.Functor D H} →
                        (α : F₀ ⟶ L.comp F₁) →
                          CategoryTheory.StructuredArrow.IsUniversal (CategoryTheory.Functor.LeftExtension.mk F₁ α) →
                            (b : L'.LeftExtension F₁) →
                              CategoryTheory.StructuredArrow.IsUniversal b ≃
                                CategoryTheory.StructuredArrow.IsUniversal
                                  ((CategoryTheory.Functor.LeftExtension.precomp₂ L' α).obj b)