∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor (CategoryTheory.Join C D) E}
  (eₗ eₗ_1 : (CategoryTheory.Join.inclLeft C D).comp F ≅ (CategoryTheory.Join.inclLeft C D).comp G) (e_eₗ : eₗ = eₗ_1)
  (eᵣ eᵣ_1 : (CategoryTheory.Join.inclRight C D).comp F ≅ (CategoryTheory.Join.inclRight C D).comp G) (e_eᵣ : eᵣ = eᵣ_1)
  (h :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) F)
        ((CategoryTheory.Prod.snd C D).isoWhiskerLeft eᵣ).hom =
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.Prod.fst C D).isoWhiskerLeft eₗ).hom
        (CategoryTheory.Functor.whiskerRight (CategoryTheory.Join.edgeTransform C D) G)),
  CategoryTheory.Join.mkNatIso eₗ eᵣ h = CategoryTheory.Join.mkNatIso eₗ_1 eᵣ_1 ⋯