{H : Type u} →
  {inst : TopologicalSpace H} →
    {G : StructureGroupoid H} →
      {M : Type u_5} →
        {M' : Type u_6} →
          {inst_1 : TopologicalSpace M} →
            {inst_2 : TopologicalSpace M'} →
              {inst_3 : ChartedSpace H M} → {inst_4 : ChartedSpace H M'} → Structomorph G M M' → ℕ