Degeneracies in all directions

[olympichek]

This PR extends construction of degeneracies to all directions.

This is a port of Alice's construction of degeneracies (built on top of old νSet construction) to the new νSet construction:
https://github.com/alicelaroche/bonak/blob/e4ee6f999312c5317392497dc0de9a4150f54b8c/theories/νType/νType.v#L1438

The construction is done in two stages - "below" and "above". In terms of Alice's construction, it can be explained as follows. The “below” operation just reflects the existing frame, producing a p-frame in dimension n+1. Once the prefix has reached or passed the direction q (q ≤ p), the “above” operation inserts the original painting as the repeated constant layer, so it takes both the frame d and painting c and produces a (p + 1)-frame.

Within the new νSet construction that follows a "zipper" pattern, p is the prefix height and k is the number of directions still above it. The dimension n is computed as p + k. Within this construction, "below" degeneracy is indexed by a relative direction q ≤ k and "above" degeneracy is indexed by a direction already inside the prefix, q ≤ p. For frames, we first define degeneracies "below" and then degeneracies "above", while for paintings it is the other way around.

We prove the following face-degeneracy coherence equations (here refl↓ means degeneracies "below" and refl↑ means degeneracies "above"):

restr-refl↓-id q ε (q ≤ k): restr q ε ∘ refl↓ q = id
refl↓-restr-inf q r ε (r ≤ q ≤ k): refl↓ q ∘ restr r ε = restr r ε ∘ refl↓ (q+1)
refl↓-restr-sup q r ε (q ≤ r ≤ k): refl↓ q ∘ restr r ε = restr (r+1) ε ∘ refl↓ q
refl↑-restr-sup q r ε (q ≤ p) (r ≤ k): refl↑ q ∘ restr r ε = restr r ε ∘ refl↑ q

The type of refl↓-restr-inf for frames is built mutually-recursively with the definition of refl↓ for frames, while the type of refl↑-restr-sup for frames is built mutually-recursively with the definition of refl↑ for frames. For frames, refl-restr-sup is first proved for refl↓ and then for refl↑, while for paintings it is the other way around.

Additionally, we also prove the degeneracy-degeneracy coherence equation. This is done in 3 stages - "below-below", "above-below" and "above-above":

refl↓-refl↓ q r (q ≤ r ≤ k): refl↓ q ∘ refl↓ r = refl↓ (r+1) ∘ refl↓ q
refl↑-refl↓ q r (q ≤ p) (r ≤ k): refl↑ q ∘ refl↓ r = refl↓ r ∘ refl↑ q
refl↑-refl↑ q r (q ≤ r ≤ p): refl↑ q ∘ refl↑ r = refl↑ (r+1) ∘ refl↑ q

For frames, we first prove refl↓-refl↓, then refl↑-refl↓ and finally refl↑-refl↑. For paintings, again, the order is reversed: refl↑-refl↑ is proved first, then refl↑-refl↓ and finally refl↓-refl↓.

P.S. Here are some diagrams of 2-dimensional coherences that we are closing with UIP:
https://olympichek.dev/bonak-higher-cohs/higher-coherences.pdf
https://github.com/olympichek/bonak-higher-cohs

[olympichek]

CI uses latest Rocq, which is now 9.2. However, we use coq package, which provides compatibility aliases such as coqc, which is required by dune-s coq stanza. The coq package is not updated for Rocq 9.2, as for or Rocq 9.2 the new rocq stanza should be used, so coq package should not be needed. We might think about upgrading the Rocq dependency to 9.2 and using the new rocq stanza, but that is as of right now impossible as we also use Rocq Stdlib, and rocq-stdlib is not upgraded for 9.2 yet. With that said, I believe the best solution is to pin the 9.1 version of Rocq in CI for now.

Update: okay, apparently I was wrong - despite rocq-stdlib latest version being 9.1, it is compatible with Rocq 9.2. So upgrading is possible.

[artagnon]

Thanks for this excellent work! It is unfortunately very large and difficult to review. I think since the CI is passing, and since I'm traveling soon until early June, let's just merge this.