{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d : B} →
      {g : a ⟶ c} →
        {h : b ⟶ d} →
          {r₁ : b ⟶ a} →
            {r₂ r₃ : d ⟶ c} →
              (CategoryTheory.CategoryStruct.comp r₁ g ⟶ CategoryTheory.CategoryStruct.comp h r₂) →
                (r₂ ⟶ r₃) → (CategoryTheory.CategoryStruct.comp r₁ g ⟶ CategoryTheory.CategoryStruct.comp h r₃)