From f8c8ec79bf8e7d04d7a0da670fec79c591111540 Mon Sep 17 00:00:00 2001
From: Andreas Lynge <andreaslyn@gmail.com>
Date: Thu, 25 Mar 2021 00:45:57 +0100
Subject: [PATCH 1/4] Algebra operations

Started work on algebra operations

Added Finite.Vect

Make some definitions monomorphic to fix universe blowup in Finite.FinNat
---
 _CoqProject                            |   2 +
 theories/Algebra/Universal/Operation.v | 219 +++++++++++++++++++++++++
 theories/Spaces/Finite.v               |   3 +-
 theories/Spaces/Finite/Fin.v           |   4 +-
 theories/Spaces/Finite/FinInduction.v  |  28 +++-
 theories/Spaces/Finite/FinNat.v        |  15 +-
 theories/Spaces/Finite/Vect.v          | 212 ++++++++++++++++++++++++
 7 files changed, 467 insertions(+), 16 deletions(-)
 create mode 100644 theories/Algebra/Universal/Operation.v
 create mode 100644 theories/Spaces/Finite/Vect.v

diff --git a/_CoqProject b/_CoqProject
index cad14615b01..65947308672 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -124,6 +124,7 @@ theories/Spaces/Finite/Fin.v
 theories/Spaces/Finite/FinNat.v
 theories/Spaces/Finite/FinInduction.v
 theories/Spaces/Finite/Finite.v
+theories/Spaces/Finite/Vect.v
 theories/Spaces/Finite/Tactics.v
 theories/Spaces/Finite.v
 
@@ -352,6 +353,7 @@ theories/Spectra/Coinductive.v
 
 theories/Algebra/Universal/Algebra.v
 theories/Algebra/Universal/Homomorphism.v
+theories/Algebra/Universal/Operation.v
 
 #
 #   Algebra
