Datatype ~= coproduct of Σ-types via reflection

[anuyts]

I'm trying to do this by looking at the existing code for record types and Σ-types in Cubical.Reflection.RecordEquiv but ~got stuck~ gave up for now because I realized I don't understand how the meat of the code there works: convertClauses and recordIsoΣClauses with its subfunctions are quite mysterious to me. Perhaps adding some comments there could help me out @ecavallo.

[ecavallo]

Made a PR to add some explanation. The 1lab version might also be clearer, I didn't look closely.