agda-unimath
agda-unimath copied to clipboard
Beyond finite sets
This PR adds the following files to the library:
- Foundation
- Symmetric cores of binary relations
- Graph Theory
- The forgetful functor from directed graphs to undirected graphs
- The forgetful functor from undirected graphs to directed graphs
- The undirected core of a directed graph
- Walks in finite undirected graphs
- Group Theory
- Powers of elements in commutative monoids
- Rational commutative monoids
- Trees
- Finite undirected trees
- Univalent combinatorics
- The category of cyclically ordered sets
- Morphisms of cyclic types
- Omega-finite types
- The reduced 1-bordism category
- Symmetric operations
- Unordered pairs of elements of finite types
The topic formalized in this PR were topics of discussion during the Beyond Finite Sets meeting. Results expected to be formalized in this PR are:
- Show that the type of undirected trees with n nodes is pi-finite, and obtain the function that returns for each n the number of unlabeled trees with n nodes
- Equip the 1-bordism category with the structure of a category.