From e168a27b99bf609a3d9ae1d2cc866db9f7726c8c Mon Sep 17 00:00:00 2001
From: Sofia-Insa <sofia.el_boufi--crouzet@insa-rouen.fr>
Date: Thu, 22 Jun 2023 14:54:48 -0400
Subject: [PATCH 1/3] Upload file `Relation.Unary.Enumerable` to stdlib

Definition of enumerability in `Relation.Unary.Enumerable`
---
 CHANGELOG.md                       | 11 +++++++++++
 src/Relation/Unary/Enumerable.agda | 20 ++++++++++++++++++++
 2 files changed, 31 insertions(+)
 create mode 100644 src/Relation/Unary/Enumerable.agda

diff --git a/CHANGELOG.md b/CHANGELOG.md
index a2e132acff..f1f0f3f7c8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1595,6 +1595,12 @@ New modules
   ```
   Algebra.Properties.KleeneAlgebra
   ```
+
+* Definition of Enumerability 
+  ```
+  Relation.Unary.Enumerable
+  ```
+
 Other minor changes
 -------------------
 
@@ -2665,6 +2671,11 @@ Other minor changes
   ⊆-trans : Trans _⊆_ _⊆_ _⊆_
   ```
 
+* Added new definition to `Relation.Unary.Enumerable` :
+  ```
+  record IsEnumerable (X : Set x) : Set x 
+  ```
+
 * Added new proofs in `Relation.Binary.Properties.Setoid`:
   ```
   ≈-isPreorder     : IsPreorder _≈_ _≈_
diff --git a/src/Relation/Unary/Enumerable.agda b/src/Relation/Unary/Enumerable.agda
new file mode 100644
index 0000000000..7312fa6a2c
--- /dev/null
+++ b/src/Relation/Unary/Enumerable.agda
@@ -0,0 +1,20 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Definition of enumerability 
+------------------------------------------------------------------------
+
+{-# OPTIONS --cubical-compatible --safe #-}
+
+module Relation.Unary.Enumerable where
+
+  open import Data.Fin using (Fin)
+  open import Data.Nat using (ℕ)
+  open import Level using (Level)
+  open import Function.Bundles using (_↔_)
+
+  record IsEnumerable {x : Level} (X : Set x) : Set x where 
+      field
+        size : ℕ
+        enum : Fin size ↔ X
+

From 256702e8430719dd3473727659606a06261a787c Mon Sep 17 00:00:00 2001
From: Sofia-Insa <sofia.el_boufi--crouzet@insa-rouen.fr>
Date: Thu, 22 Jun 2023 15:05:52 -0400
Subject: [PATCH 2/3] Upload file  to stdlib

---
 src/Relation/Unary/Enumerable.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Relation/Unary/Enumerable.agda b/src/Relation/Unary/Enumerable.agda
index 7312fa6a2c..70896e5c59 100644
--- a/src/Relation/Unary/Enumerable.agda
+++ b/src/Relation/Unary/Enumerable.agda
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Definition of enumerability 
+-- Enumerable definition 
 ------------------------------------------------------------------------
 
 {-# OPTIONS --cubical-compatible --safe #-}

From 07ac2b340406d95339c48a62d0f74ff9f27c64b4 Mon Sep 17 00:00:00 2001
From: Sofia-Insa <sofia.el_boufi--crouzet@insa-rouen.fr>
Date: Thu, 22 Jun 2023 15:15:28 -0400
Subject: [PATCH 3/3] Upload Relation.Unary.Enumerable (with correct syntaxe)
 to stdlib

---
 CHANGELOG.md                       | 2 +-
 src/Relation/Unary/Enumerable.agda | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 2bf601ad88..959b215602 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2766,7 +2766,7 @@ Other minor changes
 
 * Added new definition to `Relation.Unary.Enumerable` :
   ```
-  record IsEnumerable (X : Set x) : Set x 
+  record IsEnumerable (A : Set a) : Set a 
   ```
 
 * Added new proofs in `Relation.Binary.Properties.Setoid`:
diff --git a/src/Relation/Unary/Enumerable.agda b/src/Relation/Unary/Enumerable.agda
index 70896e5c59..c1996faa1d 100644
--- a/src/Relation/Unary/Enumerable.agda
+++ b/src/Relation/Unary/Enumerable.agda
@@ -13,8 +13,8 @@ module Relation.Unary.Enumerable where
   open import Level using (Level)
   open import Function.Bundles using (_↔_)
 
-  record IsEnumerable {x : Level} (X : Set x) : Set x where 
+  record IsEnumerable {a : Level} (A : Set a) : Set a where 
       field
         size : ℕ
-        enum : Fin size ↔ X
+        enum : Fin size ↔ A