∀ {ι : Type u_1} [inst : Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {F : ι → Type u_4}
  {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h)
  [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)]
  [inst_2 : DirectedSystem F₁ fun x1 x2 x3 => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7}
  (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [inst_3 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)]
  [inst_4 : DirectedSystem F₂ fun x1 x2 x3 => ⇑(f₂ x1 x2 x3)] {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_5 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_6 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_7 : IsDirectedOrder ι]
  (ih ih_1 : (i : ι) → F₁ i → F₂ i → F i) (e_ih : ih = ih_1)
  (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), (f i j h) (ih i x y) = ih j ((f₁ i j h) x) ((f₂ i j h) y))
  (a a_1 : DirectLimit F₁ f₁),
  a = a_1 →
    ∀ (a_2 a_3 : DirectLimit F₂ f₂),
      a_2 = a_3 → DirectLimit.map₂ f₁ f₂ f ih compat a a_2 = DirectLimit.map₂ f₁ f₂ f ih_1 ⋯ a_1 a_3