Encode arity as Fin.t n and get rid of functional extensionality axiom

[olympichek]

Overview

This PR implements a refactoring of Bonak to represent arity using Fin.t n instead of an arbitrary type. This PR adds Vec.v, a representation of vectors as n-length dependent tuples and uses them to encode layers in νSet construction.

We prove various lemmas for them, such as:

vec_nth_map: vec_nth (vec_map f xs) i = f i (vec_nth xs i)

And the extensionality principle:

vec_ext: (forall i, vec_nth xs i = vec_nth ys i) -> xs = ys

The latter replaces the use of functional_extensionality_dep axiom in the proofs of coherences for layers.

The vector module is parameterised over the module type encapsulating the algebra of Σ-types. This generality is added in order to support not only the current implementation limited to h-sets, but also the work-in-progress extension to h-groupoids.

Achievements

This refactoring allows us to make (after also making some opaque lemmas transparent) the SemiSimplicial4 example fully computable, without being stuck on opaque functional_extensionality_dep axiom.

Tradeoffs

Encoding of layers with vectors requires the use of a few additional lemmas in the proofs of coherences. In mkCohLayer and the base case of mkCohPainting we now have to perform a rewrite with vec_nth_map lemma. Similar rewrites are also added to νDgnSet coherences.

For this reason I propose to preserve the original implementation with a function-based encoding of layers in a dedicated branch. If in the future we would like to implement the construction in a more extensional type theory (such as Cubical Agda, where functional extensionality is provable and computable), the original implementation would be useful as a cleaner reference implementation.