∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y Z : CategoryTheory.Grothendieck F} (f : X.Hom Y) (g : Y.Hom Z),
  (F.map (CategoryTheory.CategoryStruct.comp f.base g.base)).toFunctor.obj X.fiber =
    (F.map g.base).toFunctor.obj ((F.map f.base).toFunctor.obj X.fiber)