We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 5ed5fdc commit 314a175Copy full SHA for 314a175
src/Relation/Nullary/Finite/Setoid.agda
@@ -39,7 +39,7 @@ record FinitelyEnumerable (X : Setoid c ℓ) : Set (c ⊔ ℓ) where
39
size : ℕ
40
srj : Surjection (≡.setoid (Fin size)) X
41
42
-record SubFinitelyEnumerable (X : Setoid c ℓ) c′ ℓ′
+record InjectsIntoFinitelyEnumerable (X : Setoid c ℓ) c′ ℓ′
43
: Set (c ⊔ ℓ ⊔ lsuc (c′ ⊔ ℓ′)) where
44
field
45
Apex : Setoid c′ ℓ′
@@ -48,7 +48,7 @@ record SubFinitelyEnumerable (X : Setoid c ℓ) c′ ℓ′
48
49
open FinitelyEnumerable finitelyEnumerable public
50
51
-record SubfinitelyEnumerable (X : Setoid c ℓ) c′ ℓ′
+record SurjectionFromFinitelyEnumerable (X : Setoid c ℓ) c′ ℓ′
52
53
54
0 commit comments