Auto-instantiate proof of adjunction alongside section and retraction (cf., #57)

[nateyazdani]

This PR pulls in Jasper's HoTT module for adjointifying equivalences and applies its generic lemmas when equivalence-proving is enabled. The module is placed at theories/Adjoint.v.

For an ornament named ${ornament}, this feature instantiates Jasper's fg_id' (to adjointify retraction) as ${ornament}_retraction and f_adjoint (to prove adjunction) as ${ornament}_adjunction.

The initial retraction proof (which is an input to the previous two lemmas) is now generated as ${ornament}_retraction0 to prevent a name collision. To actually benefit from the adjunction theorem, rewritings need to use the adjointified retraction lemma, hence the preferential naming scheme.

The test script (test.sh) passes successfully.

Some potential design concerns:

• Are you okay with adjunction sharing the same proof-generation option as section+retraction?
• Do you want the Adjoint.v module translated to use Ltac proof scripts instead of terms?
• Is the need to use adjointified retraction lemmas a problem? I wouldn't think so, but I wanted to mention it because the two versions' definitional equalities don't coincide (e.g., refold_retraction in Example.v does not hold, though a different proof could plausibly work).

If satisfactory, this feature would resolve issue #57.

[tlringer]

Linking to #39 also

[nateyazdani]

All requests for changes have been addressed, with the exception of the naming scheme and a line in the example script; I asked follow-up questions in reply to those comments.

All tests pass.

[nateyazdani]

Ah, it seems that I've let this linger too long, and there are now merge conflicts. They're pretty innocuous, so I'll leave them be for now, in case you'd like to inspect.

[tlringer]

Yeah, don't bother trying the merge, I'll do it once everything is addressed

[nateyazdani]

All done with requested changes! After switching the initial retraction name back to ${ornament}_retraction, I used ${ornament}_retraction_adjoint for the adjointified version.

[tlringer]

LGTM, I will take over and try the merge.

[tlringer]

Thanks for the great work!!