Read the following sections of the Agda documentation:
Also have a first look at:
Fin
and Vec
started
in Friday's lecture, FinVec.lagda.md
.
You will at least have to insert arguments or pattern matching
before working on the holes provided.
Use the interactive support that Agda gives you,
in particular case splitting `C-c C-c`, give `C-c C-SPACE`,
goal type and context `C-c C-,`, …