In a recent proof mining application, the proof-theoretical analysis of Dykstra's cyclic projections algorithm resulted in quantitative information expressed via primitive recursive functionals in the sense of Gödel. This ...