agda-unimath
agda-unimath copied to clipboard
UniMath
The agda-unimath library
The following is waiting to be defined in `synthetic-homotopy-theory.infinite-complex-projective-space`: - [ ] `ℂP∞` as the `2`-truncation of the `2`-sphere
Private definitions don't expand outside the module in which they are privately defined, so they should not be used, or be used very sparingly.
The following claims are not yet formalized in `foundation.connected-maps`: - [ ] The type `Connected-Map-Into-Truncated-Type l2 k k A` is contractible. and more generally - [ ] The type `Connected-Map-Into-Truncated-Type...
The following remains to be defined in `univalent-combinatorics.unlabeled-rooted-trees`: - [ ] Unlabeled rooted trees
The following remains to be defined in `univalent-combinatorics.repetitions-of-values`: - [ ] The predicate that `f` maps two different elements to the same value
The following claims remain to be formalized in `univalent-combinatorics.partitions`: - [ ] The type of finite partitions of a finite type `X` is equivalent to the type of decidable partitions...
The following is waiting to be formalized in `univalent-combinatorics.ferrers-diagrams`: - [ ] The type of Ferrers diagrams of any finite type is π-finite
The following is waiting to be formalized in `univalent-combinatorics.decidable-equivalence-relations`: - [ ] The number of decidable equivalence relations on a finite type is a Stirling number of the second kind
Show that the map from a pointed `k+1`-element type to the complement of the point is an equivalence
The following claim is waiting to be formalized in `univalent-combinatorics.complements-isolated-points`: - [ ] The map from a pointed `k+1`-element type to the complement of the point is an equivalence
The following claims are waiting to be formalized in `univalent-combinatorics.2-element-types`: - [ ] A map between `2`-element types is an equivalence if and only if its image is the full...