{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {n : ℕ} →
      {X : (k : ℕ) → k < n → (t : Type (max v w)) × (t → C)} →
        {k k' : ℕ} →
          (hk : k < n) →
            (hk' : k' < n) →
              (j : (X k hk).fst) →
                (j' : (X k' hk').fst) →
                  ((X k hk).snd j ⟶ (X k' hk').snd j') →
                    ((X k hk).snd j ⟶ (X k' hk').snd j') →
                      CategoryTheory.IsFiltered.FilteredClosureSmall.InductiveStep✝ n X