Definition of multicategories

[anshwad10]

I added some folds and maps for FinVecs in FinData.Base
I also changed the definition of tabulate to another one that has the same computation rule
I also added tabulate' which is not definitionally the same but has the same computation rule (I needed it to define the left identity law for multicategories)

[anshwad10]

What I need to prove now is that Fin (length (foldrFinVec _++_ [] yss)) is equivalent to Σ[ k ∈ Fin (length zs) ] Fin (length (yss k)).
Then I need to prove that lookup (foldrFinVec _++_ [] yss) kl is equal to lookup (yss k) l where (k , l) and kl are related by the aforementioned equivalence.
And then I'll need another path for the PathP.
I'll need a lot of lemmas which are not defined yet in the library, so this is going to be a draft PR till then.