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