diff --git a/theories/Algebra/Universal/Operation.v b/theories/Algebra/Universal/Operation.v
new file mode 100644
index 00000000000..02a944c1696
--- /dev/null
+++ b/theories/Algebra/Universal/Operation.v
@@ -0,0 +1,219 @@
+(** This file continues the development of algebra [Operation]. It
+    gives an way to construct operations using (conventional) curried
+    functions, and shows that such curried operations are equivalent
+    to the uncurried operations [Operation]. *)
+
+Require Export HoTT.Algebra.Universal.Algebra.
+
+Require Import
+  HoTT.Basics
+  HoTT.Types
+  HoTT.DProp
+  HoTT.Spaces.Finite
+  HoTT.Spaces.Nat
+  HoTT.Spaces.Finite.Vect.
+
+Import notations_algebra.
+
+(** Functions [head_dom'] and [head_dom] are used to get the first
+    element of a nonempty operation domain [a : forall i, A (ss i)]. *)
+
+Monomorphic Definition head_dom' {σ} (A : Carriers σ) (n : nat)
+  : forall (N : n > 0) (ss : Vect n (Sort σ)) (a : forall i, A (ss i)),
+    A (vhead' n N ss)
+  := match n with
+     | 0 => fun N ss _ => Empty_rec N
+     | n'.+1 => fun N ss a => a fin_zero
+     end.
+
+Monomorphic Definition head_dom {σ} (A : Carriers σ) {n : nat}
+  (ss : Vect n.+1 (Sort σ)) (a : forall i, A (ss i))
+  : A (vhead ss)
+  := head_dom' A n.+1 tt ss a.
+
+(** Functions [tail_dom'] and [tail_dom] are used to obtain the tail
+    of an operation domain [a : forall i, A (ss i)]. *)
+
+Monomorphic Definition tail_dom' {σ} (A : Carriers σ) (n : nat)
+  : forall (ss : Vect n (Sort σ)) (a : forall i, A (ss i)) (i : Fin (pred n)),
+    A (vtail' n ss i)
+  := match n with
+     | 0 => fun ss _ i => Empty_rec i
+     | n'.+1 => fun ss a i => a (fsucc i)
+     end.
+
+Monomorphic Definition tail_dom {σ} (A : Carriers σ) {n : nat}
+  (ss : Vect n.+1 (Sort σ)) (a : forall i, A (ss i))
+  : forall i, A (vtail ss i)
+  := tail_dom' A n.+1 ss a.
+
+(** Functions [cons_dom'] and [cons_dom] to add an element to
+    the front of a given domain [a : forall i, A (ss i)]. *)
+
+Monomorphic Definition cons_dom' {σ} (A : Carriers σ) {n : nat}
+  : forall (i : Fin n) (ss : Vect n (Sort σ)) (N : n > 0),
+    A (vhead' n N ss) -> (forall i, A (vtail' n ss i)) -> A (ss i)
+  := fin_ind
+      (fun n i =>
+        forall (ss : Fin n -> Sort σ) (N : n > 0),
+        A (vhead' n N ss) -> (forall i, A (vtail' n ss i)) -> A (ss i))
+      (fun n' => fun _ z => match z with tt => fun x _ => x end)
+      (fun n' i' _ => fun _ _ _ xs => xs i').
+
+Definition cons_dom {σ} (A : Carriers σ)
+  {n : nat} (ss : Vect n.+1 (Sort σ))
+  (x : A (vhead ss)) (xs : forall i, A (vtail ss i))
+  : forall i : Fin n.+1, A (ss i)
+  := fun i => cons_dom' A i ss tt x xs.
+
+(** The empty domain: *)
+
+Definition nil_dom {σ} (A : Carriers σ) (ss : Vect 0 (Sort σ))
+  : forall i : Fin 0, A (ss i)
+  := Empty_ind (A o ss).
+
+(** A specialization of [Operation] to finite [Fin n] arity. *)
+
+Definition FiniteOperation {σ : Signature} (A : Carriers σ)
+  {n : nat} (ss : Vect n (Sort σ)) (t : Sort σ) : Type
+  := Operation A {| Arity := Fin n; sorts_dom := ss; sort_cod := t |}.
+
+(** A type of curried operations
+<<
+CurriedOperation A [s1, ..., sn] t := A s1 -> ... -> A sn -> A t.
+>> *)
+
+Fixpoint CurriedOperation {σ} (A : Carriers σ) {n : nat}
+  : (Vect n (Sort σ)) -> Sort σ -> Type
+  := match n with
+     | 0 => fun ss t => A t
+     | n'.+1 =>
+        fun ss t => A (vhead ss) -> CurriedOperation A (vtail ss) t
+     end.
+
+(** Function [operation_uncurry] is used to uncurry an operation
+<<
+operation_uncurry A [s1, ..., sn] t (op : CurriedOperation A [s1, ..., sn] t)
+  : FiniteOperation A [s1, ..., sn] t
+  := fun (x1 : A s1, ..., xn : A xn) => op x1 ... xn
+>>
+See [equiv_operation_curry] below. *)
+
+Fixpoint operation_uncurry {σ} (A : Carriers σ) {n : nat}
+  : forall (ss : Vect n (Sort σ)) (t : Sort σ),
+    CurriedOperation A ss t -> FiniteOperation A ss t
+  := match n with
+     | 0 => fun ss t op _ => op
+     | n'.+1 =>
+        fun ss t op a =>
+          operation_uncurry A (vtail ss) t (op (a fin_zero)) (a o fsucc)
+     end.
+
+Local Example computation_example_operation_uncurry
+  : forall
+      (σ : Signature) (A : Carriers σ) (n : nat) (s1 s2 t : Sort σ)
+      (ss := (vcons s1 (vcons s2 vnil)))
+      (op : CurriedOperation A ss t) (a : forall i, A (ss i)),
+    operation_uncurry A ss t op
+    = fun a => op (a fin_zero) (a (fsucc fin_zero)).
+Proof.
+  reflexivity.
+Qed.
+
+(** Function [operation_curry] is used to curry an operation
+<<
+operation_curry A [s1, ..., sn] t (op : FiniteOperation A [s1, ..., sn] t)
+  : CurriedOperation A [s1, ..., sn] t
+  := fun (x1 : A s1) ... (xn : A xn) => op (x1, ..., xn)
+>>
+See [equiv_operation_curry] below. *)
+
+Fixpoint operation_curry {σ} (A : Carriers σ) {n : nat} 
+  : forall (ss : Vect n (Sort σ)) (t : Sort σ),
+    FiniteOperation A ss t -> CurriedOperation A ss t
+  := match n with
+     | 0 => fun ss t op => op (Empty_ind _)
+     | n'.+1 =>
+        fun ss t op x =>
+          operation_curry A (vtail ss) t (op o cons_dom A ss x)
+     end.
+
+Local Example computation_example_operation_curry
+  : forall
+      (σ : Signature) (A : Carriers σ) (n : nat) (s1 s2 t : Sort σ)
+      (ss := (vcons s1 (vcons s2 vnil)))
+      (op : FiniteOperation A ss t)
+      (x1 : A s1) (x2 : A s2),
+    operation_curry A ss t op
+    = fun x1 x2 => op (cons_dom A ss x1 (cons_dom A _ x2 (nil_dom A _))).
+Proof.
+  reflexivity.
+Qed.
+
+Lemma expand_cons_dom' {σ} (A : Carriers σ) (n : nat)
+  : forall (i : Fin n) (ss : Vect n (Sort σ)) (N : n > 0)
+           (a : forall i, A (ss i)),
+    cons_dom' A i ss N (head_dom' A n N ss a) (tail_dom' A n ss a) = a i.
+Proof.
+  intro i.
+  induction i using fin_ind; intros ss N a.
+  - unfold cons_dom'.
+    rewrite compute_fin_ind_fin_zero.
+    by destruct N.
+  - unfold cons_dom'.
+    by rewrite compute_fin_ind_fsucc.
+Qed.
+
+Lemma expand_cons_dom `{Funext} {σ} (A : Carriers σ)
+  {n : nat} (ss : Vect n.+1 (Sort σ)) (a : forall i, A (ss i))
+  : cons_dom A ss (head_dom A ss a) (tail_dom A ss a) = a.
+Proof.
+  funext i.
+  apply expand_cons_dom'.
+Defined.
+
+Lemma path_operation_curry_to_cunurry `{Funext} {σ} (A : Carriers σ)
+  {n : nat} (ss : Vect n (Sort σ)) (t : Sort σ)
+  : operation_uncurry A ss t o operation_curry A ss t == idmap.
+Proof.
+  intro a.
+  induction n as [| n IHn].
+  - funext d. refine (ap a _). apply path_contr.
+  - funext a'.
+    refine (ap (fun x => x _) (IHn _ _) @ _).
+    refine (ap a _).
+    apply expand_cons_dom.
+Qed.
+
+Lemma path_operation_uncurry_to_curry `{Funext} {σ} (A : Carriers σ)
+  {n : nat} (ss : Vect n (Sort σ)) (t : Sort σ)
+  : operation_curry A ss t o operation_uncurry A ss t == idmap.
+Proof.
+  intro a.
+  induction n; [reflexivity|].
+  funext x.
+  refine (_ @ IHn (vtail ss) (a x)).
+  refine (ap (operation_curry A (vtail ss) t) _).
+  funext a'.
+  simpl.
+  unfold cons_dom, cons_dom'.
+  rewrite compute_fin_ind_fin_zero.
+  refine (ap (operation_uncurry A (vtail ss) t (a x)) _).
+  funext i'.
+  now rewrite compute_fin_ind_fsucc.
+Qed.
+
+Global Instance isequiv_operation_curry `{Funext} {σ} (A : Carriers σ)
+  {n : nat} (ss : Vect n (Sort σ)) (t : Sort σ)
+  : IsEquiv (operation_curry A ss t).
+Proof.
+  srapply isequiv_adjointify.
+  - apply operation_uncurry.
+  - apply path_operation_uncurry_to_curry.
+  - apply path_operation_curry_to_cunurry.
+Defined.
+
+Definition equiv_operation_curry `{Funext} {σ} (A : Carriers σ)
+  {n : nat} (ss : Vect n (Sort σ)) (t : Sort σ)
+  : FiniteOperation A ss t <~> CurriedOperation A ss t
+  := Build_Equiv _ _ (operation_curry A ss t) _.
diff --git a/theories/Spaces/Finite.v b/theories/Spaces/Finite.v
index 7fdecd57d7c..f1c9c0291f8 100644
--- a/theories/Spaces/Finite.v
+++ b/theories/Spaces/Finite.v
@@ -1,4 +1,5 @@
-
 Require Export Finite.Fin.
+Require Export Finite.FinNat.
+Require Export Finite.FinInduction.
 Require Export Finite.Finite.
 Require Export Finite.Tactics.
diff --git a/theories/Spaces/Finite/Fin.v b/theories/Spaces/Finite/Fin.v
index 7af5124f3eb..b3a21480153 100644
--- a/theories/Spaces/Finite/Fin.v
+++ b/theories/Spaces/Finite/Fin.v
@@ -112,14 +112,14 @@ Proof.
     + rewrite path_fin_fsucc_incl, path_nat_fin_incl.
       apply IHn.
     + reflexivity.
-Qed.
+Defined.
 
 Lemma path_nat_fin_zero {n} : fin_to_nat (@fin_zero n) = 0.
 Proof.
   induction n as [|n' IHn].
   - reflexivity.
   - trivial.
-Qed.
+Defined.
 
 Lemma path_nat_fin_last {n} : fin_to_nat (@fin_last n) = n.
 Proof.
diff --git a/theories/Spaces/Finite/FinInduction.v b/theories/Spaces/Finite/FinInduction.v
index 62717c76aae..024a87117e0 100644
--- a/theories/Spaces/Finite/FinInduction.v
+++ b/theories/Spaces/Finite/FinInduction.v
@@ -11,7 +11,7 @@ Definition fin_ind (P : forall n : nat, Fin n -> Type)
   {n : nat} (k : Fin n)
   : P n k.
 Proof.
-  refine (transport (P n) (homot_fin_to_finnat_to_fin k) _).
+  refine (transport (P n) (path_fin_to_finnat_to_fin k) _).
   refine (finnat_ind (fun n u => P n (finnat_to_fin u)) _ _ _).
   - intro. apply z.
   - intros n' u c. apply s. exact c.
@@ -23,7 +23,7 @@ Lemma compute_fin_ind_fin_zero (P : forall n : nat, Fin n -> Type)
   : fin_ind P z s fin_zero = z n.
 Proof.
   unfold fin_ind.
-  generalize (homot_fin_to_finnat_to_fin (@fin_zero n)).
+  generalize (path_fin_to_finnat_to_fin (@fin_zero n)).
   induction (path_fin_to_finnat_fin_zero n)^.
   intro p.
   by induction (hset_path2 1 p).
@@ -36,13 +36,13 @@ Lemma compute_fin_ind_fsucc (P : forall n : nat, Fin n -> Type)
   : fin_ind P z s (fsucc k) = s n k (fin_ind P z s k).
 Proof.
   unfold fin_ind.
-  generalize (homot_fin_to_finnat_to_fin (fsucc k)).
+  generalize (path_fin_to_finnat_to_fin (fsucc k)).
   induction (path_fin_to_finnat_fsucc k)^.
   intro p.
   refine (ap (transport (P n.+1) p) (compute_finnat_ind_succ _ _ _ _) @ _).
   generalize dependent p.
-  induction (homot_fin_to_finnat_to_fin k).
-  induction (homot_fin_to_finnat_to_fin k)^.
+  induction (path_fin_to_finnat_to_fin k).
+  induction (path_fin_to_finnat_to_fin k)^.
   intro p.
   now induction (hset_path2 1 p).
 Defined.
@@ -51,4 +51,20 @@ Definition fin_rec (B : nat -> Type)
   : (forall n : nat, B n.+1) -> (forall (n : nat), Fin n -> B n -> B n.+1) ->
     forall {n : nat}, Fin n -> B n
   := fin_ind (fun n _ => B n).
-  
+
+Lemma compute_fin_rec_fin_zero (B : nat -> Type)
+  (z : forall n : nat, B n.+1)
+  (s : forall (n : nat) (k : Fin n), B n -> B n.+1) (n : nat)
+  : fin_rec B z s fin_zero = z n.
+Proof.
+  apply (compute_fin_ind_fin_zero (fun n _ => B n)).
+Defined.
+
+Lemma compute_fin_rec_fsucc (B : nat -> Type)
+  (z : forall n : nat, B n.+1)
+  (s : forall (n : nat) (k : Fin n), B n -> B n.+1)
+  {n : nat} (k : Fin n)
+  : fin_rec B z s (fsucc k) = s n k (fin_rec B z s k).
+Proof.
+  apply (compute_fin_ind_fsucc (fun n _ => B n)).
+Defined.
diff --git a/theories/Spaces/Finite/FinNat.v b/theories/Spaces/Finite/FinNat.v
index 89a45d19326..934420fe02e 100644
--- a/theories/Spaces/Finite/FinNat.v
+++ b/theories/Spaces/Finite/FinNat.v
@@ -79,7 +79,8 @@ Proof.
                    (hset_path2 1 (@path_succ_finnat n u u.2)) idpath).
 Defined.
 
-Definition is_bounded_fin_to_nat {n} (k : Fin n) : fin_to_nat k < n.
+Monomorphic Definition is_bounded_fin_to_nat {n} (k : Fin n)
+  : fin_to_nat k < n.
 Proof.
   induction n as [| n IHn].
   - elim k.
@@ -90,10 +91,10 @@ Proof.
     + apply leq_refl.
 Defined.
 
-Definition fin_to_finnat {n} (k : Fin n) : FinNat n
+Monomorphic Definition fin_to_finnat {n} (k : Fin n) : FinNat n
   := (fin_to_nat k; is_bounded_fin_to_nat k).
 
-Fixpoint finnat_to_fin {n : nat} : FinNat n -> Fin n
+Monomorphic Fixpoint finnat_to_fin {n : nat} : FinNat n -> Fin n
   := match n with
      | 0 => fun u => Empty_rec u.2
      | n.+1 => fun u =>
@@ -160,7 +161,7 @@ Proof.
   - exact (ap fsucc IHn).
 Defined.
 
-Lemma homot_finnat_to_fin_to_finnat {n : nat} (u : FinNat n)
+Lemma path_finnat_to_fin_to_finnat {n : nat} (u : FinNat n)
   : fin_to_finnat (finnat_to_fin u) = u.
 Proof.
   induction n as [| n IHn].
@@ -173,7 +174,7 @@ Proof.
       exact (ap S (IHn (x; h))..1).
 Defined.
 
-Lemma homot_fin_to_finnat_to_fin {n : nat} (k : Fin n)
+Lemma path_fin_to_finnat_to_fin {n : nat} (k : Fin n)
   : finnat_to_fin (fin_to_finnat k) = k.
 Proof.
   induction n as [| n IHn].
@@ -187,5 +188,5 @@ Defined.
 
 Definition equiv_fin_finnat (n : nat) : Fin n <~> FinNat n
   := equiv_adjointify fin_to_finnat finnat_to_fin
-      homot_finnat_to_fin_to_finnat
-      homot_fin_to_finnat_to_fin.
+      path_finnat_to_fin_to_finnat
+      path_fin_to_finnat_to_fin.
diff --git a/theories/Spaces/Finite/Vect.v b/theories/Spaces/Finite/Vect.v
new file mode 100644
index 00000000000..52c79363acd
--- /dev/null
+++ b/theories/Spaces/Finite/Vect.v
@@ -0,0 +1,212 @@
+Require Import
+  HoTT.Basics
+  HoTT.Types
+  HoTT.HSet
+  HoTT.DProp
+  HoTT.Spaces.Finite.Fin
+  HoTT.Spaces.Finite.FinInduction
+  HoTT.Spaces.Nat.
+
+(** Finite-dimensional vector. Note that the induction principle
+    [vect_ind] uses funext and does not compute. *)
+
+Definition Vect (n : nat) (A : Type) : Type := Fin n -> A.
+
+(** The empty vector. *)
+
+Definition vnil {A : Type} : Vect 0 A := Empty_rec.
+
+Definition path_vnil `{Funext} {A : Type} (v : Vect 0 A) : vnil = v.
+Proof.
+  apply path_contr.
+Defined.
+
+(** Add an element in the end of a vector, [vcons'] and [vcons]. *)
+
+Definition vcons' {A : Type} (n : nat) (a : A) (v : Vect (pred n) A)
+  : Vect n A
+  := fun i =>  fin_rec (fun n => Vect (pred n) A -> A)
+                       (fun _ _ => a) (fun n' i _ v => v i) i v.
+
+Definition vcons {A : Type} {n : nat} : A -> Vect n A -> Vect n.+1 A
+  := vcons' n.+1.
+
+(** Take the first element is a non-empty vector, [vhead'] and [vhead]. *)
+
+Definition vhead' {A} (n : nat) : n > 0 -> Vect n A -> A
+  := match n with
+     | 0 => fun N _ => Empty_rec N
+     | n'.+1 => fun _ v => v fin_zero
+     end.
+
+Definition vhead {A} {n : nat} : Vect n.+1 A -> A := vhead' n.+1 tt.
+
+Definition compute_vhead' {A} n (N : n > 0) (a : A) (v : Vect (pred n) A)
+  : vhead' n N (vcons' n a v) = a.
+Proof.
+  destruct n; [elim N|].
+  exact (apD10 (compute_fin_rec_fin_zero _ _ _ _) v).
+Defined.
+
+Definition compute_vhead {A} {n} (a : A) (v : Vect n A)
+  : vhead (vcons a v) = a.
+Proof.
+  apply compute_vhead'.
+Defined.
+
+(** If the vector is non-empty, then remove the first element. *)
+
+Definition vtail' {A} (n : nat) : Vect n A -> Vect (pred n) A
+  := match n with
+     | 0 => fun _ => Empty_rec
+     | n'.+1 => fun v i => v (fsucc i)
+     end.
+
+(** Remove the first element from a non-empty vector. *)
+
+Definition vtail {A} {n : nat} : Vect n.+1 A -> Vect n A := vtail' n.+1.
+
+Definition compute_vtail' {A} n (a : A) (v : Vect (pred n) A)
+  : vtail' n (vcons' n a v) == v.
+Proof.
+  intro i.
+  destruct n; [elim i|].
+  exact (apD10 (compute_fin_rec_fsucc _ _ _ _) v).
+Defined.
+
+Definition compute_vtail `{Funext} {A} {n} (a : A) (v : Vect n A)
+  : vtail (vcons a v) = v.
+Proof.
+  funext i.
+  apply compute_vtail'.
+Defined.
+
+(** A non-empty vector is the [vcons] of its head and tail,
+    [path_expand_vcons'] and [path_expand_vcons]. *)
+
+Lemma path_expand_vcons' {A : Type} (n : nat)
+  (i : Fin n) (N : n > 0) (v : Vect n A)
+  : vcons' n (vhead' n N v) (vtail' n v) i = v i.
+Proof.
+  induction i using fin_ind.
+  - apply compute_vhead.
+  - apply (compute_vtail' n.+1 (vhead v) (vtail v)).
+Defined.
+
+Lemma path_expand_vcons `{Funext} {A} {n} (v : Vect n.+1 A)
+  : vcons (vhead v) (vtail v) = v.
+Proof.
+  funext i.
+  apply path_expand_vcons'.
+Defined.
+
+(** The following [path_vcons'] and [path_vcons] gives a way to construct
+    a path between [vcons] vectors. They cooperate nicely with
+    [path_expand_vcons'] and [path_expand_vcons]. *)
+
+Definition path_vcons' {A} n {a1 a2 : A} {v1 v2 : Vect (pred n) A}
+  (p : a1 = a2) (q : forall i, v1 i = v2 i) (i : Fin n)
+  : vcons' n a1 v1 i = vcons' n a2 v2 i.
+Proof.
+  induction i using fin_ind.
+  - exact (compute_vhead _ _ @ p @ (compute_vhead _ _)^).
+  - refine (_ @ (compute_vtail' n.+1 a2 v2 i)^).
+    exact (compute_vtail' n.+1 a1 v1 i @ q i).
+Defined.
+
+Definition compute_path_vcons' {A} (n : nat)
+    (a : A) (v : Vect (pred n) A) (i : Fin n)
+    : path_vcons' n (idpath a) (fun j => idpath (v j)) i = idpath.
+Proof.
+  induction i using fin_ind; unfold path_vcons'.
+  - rewrite compute_fin_ind_fin_zero.
+    refine (ap (fun p => p @ _) (concat_p1 _) @ _).
+    apply concat_pV.
+  - rewrite compute_fin_ind_fsucc.
+    refine (ap (fun p => p @ _) (concat_p1 _) @ _).
+    apply concat_pV.
+Qed.
+
+Definition path_vcons `{Funext} {A} {n} {a1 a2 : A} (p : a1 = a2)
+  {v1 v2 : Vect n A} (q : v1 = v2)
+  : vcons a1 v1 = vcons a2 v2.
+Proof.
+  funext i. apply path_vcons'.
+  - assumption.
+  - intro j. exact (apD10 q j).
+Defined.
+
+Lemma compute_path_vcons `{Funext} {A} {n} (a : A) (v : Vect n A)
+  : path_vcons (idpath a) (idpath v) = idpath.
+Proof.
+  refine (ap (path_forall _ _) _ @ eta_path_forall _ _ _).
+  funext i. exact (compute_path_vcons' n.+1 a v i).
+Defined.
+
+(** The lemmas [path_expand_vcons_vcons'] and [path_expand_vcons_vcons]
+    identify [path_expand_vcons'] with [path_vcons'] and
+    [path_expand_vcons] with [path_vcons]. *)
+
+Lemma path_expand_vcons_vcons' {A : Type} (n : nat)
+  (N : n > 0) (a : A) (v : Vect (pred n) A) (i : Fin n)
+  : path_expand_vcons' n i N (vcons' n a v) =
+    path_vcons' n (compute_vhead' n N a v) (compute_vtail' n a v) i.
+Proof.
+  induction i using fin_ind; unfold path_vcons', path_expand_vcons'.
+  - do 2 rewrite compute_fin_ind_fin_zero.
+    refine (_ @ concat_p_pp _ _ _).
+    refine (_ @ (ap (fun p => _ @ p) (concat_pV _))^).
+    exact (concat_p1 _)^.
+  - do 2 rewrite compute_fin_ind_fsucc.
+    refine (_ @ concat_p_pp _ _ _).
+    refine (_ @ (ap (fun p => _ @ p) (concat_pV _))^).
+    exact (concat_p1 _)^.
+Qed.
+
+Lemma path_expand_vcons_vcons `{Funext}
+  {A : Type} {n : nat} (a : A) (v : Vect n A)
+  : path_expand_vcons (vcons a v) =
+    path_vcons (compute_vhead a v) (compute_vtail a v).
+Proof.
+  refine (ap (path_forall _ _) _).
+  funext i.
+  pose (p := eisretr apD10 (compute_vtail' n.+1 a v)).
+  refine (_ @ (ap (fun f => _ f i) p)^).
+  exact (path_expand_vcons_vcons' n.+1 tt a v i).
+Defined.
+
+(** The induction principle for finite dimensional vectors, [vect_ind].
+    Note that it uses funext and does not compute. *)
+
+Lemma vect_ind `{Funext} {A : Type} (P : forall n, Vect n A -> Type)
+  (z : P 0 vnil) (s : forall n a (v : Vect n A), P n v -> P n.+1 (vcons a v))
+  {n : nat} (v : Vect n A)
+  : P n v.
+Proof.
+  induction n.
+  - exact (transport (P 0) (path_vnil v) z).
+  - refine (transport (P n.+1) (path_expand_vcons v) _).
+    apply s. apply IHn.
+Defined.
+
+Lemma compute_vect_ind_vnil `{Funext} {A : Type}
+  (P : forall n, Vect n A -> Type) (z : P 0 vnil)
+  (s : forall (n : nat) (a : A) (v : Vect n A), P n v -> P n.+1 (vcons a v))
+  : vect_ind P z s vnil = z.
+Proof.
+  exact (ap (fun x => _ x z) (hset_path2 1 (path_vnil vnil)))^.
+Defined.
+
+Lemma compute_vect_ind_vcons `{Funext} {A : Type}
+  (P : forall n, Vect n A -> Type) (z : P 0 vnil)
+  (s : forall (n : nat) (a : A) (v : Vect n A), P n v -> P n.+1 (vcons a v))
+  {n : nat} (a : A) (v : Vect n A)
+  : vect_ind P z s (vcons a v) = s n a v (vect_ind P z s v).
+Proof.
+  simpl.
+  induction (path_expand_vcons_vcons a v)^.
+  set (p1 := compute_vhead a v).
+  set (p2 := compute_vtail a v).
+  induction p1, p2.
+  exact (ap (fun p => transport _ p _) (compute_path_vcons _ _)).
+Defined.

From 67be5bc58182902059cd46ebe89cfefc040af981 Mon Sep 17 00:00:00 2001
From: Andreas Lynge <andreaslyn@gmail.com>
Date: Thu, 25 Mar 2021 20:39:24 +0100
Subject: [PATCH 2/4] New line in the end of files and typo

---
 theories/Algebra/Universal/Operation.v | 3 ++-
 theories/Spaces/Finite/Vect.v          | 1 +
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/Algebra/Universal/Operation.v b/theories/Algebra/Universal/Operation.v
index 02a944c1696..2c57052e9ba 100644
--- a/theories/Algebra/Universal/Operation.v
+++ b/theories/Algebra/Universal/Operation.v
@@ -1,5 +1,5 @@
 (** This file continues the development of algebra [Operation]. It
-    gives an way to construct operations using (conventional) curried
+    gives a way to construct operations using (conventional) curried
     functions, and shows that such curried operations are equivalent
     to the uncurried operations [Operation]. *)
 
@@ -217,3 +217,4 @@ Definition equiv_operation_curry `{Funext} {σ} (A : Carriers σ)
   {n : nat} (ss : Vect n (Sort σ)) (t : Sort σ)
   : FiniteOperation A ss t <~> CurriedOperation A ss t
   := Build_Equiv _ _ (operation_curry A ss t) _.
+
diff --git a/theories/Spaces/Finite/Vect.v b/theories/Spaces/Finite/Vect.v
index 52c79363acd..05362ce4080 100644
--- a/theories/Spaces/Finite/Vect.v
+++ b/theories/Spaces/Finite/Vect.v
@@ -210,3 +210,4 @@ Proof.
   induction p1, p2.
   exact (ap (fun p => transport _ p _) (compute_path_vcons _ _)).
 Defined.
+

From 69065463520061944ad1f8f4cb97f8289cca0056 Mon Sep 17 00:00:00 2001
From: Andreas Lynge <andreaslyn@gmail.com>
Date: Thu, 1 Apr 2021 00:00:50 +0200
Subject: [PATCH 3/4] Change Vect to FinSeq

---
 _CoqProject                            |   2 +-
 theories/Algebra/Universal/Operation.v |  66 ++++----
 theories/Spaces/Finite/FinSeq.v        | 217 +++++++++++++++++++++++++
 theories/Spaces/Finite/Vect.v          | 213 ------------------------
 4 files changed, 251 insertions(+), 247 deletions(-)
 create mode 100644 theories/Spaces/Finite/FinSeq.v
 delete mode 100644 theories/Spaces/Finite/Vect.v

diff --git a/_CoqProject b/_CoqProject
index 65947308672..5e726ebd9df 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -124,7 +124,7 @@ theories/Spaces/Finite/Fin.v
 theories/Spaces/Finite/FinNat.v
 theories/Spaces/Finite/FinInduction.v
 theories/Spaces/Finite/Finite.v
-theories/Spaces/Finite/Vect.v
+theories/Spaces/Finite/FinSeq.v
 theories/Spaces/Finite/Tactics.v
 theories/Spaces/Finite.v
 
diff --git a/theories/Algebra/Universal/Operation.v b/theories/Algebra/Universal/Operation.v
index 2c57052e9ba..1f1352e43cc 100644
--- a/theories/Algebra/Universal/Operation.v
+++ b/theories/Algebra/Universal/Operation.v
@@ -11,7 +11,7 @@ Require Import
   HoTT.DProp
   HoTT.Spaces.Finite
   HoTT.Spaces.Nat
-  HoTT.Spaces.Finite.Vect.
+  HoTT.Spaces.Finite.FinSeq.
 
 Import notations_algebra.
 
@@ -19,63 +19,63 @@ Import notations_algebra.
     element of a nonempty operation domain [a : forall i, A (ss i)]. *)
 
 Monomorphic Definition head_dom' {σ} (A : Carriers σ) (n : nat)
-  : forall (N : n > 0) (ss : Vect n (Sort σ)) (a : forall i, A (ss i)),
-    A (vhead' n N ss)
+  : forall (N : n > 0) (ss : FinSeq n (Sort σ)) (a : forall i, A (ss i)),
+    A (fshead' n N ss)
   := match n with
      | 0 => fun N ss _ => Empty_rec N
      | n'.+1 => fun N ss a => a fin_zero
      end.
 
 Monomorphic Definition head_dom {σ} (A : Carriers σ) {n : nat}
-  (ss : Vect n.+1 (Sort σ)) (a : forall i, A (ss i))
-  : A (vhead ss)
+  (ss : FinSeq n.+1 (Sort σ)) (a : forall i, A (ss i))
+  : A (fshead ss)
   := head_dom' A n.+1 tt ss a.
 
 (** Functions [tail_dom'] and [tail_dom] are used to obtain the tail
     of an operation domain [a : forall i, A (ss i)]. *)
 
 Monomorphic Definition tail_dom' {σ} (A : Carriers σ) (n : nat)
-  : forall (ss : Vect n (Sort σ)) (a : forall i, A (ss i)) (i : Fin (pred n)),
-    A (vtail' n ss i)
+  : forall (ss : FinSeq n (Sort σ)) (a : forall i, A (ss i)) (i : Fin (pred n)),
+    A (fstail' n ss i)
   := match n with
      | 0 => fun ss _ i => Empty_rec i
      | n'.+1 => fun ss a i => a (fsucc i)
      end.
 
 Monomorphic Definition tail_dom {σ} (A : Carriers σ) {n : nat}
-  (ss : Vect n.+1 (Sort σ)) (a : forall i, A (ss i))
-  : forall i, A (vtail ss i)
+  (ss : FinSeq n.+1 (Sort σ)) (a : forall i, A (ss i))
+  : forall i, A (fstail ss i)
   := tail_dom' A n.+1 ss a.
 
 (** Functions [cons_dom'] and [cons_dom] to add an element to
     the front of a given domain [a : forall i, A (ss i)]. *)
 
 Monomorphic Definition cons_dom' {σ} (A : Carriers σ) {n : nat}
-  : forall (i : Fin n) (ss : Vect n (Sort σ)) (N : n > 0),
-    A (vhead' n N ss) -> (forall i, A (vtail' n ss i)) -> A (ss i)
+  : forall (i : Fin n) (ss : FinSeq n (Sort σ)) (N : n > 0),
+    A (fshead' n N ss) -> (forall i, A (fstail' n ss i)) -> A (ss i)
   := fin_ind
       (fun n i =>
         forall (ss : Fin n -> Sort σ) (N : n > 0),
-        A (vhead' n N ss) -> (forall i, A (vtail' n ss i)) -> A (ss i))
+        A (fshead' n N ss) -> (forall i, A (fstail' n ss i)) -> A (ss i))
       (fun n' => fun _ z => match z with tt => fun x _ => x end)
       (fun n' i' _ => fun _ _ _ xs => xs i').
 
 Definition cons_dom {σ} (A : Carriers σ)
-  {n : nat} (ss : Vect n.+1 (Sort σ))
-  (x : A (vhead ss)) (xs : forall i, A (vtail ss i))
+  {n : nat} (ss : FinSeq n.+1 (Sort σ))
+  (x : A (fshead ss)) (xs : forall i, A (fstail ss i))
   : forall i : Fin n.+1, A (ss i)
   := fun i => cons_dom' A i ss tt x xs.
 
 (** The empty domain: *)
 
-Definition nil_dom {σ} (A : Carriers σ) (ss : Vect 0 (Sort σ))
+Definition nil_dom {σ} (A : Carriers σ) (ss : FinSeq 0 (Sort σ))
   : forall i : Fin 0, A (ss i)
   := Empty_ind (A o ss).
 
 (** A specialization of [Operation] to finite [Fin n] arity. *)
 
 Definition FiniteOperation {σ : Signature} (A : Carriers σ)
-  {n : nat} (ss : Vect n (Sort σ)) (t : Sort σ) : Type
+  {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ) : Type
   := Operation A {| Arity := Fin n; sorts_dom := ss; sort_cod := t |}.
 
 (** A type of curried operations
@@ -84,11 +84,11 @@ CurriedOperation A [s1, ..., sn] t := A s1 -> ... -> A sn -> A t.
 >> *)
 
 Fixpoint CurriedOperation {σ} (A : Carriers σ) {n : nat}
-  : (Vect n (Sort σ)) -> Sort σ -> Type
+  : (FinSeq n (Sort σ)) -> Sort σ -> Type
   := match n with
      | 0 => fun ss t => A t
      | n'.+1 =>
-        fun ss t => A (vhead ss) -> CurriedOperation A (vtail ss) t
+        fun ss t => A (fshead ss) -> CurriedOperation A (fstail ss) t
      end.
 
 (** Function [operation_uncurry] is used to uncurry an operation
@@ -100,19 +100,19 @@ operation_uncurry A [s1, ..., sn] t (op : CurriedOperation A [s1, ..., sn] t)
 See [equiv_operation_curry] below. *)
 
 Fixpoint operation_uncurry {σ} (A : Carriers σ) {n : nat}
-  : forall (ss : Vect n (Sort σ)) (t : Sort σ),
+  : forall (ss : FinSeq n (Sort σ)) (t : Sort σ),
     CurriedOperation A ss t -> FiniteOperation A ss t
   := match n with
      | 0 => fun ss t op _ => op
      | n'.+1 =>
         fun ss t op a =>
-          operation_uncurry A (vtail ss) t (op (a fin_zero)) (a o fsucc)
+          operation_uncurry A (fstail ss) t (op (a fin_zero)) (a o fsucc)
      end.
 
 Local Example computation_example_operation_uncurry
   : forall
       (σ : Signature) (A : Carriers σ) (n : nat) (s1 s2 t : Sort σ)
-      (ss := (vcons s1 (vcons s2 vnil)))
+      (ss := (fscons s1 (fscons s2 fsnil)))
       (op : CurriedOperation A ss t) (a : forall i, A (ss i)),
     operation_uncurry A ss t op
     = fun a => op (a fin_zero) (a (fsucc fin_zero)).
@@ -129,19 +129,19 @@ operation_curry A [s1, ..., sn] t (op : FiniteOperation A [s1, ..., sn] t)
 See [equiv_operation_curry] below. *)
 
 Fixpoint operation_curry {σ} (A : Carriers σ) {n : nat} 
-  : forall (ss : Vect n (Sort σ)) (t : Sort σ),
+  : forall (ss : FinSeq n (Sort σ)) (t : Sort σ),
     FiniteOperation A ss t -> CurriedOperation A ss t
   := match n with
      | 0 => fun ss t op => op (Empty_ind _)
      | n'.+1 =>
         fun ss t op x =>
-          operation_curry A (vtail ss) t (op o cons_dom A ss x)
+          operation_curry A (fstail ss) t (op o cons_dom A ss x)
      end.
 
 Local Example computation_example_operation_curry
   : forall
       (σ : Signature) (A : Carriers σ) (n : nat) (s1 s2 t : Sort σ)
-      (ss := (vcons s1 (vcons s2 vnil)))
+      (ss := (fscons s1 (fscons s2 fsnil)))
       (op : FiniteOperation A ss t)
       (x1 : A s1) (x2 : A s2),
     operation_curry A ss t op
@@ -151,7 +151,7 @@ Proof.
 Qed.
 
 Lemma expand_cons_dom' {σ} (A : Carriers σ) (n : nat)
-  : forall (i : Fin n) (ss : Vect n (Sort σ)) (N : n > 0)
+  : forall (i : Fin n) (ss : FinSeq n (Sort σ)) (N : n > 0)
            (a : forall i, A (ss i)),
     cons_dom' A i ss N (head_dom' A n N ss a) (tail_dom' A n ss a) = a i.
 Proof.
@@ -165,7 +165,7 @@ Proof.
 Qed.
 
 Lemma expand_cons_dom `{Funext} {σ} (A : Carriers σ)
-  {n : nat} (ss : Vect n.+1 (Sort σ)) (a : forall i, A (ss i))
+  {n : nat} (ss : FinSeq n.+1 (Sort σ)) (a : forall i, A (ss i))
   : cons_dom A ss (head_dom A ss a) (tail_dom A ss a) = a.
 Proof.
   funext i.
@@ -173,7 +173,7 @@ Proof.
 Defined.
 
 Lemma path_operation_curry_to_cunurry `{Funext} {σ} (A : Carriers σ)
-  {n : nat} (ss : Vect n (Sort σ)) (t : Sort σ)
+  {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ)
   : operation_uncurry A ss t o operation_curry A ss t == idmap.
 Proof.
   intro a.
@@ -186,25 +186,25 @@ Proof.
 Qed.
 
 Lemma path_operation_uncurry_to_curry `{Funext} {σ} (A : Carriers σ)
-  {n : nat} (ss : Vect n (Sort σ)) (t : Sort σ)
+  {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ)
   : operation_curry A ss t o operation_uncurry A ss t == idmap.
 Proof.
   intro a.
   induction n; [reflexivity|].
   funext x.
-  refine (_ @ IHn (vtail ss) (a x)).
-  refine (ap (operation_curry A (vtail ss) t) _).
+  refine (_ @ IHn (fstail ss) (a x)).
+  refine (ap (operation_curry A (fstail ss) t) _).
   funext a'.
   simpl.
   unfold cons_dom, cons_dom'.
   rewrite compute_fin_ind_fin_zero.
-  refine (ap (operation_uncurry A (vtail ss) t (a x)) _).
+  refine (ap (operation_uncurry A (fstail ss) t (a x)) _).
   funext i'.
   now rewrite compute_fin_ind_fsucc.
 Qed.
 
 Global Instance isequiv_operation_curry `{Funext} {σ} (A : Carriers σ)
-  {n : nat} (ss : Vect n (Sort σ)) (t : Sort σ)
+  {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ)
   : IsEquiv (operation_curry A ss t).
 Proof.
   srapply isequiv_adjointify.
@@ -214,7 +214,7 @@ Proof.
 Defined.
 
 Definition equiv_operation_curry `{Funext} {σ} (A : Carriers σ)
-  {n : nat} (ss : Vect n (Sort σ)) (t : Sort σ)
+  {n : nat} (ss : FinSeq n (Sort σ)) (t : Sort σ)
   : FiniteOperation A ss t <~> CurriedOperation A ss t
   := Build_Equiv _ _ (operation_curry A ss t) _.
 
diff --git a/theories/Spaces/Finite/FinSeq.v b/theories/Spaces/Finite/FinSeq.v
new file mode 100644
index 00000000000..07c34ed45f3
--- /dev/null
+++ b/theories/Spaces/Finite/FinSeq.v
@@ -0,0 +1,217 @@
+Require Import
+  HoTT.Basics
+  HoTT.Types
+  HoTT.HSet
+  HoTT.DProp
+  HoTT.Spaces.Finite.Fin
+  HoTT.Spaces.Finite.FinInduction
+  HoTT.Spaces.Nat.
+
+(** Finite-dimensional sequence. It is often referred to as vector,
+    but we call it finite sequence [FinSeq] to avoid confusion with
+    vector from linear algebra.
+
+    Note that the induction principle [finseq_]*)
+
+Definition FinSeq (n : nat) (A : Type) : Type := Fin n -> A.
+
+(** The empty finite sequence. *)
+
+Definition fsnil {A : Type} : FinSeq 0 A := Empty_rec.
+
+Definition path_fsnil `{Funext} {A : Type} (v : FinSeq 0 A) : fsnil = v.
+Proof.
+  apply path_contr.
+Defined.
+
+(** Add an element in the end of a finite sequence, [fscons'] and [fscons]. *)
+
+Definition fscons' {A : Type} (n : nat) (a : A) (v : FinSeq (pred n) A)
+  : FinSeq n A
+  := fun i =>  fin_rec (fun n => FinSeq (pred n) A -> A)
+                       (fun _ _ => a) (fun n' i _ v => v i) i v.
+
+Definition fscons {A : Type} {n : nat} : A -> FinSeq n A -> FinSeq n.+1 A
+  := fscons' n.+1.
+
+(** Take the first element of a non-empty finite sequence,
+    [fshead'] and [fshead]. *)
+
+Definition fshead' {A} (n : nat) : n > 0 -> FinSeq n A -> A
+  := match n with
+     | 0 => fun N _ => Empty_rec N
+     | n'.+1 => fun _ v => v fin_zero
+     end.
+
+Definition fshead {A} {n : nat} : FinSeq n.+1 A -> A := fshead' n.+1 tt.
+
+Definition compute_fshead' {A} n (N : n > 0) (a : A) (v : FinSeq (pred n) A)
+  : fshead' n N (fscons' n a v) = a.
+Proof.
+  destruct n; [elim N|].
+  exact (apD10 (compute_fin_rec_fin_zero _ _ _ _) v).
+Defined.
+
+Definition compute_fshead {A} {n} (a : A) (v : FinSeq n A)
+  : fshead (fscons a v) = a.
+Proof.
+  apply compute_fshead'.
+Defined.
+
+(** If the sequence is non-empty, then remove the first element. *)
+
+Definition fstail' {A} (n : nat) : FinSeq n A -> FinSeq (pred n) A
+  := match n with
+     | 0 => fun _ => Empty_rec
+     | n'.+1 => fun v i => v (fsucc i)
+     end.
+
+(** Remove the first element from a non-empty sequence. *)
+
+Definition fstail {A} {n : nat} : FinSeq n.+1 A -> FinSeq n A := fstail' n.+1.
+
+Definition compute_fstail' {A} n (a : A) (v : FinSeq (pred n) A)
+  : fstail' n (fscons' n a v) == v.
+Proof.
+  intro i.
+  destruct n; [elim i|].
+  exact (apD10 (compute_fin_rec_fsucc _ _ _ _) v).
+Defined.
+
+Definition compute_fstail `{Funext} {A} {n} (a : A) (v : FinSeq n A)
+  : fstail (fscons a v) = v.
+Proof.
+  funext i.
+  apply compute_fstail'.
+Defined.
+
+(** A non-empty finite sequence is equal to [fscons] of head and tail,
+    [path_expand_fscons'] and [path_expand_fscons]. *)
+
+Lemma path_expand_fscons' {A : Type} (n : nat)
+  (i : Fin n) (N : n > 0) (v : FinSeq n A)
+  : fscons' n (fshead' n N v) (fstail' n v) i = v i.
+Proof.
+  induction i using fin_ind.
+  - apply compute_fshead.
+  - apply (compute_fstail' n.+1 (fshead v) (fstail v)).
+Defined.
+
+Lemma path_expand_fscons `{Funext} {A} {n} (v : FinSeq n.+1 A)
+  : fscons (fshead v) (fstail v) = v.
+Proof.
+  funext i.
+  apply path_expand_fscons'.
+Defined.
+
+(** The following [path_fscons'] and [path_fscons] gives a way to construct
+    a path between [fscons] finite sequences. They cooperate nicely with
+    [path_expand_fscons'] and [path_expand_fscons]. *)
+
+Definition path_fscons' {A} n {a1 a2 : A} {v1 v2 : FinSeq (pred n) A}
+  (p : a1 = a2) (q : forall i, v1 i = v2 i) (i : Fin n)
+  : fscons' n a1 v1 i = fscons' n a2 v2 i.
+Proof.
+  induction i using fin_ind.
+  - exact (compute_fshead _ _ @ p @ (compute_fshead _ _)^).
+  - refine (_ @ (compute_fstail' n.+1 a2 v2 i)^).
+    exact (compute_fstail' n.+1 a1 v1 i @ q i).
+Defined.
+
+Definition compute_path_fscons' {A} (n : nat)
+    (a : A) (v : FinSeq (pred n) A) (i : Fin n)
+    : path_fscons' n (idpath a) (fun j => idpath (v j)) i = idpath.
+Proof.
+  induction i using fin_ind; unfold path_fscons'.
+  - rewrite compute_fin_ind_fin_zero.
+    refine (ap (fun p => p @ _) (concat_p1 _) @ _).
+    apply concat_pV.
+  - rewrite compute_fin_ind_fsucc.
+    refine (ap (fun p => p @ _) (concat_p1 _) @ _).
+    apply concat_pV.
+Qed.
+
+Definition path_fscons `{Funext} {A} {n} {a1 a2 : A} (p : a1 = a2)
+  {v1 v2 : FinSeq n A} (q : v1 = v2)
+  : fscons a1 v1 = fscons a2 v2.
+Proof.
+  funext i. apply path_fscons'.
+  - assumption.
+  - intro j. exact (apD10 q j).
+Defined.
+
+Lemma compute_path_fscons `{Funext} {A} {n} (a : A) (v : FinSeq n A)
+  : path_fscons (idpath a) (idpath v) = idpath.
+Proof.
+  refine (ap (path_forall _ _) _ @ eta_path_forall _ _ _).
+  funext i. exact (compute_path_fscons' n.+1 a v i).
+Defined.
+
+(** The lemmas [path_expand_fscons_fscons'] and [path_expand_fscons_fscons]
+    identify [path_expand_fscons'] with [path_fscons'] and
+    [path_expand_fscons] with [path_fscons]. *)
+
+Lemma path_expand_fscons_fscons' {A : Type} (n : nat)
+  (N : n > 0) (a : A) (v : FinSeq (pred n) A) (i : Fin n)
+  : path_expand_fscons' n i N (fscons' n a v) =
+    path_fscons' n (compute_fshead' n N a v) (compute_fstail' n a v) i.
+Proof.
+  induction i using fin_ind; unfold path_fscons', path_expand_fscons'.
+  - do 2 rewrite compute_fin_ind_fin_zero.
+    refine (_ @ concat_p_pp _ _ _).
+    refine (_ @ (ap (fun p => _ @ p) (concat_pV _))^).
+    exact (concat_p1 _)^.
+  - do 2 rewrite compute_fin_ind_fsucc.
+    refine (_ @ concat_p_pp _ _ _).
+    refine (_ @ (ap (fun p => _ @ p) (concat_pV _))^).
+    exact (concat_p1 _)^.
+Qed.
+
+Lemma path_expand_fscons_fscons `{Funext}
+  {A : Type} {n : nat} (a : A) (v : FinSeq n A)
+  : path_expand_fscons (fscons a v) =
+    path_fscons (compute_fshead a v) (compute_fstail a v).
+Proof.
+  refine (ap (path_forall _ _) _).
+  funext i.
+  pose (p := eisretr apD10 (compute_fstail' n.+1 a v)).
+  refine (_ @ (ap (fun f => _ f i) p)^).
+  exact (path_expand_fscons_fscons' n.+1 tt a v i).
+Defined.
+
+(** The induction principle for finite sequence, [finseq_ind].
+    Note that it uses funext and does not compute. *)
+
+Lemma finseq_ind `{Funext} {A : Type} (P : forall n, FinSeq n A -> Type)
+  (z : P 0 fsnil) (s : forall n a (v : FinSeq n A), P n v -> P n.+1 (fscons a v))
+  {n : nat} (v : FinSeq n A)
+  : P n v.
+Proof.
+  induction n.
+  - exact (transport (P 0) (path_fsnil v) z).
+  - refine (transport (P n.+1) (path_expand_fscons v) _).
+    apply s. apply IHn.
+Defined.
+
+Lemma compute_finseq_ind_fsnil `{Funext} {A : Type}
+  (P : forall n, FinSeq n A -> Type) (z : P 0 fsnil)
+  (s : forall (n : nat) (a : A) (v : FinSeq n A), P n v -> P n.+1 (fscons a v))
+  : finseq_ind P z s fsnil = z.
+Proof.
+  exact (ap (fun x => _ x z) (hset_path2 1 (path_fsnil fsnil)))^.
+Defined.
+
+Lemma compute_finseq_ind_fscons `{Funext} {A : Type}
+  (P : forall n, FinSeq n A -> Type) (z : P 0 fsnil)
+  (s : forall (n : nat) (a : A) (v : FinSeq n A), P n v -> P n.+1 (fscons a v))
+  {n : nat} (a : A) (v : FinSeq n A)
+  : finseq_ind P z s (fscons a v) = s n a v (finseq_ind P z s v).
+Proof.
+  simpl.
+  induction (path_expand_fscons_fscons a v)^.
+  set (p1 := compute_fshead a v).
+  set (p2 := compute_fstail a v).
+  induction p1, p2.
+  exact (ap (fun p => transport _ p _) (compute_path_fscons _ _)).
+Defined.
+
diff --git a/theories/Spaces/Finite/Vect.v b/theories/Spaces/Finite/Vect.v
deleted file mode 100644
index 05362ce4080..00000000000
--- a/theories/Spaces/Finite/Vect.v
+++ /dev/null
@@ -1,213 +0,0 @@
-Require Import
-  HoTT.Basics
-  HoTT.Types
-  HoTT.HSet
-  HoTT.DProp
-  HoTT.Spaces.Finite.Fin
-  HoTT.Spaces.Finite.FinInduction
-  HoTT.Spaces.Nat.
-
-(** Finite-dimensional vector. Note that the induction principle
-    [vect_ind] uses funext and does not compute. *)
-
-Definition Vect (n : nat) (A : Type) : Type := Fin n -> A.
-
-(** The empty vector. *)
-
-Definition vnil {A : Type} : Vect 0 A := Empty_rec.
-
-Definition path_vnil `{Funext} {A : Type} (v : Vect 0 A) : vnil = v.
-Proof.
-  apply path_contr.
-Defined.
-
-(** Add an element in the end of a vector, [vcons'] and [vcons]. *)
-
-Definition vcons' {A : Type} (n : nat) (a : A) (v : Vect (pred n) A)
-  : Vect n A
-  := fun i =>  fin_rec (fun n => Vect (pred n) A -> A)
-                       (fun _ _ => a) (fun n' i _ v => v i) i v.
-
-Definition vcons {A : Type} {n : nat} : A -> Vect n A -> Vect n.+1 A
-  := vcons' n.+1.
-
-(** Take the first element is a non-empty vector, [vhead'] and [vhead]. *)
-
-Definition vhead' {A} (n : nat) : n > 0 -> Vect n A -> A
-  := match n with
-     | 0 => fun N _ => Empty_rec N
-     | n'.+1 => fun _ v => v fin_zero
-     end.
-
-Definition vhead {A} {n : nat} : Vect n.+1 A -> A := vhead' n.+1 tt.
-
-Definition compute_vhead' {A} n (N : n > 0) (a : A) (v : Vect (pred n) A)
-  : vhead' n N (vcons' n a v) = a.
-Proof.
-  destruct n; [elim N|].
-  exact (apD10 (compute_fin_rec_fin_zero _ _ _ _) v).
-Defined.
-
-Definition compute_vhead {A} {n} (a : A) (v : Vect n A)
-  : vhead (vcons a v) = a.
-Proof.
-  apply compute_vhead'.
-Defined.
-
-(** If the vector is non-empty, then remove the first element. *)
-
-Definition vtail' {A} (n : nat) : Vect n A -> Vect (pred n) A
-  := match n with
-     | 0 => fun _ => Empty_rec
-     | n'.+1 => fun v i => v (fsucc i)
-     end.
-
-(** Remove the first element from a non-empty vector. *)
-
-Definition vtail {A} {n : nat} : Vect n.+1 A -> Vect n A := vtail' n.+1.
-
-Definition compute_vtail' {A} n (a : A) (v : Vect (pred n) A)
-  : vtail' n (vcons' n a v) == v.
-Proof.
-  intro i.
-  destruct n; [elim i|].
-  exact (apD10 (compute_fin_rec_fsucc _ _ _ _) v).
-Defined.
-
-Definition compute_vtail `{Funext} {A} {n} (a : A) (v : Vect n A)
-  : vtail (vcons a v) = v.
-Proof.
-  funext i.
-  apply compute_vtail'.
-Defined.
-
-(** A non-empty vector is the [vcons] of its head and tail,
-    [path_expand_vcons'] and [path_expand_vcons]. *)
-
-Lemma path_expand_vcons' {A : Type} (n : nat)
-  (i : Fin n) (N : n > 0) (v : Vect n A)
-  : vcons' n (vhead' n N v) (vtail' n v) i = v i.
-Proof.
-  induction i using fin_ind.
-  - apply compute_vhead.
-  - apply (compute_vtail' n.+1 (vhead v) (vtail v)).
-Defined.
-
-Lemma path_expand_vcons `{Funext} {A} {n} (v : Vect n.+1 A)
-  : vcons (vhead v) (vtail v) = v.
-Proof.
-  funext i.
-  apply path_expand_vcons'.
-Defined.
-
-(** The following [path_vcons'] and [path_vcons] gives a way to construct
-    a path between [vcons] vectors. They cooperate nicely with
-    [path_expand_vcons'] and [path_expand_vcons]. *)
-
-Definition path_vcons' {A} n {a1 a2 : A} {v1 v2 : Vect (pred n) A}
-  (p : a1 = a2) (q : forall i, v1 i = v2 i) (i : Fin n)
-  : vcons' n a1 v1 i = vcons' n a2 v2 i.
-Proof.
-  induction i using fin_ind.
-  - exact (compute_vhead _ _ @ p @ (compute_vhead _ _)^).
-  - refine (_ @ (compute_vtail' n.+1 a2 v2 i)^).
-    exact (compute_vtail' n.+1 a1 v1 i @ q i).
-Defined.
-
-Definition compute_path_vcons' {A} (n : nat)
-    (a : A) (v : Vect (pred n) A) (i : Fin n)
-    : path_vcons' n (idpath a) (fun j => idpath (v j)) i = idpath.
-Proof.
-  induction i using fin_ind; unfold path_vcons'.
-  - rewrite compute_fin_ind_fin_zero.
-    refine (ap (fun p => p @ _) (concat_p1 _) @ _).
-    apply concat_pV.
-  - rewrite compute_fin_ind_fsucc.
-    refine (ap (fun p => p @ _) (concat_p1 _) @ _).
-    apply concat_pV.
-Qed.
-
-Definition path_vcons `{Funext} {A} {n} {a1 a2 : A} (p : a1 = a2)
-  {v1 v2 : Vect n A} (q : v1 = v2)
-  : vcons a1 v1 = vcons a2 v2.
-Proof.
-  funext i. apply path_vcons'.
-  - assumption.
-  - intro j. exact (apD10 q j).
-Defined.
-
-Lemma compute_path_vcons `{Funext} {A} {n} (a : A) (v : Vect n A)
-  : path_vcons (idpath a) (idpath v) = idpath.
-Proof.
-  refine (ap (path_forall _ _) _ @ eta_path_forall _ _ _).
-  funext i. exact (compute_path_vcons' n.+1 a v i).
-Defined.
-
-(** The lemmas [path_expand_vcons_vcons'] and [path_expand_vcons_vcons]
-    identify [path_expand_vcons'] with [path_vcons'] and
-    [path_expand_vcons] with [path_vcons]. *)
-
-Lemma path_expand_vcons_vcons' {A : Type} (n : nat)
-  (N : n > 0) (a : A) (v : Vect (pred n) A) (i : Fin n)
-  : path_expand_vcons' n i N (vcons' n a v) =
-    path_vcons' n (compute_vhead' n N a v) (compute_vtail' n a v) i.
-Proof.
-  induction i using fin_ind; unfold path_vcons', path_expand_vcons'.
-  - do 2 rewrite compute_fin_ind_fin_zero.
-    refine (_ @ concat_p_pp _ _ _).
-    refine (_ @ (ap (fun p => _ @ p) (concat_pV _))^).
-    exact (concat_p1 _)^.
-  - do 2 rewrite compute_fin_ind_fsucc.
-    refine (_ @ concat_p_pp _ _ _).
-    refine (_ @ (ap (fun p => _ @ p) (concat_pV _))^).
-    exact (concat_p1 _)^.
-Qed.
-
-Lemma path_expand_vcons_vcons `{Funext}
-  {A : Type} {n : nat} (a : A) (v : Vect n A)
-  : path_expand_vcons (vcons a v) =
-    path_vcons (compute_vhead a v) (compute_vtail a v).
-Proof.
-  refine (ap (path_forall _ _) _).
-  funext i.
-  pose (p := eisretr apD10 (compute_vtail' n.+1 a v)).
-  refine (_ @ (ap (fun f => _ f i) p)^).
-  exact (path_expand_vcons_vcons' n.+1 tt a v i).
-Defined.
-
-(** The induction principle for finite dimensional vectors, [vect_ind].
-    Note that it uses funext and does not compute. *)
-
-Lemma vect_ind `{Funext} {A : Type} (P : forall n, Vect n A -> Type)
-  (z : P 0 vnil) (s : forall n a (v : Vect n A), P n v -> P n.+1 (vcons a v))
-  {n : nat} (v : Vect n A)
-  : P n v.
-Proof.
-  induction n.
-  - exact (transport (P 0) (path_vnil v) z).
-  - refine (transport (P n.+1) (path_expand_vcons v) _).
-    apply s. apply IHn.
-Defined.
-
-Lemma compute_vect_ind_vnil `{Funext} {A : Type}
-  (P : forall n, Vect n A -> Type) (z : P 0 vnil)
-  (s : forall (n : nat) (a : A) (v : Vect n A), P n v -> P n.+1 (vcons a v))
-  : vect_ind P z s vnil = z.
-Proof.
-  exact (ap (fun x => _ x z) (hset_path2 1 (path_vnil vnil)))^.
-Defined.
-
-Lemma compute_vect_ind_vcons `{Funext} {A : Type}
-  (P : forall n, Vect n A -> Type) (z : P 0 vnil)
-  (s : forall (n : nat) (a : A) (v : Vect n A), P n v -> P n.+1 (vcons a v))
-  {n : nat} (a : A) (v : Vect n A)
-  : vect_ind P z s (vcons a v) = s n a v (vect_ind P z s v).
-Proof.
-  simpl.
-  induction (path_expand_vcons_vcons a v)^.
-  set (p1 := compute_vhead a v).
-  set (p2 := compute_vtail a v).
-  induction p1, p2.
-  exact (ap (fun p => transport _ p _) (compute_path_vcons _ _)).
-Defined.
-

From 71370296b2a2a086c59d085cba9af1e326cb978c Mon Sep 17 00:00:00 2001
From: Andreas Lynge <andreaslyn@gmail.com>
Date: Fri, 2 Apr 2021 20:06:37 +0200
Subject: [PATCH 4/4] Decrease number of universes

Put Fin in lowest universe and 1 universe for FinSeq.
---
 theories/Spaces/Finite/Fin.v    | 2 +-
 theories/Spaces/Finite/FinSeq.v | 2 +-
 theories/Spaces/Finite/Finite.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/Spaces/Finite/Fin.v b/theories/Spaces/Finite/Fin.v
index b3a21480153..ea16cef1a8b 100644
--- a/theories/Spaces/Finite/Fin.v
+++ b/theories/Spaces/Finite/Fin.v
@@ -15,7 +15,7 @@ Local Open Scope nat_scope.
 
 (** A *finite set* is a type that is merely equivalent to the canonical finite set determined by some natural number.  There are many equivalent ways to define the canonical finite sets, such as [{ k : nat & k < n}]; we instead choose a recursive one. *)
 
-Fixpoint Fin (n : nat) : Type
+Fixpoint Fin (n : nat) : Type0
   := match n with
        | 0 => Empty
        | S n => Fin n + Unit
diff --git a/theories/Spaces/Finite/FinSeq.v b/theories/Spaces/Finite/FinSeq.v
index 07c34ed45f3..8a4b858fe40 100644
--- a/theories/Spaces/Finite/FinSeq.v
+++ b/theories/Spaces/Finite/FinSeq.v
@@ -13,7 +13,7 @@ Require Import
 
     Note that the induction principle [finseq_]*)
 
-Definition FinSeq (n : nat) (A : Type) : Type := Fin n -> A.
+Definition FinSeq@{u} (n : nat) (A : Type@{u}) : Type@{u} := Fin n -> A.
 
 (** The empty finite sequence. *)
 
diff --git a/theories/Spaces/Finite/Finite.v b/theories/Spaces/Finite/Finite.v
index 347c4314ee5..105efc519ef 100644
--- a/theories/Spaces/Finite/Finite.v
+++ b/theories/Spaces/Finite/Finite.v
@@ -686,7 +686,7 @@ Qed.
 
 (** A function from [nat] to a finite set must repeat itself eventually. *)
 Section Enumeration.
-  Context `{Funext} {X} `{Finite X} (e : nat -> X).
+  Context `{Funext} {X} `{Finite@{_ Set _} X} (e : nat -> X).
 
   Let er (n : nat) : Fin n -> X
     := fun k => e (nat_fin n k).