Rewrite rules for pushouts

[fredrik-bakke]

Adds strict β-laws for the standard pushouts in a new module synthetic-homotopy-theory.rewriting-pushouts.

Todo

• Wait for Rebase infrastructure for pushouts to span diagrams #885.
• Refactor postulates of universal properties to be phrased in terms of coherently invertible maps.
• Add separate file for rewrites synthetic-homotopy-theory.rewriting-pushouts.

[fredrik-bakke]

I just realized, If we add rewrite rules for the computation rules of the eliminator for pushouts, then we should be able to prove funext from the existence of the interval, thus maybe it will be possible to construct eq-htpy in such a way that eq-htpy refl ≐ refl-htpy...

[fredrik-bakke]

Okay, this PR is already blocked on #885. I'll just write my thoughts for the next steps here: To have the most reasonable definitions for the rewrite rules, it is quite important that cogap is definitionally both the left and right inverse of cocone-map, hence we should postulate up-pushout in terms of a version of universal-property-pushout using is-coherently-invertible.

[fredrik-bakke]

This PR reopens #515.

[fredrik-bakke]

As @EgbertRijke pointed out to me and I had completely forgotten, we should only implement rewrite rules for the point constructors. Here's the relevant justification from the HoTT/UF book:

[fredrik-bakke]

Just to remind my future self. It seems we may want to use primEraseEquality with our rewrite rules, so that the computation rules hold by reflexivity, as expected... I believe.

[fredrik-bakke]

I just came across the following sources again today:

• https://groups.google.com/g/homotopytypetheory/c/-5mLEi_qMTo/m/yj9B-XobWOsJ%3Fctz=2597977_56_56_123900_52_436380
• https://www.cs.bham.ac.uk/~mhe/truncation-and-extensionality/hprop-truncation.html
• https://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/

which reminded me that it should be possible to define pushouts in a way that computes on point constructors without using rewrites! This approach sounds preferable to me if we can be guaranteed that Agda does not leak any additional implementation details.

EDIT: Never mind, this is indeed inconsistent https://homotopytypetheory.org/2011/04/23/running-circles-around-in-your-proof-assistant/#comment-80163

[fredrik-bakke]

Good news! Agda does support adding rewrite rules in a separate file. This means that formalizations that use the rewrite rules for pushouts can live alongside formalizations that don't. The only limitation is that one cannot import formalizations that use rewriting without enabling rewriting, as expected.

[fredrik-bakke]

I'm opening this PR up to comments now. Note that the infrastructure for pushouts is not perfect. I'm hoping to improve it a bit over the next week with some additional refactoring.

[EgbertRijke]

Looks very good!

[VojtechStep]

Great job! I'd like to see what you have in mind to use these for. I would like to see a bit more docs on how to "enable rewriting for pushouts" though.