∀ {C : Type u_4} [inst : CategoryTheory.Category.{u_3, u_4} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y : CategoryTheory.Grothendieck F} (e₁ : X.base ≅ Y.base) (e₂ : (F.map e₁.hom).toFunctor.obj X.fiber ≅ Y.fiber),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp { base := e₁.hom, fiber := e₂.hom }
          { base := e₁.inv,
            fiber :=
              CategoryTheory.CategoryStruct.comp ((F.map e₁.inv).toFunctor.map e₂.inv)
                (CategoryTheory.eqToHom ⋯) }).fiber =
    (CategoryTheory.CategoryStruct.id X).fiber