∀ {X Y : Type u_1ᵒᵖ} (f : X ⟶ Y) ⦃X_1 Y_1 : CommMonCat⦄ (f_1 : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp
      ({ obj := fun M => CommMonCat.of (Opposite.unop X → ↑M),
            map := fun {X_2 Y} f =>
              CommMonCat.ofHom (Pi.monoidHom fun i => (CommMonCat.Hom.hom f).comp (Pi.evalMonoidHom (fun a => ↑X_2) i)),
            map_id := ⋯, map_comp := ⋯ }.map
        f_1)
      (CommMonCat.ofHom (Pi.monoidHom fun i => Pi.evalMonoidHom (fun a => ↑Y_1) (f.unop i))) =
    CategoryTheory.CategoryStruct.comp
      (CommMonCat.ofHom (Pi.monoidHom fun i => Pi.evalMonoidHom (fun a => ↑X_1) (f.unop i)))
      ({ obj := fun M => CommMonCat.of (Opposite.unop Y → ↑M),
            map := fun {X Y_2} f =>
              CommMonCat.ofHom (Pi.monoidHom fun i => (CommMonCat.Hom.hom f).comp (Pi.evalMonoidHom (fun a => ↑X) i)),
            map_id := ⋯, map_comp := ⋯ }.map
        f_1)