1. Overview
  2. 1. Overview
    ❱
    1. 1.1. Home
    2. 1.2. Community
      ❱
      1. 1.2.1. Maintainers
      2. 1.2.2. Contributors
      3. 1.2.3. Statement of inclusivity
      4. 1.2.4. Projects using Agda-Unimath
      5. 1.2.5. Grant acknowledgements
    3. 1.3. Guides
      ❱
      1. 1.3.1. Installing the library
      2. 1.3.2. Design principles
      3. 1.3.3. Contributing to the library
      4. 1.3.4. Structuring your file
        ❱
        1. 1.3.4.1. File template
      5. 1.3.5. The library coding style
      6. 1.3.6. Guidelines for mixfix operators
      7. 1.3.7. Citing the library
    4. 1.4. Library contents
    5. 1.5. Art
  3. The agda-unimath library
  4. 2. Category theory
    ❱
    1. 2.1. Adjunctions between large precategories
    2. 2.2. Anafunctors between categories
    3. 2.3. Anafunctors between precategories
    4. 2.4. Categories
    5. 2.5. The category of functors and natural transformations between two categories
    6. 2.6. The category of functors and natural transformations from small to large categories
    7. 2.7. The category of maps and natural transformations between two categories
    8. 2.8. The category of maps and natural transformations from small to large categories
    9. 2.9. Commuting squares of morphisms in large precategories
    10. 2.10. Commuting squares of morphisms in precategories
    11. 2.11. Coproducts in precategories
    12. 2.12. Dependent products of categories
    13. 2.13. Dependent products of large categories
    14. 2.14. Dependent products of large precategories
    15. 2.15. Dependent products of precategories
    16. 2.16. Discrete categories
    17. 2.17. Endomorphisms in categories
    18. 2.18. Endomorphisms in precategories
    19. 2.19. Epimorphism in large precategories
    20. 2.20. Equivalences between categories
    21. 2.21. Equivalences between large precategories
    22. 2.22. Equivalences between precategories
    23. 2.23. Exponential objects in precategories
    24. 2.24. Faithful functors between precategories
    25. 2.25. Full large subcategories
    26. 2.26. Full large subprecategories
    27. 2.27. Function categories
    28. 2.28. Function precategories
    29. 2.29. Functors between categories
    30. 2.30. Functors from small to large categories
    31. 2.31. Functors from small to large precategories
    32. 2.32. Functors between large precategories
    33. 2.33. Functors between precategories
    34. 2.34. Groupoids
    35. 2.35. Homotopies of natural transformations in large precategories
    36. 2.36. Initial objects of large categories
    37. 2.37. Initial objects of large precategories
    38. 2.38. Initial objects in a precategory
    39. 2.39. Isomorphisms in categories
    40. 2.40. Isomorphisms in large categories
    41. 2.41. Isomorphisms in large precategories
    42. 2.42. Isomorphisms in precategories
    43. 2.43. Large categories
    44. 2.44. Large function categories
    45. 2.45. Large function precategories
    46. 2.46. Large precategories
    47. 2.47. Large subcategories
    48. 2.48. Large subprecategories
    49. 2.49. Maps between categories
    50. 2.50. Maps from small to large categories
    51. 2.51. Maps from small to large precategories
    52. 2.52. Maps between precategories
    53. 2.53. Monomorphisms in large precategories
    54. 2.54. Natural isomorphisms between functors between categories
    55. 2.55. Natural isomorphisms between functors between large precategories
    56. 2.56. Natural isomorphisms between functors between precategories
    57. 2.57. Natural isomorphisms between maps between categories
    58. 2.58. Natural isomorphisms between maps between precategories
    59. 2.59. Natural numbers object in a precategory
    60. 2.60. Natural transformations between functors between categories
    61. 2.61. Natural transformations between functors from small to large precategories
    62. 2.62. Natural transformations between functors between large precategories
    63. 2.63. Natural transformations between functors between precategories
    64. 2.64. Natural transformations between maps between categories
    65. 2.65. Natural transformations between maps from small to large precategories
    66. 2.66. Natural transformations between maps between precategories
    67. 2.67. One object precategories
    68. 2.68. Opposite precategories
    69. 2.69. Precategories
    70. 2.70. The precategory of functors and natural transformations between two precategories
    71. 2.71. The precategory of functors and natural transformations from small to large precategories
    72. 2.72. The precategory of maps and natural transformations from a small to a large precategory
    73. 2.73. The precategory of maps and natural transformations between two precategories
    74. 2.74. Pregroupoids
    75. 2.75. Presheaf categories
    76. 2.76. Products in precategories
    77. 2.77. Products of precategories
    78. 2.78. Pullbacks in precategories
    79. 2.79. Representable functors between categories
    80. 2.80. Representable functors between large precategories
    81. 2.81. Representable functors between precategories
    82. 2.82. The representing arrow category
    83. 2.83. Sieves in categories
    84. 2.84. Slice precategories
    85. 2.85. Subprecategories
    86. 2.86. Terminal object in a precategory
    87. 2.87. The Yoneda lemma for categories
    88. 2.88. The Yoneda lemma for precategories
  5. 3. Commutative algebra
    ❱
    1. 3.1. The binomial theorem in commutative rings
    2. 3.2. The binomial theorem in commutative semirings
    3. 3.3. Boolean rings
    4. 3.4. The category of commutative rings
    5. 3.5. Commutative rings
    6. 3.6. Commutative semirings
    7. 3.7. Dependent products of commutative rings
    8. 3.8. Dependent products of commutative semirings
    9. 3.9. Discrete fields
    10. 3.10. The Eisenstein integers
    11. 3.11. Euclidean domains
    12. 3.12. Full ideals of commutative rings
    13. 3.13. Function commutative rings
    14. 3.14. Function commutative semirings
    15. 3.15. The Gaussian integers
    16. 3.16. The group of multiplicative units of a commutative ring
    17. 3.17. Homomorphisms of commutative rings
    18. 3.18. Homomorphisms of commutative semirings
    19. 3.19. Ideals of commutative rings
    20. 3.20. Ideals of commutative semirings
    21. 3.21. Ideals generated by subsets of commutative rings
    22. 3.22. Integer multiples of elements of commutative rings
    23. 3.23. Integral domains
    24. 3.24. Intersections of ideals of commutative rings
    25. 3.25. Intersections of radical ideals of commutative rings
    26. 3.26. Invertible elements in commutative rings
    27. 3.27. Isomorphisms of commutative rings
    28. 3.28. Joins of ideals of commutative rings
    29. 3.29. Joins of radical ideals of commutative rings
    30. 3.30. Local commutative rings
    31. 3.31. Maximal ideals of commutative rings
    32. 3.32. Multiples of elements in commutative rings
    33. 3.33. Nilradical of a commutative ring
    34. 3.34. The nilradical of a commutative semiring
    35. 3.35. The poset of ideals of a commutative ring
    36. 3.36. The poset of radical ideals of a commutative ring
    37. 3.37. Powers of elements in commutative rings
    38. 3.38. Powers of elements in commutative semirings
    39. 3.39. The precategory of commutative rings
    40. 3.40. The precategory of commutative semirings
    41. 3.41. Prime ideals of commutative rings
    42. 3.42. Products of commutative rings
    43. 3.43. Products of ideals of commutative rings
    44. 3.44. Products of radical ideals of a commutative ring
    45. 3.45. Products of subsets of commutative rings
    46. 3.46. Radical ideals of commutative rings
    47. 3.47. Radical ideals generated by subsets of commutative rings
    48. 3.48. Radicals of ideals of commutative rings
    49. 3.49. Subsets of commutative rings
    50. 3.50. Subsets of commutative semirings
    51. 3.51. Sums in commutative rings
    52. 3.52. Sums in commutative semirings
    53. 3.53. Transporting commutative ring structures along isomorphisms of abelian groups
    54. 3.54. Trivial commutative rings
    55. 3.55. The Zariski locale
    56. 3.56. The Zariski topology on the set of prime ideals of a commutative ring
  6. 4. Elementary number theory
    ❱
    1. 4.1. The absolute value function on the integers
    2. 4.2. The Ackermann function
    3. 4.3. Addition on integer fractions
    4. 4.4. Addition on the integers
    5. 4.5. Addition on the natural numbers
    6. 4.6. Addition on the rational numbers
    7. 4.7. Arithmetic functions
    8. 4.8. The based induction principle of the natural numbers
    9. 4.9. Based strong induction for the natural numbers
    10. 4.10. Bezout's lemma in the integers
    11. 4.11. Bezout's lemma on the natural numbers
    12. 4.12. The binomial coefficients
    13. 4.13. The binomial theorem for the integers
    14. 4.14. The binomial theorem for the natural numbers
    15. 4.15. Bounded sums of arithmetic functions
    16. 4.16. Catalan numbers
    17. 4.17. The cofibonacci sequence
    18. 4.18. The Collatz bijection
    19. 4.19. The Collatz conjecture
    20. 4.20. The commutative semiring of natural numbers
    21. 4.21. The congruence relations on the integers
    22. 4.22. The congruence relations on the natural numbers
    23. 4.23. Decidable dependent function types
    24. 4.24. Natural numbers are a total decidable poset
    25. 4.25. Decidable types in elementary number theory
    26. 4.26. The difference between integers
    27. 4.27. Dirichlet convolution
    28. 4.28. The distance between integers
    29. 4.29. The distance between natural numbers
    30. 4.30. Divisibility of integers
    31. 4.31. Divisibility in modular arithmetic
    32. 4.32. Divisibility of natural numbers
    33. 4.33. The divisibility relation on the standard finite types
    34. 4.34. Equality of integers
    35. 4.35. Equality of natural numbers
    36. 4.36. Euclidean division on the natural numbers
    37. 4.37. Euler's totient function
    38. 4.38. Exponentiation of natural numbers
    39. 4.39. Factorials of natural numbers
    40. 4.40. Falling factorials
    41. 4.41. The Fibonacci sequence
    42. 4.42. The natural numbers base k
    43. 4.43. Finitely cyclic maps
    44. 4.44. The fundamental theorem of arithmetic
    45. 4.45. The Goldbach conjecture
    46. 4.46. The greatest common divisor of integers
    47. 4.47. The greatest common divisor of natural numbers
    48. 4.48. The group of integers
    49. 4.49. The groups ℤ/kℤ
    50. 4.50. The half-integers
    51. 4.51. Inequality on integer fractions
    52. 4.52. Inequality on the integers
    53. 4.53. Inequality of natural numbers
    54. 4.54. Inequality on the rational numbers
    55. 4.55. Inequality on the standard finite types
    56. 4.56. The infinitude of primes
    57. 4.57. Initial segments of the natural numbers
    58. 4.58. Integer fractions
    59. 4.59. Integer partitions
    60. 4.60. The integers
    61. 4.61. The Jacobi symbol
    62. 4.62. The Kolakoski sequence
    63. 4.63. The Legendre symbol
    64. 4.64. Lower bounds of type families over the natural numbers
    65. 4.65. Maximum on the natural numbers
    66. 4.66. Maximum on the standard finite types
    67. 4.67. Mersenne primes
    68. 4.68. Minimum on the natural numbers
    69. 4.69. Minimum on the standard finite types
    70. 4.70. Modular arithmetic
    71. 4.71. Modular arithmetic on the standard finite types
    72. 4.72. The monoid of natural numbers with addition
    73. 4.73. The monoid of the natural numbers with maximum
    74. 4.74. Multiplication on integer fractions
    75. 4.75. Multiplication of integers
    76. 4.76. Multiplication of the elements of a list of natural numbers
    77. 4.77. Multiplication of natural numbers
    78. 4.78. Multiplication on the rational numbers
    79. 4.79. The multiplicative monoid of natural numbers
    80. 4.80. Multiplicative units in the integers
    81. 4.81. Multiplicative units in modular arithmetic
    82. 4.82. Multiset coefficients
    83. 4.83. The type of natural numbers
    84. 4.84. Nonzero natural numbers
    85. 4.85. The ordinal induction principle for the natural numbers
    86. 4.86. Parity of the natural numbers
    87. 4.87. Pisano periods
    88. 4.88. The poset of natural numbers ordered by divisibility
    89. 4.89. Powers of integers
    90. 4.90. Powers of two
    91. 4.91. Prime numbers
    92. 4.92. Products of natural numbers
    93. 4.93. Proper divisors of natural numbers
    94. 4.94. Pythagorean triples
    95. 4.95. The rational numbers
    96. 4.96. Reduced integer fractions
    97. 4.97. Relatively prime integers
    98. 4.98. Relatively prime natural numbers
    99. 4.99. Repeating an element in a standard finite type
    100. 4.100. Retracts of the type of natural numbers
    101. 4.101. The ring of integers
    102. 4.102. Rings of modular arithmetic
    103. 4.103. The sieve of Eratosthenes
    104. 4.104. Square-free natural numbers
    105. 4.105. Squares in the integers
    106. 4.106. Squares in ℤₚ
    107. 4.107. Squares in the natural numbers
    108. 4.108. Stirling numbers of the second kind
    109. 4.109. Strict inequality natural numbers
    110. 4.110. Strictly ordered pairs of natural numbers
    111. 4.111. The strong induction principle for the natural numbers
    112. 4.112. Sums of natural numbers
    113. 4.113. Telephone numbers
    114. 4.114. The triangular numbers
    115. 4.115. The Twin Prime conjecture
    116. 4.116. Type arithmetic with natural numbers
    117. 4.117. Unit elements in the standard finite types
    118. 4.118. Unit similarity on the standard finite types
    119. 4.119. The universal property of the integers
    120. 4.120. The universal property of the natural numbers
    121. 4.121. Upper bounds for type families over the natural numbers
    122. 4.122. The Well-Ordering Principle of the natural numbers
    123. 4.123. The well-ordering principle of the standard finite types
  7. 5. Finite algebra
    ❱
    1. 5.1. Commutative finite rings
    2. 5.2. Dependent products of commutative finit rings
    3. 5.3. Dependent products of finite rings
    4. 5.4. Abelian groups
    5. 5.5. Finite Commutative monoids
    6. 5.6. Finite fields
    7. 5.7. Abstract finite groups
    8. 5.8. Finite monoids
    9. 5.9. Finite rings
    10. 5.10. Finite semigroups
    11. 5.11. Homomorphisms of commutative finite rings
    12. 5.12. Homomorphisms of finite rings
    13. 5.13. Products of commutative finite rings
    14. 5.14. Products of finite rings
    15. 5.15. Semisimple commutative finite rings
  8. 6. Finite group theory
    ❱
    1. 6.1. The abstract quaternion group of order 8
    2. 6.2. Alternating concrete groups
    3. 6.3. Alternating groups
    4. 6.4. Cartier's delooping of the sign homomorphism
    5. 6.5. The concrete quaternion group
    6. 6.6. Deloopings of the sign homomorphism
    7. 6.7. Finite groups
    8. 6.8. Finite monoids
    9. 6.9. Finite semigroups
    10. 6.10. The group of n-element types
    11. 6.11. Groups of order 2
    12. 6.12. Orbits of permutations
    13. 6.13. Permutations
    14. 6.14. Permutations of standard finite types
    15. 6.15. The sign homomorphism
    16. 6.16. Simpson's delooping of the sign homomorphism
    17. 6.17. Subgroups of finite groups
    18. 6.18. Tetrahedra in 3-dimensional space
    19. 6.19. Transpositions
    20. 6.20. Transpositions of standard finite types
  9. 7. Foundation
    ❱
    1. 7.1. 0-Connected types
    2. 7.2. 0-Images of maps
    3. 7.3. 0-Maps
    4. 7.4. 1-Types
    5. 7.5. 2-Types
    6. 7.6. Action on equivalences of functions
    7. 7.7. The action on equivalences of functions out of subuniverses
    8. 7.8. Action on equivalences of type families
    9. 7.9. Action on equivalences in type families over subuniverses
    10. 7.10. The binary action on identifications of binary functions
    11. 7.11. The action on identifications of dependent functions
    12. 7.12. The action on identifications of functions
    13. 7.13. Apartness relations
    14. 7.14. Arithmetic law for coproduct decomposition and Σ-decomposition
    15. 7.15. Arithmetic law for product decomposition and Π-decomposition
    16. 7.16. Automorphisms
    17. 7.17. Axiom L
    18. 7.18. The axiom of choice
    19. 7.19. Bands
    20. 7.20. Binary embeddings
    21. 7.21. Binary equivalences
    22. 7.22. Binary equivalences on unordered pairs of types
    23. 7.23. Binary functoriality of set quotients
    24. 7.24. Homotopies of binary operations
    25. 7.25. Binary operations on unordered pairs of types
    26. 7.26. Binary reflecting maps of equivalence relations
    27. 7.27. Binary relations
    28. 7.28. Binary transport
    29. 7.29. The booleans
    30. 7.30. The Cantor–Schröder–Bernstein–Escardó theorem
    31. 7.31. Cantor's diagonal argument
    32. 7.32. Cartesian product types
    33. 7.33. Cartesian products of set quotients
    34. 7.34. The category of families of sets
    35. 7.35. The category of sets
    36. 7.36. Choice of representatives for an equivalence relation
    37. 7.37. Codiagonal maps of types
    38. 7.38. Coherently invertible maps
    39. 7.39. Commuting 3-simplices of homotopies
    40. 7.40. Commuting 3-simplices of maps
    41. 7.41. Commuting cubes of maps
    42. 7.42. Commuting hexagons of identifications
    43. 7.43. Commuting squares of identifications
    44. 7.44. Commuting squares of maps
    45. 7.45. Commuting triangles of homotopies
    46. 7.46. Commuting triangles of maps
    47. 7.47. Complements of type families
    48. 7.48. Complements of subtypes
    49. 7.49. Cones over cospans
    50. 7.50. Conjunction of propositions
    51. 7.51. Connected components of types
    52. 7.52. Connected components of universes
    53. 7.53. Connected maps
    54. 7.54. Connected types
    55. 7.55. Constant maps
    56. 7.56. Constant type families
    57. 7.57. Contractible maps
    58. 7.58. Contractible types
    59. 7.59. Coproduct decompositions
    60. 7.60. Coproduct decompositions in a subuniverse
    61. 7.61. Coproduct types
    62. 7.62. Morphisms in the coslice category of types
    63. 7.63. Cospans of types
    64. 7.64. Decidability of dependent function types
    65. 7.65. Decidability of dependent pair types
    66. 7.66. Decidable embeddings
    67. 7.67. Decidable equality
    68. 7.68. Decidable equivalence relations
    69. 7.69. Decidable maps
    70. 7.70. Decidable propositions
    71. 7.71. Decidable relations on types
    72. 7.72. Decidable subtypes
    73. 7.73. Decidable types
    74. 7.74. Dependent binary homotopies
    75. 7.75. The dependent binomial theorem for types (distributivity of dependent function types over coproduct types)
    76. 7.76. Dependent identifications
    77. 7.77. Dependent pair types
    78. 7.78. Descent for coproduct types
    79. 7.79. Descent for dependent pair types
    80. 7.80. Descent for the empty type
    81. 7.81. Descent for equivalences
    82. 7.82. Diagonal maps of types
    83. 7.83. Diagonals of maps
    84. 7.84. Discrete reflexive relations
    85. 7.85. Discrete relaxed Σ-decompositions
    86. 7.86. Discrete Σ-decompositions
    87. 7.87. Discrete types
    88. 7.88. Disjunction of propositions
    89. 7.89. Double negation
    90. 7.90. The double negation modality
    91. 7.91. Double powersets
    92. 7.92. Dubuc-Penon compact types
    93. 7.93. Effective maps for equivalence relations
    94. 7.94. Embeddings
    95. 7.95. Empty types
    96. 7.96. Endomorphisms
    97. 7.97. Epimorphisms
    98. 7.98. Epimorphisms with respect to maps into sets
    99. 7.99. Epimorphisms with respect to truncated types
    100. 7.100. Equality of cartesian product types
    101. 7.101. Equality of coproduct types
    102. 7.102. Equality on dependent function types
    103. 7.103. Equality of dependent pair types
    104. 7.104. Equality in the fibers of a map
    105. 7.105. Equivalence classes
    106. 7.106. Equivalence extensionality
    107. 7.107. Equivalence induction
    108. 7.108. Equivalence relations
    109. 7.109. Equivalences
    110. 7.110. Equivalences on Maybe
    111. 7.111. Exclusive disjunction of propositions
    112. 7.112. Existential quantification
    113. 7.113. Exponents of set quotients
    114. 7.114. Faithful maps
    115. 7.115. Fiber inclusions
    116. 7.116. Fibered equivalences
    117. 7.117. Fibered involutions
    118. 7.118. Maps fibered over a map
    119. 7.119. Fibers of maps
    120. 7.120. Full subtypes of types
    121. 7.121. Function extensionality
    122. 7.122. Function types
    123. 7.123. Functional correspondences
    124. 7.124. Functoriality of cartesian product types
    125. 7.125. Functoriality of coproduct types
    126. 7.126. Functoriality of dependent function types
    127. 7.127. Functoriality of dependent pair types
    128. 7.128. The functoriality of fiber
    129. 7.129. Functoriality of function types
    130. 7.130. Functoriality of propositional truncations
    131. 7.131. Functoriality of set quotients
    132. 7.132. Functoriality of set truncation
    133. 7.133. Functoriality of truncations
    134. 7.134. The fundamental theorem of identity types
    135. 7.135. Global choice
    136. 7.136. Hilbert's ε-operators
    137. 7.137. Homotopies
    138. 7.138. Homotopy induction
    139. 7.139. Identity systems
    140. 7.140. Identity types of truncated types
    141. 7.141. Identity types
    142. 7.142. The image of a map
    143. 7.143. Images of subtypes
    144. 7.144. Impredicative encodings of the logical operations
    145. 7.145. Impredicative universes
    146. 7.146. The induction principle for propositional truncation
    147. 7.147. Inhabited subtypes
    148. 7.148. Inhabited types
    149. 7.149. Injective maps
    150. 7.150. The interchange law
    151. 7.151. Intersections of subtypes
    152. 7.152. Invertible maps
    153. 7.153. Involutions
    154. 7.154. Isolated points
    155. 7.155. Isomorphisms of sets
    156. 7.156. Iterated cartesian product types
    157. 7.157. Iterating automorphisms
    158. 7.158. Iterating functions
    159. 7.159. Iterating involutions
    160. 7.160. Large binary relations
    161. 7.161. Large dependent pair types
    162. 7.162. Large homotopies
    163. 7.163. Large identity types
    164. 7.164. The large locale of propositions
    165. 7.165. The large locale of subtypes
    166. 7.166. The law of excluded middle
    167. 7.167. Lawvere's fixed point theorem
    168. 7.168. The lesser limited principle of omniscience
    169. 7.169. The limited principle of omniscience
    170. 7.170. Locally small types
    171. 7.171. Logical equivalences
    172. 7.172. The maybe modality
    173. 7.173. Mere embeddings
    174. 7.174. Mere equality
    175. 7.175. Mere equivalences
    176. 7.176. Monomorphisms
    177. 7.177. Morphisms of binary relations
    178. 7.178. Morphisms of cospans
    179. 7.179. Multisubsets
    180. 7.180. Multivariable correspondences
    181. 7.181. Multivariable decidable relations
    182. 7.182. Multivariable functoriality of set quotients
    183. 7.183. Multivariable operations
    184. 7.184. Multivariable relations
    185. 7.185. Negation
    186. 7.186. Non-contractible types
    187. 7.187. Pairs of distinct elements
    188. 7.188. Partial elements
    189. 7.189. Partitions
    190. 7.190. Path algebra
    191. 7.191. Path-split maps
    192. 7.192. Perfect images
    193. 7.193. Π-decompositions of types
    194. 7.194. Π-decompositions of types into types in a subuniverse
    195. 7.195. Pointed torsorial type families
    196. 7.196. Powersets
    197. 7.197. Preidempotent maps
    198. 7.198. Preimages of subtypes
    199. 7.199. The principle of omniscience
    200. 7.200. Product decompositions
    201. 7.201. Product decompositions of types in a subuniverse
    202. 7.202. Products of binary relations
    203. 7.203. Products of equivalence relataions
    204. 7.204. Products of tuples of types
    205. 7.205. Products of unordered pairs of types
    206. 7.206. Products of unordered tuples of types
    207. 7.207. Projective types
    208. 7.208. Proper subsets
    209. 7.209. Propositional extensionality
    210. 7.210. Propositional maps
    211. 7.211. Propositional resizing
    212. 7.212. Propositional truncations
    213. 7.213. Propositions
    214. 7.214. Pullback squares
    215. 7.215. Pullbacks
    216. 7.216. Raising universe levels
    217. 7.217. Reflecting maps for equivalence relations
    218. 7.218. Reflexive relations
    219. 7.219. The Regensburg extension of the fundamental theorem of identity types
    220. 7.220. Relaxed Σ-decompositions of types
    221. 7.221. Repetitions of values of maps
    222. 7.222. Repetitions in sequences
    223. 7.223. The replacement axiom for type theory
    224. 7.224. Retractions
    225. 7.225. Russell's paradox
    226. 7.226. Sections
    227. 7.227. Separated types
    228. 7.228. Sequences
    229. 7.229. Set presented types
    230. 7.230. Set quotients
    231. 7.231. Set truncations
    232. 7.232. Sets
    233. 7.233. Shifting sequences
    234. 7.234. Σ-closed subuniverses
    235. 7.235. Σ-decompositions of types into types in a subuniverse
    236. 7.236. Σ-decompositions of types
    237. 7.237. Singleton induction
    238. 7.238. Singleton subtypes
    239. 7.239. Morphisms in the slice category of types
    240. 7.240. Small maps
    241. 7.241. Small types
    242. 7.242. Small universes
    243. 7.243. Sorial type families
    244. 7.244. Spans of types
    245. 7.245. Split surjective maps
    246. 7.246. Standard apartness relations
    247. 7.247. Strongly extensional maps
    248. 7.248. Structure
    249. 7.249. The structure identity principle
    250. 7.250. Structured type duality
    251. 7.251. Subterminal types
    252. 7.252. Subtype duality
    253. 7.253. The subtype identity principle
    254. 7.254. Subtypes
    255. 7.255. Subuniverses
    256. 7.256. Surjective maps
    257. 7.257. Symmetric binary relations
    258. 7.258. Symmetric cores of binary relations
    259. 7.259. Symmetric difference of subtypes
    260. 7.260. The symmetric identity types
    261. 7.261. Symmetric operations
    262. 7.262. Tight apartness relations
    263. 7.263. Torsorial type families
    264. 7.264. Transport along equivalences
    265. 7.265. Transport along higher identifications
    266. 7.266. Transport along identifications
    267. 7.267. Trivial relaxed Σ-decompositions
    268. 7.268. Trivial Σ-decompositions
    269. 7.269. Truncated equality
    270. 7.270. Truncated maps
    271. 7.271. Truncated types
    272. 7.272. k-Equivalences
    273. 7.273. Truncation images of maps
    274. 7.274. Truncation levels
    275. 7.275. The truncation modalities
    276. 7.276. Truncations
    277. 7.277. Tuples of types
    278. 7.278. Type arithmetic with the booleans
    279. 7.279. Type arithmetic for cartesian product types
    280. 7.280. Type arithmetic for coproduct types
    281. 7.281. Type arithmetic with dependent function types
    282. 7.282. Type arithmetic for dependent pair types
    283. 7.283. Type arithmetic with the empty type
    284. 7.284. Type arithmetic with the unit type
    285. 7.285. Type duality
    286. 7.286. The type theoretic principle of choice
    287. 7.287. Unions of subtypes
    288. 7.288. Unique existence
    289. 7.289. Uniqueness of the image of a map
    290. 7.290. The uniqueness of set quotients
    291. 7.291. Uniqueness of set truncations
    292. 7.292. Uniqueness of the truncations
    293. 7.293. The unit type
    294. 7.294. Unital binary operations
    295. 7.295. The univalence axiom
    296. 7.296. The univalence axiom implies function extensionality
    297. 7.297. Univalent type families
    298. 7.298. The universal property of booleans
    299. 7.299. The universal propert of cartesian product types
    300. 7.300. The universal property of coproduct types
    301. 7.301. The universal property of dependent pair types
    302. 7.302. The universal property of the empty type
    303. 7.303. The universal property of fiber products
    304. 7.304. The universal property of identity systems
    305. 7.305. The universal property of identity types
    306. 7.306. The universal property of the image of a map
    307. 7.307. The universal property of maybe
    308. 7.308. The universal property of propositional truncations
    309. 7.309. The universal property of propositional truncations with respect to sets
    310. 7.310. The universal property of pullbacks
    311. 7.311. The universal property of set quotients
    312. 7.312. The universal property of set truncations
    313. 7.313. The universal property of truncations
    314. 7.314. The universal property of the unit type
    315. 7.315. Universe levels
    316. 7.316. Unordered pairs of elements in a type
    317. 7.317. Unordered pairs of types
    318. 7.318. Unordered n-tuples of elements in a type
    319. 7.319. Unordered tuples of types
    320. 7.320. Vectors of set quotients
    321. 7.321. Weak function extensionality
    322. 7.322. The weak limited principle of omniscience
    323. 7.323. Weakly constant maps
    324. 7.324. Whiskering homotopies
  10. 8. Foundation core
    ❱
    1. 8.1. 1-Types
    2. 8.2. Cartesian product types
    3. 8.3. Coherently invertible maps
    4. 8.4. Commuting squares of maps
    5. 8.5. Commuting triangles of maps
    6. 8.6. Constant maps
    7. 8.7. Contractible maps
    8. 8.8. Contractible types
    9. 8.9. Coproduct types
    10. 8.10. Decidable propositions
    11. 8.11. Dependent identifications
    12. 8.12. Diagonal maps of types
    13. 8.13. Discrete types
    14. 8.14. Embeddings
    15. 8.15. Empty types
    16. 8.16. Endomorphisms
    17. 8.17. Equality of dependent pair types
    18. 8.18. Equivalence induction
    19. 8.19. Equivalence relations
    20. 8.20. Equivalences
    21. 8.21. Fibers of maps
    22. 8.22. Function extensionality
    23. 8.23. Function types
    24. 8.24. Functoriality of dependent function types
    25. 8.25. Functoriality of dependent pair types
    26. 8.26. Functoriality of function types
    27. 8.27. Homotopies
    28. 8.28. Identity types
    29. 8.29. Injective maps
    30. 8.30. Invertible maps
    31. 8.31. Negation
    32. 8.32. Path-split maps
    33. 8.33. Propositional maps
    34. 8.34. Propositions
    35. 8.35. Pullbacks
    36. 8.36. Retractions
    37. 8.37. Sections
    38. 8.38. Sets
    39. 8.39. Singleton induction
    40. 8.40. Small types
    41. 8.41. Subtypes
    42. 8.42. Transport along identifications
    43. 8.43. Truncated maps
    44. 8.44. Truncated types
    45. 8.45. Truncation levels
    46. 8.46. The univalence axiom
    47. 8.47. The universal property of pullbacks
    48. 8.48. The universal property of truncations
    49. 8.49. Whiskering homotopies
  11. 9. Graph theory
    ❱
    1. 9.1. Acyclic undirected graphs
    2. 9.2. Circuits in undirected graphs
    3. 9.3. Closed walks in undirected graphs
    4. 9.4. Complete bipartite graphs
    5. 9.5. Complete multipartite graphs
    6. 9.6. Complete undirected graphs
    7. 9.7. Connected graphs
    8. 9.8. Cycles in undirected graphs
    9. 9.9. Directed graph structures on standard finite sets
    10. 9.10. Directed graphs
    11. 9.11. Edge-coloured undirected graphs
    12. 9.12. Embeddings of directed graphs
    13. 9.13. Embeddings of undirected graphs
    14. 9.14. Enriched undirected graphs
    15. 9.15. Equivalences of directed graphs
    16. 9.16. Equivalences of enriched undirected graphs
    17. 9.17. Equivalences of undirected graphs
    18. 9.18. Eulerian circuits in undirected graphs
    19. 9.19. Faithful morphisms of undirected graphs
    20. 9.20. Fibers of directed graphs
    21. 9.21. Finite graphs
    22. 9.22. Geometric realizations of undirected graphs
    23. 9.23. Hypergraphs
    24. 9.24. Matchings
    25. 9.25. Mere equivalences of undirected graphs
    26. 9.26. Morphisms of directed graphs
    27. 9.27. Morphisms of undirected graphs
    28. 9.28. Incidence in undirected graphs
    29. 9.29. Orientations of undirected graphs
    30. 9.30. Paths in undirected graphs
    31. 9.31. Polygons
    32. 9.32. Raising universe levels of directed graphs
    33. 9.33. Reflecting maps of undirected graphs
    34. 9.34. Reflexive graphs
    35. 9.35. Regular undirected graph
    36. 9.36. Simple undirected graphs
    37. 9.37. Stereoisomerism for enriched undirected graphs
    38. 9.38. Totally faithful morphisms of undirected graphs
    39. 9.39. Trails in directed graphs
    40. 9.40. Trails in undirected graphs
    41. 9.41. Undirected graph structures on standard finite sets
    42. 9.42. Undirected graphs
    43. 9.43. Vertex covers
    44. 9.44. Voltage graphs
    45. 9.45. Walks in directed graphs
    46. 9.46. Walks in undirected graphs
  12. 10. Group theory
    ❱
    1. 10.1. Abelian groups
    2. 10.2. Pointwise addition of morphisms of abelian groups
    3. 10.3. Automorphism groups
    4. 10.4. Cartesian products of abelian groups
    5. 10.5. Cartesian products of concrete groups
    6. 10.6. Cartesian products of groups
    7. 10.7. Cartesian products of monoids
    8. 10.8. Cartesian products of semigroups
    9. 10.9. The category of concrete groups
    10. 10.10. The category of groups
    11. 10.11. The category of semigroups
    12. 10.12. Cayley's theorem
    13. 10.13. The center of a group
    14. 10.14. Center of a monoid
    15. 10.15. Center of a semigroup
    16. 10.16. Central elements of groups
    17. 10.17. Central elements of monoids
    18. 10.18. Central elements of semirings
    19. 10.19. Centralizer subgroups
    20. 10.20. Commutative monoids
    21. 10.21. Commutators of elements in groups
    22. 10.22. Commuting elements of groups
    23. 10.23. Commuting elements of monoids
    24. 10.24. Commuting elements of semigroups
    25. 10.25. Concrete group actions
    26. 10.26. Concrete groups
    27. 10.27. Concrete monoids
    28. 10.28. Congruence relations on abelian groups
    29. 10.29. Congruence relations on commutative monoids
    30. 10.30. Congruence relations on groups
    31. 10.31. Congruence relations on monoids
    32. 10.32. Congruence relations on semigroups
    33. 10.33. Conjugation in groups
    34. 10.34. Conjugation on concrete groups
    35. 10.35. Contravariant pushforwards of concrete group actions
    36. 10.36. Core of a monoid
    37. 10.37. Cyclic groups
    38. 10.38. Decidable subgroups of groups
    39. 10.39. Dependent products of abelian groups
    40. 10.40. Dependent products of commutative monoids
    41. 10.41. Dependent products of groups
    42. 10.42. Dependent products of monoids
    43. 10.43. Dependent products of semigroups
    44. 10.44. The dihedral group construction
    45. 10.45. The dihedral groups
    46. 10.46. The E₈-lattice
    47. 10.47. Embeddings of abelian groups
    48. 10.48. Embeddings of groups
    49. 10.49. The endomorphism rings of abelian groups
    50. 10.50. Epimorphisms in groups
    51. 10.51. Equivalences of concrete group actions
    52. 10.52. Equivalences of concrete groups
    53. 10.53. Equivalences of group actions
    54. 10.54. Equivalences between semigroups
    55. 10.55. Exponents of abelian groups
    56. 10.56. Exponents of groups
    57. 10.57. Free concrete group actions
    58. 10.58. Free groups with one generator
    59. 10.59. The full subgroup of a group
    60. 10.60. Function groups of abelian groups
    61. 10.61. Function commutative monoids
    62. 10.62. Function groups
    63. 10.63. Function monoids
    64. 10.64. Function semigroups
    65. 10.65. Furstenberg groups
    66. 10.66. Generating elements of groups
    67. 10.67. Generating sets of groups
    68. 10.68. Group actions
    69. 10.69. Abstract groups
    70. 10.70. Homomorphisms of abelian groups
    71. 10.71. Homomorphisms of commutative monoids
    72. 10.72. Morphisms of concrete group actions
    73. 10.73. Homomorphisms of concrete groups
    74. 10.74. Homomorphisms of generated subgroups
    75. 10.75. Homomorphisms of group actions
    76. 10.76. Homomorphisms of groups
    77. 10.77. Homomorphisms of monoids
    78. 10.78. Homomorphisms of semigroups
    79. 10.79. Images of group homomorphisms
    80. 10.80. Integer multiples of elements in abelian groups
    81. 10.81. Integer powers of elements of groups
    82. 10.82. Intersections of subgroups of abelian groups
    83. 10.83. Intersections of subgroups of groups
    84. 10.84. Inverse semigroups
    85. 10.85. Invertible elements in monoids
    86. 10.86. Isomorphisms of abelian groups
    87. 10.87. Isomorphisms of concrete groups
    88. 10.88. Isomorphisms of group actions
    89. 10.89. Isomorphisms of groups
    90. 10.90. Isomorphisms of monoids
    91. 10.91. Isomorphisms of semigroups
    92. 10.92. Iterated cartesian products of concrete groups
    93. 10.93. Kernels
    94. 10.94. Kernels of homomorphisms of concrete groups
    95. 10.95. Large semigroups
    96. 10.96. Concrete automorphism groups on sets
    97. 10.97. Mere equivalences of concrete group actions
    98. 10.98. Mere equivalences of group actions
    99. 10.99. Monoid actions
    100. 10.100. Monoids
    101. 10.101. Monomorphisms of concrete groups
    102. 10.102. Monomorphisms in the category of groups
    103. 10.103. Multiples of elements in abelian groups
    104. 10.104. Normal closures of subgroups
    105. 10.105. Normal cores of subgroups
    106. 10.106. Normal subgroups
    107. 10.107. Normal subgroups of concrete groups
    108. 10.108. Normal submonoids
    109. 10.109. Normal submonoids of commutative monoids
    110. 10.110. Normalizer subgroups
    111. 10.111. The opposite of a group
    112. 10.112. The orbit-stabilizer theorem for concrete groups
    113. 10.113. Orbits of concrete group actions
    114. 10.114. Orbits of group actions
    115. 10.115. The precategory of orbits of a monoid action
    116. 10.116. The order of an element in a group
    117. 10.117. Powers of elements in commutative monoids
    118. 10.118. Powers of elements in groups
    119. 10.119. Powers of elements in monoids
    120. 10.120. The precategory of abelian groups
    121. 10.121. The precategory of commutative monoids
    122. 10.122. The precategory of concrete groups
    123. 10.123. The precategory of group actions
    124. 10.124. The precategory of groups
    125. 10.125. The precategory of monoids
    126. 10.126. The precategory of semigroups
    127. 10.127. Principal group actions
    128. 10.128. Principal torsors of concrete groups
    129. 10.129. Products of elements in a monoid
    130. 10.130. Products of tuples of elements in commutative monoids
    131. 10.131. Quotient groups
    132. 10.132. Quotient groups of concrete groups
    133. 10.133. Quotients of abelian groups
    134. 10.134. Rational commutative monoids
    135. 10.135. Representations of monoids in precategories
    136. 10.136. Saturated congruence relations on commutative monoids
    137. 10.137. Saturated congruence relations on monoids
    138. 10.138. Semigroups
    139. 10.139. Sheargroups
    140. 10.140. Shriek of concrete group homomorphisms
    141. 10.141. Stabilizer groups
    142. 10.142. Stabilizers of concrete group actions
    143. 10.143. Subgroups
    144. 10.144. Subgroups of abelian groups
    145. 10.145. Subgroups of concrete groups
    146. 10.146. Subgroups generated by elements of a group
    147. 10.147. Subgroups generated by subsets of groups
    148. 10.148. Submonoids
    149. 10.149. Submonoids of commutative monoids
    150. 10.150. Subsemigroups
    151. 10.151. Subsets of abelian groups
    152. 10.152. Subsets of commutative monoids
    153. 10.153. Subsets of groups
    154. 10.154. Subsets of monoids
    155. 10.155. The substitution functor of concrete group actions
    156. 10.156. The substitution functor of group actions
    157. 10.157. Surjective group homomorphisms
    158. 10.158. Symmetric concrete groups
    159. 10.159. Symmetric groups
    160. 10.160. Torsors of abstract groups
    161. 10.161. Transitive concrete group actions
    162. 10.162. Transitive group actions
    163. 10.163. Trivial concrete groups
    164. 10.164. Trivial group homomorphisms
    165. 10.165. Trivial subgroups
    166. 10.166. Unordered tuples of elements in commutative monoids
    167. 10.167. Wild representations of monoids
  13. 11. Higher group theory
    ❱
    1. 11.1. Cartesian products of higher groups
    2. 11.2. Conjugation in higher groups
    3. 11.3. Cyclic higher groups
    4. 11.4. Equivalences of higher groups
    5. 11.5. Fixed points of higher group actions
    6. 11.6. Free higher group actions
    7. 11.7. Higher group actions
    8. 11.8. Higher groups
    9. 11.9. Homomorphisms of higher group actions
    10. 11.10. Homomorphisms of higher groups
    11. 11.11. The higher group of integers
    12. 11.12. Iterated cartesian products of higher groups
    13. 11.13. Orbits of higher group actions
    14. 11.14. Subgroups of higher groups
    15. 11.15. Symmetric higher groups
    16. 11.16. Trivial higher groups
  14. 12. Linear algebra
    ❱
    1. 12.1. Constant matrices
    2. 12.2. Diagonal vectors
    3. 12.3. Diagonal matrices on rings
    4. 12.4. Functoriality of matrices
    5. 12.5. Functoriality of the type of vectors
    6. 12.6. Matrices
    7. 12.7. Matrices on rings
    8. 12.8. Multiplication of matrices
    9. 12.9. Scalar multiplication on matrices
    10. 12.10. Scalar multiplication of vectors
    11. 12.11. Scalar multiplication of vectors on rings
    12. 12.12. Transposition of matrices
    13. 12.13. Vectors
    14. 12.14. Vectors on commutative rings
    15. 12.15. Vectors on commutative semirings
    16. 12.16. Vectors on euclidean domains
    17. 12.17. Vectors on rings
    18. 12.18. Vectors on semirings
  15. 13. Lists
    ❱
    1. 13.1. Arrays
    2. 13.2. Concatenation of lists
    3. 13.3. Flattening of lists
    4. 13.4. Functoriality of the list operation
    5. 13.5. Lists
    6. 13.6. Lists of elements in discrete types
    7. 13.7. Permutations of lists
    8. 13.8. Permutations of vectors
    9. 13.9. Predicates on lists
    10. 13.10. Quicksort for lists
    11. 13.11. Reversing lists
    12. 13.12. Sort by insertion for lists
    13. 13.13. Sort by insertion for vectors
    14. 13.14. Sorted lists
    15. 13.15. Sorted vectors
    16. 13.16. Sorting algorithms for lists
    17. 13.17. Sorting algorithms for vectors
    18. 13.18. The universal property of lists with respect to wild monoids
  16. 14. Online encyclopedia of integer sequences
    ❱
    1. 14.1. Sequences of the online encyclopedia of integer sequences
  17. 15. Order theory
    ❱
    1. 15.1. Bottom elements in posets
    2. 15.2. Bottom elements in preorders
    3. 15.3. Chains in posets
    4. 15.4. Chains in preorders
    5. 15.5. Closure operators on large locales
    6. 15.6. Closure operators on large posets
    7. 15.7. Coverings in locales
    8. 15.8. Decidable posets
    9. 15.9. Decidable preorders
    10. 15.10. Decidable subposets
    11. 15.11. Decidable subpreorders
    12. 15.12. Decidable total orders
    13. 15.13. Decidable total preorders
    14. 15.14. Dependent products of large frames
    15. 15.15. Dependent products of large locales
    16. 15.16. Dependent products of large meet-semilattices
    17. 15.17. Dependent products of large posets
    18. 15.18. Dependent products large preorders
    19. 15.19. Dependent products of large suplattices
    20. 15.20. Directed complete posets
    21. 15.21. Directed families in posets
    22. 15.22. Distributive lattices
    23. 15.23. Finite coverings in locales
    24. 15.24. Finite posets
    25. 15.25. Finite preorders
    26. 15.26. Finitely graded posets
    27. 15.27. Frames
    28. 15.28. Galois connections
    29. 15.29. Galois connections between large posets
    30. 15.30. Greatest lower bounds in large posets
    31. 15.31. Greatest lower bounds in posets
    32. 15.32. Homomorphisms of frames
    33. 15.33. Homomorphisms of large frames
    34. 15.34. Homomorphisms of large locales
    35. 15.35. Homomorphisms of large meet-semilattices
    36. 15.36. Homomorphisms of large suplattices
    37. 15.37. Homomorphisms of meet-semilattices
    38. 15.38. Homomorphisms of meet sup lattices
    39. 15.39. Homomorphisms of suplattices
    40. 15.40. Ideals in preorders
    41. 15.41. Interval subposets
    42. 15.42. Join-semilattices
    43. 15.43. Large frames
    44. 15.44. Large locales
    45. 15.45. Large meet-semilattices
    46. 15.46. Large meet-subsemilattices
    47. 15.47. Large posets
    48. 15.48. Large preorders
    49. 15.49. Large quotient locales
    50. 15.50. Large subframes
    51. 15.51. Large subposets
    52. 15.52. Large subpreorders
    53. 15.53. Large subsuplattices
    54. 15.54. Large suplattices
    55. 15.55. Lattices
    56. 15.56. Least upper bounds in large posets
    57. 15.57. Least upper bounds in posets
    58. 15.58. Locales
    59. 15.59. Locally finite posets
    60. 15.60. Lower bounds in large posets
    61. 15.61. Lower bounds in posets
    62. 15.62. Lower types in preorders
    63. 15.63. Maximal chains in posets
    64. 15.64. Maximal chains in preorders
    65. 15.65. Meet-semilattices
    66. 15.66. Meet-suplattices
    67. 15.67. Nuclei on large locales
    68. 15.68. Order preserving maps between large posets
    69. 15.69. Order preserving maps between large preorders
    70. 15.70. Order preserving maps on posets
    71. 15.71. Order preserving maps on preorders
    72. 15.72. Posets
    73. 15.73. Powers of large locales
    74. 15.74. Preorders
    75. 15.75. Reflective Galois connections between large posets
    76. 15.76. Similarity of elements in large posets
    77. 15.77. Similarity of elements in large preorders
    78. 15.78. Subposets
    79. 15.79. Subpreorders
    80. 15.80. Suplattices
    81. 15.81. Top elements in large posets
    82. 15.82. Top elements in posets
    83. 15.83. Top elements in preorders
    84. 15.84. Total orders
    85. 15.85. Total preorders
    86. 15.86. Upper bounds in large posets
    87. 15.87. Upper bounds in posets
  18. 16. Organic Chemistry
    ❱
    1. 16.1. Alcohols
    2. 16.2. Alkanes
    3. 16.3. Alkenes
    4. 16.4. Alkynes
    5. 16.5. Ethane
    6. 16.6. Hydrocarbons
    7. 16.7. Methane
    8. 16.8. Saturated carbons
  19. 17. Orthogonal factorization systems
    ❱
    1. 17.1. The closed modalities
    2. 17.2. Extensions of maps
    3. 17.3. Factorization operations
    4. 17.4. Factorization operations into function classes
    5. 17.5. Factorizations of maps
    6. 17.6. Function classes
    7. 17.7. Higher modalities
    8. 17.8. The identity modality
    9. 17.9. Lifting operations
    10. 17.10. Lifting squares
    11. 17.11. Lifts of maps
    12. 17.12. Local families
    13. 17.13. Local maps
    14. 17.14. Local types
    15. 17.15. Localizations at maps
    16. 17.16. Localizations at subuniverses
    17. 17.17. Locally small modal-operators
    18. 17.18. Mere lifting properties
    19. 17.19. Modal operators
    20. 17.20. Null types
    21. 17.21. The open modalities
    22. 17.22. Orthogonal factorization systems
    23. 17.23. Orthogonal maps
    24. 17.24. The pullback-hom
    25. 17.25. The raise modalities
    26. 17.26. Reflective modalities
    27. 17.27. Reflective subuniverses
    28. 17.28. Separated types
    29. 17.29. Σ-closed modalities
    30. 17.30. Σ-closed reflective modalities
    31. 17.31. Σ-closed reflective subuniverses
    32. 17.32. Stable orthogonal factorization systems
    33. 17.33. Uniquely eliminating modalities
    34. 17.34. Wide function classes
    35. 17.35. The zero modality
  20. 18. Polytopes
    ❱
    1. 18.1. Abstract polytopes
  21. 19. Primitives
    ❱
    1. 19.1. Characters
    2. 19.2. Floats
    3. 19.3. Machine integers
    4. 19.4. Strings
  22. 20. Real numbers
    ❱
    1. 20.1. Dedekind real numbers
  23. 21. Reflection
    ❱
    1. 21.1. Abstractions
    2. 21.2. Arguments
    3. 21.3. Boolean reflection
    4. 21.4. Definitions
    5. 21.5. Fixity
    6. 21.6. Group solver
    7. 21.7. Literals
    8. 21.8. Metavariables
    9. 21.9. Names
    10. 21.10. Precategory solver
    11. 21.11. Terms
    12. 21.12. The type checking monad
  24. 22. Ring theory
    ❱
    1. 22.1. Additive orders of elements of rings
    2. 22.2. Algebras over rings
    3. 22.3. The binomial theorem for rings
    4. 22.4. The binomial theorem for semirings
    5. 22.5. The category of cyclic rings
    6. 22.6. The category of rings
    7. 22.7. Central elements of rings
    8. 22.8. Central elements of semirings
    9. 22.9. Characteristics of rings
    10. 22.10. Commuting elements of rings
    11. 22.11. Congruence relations on rings
    12. 22.12. Congruence relations on semirings
    13. 22.13. Cyclic rings
    14. 22.14. Dependent products of rings
    15. 22.15. Dependent products of semirings
    16. 22.16. Division rings
    17. 22.17. The free ring with one generator
    18. 22.18. Full ideals of rings
    19. 22.19. Function rings
    20. 22.20. Function semirings
    21. 22.21. Generating elements of rings
    22. 22.22. The group of multiplicative units of a ring
    23. 22.23. Homomorphisms of cyclic rings
    24. 22.24. Homomorphisms of rings
    25. 22.25. Homomorphisms of semirings
    26. 22.26. Ideals generated by subsets of rings
    27. 22.27. Ideals of rings
    28. 22.28. Ideals of semirings
    29. 22.29. Idempotent elements in rings
    30. 22.30. Initial rings
    31. 22.31. Integer multiples of elements of rings
    32. 22.32. Intersections of ideals of rings
    33. 22.33. Intersections of ideals of semirings
    34. 22.34. The invariant basis property of rings
    35. 22.35. Invertible elements in rings
    36. 22.36. Isomorphisms of rings
    37. 22.37. Joins of ideals of rings
    38. 22.38. Joins of left ideals of rings
    39. 22.39. Joins of right ideals of rings
    40. 22.40. Kernels of ring homomorphisms
    41. 22.41. Left ideals generated by subsets of rings
    42. 22.42. Left ideals of rings
    43. 22.43. Local rings
    44. 22.44. Localizations of rings
    45. 22.45. Maximal ideals of rings
    46. 22.46. Modules over rings
    47. 22.47. Multiples of elements in rings
    48. 22.48. Multiplicative orders of elements of rings
    49. 22.49. Nil ideals of rings
    50. 22.50. Nilpotent elements in rings
    51. 22.51. Nilpotent elements in semirings
    52. 22.52. Opposite rings
    53. 22.53. The poset of cyclic rings
    54. 22.54. The poset of ideals of a ring
    55. 22.55. The poset of left ideals of a ring
    56. 22.56. The poset of right ideals of a ring
    57. 22.57. Powers of elements in rings
    58. 22.58. Powers of elements in semirings
    59. 22.59. The precategory of rings
    60. 22.60. The precategory of semirings
    61. 22.61. Products of ideals of rings
    62. 22.62. Products of left ideals of rings
    63. 22.63. Products of right ideals of rings
    64. 22.64. Products of rings
    65. 22.65. Products of subsets of rings
    66. 22.66. Quotient rings
    67. 22.67. Radical ideals of rings
    68. 22.68. Right ideals generated by subsets of rings
    69. 22.69. Right ideals of rings
    70. 22.70. Rings
    71. 22.71. Semirings
    72. 22.72. Subsets of rings
    73. 22.73. Subsets of semirings
    74. 22.74. Sums of elements in rings
    75. 22.75. Sums of elements in semirings
    76. 22.76. Transporting ring structures along isomorphisms of abelian groups
    77. 22.77. Trivial rings
  25. 23. Set theory
    ❱
    1. 23.1. Baire space
    2. 23.2. Cantor space
    3. 23.3. Cardinalities of sets
    4. 23.4. Countable sets
    5. 23.5. Cumulative hierarchy
    6. 23.6. Infinite sets
    7. 23.7. Uncountable sets
  26. 24. Species
    ❱
    1. 24.1. Cartesian exponents of species
    2. 24.2. Cartesian products of species of types
    3. 24.3. Cauchy composition of species of types
    4. 24.4. Cauchy composition of species of types in a subuniverse
    5. 24.5. Cauchy exponentials of species of types
    6. 24.6. Cauchy exponentials of species of types in a subuniverse
    7. 24.7. Cauchy products of species of types
    8. 24.8. Cauchy products of species of types in a subuniverse
    9. 24.9. Cauchy series of species of types
    10. 24.10. Cauchy series of species of types in a subuniverse
    11. 24.11. Composition of Cauchy series of species of types
    12. 24.12. Composition of Cauchy series of species of types in subuniverses
    13. 24.13. Coproducts of species of types
    14. 24.14. Coproducts of species of types in subuniverses
    15. 24.15. Cycle index series of species
    16. 24.16. Derivatives of species
    17. 24.17. Dirichlet exponentials of a species of types
    18. 24.18. Dirichlet exponentials of species of types in a subuniverse
    19. 24.19. Dirichlet products of species of types
    20. 24.20. Dirichlet products of species of types in subuniverses
    21. 24.21. Dirichlet series of species of finite inhabited types
    22. 24.22. Dirichlet series of species of types
    23. 24.23. Dirichlet series of species of types in subuniverses
    24. 24.24. Equivalences of species of types
    25. 24.25. Equivalences of species of types in subuniverses
    26. 24.26. Exponential of Cauchy series of species of types
    27. 24.27. Exponential of Cauchy series of species of types in subuniverses
    28. 24.28. Hasse-Weil species
    29. 24.29. Morphisms of finite species
    30. 24.30. Morphisms of species of types
    31. 24.31. Pointing of species of types
    32. 24.32. The precategory of finite species
    33. 24.33. Products of Cauchy series of species of types
    34. 24.34. Products of Cauchy series of species of types in subuniverses
    35. 24.35. Products of Dirichlet series of species of finite inhabited types
    36. 24.36. Products of Dirichlet series of species of types
    37. 24.37. Products of Dirichlet series of species of types in subuniverses
    38. 24.38. Small Composition of species of finite inhabited types
    39. 24.39. Small Cauchy composition of species types in subuniverses
    40. 24.40. Species of finite inhabited types
    41. 24.41. Species of finite types
    42. 24.42. Species of inhabited types
    43. 24.43. Species of types
    44. 24.44. Species of types in subuniverses
    45. 24.45. The unit of Cauchy composition of types
    46. 24.46. The unit of Cauchy composition of species of types in subuniverses
    47. 24.47. Unlabeled structures of finite species
  27. 25. Structured types
    ❱
    1. 25.1. Cartesian products of types equipped with endomorphisms
    2. 25.2. Central H-spaces
    3. 25.3. Commuting squares of pointed maps
    4. 25.4. Conjugation of pointed types
    5. 25.5. Constant maps of pointed types
    6. 25.6. Contractible pointed types
    7. 25.7. Cyclic types
    8. 25.8. Dependent products of H-spaces
    9. 25.9. Dependent products of pointed types
    10. 25.10. Dependent products of wild monoids
    11. 25.11. Equivalences of types equipped with endomorphisms
    12. 25.12. Faithful pointed maps
    13. 25.13. Fibers of pointed maps
    14. 25.14. Finite multiplication in magmas
    15. 25.15. Function H-spaces
    16. 25.16. Function magmas
    17. 25.17. Function wild monoids
    18. 25.18. H-spaces
    19. 25.19. The initial pointed type equipped with an automorphism
    20. 25.20. The involutive type of H-space structures on a pointed type
    21. 25.21. Involutive types
    22. 25.22. Iterated cartesian products of types equipped with endomorphisms
    23. 25.23. Iterated cartesian products of pointed types
    24. 25.24. Magmas
    25. 25.25. Mere equivalences of types equipped with endomorphisms
    26. 25.26. Morphisms of H-spaces
    27. 25.27. Morphisms of magmas
    28. 25.28. Morphisms of types equipped with endomorphisms
    29. 25.29. Morphisms of wild monoids
    30. 25.30. Non-coherent H-spaces
    31. 25.31. Pointed cartesian product types
    32. 25.32. Pointed dependent functions
    33. 25.33. Pointed dependent pair types
    34. 25.34. Pointed equivalences
    35. 25.35. Pointed families of types
    36. 25.36. Pointed homotopies
    37. 25.37. Pointed maps
    38. 25.38. Pointed sections of pointed maps
    39. 25.39. Pointed types
    40. 25.40. Pointed types equipped with automorphisms
    41. 25.41. The pointed unit type
    42. 25.42. Symmetric elements of involutive types
    43. 25.43. Symmetric H-spaces
    44. 25.44. Types equipped with automorphisms
    45. 25.45. Types equipped with endomorphisms
    46. 25.46. Unpointed maps between pointed types
    47. 25.47. Wild groups
    48. 25.48. Wild loops
    49. 25.49. Wild monoids
    50. 25.50. Wild quasigroups
    51. 25.51. Wild semigroups
  28. 26. Synthetic homotopy theory
    ❱
    1. 26.1. Formalization of the Symmetry book - 26 descent
    2. 26.2. Formalization of the Symmetry book - 26 id pushout
    3. 26.3. Formalization of the Symmetry book - 27 sequences
    4. 26.4. Acyclic maps
    5. 26.5. Acyclic types
    6. 26.6. The category of connected set bundles over the circle
    7. 26.7. Cavallo's trick
    8. 26.8. The circle
    9. 26.9. Cocones under spans
    10. 26.10. Cocones under spans of pointed types
    11. 26.11. Coequalizers
    12. 26.12. Cofibers
    13. 26.13. Coforks
    14. 26.14. Conjugation of loops
    15. 26.15. Connected set bundles over the circle
    16. 26.16. Dependent cocones under spans
    17. 26.17. Dependent coforks
    18. 26.18. The dependent pullback property of pushouts
    19. 26.19. Dependent suspension structures
    20. 26.20. The dependent universal property of coequalizers
    21. 26.21. The dependent universal property of pushouts
    22. 26.22. Dependent universal property of suspensions
    23. 26.23. The descent property of the circle
    24. 26.24. Descent data for constant type families over the circle
    25. 26.25. Descent data for families of dependent pair types over the circle
    26. 26.26. Descent data for families of equivalence types over the circle
    27. 26.27. Descent data for families of function types over the circle
    28. 26.28. Subtypes of descent data for the circle
    29. 26.29. Double loop spaces
    30. 26.30. The Eckmann-Hilton Argument
    31. 26.31. The flattening lemma for coequalizers
    32. 26.32. The flattening lemma for pushouts
    33. 26.33. Free loops
    34. 26.34. Functoriality of the loop space operation
    35. 26.35. Groups of loops in 1-types
    36. 26.36. Hatcher's acyclic type
    37. 26.37. The induction principle of pushouts
    38. 26.38. The infinite complex projective space
    39. 26.39. Infinite cyclic types
    40. 26.40. The interval
    41. 26.41. Iterated loop spaces
    42. 26.42. Join powers of types
    43. 26.43. Joins of types
    44. 26.44. Loop spaces
    45. 26.45. The multiplication operation on the circle
    46. 26.46. The plus-principle
    47. 26.47. Powers of loops
    48. 26.48. Prespectra
    49. 26.49. The pullback property of pushouts
    50. 26.50. Pushouts
    51. 26.51. Pushouts of pointed types
    52. 26.52. Sections of families over the circle
    53. 26.53. Smash products of pointed types
    54. 26.54. Spectra
    55. 26.55. Spheres
    56. 26.56. Suspension Structures
    57. 26.57. Suspensions of pointed types
    58. 26.58. Suspensions of types
    59. 26.59. Triple loop spaces
    60. 26.60. The universal cover of the circle
    61. 26.61. The universal property of the circle
    62. 26.62. The universal property of coequalizers
    63. 26.63. The universal property of pushouts
    64. 26.64. Universal property of suspensions
    65. 26.65. Universal Property of suspensions of pointed types
    66. 26.66. Wedges of pointed types
  29. 27. Trees
    ❱
    1. 27.1. Algebras for polynomial endofunctors
    2. 27.2. Bases of directed trees
    3. 27.3. Bases of enriched directed trees
    4. 27.4. The coalgebra of directed trees
    5. 27.5. The coalgebra of enriched directed trees
    6. 27.6. Coalgebras of polynomial endofunctors
    7. 27.7. The combinator of directed trees
    8. 27.8. Combinators of enriched directed trees
    9. 27.9. Directed trees
    10. 27.10. The elementhood relation on coalgebras of polynomial endofunctors
    11. 27.11. The elementhood relation on W-types
    12. 27.12. Enriched directed trees
    13. 27.13. Equivalences of directed trees
    14. 27.14. Equivalences of enriched directed trees
    15. 27.15. Extensional W-types
    16. 27.16. Fibers of directed trees
    17. 27.17. Fibers of enriched directed trees
    18. 27.18. Functoriality of the combinator of directed trees
    19. 27.19. Functoriality of the fiber operation on directed trees
    20. 27.20. Functoriality of W-types
    21. 27.21. Indexed W-types
    22. 27.22. Induction principles on W-types
    23. 27.23. Inequality on W-types
    24. 27.24. Lower types of elements in W-types
    25. 27.25. Morphisms of algebras of polynomial endofunctors
    26. 27.26. Morphisms of coalgebras of polynomial endofunctors
    27. 27.27. Morphisms of directed trees
    28. 27.28. Morphisms of enriched directed trees
    29. 27.29. Multisets
    30. 27.30. Planar binary trees
    31. 27.31. Polynomial endofunctors
    32. 27.32. Raising universe levels of directed trees
    33. 27.33. Ranks of elements in W-types
    34. 27.34. Rooted morphisms of directed trees
    35. 27.35. Rooted morphisms of enriched directed trees
    36. 27.36. Rooted quasitrees
    37. 27.37. Rooted undirected trees
    38. 27.38. Small multisets
    39. 27.39. Submultisets
    40. 27.40. Transitive multisets
    41. 27.41. The underlying trees of elements of coalgebras of polynomial endofunctors
    42. 27.42. The underlying trees of elements of W-types
    43. 27.43. Undirected rees
    44. 27.44. The universal multiset
    45. 27.45. The W-type of natural numbers
    46. 27.46. The W-type of the type of propositions
    47. 27.47. W-types
  30. 28. Type theories
    ❱
    1. 28.1. Comprehension of fibered type theories
    2. 28.2. Dependent type theories
    3. 28.3. Fibered dependent type theories
    4. 28.4. Sections of dependent type theories
    5. 28.5. Simple type theories
    6. 28.6. Unityped type theories
  31. 29. Univalent combinatorics
    ❱
    1. 29.1. 2-element decidable subtypes
    2. 29.2. 2-element subtypes
    3. 29.3. 2-element types
    4. 29.4. The binomial types
    5. 29.5. Bracelets
    6. 29.6. Cartesian products of finite types
    7. 29.7. The classical definition of the standard finite types
    8. 29.8. Complements of isolated points of finite types
    9. 29.9. Coproducts of finite types
    10. 29.10. Counting in type theory
    11. 29.11. Counting the elements of decidable subtypes
    12. 29.12. Counting the elements of dependent pair types
    13. 29.13. Counting the elements of the fiber of a map
    14. 29.14. Counting the elements in Maybe
    15. 29.15. Cubes
    16. 29.16. Cycle partitions of finite types
    17. 29.17. Cycle prime decompositions of natural numbers
    18. 29.18. Cyclic types
    19. 29.19. Decidable dependent function types
    20. 29.20. Decidability of dependent pair types
    21. 29.21. Decidable equivalence relations on finite types
    22. 29.22. Decidable propositions
    23. 29.23. Decidable subtypes of finite types
    24. 29.24. Dedekind finite sets
    25. 29.25. Counting the elements of dependent function types
    26. 29.26. Dependent pair types of finite types
    27. 29.27. Finite discrete Σ-decompositions
    28. 29.28. Distributivity of set truncation over finite products
    29. 29.29. Double counting
    30. 29.30. Injective maps
    31. 29.31. Embeddings between standard finite types
    32. 29.32. Equality in finite types
    33. 29.33. Equality in the standard finite types
    34. 29.34. Equivalences between finite types
    35. 29.35. Equivalences of cubes
    36. 29.36. Equivalences between standard finite types
    37. 29.37. Ferrers diagrams (unlabeled partitions)
    38. 29.38. Fibers of maps between finite types
    39. 29.39. Finite choice
    40. 29.40. Finiteness of the type of connected components
    41. 29.41. Finite presentations of types
    42. 29.42. Finite types
    43. 29.43. Finitely presented types
    44. 29.44. Finite function types
    45. 29.45. The image of a map
    46. 29.46. Inequality on types equipped with a counting
    47. 29.47. Inhabited finite types
    48. 29.48. Injective maps between finite types
    49. 29.49. An involution on the standard finite types
    50. 29.50. Isotopies of Latin squares
    51. 29.51. Kuratowsky finite sets
    52. 29.52. Latin squares
    53. 29.53. The groupoid of main classes of Latin hypercubes
    54. 29.54. The groupoid of main classes of Latin squares
    55. 29.55. The maybe modality on finite types
    56. 29.56. Necklaces
    57. 29.57. Orientations of the complete undirected graph
    58. 29.58. Orientations of cubes
    59. 29.59. Partitions of finite types
    60. 29.60. Petri-nets
    61. 29.61. π-finite types
    62. 29.62. The pigeonhole principle
    63. 29.63. Finitely π-presented types
    64. 29.64. Quotients of finite types
    65. 29.65. Ramsey theory
    66. 29.66. Repetitions of values
    67. 29.67. Repetitions of values in sequences
    68. 29.68. Retracts of finite types
    69. 29.69. Sequences of elements in finite types
    70. 29.70. Set quotients of index 2
    71. 29.71. Finite Σ-decompositions of finite types
    72. 29.72. Skipping elements in standard finite types
    73. 29.73. Small types
    74. 29.74. Standard finite pruned trees
    75. 29.75. Standard finite trees
    76. 29.76. The standard finite types
    77. 29.77. Steiner systems
    78. 29.78. Steiner triple systems
    79. 29.79. Combinatorial identities of sums of natural numbers
    80. 29.80. Surjective maps between finite types
    81. 29.81. Symmetric difference of finite subtypes
    82. 29.82. Finite trivial Σ-decompositions
    83. 29.83. Type duality of finite types
    84. 29.84. Unions of finite subtypes
    85. 29.85. The universal property of the standard finite types
    86. 29.86. Unlabeled partitions
    87. 29.87. Unlabeled rooted trees
    88. 29.88. Unlabeled trees
  32. 30. Universal Algebra
    ❱
    1. 30.1. Abstract equations over signatures
    2. 30.2. Algebraic theories
    3. 30.3. Algebraic theory of groups
    4. 30.4. Algebras
    5. 30.5. Congruences
    6. 30.6. Homomorphisms of algebras
    7. 30.7. Kernels of homomorphisms of algebras
    8. 30.8. Models of signatures
    9. 30.9. Quotient algebras
    10. 30.10. Signatures
    11. 30.11. Terms over signatures

agda-unimath

Species of finite types

Content created by Egbert Rijke, Fredrik Bakke and Victor Blanchi.

Created on 2023-03-21.
Last modified on 2023-04-27.

module species.species-of-finite-types where
Imports
open import foundation.universe-levels

open import species.species-of-types-in-subuniverses

open import univalent-combinatorics.finite-types

Idea

A species of finite types is a map from 𝔽 to a 𝔽.

Definition

species-𝔽 : (l1 l2 : Level) → UU (lsuc l1 ⊔ lsuc l2)
species-𝔽 l1 l2 =
  species-subuniverse (is-finite-Prop {l1}) (is-finite-Prop {l2})

Recent changes

  • 2023-04-27. Egbert Rijke. Cleaning up some stuff in species (#575).
  • 2023-03-21. Fredrik Bakke. Formatting fixes (#530).
  • 2023-03-21. Victor Blanchi. Associativity of species composition (#478).