∀ (R : Type u_3) (G : Type u_1) [inst : CommRing R] [inst_1 : Group G] [inst_2 : TopologicalSpace R]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] {X Y : Action (TopModuleCat R) G} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((continuousCohomology R G 0).map f)
      ((fun X =>
            (CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork
                    (HomologicalComplex.sc ((ContinuousCohomology.homogeneousCochains R G).obj X) 0) ⋯
                    (CategoryTheory.Limits.KernelFork.ofι
                      (TopModuleCat.kerι
                        (HomologicalComplex.sc ((ContinuousCohomology.homogeneousCochains R G).obj X) 0).g)
                      ⋯)
                    (TopModuleCat.isLimitKer
                      (HomologicalComplex.sc ((ContinuousCohomology.homogeneousCochains R G).obj X)
                          0).g)).left.homologyIso ≪≫
              TopModuleCat.ofIso
                (ContinuousCohomology.kerHomogeneousCochainsZeroEquiv R G X ((ComplexShape.up ℕ).next 0)
                  ContinuousCohomology.continuousCohomologyZeroIso._proof_2))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun X =>
            (CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork
                    (HomologicalComplex.sc ((ContinuousCohomology.homogeneousCochains R G).obj X) 0) ⋯
                    (CategoryTheory.Limits.KernelFork.ofι
                      (TopModuleCat.kerι
                        (HomologicalComplex.sc ((ContinuousCohomology.homogeneousCochains R G).obj X) 0).g)
                      ⋯)
                    (TopModuleCat.isLimitKer
                      (HomologicalComplex.sc ((ContinuousCohomology.homogeneousCochains R G).obj X)
                          0).g)).left.homologyIso ≪≫
              TopModuleCat.ofIso
                (ContinuousCohomology.kerHomogeneousCochainsZeroEquiv R G X ((ComplexShape.up ℕ).next 0)
                  ContinuousCohomology.continuousCohomologyZeroIso._proof_2))
          X).hom
      ((ContinuousCohomology.invariants R G).map f)