∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (G : CategoryTheory.Functor C (Type u_3))
  {X Y : CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat)} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.id (CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat))).map f)
      ((fun X =>
            CategoryTheory.Grothendieck.casesOn X fun base fiber =>
              CategoryTheory.Discrete.casesOn fiber fun as =>
                CategoryTheory.Iso.refl
                  ((CategoryTheory.Functor.id (CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat))).obj
                    { base := base, fiber := { as := as } }))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun X =>
            CategoryTheory.Grothendieck.casesOn X fun base fiber =>
              CategoryTheory.Discrete.casesOn fiber fun as =>
                CategoryTheory.Iso.refl
                  ((CategoryTheory.Functor.id (CategoryTheory.Grothendieck (G.comp CategoryTheory.typeToCat))).obj
                    { base := base, fiber := { as := as } }))
          X).hom
      (((CategoryTheory.Grothendieck.grothendieckTypeToCatFunctor G).comp
            (CategoryTheory.Grothendieck.grothendieckTypeToCatInverse G)).map
        f)