Inserting and removing elements in finite sequences

[malarbol]

This PR introduces the following maps for finite sequences:

• (x₀,...xᵢ₋₁,xᵢ,xᵢ₊₁,...,xₙ) ↦ xᵢ;
• (x₀,...xᵢ₋₁,xᵢ,xᵢ₊₁,...,xₙ) ↦ (x₀,...xᵢ₋₁,xᵢ₊₁,...,xₙ);
• xᵢ ↦ (x₀,...xᵢ₋₁,xᵢ₊₁,...,xₙ) ↦ (x₀,...xᵢ₋₁,xᵢ,xᵢ₊₁,...,xₙ);

and the corresponding equivalences Aⁿ⁺¹ ≃ A × Aⁿ:

• (x₀,...xᵢ₋₁,xᵢ,xᵢ₊₁,...,xₙ) ↔ (xᵢ , (x₀,...xᵢ₋₁,xᵢ₊₁,...,xₙ)).

We apply these to the case of finite sequences of types A : Fin n → UU l and define

  Πₙ A = (i : Fin n) → A i ≃ A₀ × A₁ × ... × Aᵢ × ... Aₙ₋₁

to prove that

  Πₙ₊₁ A ≃ Aᵢ × Πₙ Aⁱ

where Aⁱ denotes the finite sequence of types obtained by removing the ith component of A so

Πₙ Aⁱ = A₀ × ... Aᵢ₋₁ × Aᵢ₊ᵢ × ... × Aₙ.