{S : Type u_1} →
  {Y : Type u_2} →
    (f : S → Y) →
      (motive : (x : Function.Fiber f) × ↑↑x → Sort u_3) →
        (x : (x : Function.Fiber f) × ↑↑x) → ((a : Function.Fiber f) → (x : ↑↑a) → motive ⟨a, x⟩) → motive x