Decrease number of universes

Put Fin in lowest universe and 1 universe for FinSeq.

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

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. *)
 

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).