{P : Sort u} →
  {𝕜 : Type u_1} →
    {inst : NontriviallyNormedField 𝕜} →
      {H : Type u_2} →
        {inst_1 : TopologicalSpace H} →
          {E : Type u_3} →
            {inst_2 : NormedAddCommGroup E} →
              {inst_3 : NormedSpace 𝕜 E} →
                {H' : Type u_5} →
                  {inst_4 : TopologicalSpace H'} →
                    {E' : Type u_6} →
                      {inst_5 : NormedAddCommGroup E'} →
                        {inst_6 : NormedSpace 𝕜 E'} →
                          {I : ModelWithCorners 𝕜 E H} →
                            {I' : ModelWithCorners 𝕜 E' H'} →
                              {n : WithTop ℕ∞} →
                                {G : Type u_8} →
                                  {inst_7 : TopologicalSpace G} →
                                    {inst_8 : ChartedSpace H G} →
                                      {inst_9 : Monoid G} →
                                        {G' : Type u_9} →
                                          {inst_10 : TopologicalSpace G'} →
                                            {inst_11 : ChartedSpace H' G'} →
                                              {inst_12 : Monoid G'} →
                                                {t : ContMDiffMonoidMorphism I I' n G G'} →
                                                  {𝕜' : Type u_1} →
                                                    {inst' : NontriviallyNormedField 𝕜'} →
                                                      {H'_1 : Type u_2} →
                                                        {inst'_1 : TopologicalSpace H'_1} →
                                                          {E'_1 : Type u_3} →
                                                            {inst'_2 : NormedAddCommGroup E'_1} →
                                                              {inst'_3 : NormedSpace 𝕜' E'_1} →
                                                                {H'' : Type u_5} →
                                                                  {inst'_4 : TopologicalSpace H''} →
                                                                    {E'' : Type u_6} →
                                                                      {inst'_5 : NormedAddCommGroup E''} →
                                                                        {inst'_6 : NormedSpace 𝕜' E''} →
                                                                          {I'_1 : ModelWithCorners 𝕜' E'_1 H'_1} →
                                                                            {I'' : ModelWithCorners 𝕜' E'' H''} →
                                                                              {n' : WithTop ℕ∞} →
                                                                                {G'_1 : Type u_8} →
                                                                                  {inst'_7 : TopologicalSpace G'_1} →
                                                                                    {inst'_8 : ChartedSpace H'_1 G'_1} →
                                                                                      {inst'_9 : Monoid G'_1} →
                                                                                        {G'' : Type u_9} →
                                                                                          {inst'_10 :
                                                                                              TopologicalSpace G''} →
                                                                                            {inst'_11 :
                                                                                                ChartedSpace H'' G''} →
                                                                                              {inst'_12 : Monoid G''} →
                                                                                                {t' :
                                                                                                    ContMDiffMonoidMorphism
                                                                                                      I'_1 I'' n' G'_1
                                                                                                      G''} →
                                                                                                  𝕜 = 𝕜' →
                                                                                                    inst ≍ inst' → ⋯