Upload file Relation.Unary.Enumerable to stdlib

CHANGELOG.md

@@ -1682,6 +1682,10 @@ New modules
   Algebra.Properties.KleeneAlgebra
   ```
 
+* Definition of Enumerability 
+  ```
+  Relation.Unary.Enumerable
+
 * Relations on indexed sets
   ```
   Function.Indexed.Bundles
@@ -2760,6 +2764,11 @@ Other minor changes
   ⊆-trans : Trans _⊆_ _⊆_ _⊆_
   ```
 
+* Added new definition to `Relation.Unary.Enumerable` :
+  ```
+  record IsEnumerable (A : Set a) : Set a 
+  ```
+
 * Added new proofs in `Relation.Binary.Properties.Setoid`:
   ```
   ≈-isPreorder     : IsPreorder _≈_ _≈_

src/Relation/Unary/Enumerable.agda

@@ -0,0 +1,20 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Enumerable definition 
+------------------------------------------------------------------------
+
+{-# 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 {a : Level} (A : Set a) : Set a where 
+      field
+        size : ℕ
+        enum : Fin size ↔ A
+