{ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      [inst_1 : (i : ι) → AddCommMonoid (G i)] →
        {f : (i j : ι) → i ≤ j → G i →+ G j} →
          [inst_2 : DecidableEq ι] →
            {G' : ι → Type u_5} →
              [inst_3 : (i : ι) → AddCommMonoid (G' i)] →
                {f' : (i j : ι) → i ≤ j → G' i →+ G' j} →
                  (e : (i : ι) → G i ≃+ G' i) →
                    (∀ (i j : ι) (h : i ≤ j), (e j).toAddMonoidHom.comp (f i j h) = (f' i j h).comp ↑(e i)) →
                      AddCommGroup.DirectLimit G f ≃+ AddCommGroup.DirectLimit G' f'