{ι : Type u_1} →
  {σ : Type u_3} →
    [inst : Preorder ι] →
      [inst_1 : Preorder σ] →
        {F F_lt : ι → σ} →
          {motive : IsFiltration F F_lt → Sort u} →
            (t : IsFiltration F F_lt) →
              ((mono : Monotone F) →
                  (is_le : ∀ {i j : ι}, i < j → F i ≤ F_lt j) →
                    (is_sup : ∀ (B : σ) (j : ι), (∀ i < j, F i ≤ B) → F_lt j ≤ B) → motive ⋯) →
                motive t