∀ {X Y : AddCommMonCatᵒᵖ} (f : X ⟶ Y) ⦃X_1 Y_1 : AddCommMonCat⦄ (f_1 : X_1 ⟶ Y_1),
  CategoryTheory.CategoryStruct.comp
      ({ obj := fun N => AddCommMonCat.of (↑(Opposite.unop X) →+ ↑N),
            map := fun {X_2 Y} f => AddCommMonCat.ofHom (AddMonoidHom.compHom (AddCommMonCat.Hom.hom f)), map_id := ⋯,
            map_comp := ⋯ }.map
        f_1)
      (AddCommMonCat.ofHom (AddCommMonCat.Hom.hom f.unop).compHom') =
    CategoryTheory.CategoryStruct.comp (AddCommMonCat.ofHom (AddCommMonCat.Hom.hom f.unop).compHom')
      ({ obj := fun N => AddCommMonCat.of (↑(Opposite.unop Y) →+ ↑N),
            map := fun {X Y_2} f => AddCommMonCat.ofHom (AddMonoidHom.compHom (AddCommMonCat.Hom.hom f)), map_id := ⋯,
            map_comp := ⋯ }.map
        f_1)