∀ (X : Type u_1ᵒᵖ),
  {
      app := fun N =>
        CommMonCat.ofHom
          (Pi.monoidHom fun i => Pi.evalMonoidHom (fun a => ↑N) ((CategoryTheory.CategoryStruct.id X).unop i)),
      naturality := ⋯ } =
    CategoryTheory.CategoryStruct.id
      { obj := fun M => CommMonCat.of (Opposite.unop X → ↑M),
        map := fun {X_1 Y} f =>
          CommMonCat.ofHom (Pi.monoidHom fun i => (CommMonCat.Hom.hom f).comp (Pi.evalMonoidHom (fun a => ↑X_1) i)),
        map_id := ⋯, map_comp := ⋯ }