If d̂' = (f' : d → d') is last then this lets you factor f̂ : R̂(d̂) → c uniquely via some w : d̂ → d̂'. In terms of d/D this looks like

        f̂           R̂(w)     f̂'
  (R̂(d̂) → c) = (R̂(d̂) → R̂(d̂') → c)

and if we expand it in terms of D

  f̂ = f : R(d) → c

  w : d → d'
  R̂(w) = R(w)

  f̂' = f' : R(d') → c

it looks like

        f           R(w)     f'
  (R(d) → c) = (R(d) → R(d') → c).