{𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F G H : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} →
      (α : F ⟶ G) →
        (β : G ⟶ H) →
          CategoryTheory.Pseudofunctor.CoGrothendieck.map (CategoryTheory.CategoryStruct.comp α β) ≅
            (CategoryTheory.Pseudofunctor.CoGrothendieck.map α).comp (CategoryTheory.Pseudofunctor.CoGrothendieck.map β)