experiment with HITs and rewritng rules

[Alizter]

Here is an experiment with rewriting rule based HITs. We redefine apand apD as a symbol with a computation rule in Overture.v and introduce a new file Interval2.v which demonstrates how new HITs can be written. Interval2 seems to be capable of proving funext which is quite cool, but it doesn't appear to compute nicely due to how we prove funext.

The change to ap was a bit more non-trivial than was indicated in #1868 and there are lots and lots of universe issues with the rewrite rules, so I had to come up with some hacky workarounds.

This PR isn't intended to be merged, but just to get a feel for what it could be like in the future.

[jdchristensen]

Cool! The build failed in Overture.v, but it looks like you got the build to go further on your machine. Not sure what is up with that.

[Alizter]

@jdchristensen I didn't update the flags for the non-dev dune build and _CoqProject. Should get further now.

[Alizter]

OK some clarification. apD and Interval_ind computes fine. I suppose if we defined ap as apD and transport_const then we can define the non-dependent recursor in a similar fashion.

However since I made ap and Interval_rec symbols I need the to reduce in the fuenxt proof modulo eta which rewrite rules are currently not able to do. So this is still a bit broken.