Add Cartesian multicategories

[laMudri]

While general multicategories have proved to be a pain to implement, Cartesian multicategories are easy. We can carry over techniques from simply typed λ-calculus, in particular simultaneous substitution. Indeed, the contents of this pull request give the machinery to derive the category of contexts and substitutions from some basic properties of the actions of substitutions.

Things left to do (along with general cleaning up and responding to comments):

• [x] Populate HomReasoning and HomˢReasoning with similar stuff as in Category.
• [ ] Move _∈_ properties over to stdlib.

[JacquesCarette]

That's looking really great! Is this still WIP, or is it ready to go?

[laMudri]

I'd like to at least give it a once-over. Do you have any opinions on the things that should be in stdlib rather than here, and getting versions synced up, &c? (Funnily enough, this kind of problem has been a topic in the SPLS pub.)

[laMudri]

Also, I think we should eventually axiomatise all of the required properties about List and _∈_. The only challenge I see there is what to do about prod, ⟨_⟩Π, and π[_], but maybe the literature has an answer (or we just axiomatise everything as-is).

[laMudri]

I suppose I'll need to rebase at some point to turn Structure into Bundle.

[JacquesCarette]

Yes please!

[JacquesCarette]

@laMudri I'm looking back at this now: can you tell me what you think the status is, in your opinion?

[laMudri]

Thanks for the reminder. agda/agda-stdlib#1756 should now be ready, so after that gets merged I should be able to delete those parts from this PR.