Upstreaming some of the material in Auxiliary to UniMath/UniMath?

[benediktahrens]

Great work was done by @peterlefanulumsdaine in #202 regarding organization of auxiliary material in Auxiliary.

Question: would some of the material from Auxiliary fit well into UniMath/UniMath? The advantages of upstreaming such material are:

1. It would be easier to find and use in other libraries (though I am not aware of any development outside UniMath/UniMath and UniMath/TypeTheory).
2. Material in U/U (but not in U/T) is regularly checked for compatibility with Coq development versions.

Upstreaming would not make the work of #202 superfluous - on the contrary, the good organization of the material makes it feasible at all to discuss the possibility of upstreaming, and would make upstreaming much easier.

[peterlefanulumsdaine]

Yes, I strongly support this! Several bits of the recent housekeeping (especially the reorganisation of the auxiliary files) were done with this in mind, and I have a rough plan for how to do it, so can happily take this on over the next few weeks (after UniMath/UniMath#1396 which I’m working on now).