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 c1eb427 commit fa0e4c6Copy full SHA for fa0e4c6
src/univalent-combinatorics/finitely-enumerable-types.lagda.md
@@ -51,7 +51,7 @@ open import univalent-combinatorics.surjective-maps
51
## Idea
52
53
A type `X` is
54
-{{#concept "finitely enumerable" disambiguation="type" Agda=finitely-enumerable-type}}
+{{#concept "finitely enumerable" disambiguation="type" Agda=is-finitely-enumerable}}
55
if there [exists](foundation.existential-quantification.md) an `n : ℕ` and a
56
[surjection](foundation.surjective-maps.md) from `Fin n → X`.
57
0 commit comments