Add built-in coherence schemes

[thibautbenjamin]

Some operations need to be built-in as they are used constantly. This will allow to both spare the user from defining them and hard-code some automation to make them into a scheme.

Coherence schemes that should be built-in for sure:

• compositions (see add compositions as built-ins #29): The built-in composition can be defined as a variadic operation, where we infer the arity with the number of arguments. In combination with suspensions and functorialisation (if we allow functorialising a variable several times in a go) this could produce all the possible composites that one could imagine.
• identity (see add identity as a built-in #31): The identity is used all the time. There does not seem to be a particularly relevant scheme, and implementing it should be straightforward

One of the perks of defining these as built-ins is that we can use these built-ins as part of the generation of more complex automation, such as automation of the witnesses for equivalence (#8) and of naturality moves (#17)

Other possible built-ins:

• associativity: is it possible to define a scheme for variadic associativity and have it infer which kind of composition it applies to? It seems doable for iterated suspensions of the composition, but will not work for the associativity of horizontal composition for instance, where we need a naturality move
• unitors: How to indicate which unitor should be used?

In general, I do not think we should introduce built-ins requiring additional syntactic sugar, unless we have a good reason to do so. So introducing unitors and associativity in general seems a bit of a stretch, since it requires the user writing which unitor or associator they are trying to apply. However, we could introduce such things to be used inside of a context. For instance, one could probably write comp (...) (...) (eq) (...) where the keyword eq indicates that the system should infer an equivalence between the target of the previous term and the source of the next term. Ideally, those source and target are defined in the same pasting scheme, and the inferred equivalence is a single coherence. If it is not the case, then it is unclear how to proceed. We could consider the builtin eq to be a sort of tactics that may fail to infer in cases where there is not an obvious answer.