StronglyFinite

Author: Saransh-cpp

src/Relation/Nullary/Finite/Setoid.agda

@@ -111,10 +111,9 @@ include-/ {X = X} R = record
   open Setoid X
   open EquivalenceRelation R
 
-record StrictlyFinite (X : Setoid c ℓ) : Set (c ⊔ ℓ) where
+record StronglyFinite (X : Setoid c ℓ) (n : ℕ) : Set (c ⊔ ℓ) where
   field
-    size : ℕ
-    inv : Inverse X (≡.setoid (Fin size))
+    inv : Inverse X (≡.setoid (Fin n))
 
 record Subfinite (X : Setoid c ℓ) : Set (c ⊔ ℓ) where
   field