sum of Fin maps in Agda

How would I implement the sum of two functions on Fin in Agda with the following type?

open import Data.Fin hiding (_+_)
open import Data.Nat

sum : (a b c d : ℕ) → (x : Fin a → Fin b) → (y : Fin c → Fin d) → (Fin (a + c) → Fin (b + d))
sum = ?

Solution

@Ruben, there are/might be several approaches to solving your problem (homework? or otherwise?), but here's a specimen problem decomposition:

in order to use to use the function arguments x and y, you somehow need to manufacture arguments of the correct type to each of them, from the input(s) available;
so, you need some way to get from Fin (a + c) to either Fin a (so that you can use x), or Fin c (so that you can use y);
but even then, you're not done, as you then need some way to take the results of applying x (resp. y) and then transform them into results of the correct type Fin (b + d).

Fortunately, all the necessary pieces to do this kind of decomposition/recomposition are already present in the standard library:

for 'either/or' reasoning/construction, in Data.Sum;
for decomposition of Fin (a + c)/recomposition of Fin (b + d), in Data.Fin.

Hope these hints are useful!