{ι : Type u_1} →
  [Fintype ι] →
    [DecidableEq ι] →
      {α : ι → Sort u_2} →
        {S : (i : ι) → Setoid (α i)} →
          {C : ((i : ι) → Quotient (S i)) → Sort u_4} →
            (q : (i : ι) → Quotient (S i)) →
              (f : (a : (i : ι) → α i) → C fun x => ⟦a x⟧) →
                (∀ (a b : (i : ι) → α i) (h : ∀ (i : ι), a i ≈ b i), ⋯ ▸ f a = f b) → C q