{B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d : B} →
      {p : a ⟶ b} →
        {f : b ⟶ c} →
          {g : c ⟶ d} →
            {pf : a ⟶ c} →
              {pfg : a ⟶ d} →
                (CategoryTheory.CategoryStruct.comp p f ≅ pf) →
                  (CategoryTheory.CategoryStruct.comp pf g ≅ pfg) →
                    (CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp f g) ≅ pfg)