Misc
Try to model deltas on generic values using a group

This attempt failed: Agda let me see that this is in fact not a group.
I'll provide other attempts soon.
Deltas form a groupoid - proofs

No groupoid structure is yet declared, only a first attempt at the proofs is there.
Cleanup a bit DeltaGroupoid

A better version, which avoids the need for this weird cast, will arrive soon.
Simplify DeltaGroupoid very much

Make it more apparent to Agda that Delta is a singleton type, so that everything is
part of the type. That was thanks to a tip on #agda by Andrea Vezzosi.