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. Coproducts in precategories
    6. 2.6. Dependent products of categories
    7. 2.7. Dependent products of precategories
    8. 2.8. Discrete categories
    9. 2.9. Endomorphisms in categories
    10. 2.10. Endomorphisms in precategories
    11. 2.11. Epimorphism in large precategories
    12. 2.12. Equivalences between categories
    13. 2.13. Equivalences between large precategories
    14. 2.14. Equivalences between precategories
    15. 2.15. Exponential objects in precategories
    16. 2.16. Function categories
    17. 2.17. Function precategories
    18. 2.18. Functors between categories
    19. 2.19. Functors between large precategories
    20. 2.20. Functors between precategories
    21. 2.21. Groupoids
    22. 2.22. Homotopies of natural transformations in large precategories
    23. 2.23. Initial objects of large categories
    24. 2.24. Initial objects of large precategories
    25. 2.25. Initial objects of a precategory
    26. 2.26. Isomorphisms in categories
    27. 2.27. Isomorphisms in large categories
    28. 2.28. Isomorphisms in large precategories
    29. 2.29. Isomorphisms in precategories
    30. 2.30. Large categories
    31. 2.31. Large precategories
    32. 2.32. Monomorphisms in large precategories
    33. 2.33. Natural isomorphisms between functors between categories
    34. 2.34. Natural isomorphisms between functors on large precategories
    35. 2.35. Natural isomorphisms between functors between precategories
    36. 2.36. Natural numbers object in a precategory
    37. 2.37. Natural transformations between functors between categories
    38. 2.38. Natural transformations between functors between large precategories
    39. 2.39. Natural transformations between functors on precategories
    40. 2.40. One object precategories
    41. 2.41. Opposite precategories
    42. 2.42. Precategories
    43. 2.43. The precategory of functors and natural transformations between two fixed precategories
    44. 2.44. Pregroupoids
    45. 2.45. Products in precategories
    46. 2.46. Products of precategories
    47. 2.47. Pullbacks in precategories
    48. 2.48. Representable functors between categories
    49. 2.49. Representable functors between precategories
    50. 2.50. Sieves in categories
    51. 2.51. Slice precategories
    52. 2.52. Terminal object of a precategory
    53. 2.53. The Yoneda lemma for categories
    54. 2.54. 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 Kolakoski sequence
    62. 4.62. Lower bounds of type families over the natural numbers
    63. 4.63. Maximum on the natural numbers
    64. 4.64. Maximum on the standard finite types
    65. 4.65. Mersenne primes
    66. 4.66. Minimum on the natural numbers
    67. 4.67. Minimum on the standard finite types
    68. 4.68. Modular arithmetic
    69. 4.69. Modular arithmetic on the standard finite types
    70. 4.70. The monoid of natural numbers with addition
    71. 4.71. The monoid of the natural numbers with maximum
    72. 4.72. Multiplication on integer fractions
    73. 4.73. Multiplication of integers
    74. 4.74. Multiplication of the elements of a list of natural numbers
    75. 4.75. Multiplication of natural numbers
    76. 4.76. Multiplication on the rational numbers
    77. 4.77. Multiplicative units in the integers
    78. 4.78. Multiplicative units in modular arithmetic
    79. 4.79. Multiset coefficients
    80. 4.80. The type of natural numbers
    81. 4.81. Nonzero natural numbers
    82. 4.82. The ordinal induction principle for the natural numbers
    83. 4.83. Parity of the natural numbers
    84. 4.84. Pisano periods
    85. 4.85. Powers of integers
    86. 4.86. Powers of two
    87. 4.87. Prime numbers
    88. 4.88. Products of natural numbers
    89. 4.89. Proper divisors of natural numbers
    90. 4.90. Pythagorean triples
    91. 4.91. The rational numbers
    92. 4.92. Reduced integer fractions
    93. 4.93. Relatively prime integers
    94. 4.94. Relatively prime natural numbers
    95. 4.95. Repeating an element in a standard finite type
    96. 4.96. Retracts of the type of natural numbers
    97. 4.97. The ring of integers
    98. 4.98. Rings of modular arithmetic
    99. 4.99. The sieve of Eratosthenes
    100. 4.100. Square-free natural numbers
    101. 4.101. Stirling numbers of the second kind
    102. 4.102. Strict inequality natural numbers
    103. 4.103. Strictly ordered pairs of natural numbers
    104. 4.104. The strong induction principle for the natural numbers
    105. 4.105. Sums of natural numbers
    106. 4.106. Telephone numbers
    107. 4.107. The triangular numbers
    108. 4.108. The Twin Prime conjecture
    109. 4.109. Type arithmetic with natural numbers
    110. 4.110. Unit elements in the standard finite types
    111. 4.111. Unit similarity on the standard finite types
    112. 4.112. The universal property of the integers
    113. 4.113. The universal property of the natural numbers
    114. 4.114. Upper bounds for type families over the natural numbers
    115. 4.115. The Well-Ordering Principle of the natural numbers
    116. 4.116. 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 sets
    35. 7.35. Choice of representatives for an equivalence relation
    36. 7.36. Codiagonal maps of types
    37. 7.37. Coherently invertible maps
    38. 7.38. Commuting 3-simplices of homotopies
    39. 7.39. Commuting 3-simplices of maps
    40. 7.40. Commuting cubes of maps
    41. 7.41. Commuting hexagons of identifications
    42. 7.42. Commuting squares of identifications
    43. 7.43. Commuting squares of maps
    44. 7.44. Commuting triangles of homotopies
    45. 7.45. Commuting triangles of maps
    46. 7.46. Complements of type families
    47. 7.47. Complements of subtypes
    48. 7.48. Cones over cospans
    49. 7.49. Conjunction of propositions
    50. 7.50. Connected components of types
    51. 7.51. Connected components of universes
    52. 7.52. Connected maps
    53. 7.53. Connected types
    54. 7.54. Constant maps
    55. 7.55. Constant type families
    56. 7.56. Contractible maps
    57. 7.57. Contractible types
    58. 7.58. Coproduct decompositions
    59. 7.59. Coproduct decompositions in a subuniverse
    60. 7.60. Coproduct types
    61. 7.61. Morphisms in the coslice category of types
    62. 7.62. Cospans of types
    63. 7.63. Decidability of dependent function types
    64. 7.64. Decidability of dependent pair types
    65. 7.65. Decidable embeddings
    66. 7.66. Decidable equality
    67. 7.67. Decidable equivalence relations
    68. 7.68. Decidable maps
    69. 7.69. Decidable propositions
    70. 7.70. Decidable relations on types
    71. 7.71. Decidable subtypes
    72. 7.72. Decidable types
    73. 7.73. The dependent binomial theorem for types (distributivity of dependent function types over coproduct types)
    74. 7.74. Dependent identifications
    75. 7.75. Dependent pair types
    76. 7.76. Descent for coproduct types
    77. 7.77. Descent for dependent pair types
    78. 7.78. Descent for the empty type
    79. 7.79. Descent for equivalences
    80. 7.80. Diagonal maps of types
    81. 7.81. Diagonals of maps
    82. 7.82. Discrete reflexive relations
    83. 7.83. Discrete relaxed Σ-decompositions
    84. 7.84. Discrete Σ-decompositions
    85. 7.85. Discrete types
    86. 7.86. Disjunction of propositions
    87. 7.87. Double negation
    88. 7.88. The double negation modality
    89. 7.89. Double powersets
    90. 7.90. Dubuc-Penon compact types
    91. 7.91. Effective maps for equivalence relations
    92. 7.92. Embeddings
    93. 7.93. Empty types
    94. 7.94. Endomorphisms
    95. 7.95. Epimorphisms
    96. 7.96. Epimorphisms with respect to maps into sets
    97. 7.97. Epimorphisms with respect to truncated types
    98. 7.98. Equality of cartesian product types
    99. 7.99. Equality of coproduct types
    100. 7.100. Equality on dependent function types
    101. 7.101. Equality of dependent pair types
    102. 7.102. Equality in the fibers of a map
    103. 7.103. Equivalence classes
    104. 7.104. Equivalence extensionality
    105. 7.105. Equivalence induction
    106. 7.106. Equivalence relations
    107. 7.107. Equivalences
    108. 7.108. Equivalences on Maybe
    109. 7.109. Exclusive disjunction of propositions
    110. 7.110. Existential quantification
    111. 7.111. Exponents of set quotients
    112. 7.112. Faithful maps
    113. 7.113. Fiber inclusions
    114. 7.114. Fibered equivalences
    115. 7.115. Fibered involutions
    116. 7.116. Maps fibered over a map
    117. 7.117. Fibers of maps
    118. 7.118. Full subtypes of types
    119. 7.119. Function extensionality
    120. 7.120. Function types
    121. 7.121. Functional correspondences
    122. 7.122. Functoriality of cartesian product types
    123. 7.123. Functoriality of coproduct types
    124. 7.124. Functoriality of dependent function types
    125. 7.125. Functoriality of dependent pair types
    126. 7.126. The functoriality of fiber
    127. 7.127. Functoriality of function types
    128. 7.128. Functoriality of propositional truncations
    129. 7.129. Functoriality of set quotients
    130. 7.130. Functoriality of set truncation
    131. 7.131. Functoriality of truncations
    132. 7.132. The fundamental theorem of identity types
    133. 7.133. Global choice
    134. 7.134. Hilbert's ε-operators
    135. 7.135. Homotopies
    136. 7.136. Homotopy induction
    137. 7.137. Identity systems
    138. 7.138. Identity types of truncated types
    139. 7.139. Identity types
    140. 7.140. The image of a map
    141. 7.141. Images of subtypes
    142. 7.142. Impredicative encodings of the logical operations
    143. 7.143. Impredicative universes
    144. 7.144. The induction principle for propositional truncation
    145. 7.145. Inhabited subtypes
    146. 7.146. Inhabited types
    147. 7.147. Injective maps
    148. 7.148. The interchange law
    149. 7.149. Intersections of subtypes
    150. 7.150. Invertible maps
    151. 7.151. Involutions
    152. 7.152. Isolated points
    153. 7.153. Isomorphisms of sets
    154. 7.154. Iterated cartesian product types
    155. 7.155. Iterating automorphisms
    156. 7.156. Iterating functions
    157. 7.157. Iterating involutions
    158. 7.158. Large binary relations
    159. 7.159. Large dependent pair types
    160. 7.160. Large homotopies
    161. 7.161. Large identity types
    162. 7.162. The large locale of propositions
    163. 7.163. The large locale of subtypes
    164. 7.164. The law of excluded middle
    165. 7.165. Lawvere's fixed point theorem
    166. 7.166. The lesser limited principle of omniscience
    167. 7.167. The limited principle of omniscience
    168. 7.168. Locally small types
    169. 7.169. Logical equivalences
    170. 7.170. The maybe modality
    171. 7.171. Mere embeddings
    172. 7.172. Mere equality
    173. 7.173. Mere equivalences
    174. 7.174. Monomorphisms
    175. 7.175. Morphisms of cospans
    176. 7.176. Multisubsets
    177. 7.177. Multivariable correspondences
    178. 7.178. Multivariable decidable relations
    179. 7.179. Multivariable functoriality of set quotients
    180. 7.180. Multivariable operations
    181. 7.181. Multivariable relations
    182. 7.182. Negation
    183. 7.183. Non-contractible types
    184. 7.184. Pairs of distinct elements
    185. 7.185. Partial elements
    186. 7.186. Partitions
    187. 7.187. Path algebra
    188. 7.188. Path-split maps
    189. 7.189. Perfect images
    190. 7.190. Π-decompositions of types
    191. 7.191. Π-decompositions of types into types in a subuniverse
    192. 7.192. Pointed torsorial type families
    193. 7.193. Powersets
    194. 7.194. Preidempotent maps
    195. 7.195. Preimages of subtypes
    196. 7.196. The principle of omniscience
    197. 7.197. Product decompositions
    198. 7.198. Product decompositions of types in a subuniverse
    199. 7.199. Products of binary relations
    200. 7.200. Products of equivalence relataions
    201. 7.201. Products of tuples of types
    202. 7.202. Products of unordered pairs of types
    203. 7.203. Products of unordered tuples of types
    204. 7.204. Projective types
    205. 7.205. Proper subsets
    206. 7.206. Propositional extensionality
    207. 7.207. Propositional maps
    208. 7.208. Propositional resizing
    209. 7.209. Propositional truncations
    210. 7.210. Propositions
    211. 7.211. Pullback squares
    212. 7.212. Pullbacks
    213. 7.213. Raising universe levels
    214. 7.214. Reflecting maps for equivalence relations
    215. 7.215. Reflexive relations
    216. 7.216. Relaxed Σ-decompositions of types
    217. 7.217. Repetitions of values of maps
    218. 7.218. Repetitions in sequences
    219. 7.219. The replacement axiom for type theory
    220. 7.220. Retractions
    221. 7.221. Russell's paradox
    222. 7.222. Sections
    223. 7.223. Sequences
    224. 7.224. Set presented types
    225. 7.225. Set quotients
    226. 7.226. Set truncations
    227. 7.227. Sets
    228. 7.228. Shifting sequences
    229. 7.229. Σ-closed subuniverses
    230. 7.230. Σ-decompositions of types into types in a subuniverse
    231. 7.231. Σ-decompositions of types
    232. 7.232. Singleton induction
    233. 7.233. Singleton subtypes
    234. 7.234. Morphisms in the slice category of types
    235. 7.235. Small maps
    236. 7.236. Small types
    237. 7.237. Small universes
    238. 7.238. Sorial type families
    239. 7.239. Spans of types
    240. 7.240. Split surjective maps
    241. 7.241. Standard apartness relations
    242. 7.242. Strongly extensional maps
    243. 7.243. Structure
    244. 7.244. The structure identity principle
    245. 7.245. Structured type duality
    246. 7.246. Subterminal types
    247. 7.247. Subtype duality
    248. 7.248. The subtype identity principle
    249. 7.249. Subtypes
    250. 7.250. Subuniverses
    251. 7.251. Surjective maps
    252. 7.252. Symmetric binary relations
    253. 7.253. Symmetric cores of binary relations
    254. 7.254. Symmetric difference of subtypes
    255. 7.255. The symmetric identity types
    256. 7.256. Symmetric operations
    257. 7.257. Tight apartness relations
    258. 7.258. Torsorial type families
    259. 7.259. Transport along equivalences
    260. 7.260. Transport along identifications
    261. 7.261. Trivial relaxed Σ-decompositions
    262. 7.262. Trivial Σ-decompositions
    263. 7.263. Truncated equality
    264. 7.264. Truncated maps
    265. 7.265. Truncated types
    266. 7.266. k-Equivalences
    267. 7.267. Truncation images of maps
    268. 7.268. Truncation levels
    269. 7.269. The truncation modalities
    270. 7.270. Truncations
    271. 7.271. Tuples of types
    272. 7.272. Type arithmetic with the booleans
    273. 7.273. Type arithmetic for cartesian product types
    274. 7.274. Type arithmetic for coproduct types
    275. 7.275. Type arithmetic with dependent function types
    276. 7.276. Type arithmetic for dependent pair types
    277. 7.277. Type arithmetic with the empty type
    278. 7.278. Type arithmetic with the unit type
    279. 7.279. Type duality
    280. 7.280. The type theoretic principle of choice
    281. 7.281. Unions of subtypes
    282. 7.282. Unique existence
    283. 7.283. Uniqueness of the image of a map
    284. 7.284. The uniqueness of set quotients
    285. 7.285. Uniqueness of set truncations
    286. 7.286. Uniqueness of the truncations
    287. 7.287. The unit type
    288. 7.288. Unital binary operations
    289. 7.289. The univalence axiom
    290. 7.290. The univalence axiom implies function extensionality
    291. 7.291. Univalent type families
    292. 7.292. The universal property of booleans
    293. 7.293. The universal propert of cartesian product types
    294. 7.294. The universal property of coproduct types
    295. 7.295. The universal property of dependent pair types
    296. 7.296. The universal property of the empty type
    297. 7.297. The universal property of fiber products
    298. 7.298. The universal property of identity systems
    299. 7.299. The universal property of identity types
    300. 7.300. The universal property of the image of a map
    301. 7.301. The universal property of maybe
    302. 7.302. The universal property of propositional truncations
    303. 7.303. The universal property of propositional truncations with respect to sets
    304. 7.304. The universal property of pullbacks
    305. 7.305. The universal property of set quotients
    306. 7.306. The universal property of set truncations
    307. 7.307. The universal property of truncations
    308. 7.308. The universal property of the unit type
    309. 7.309. Universe levels
    310. 7.310. Unordered pairs of elements in a type
    311. 7.311. Unordered pairs of types
    312. 7.312. Unordered n-tuples of elements in a type
    313. 7.313. Unordered tuples of types
    314. 7.314. Vectors of set quotients
    315. 7.315. Weak function extensionality
    316. 7.316. The weak limited principle of omniscience
    317. 7.317. Weakly constant maps
    318. 7.318. 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. Dependent products of H-spaces
    8. 25.8. Dependent products of pointed types
    9. 25.9. Dependent products of wild monoids
    10. 25.10. Equivalences of types equipped with endomorphisms
    11. 25.11. Faithful pointed maps
    12. 25.12. Fibers of pointed maps
    13. 25.13. Finite multiplication in magmas
    14. 25.14. Function H-spaces
    15. 25.15. Function magmas
    16. 25.16. Function wild monoids
    17. 25.17. H-spaces
    18. 25.18. The initial pointed type equipped with an automorphism
    19. 25.19. The involutive type of H-space structures on a pointed type
    20. 25.20. Involutive types
    21. 25.21. Iterated cartesian products of types equipped with endomorphisms
    22. 25.22. Iterated cartesian products of pointed types
    23. 25.23. Magmas
    24. 25.24. Mere equivalences of types equipped with endomorphisms
    25. 25.25. Morphisms of H-spaces
    26. 25.26. Morphisms of magmas
    27. 25.27. Morphisms of types equipped with endomorphisms
    28. 25.28. Morphisms of wild monoids
    29. 25.29. Non-coherent H-spaces
    30. 25.30. Pointed cartesian product types
    31. 25.31. Pointed dependent functions
    32. 25.32. Pointed dependent pair types
    33. 25.33. Pointed equivalences
    34. 25.34. Pointed families of types
    35. 25.35. Pointed homotopies
    36. 25.36. Pointed maps
    37. 25.37. Pointed sections of pointed maps
    38. 25.38. Pointed types
    39. 25.39. Pointed types equipped with automorphisms
    40. 25.40. The pointed unit type
    41. 25.41. Symmetric elements of involutive types
    42. 25.42. Symmetric H-spaces
    43. 25.43. Types equipped with automorphisms
    44. 25.44. Types equipped with endomorphisms
    45. 25.45. Unpointed maps between pointed types
    46. 25.46. Wild groups
    47. 25.47. Wild loops
    48. 25.48. Wild monoids
    49. 25.49. Wild quasigroups
    50. 25.50. 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. Cavallo's trick
    7. 26.7. The circle
    8. 26.8. Cocones under spans
    9. 26.9. Cocones under spans of pointed types
    10. 26.10. Coequalizers
    11. 26.11. Cofibers
    12. 26.12. Coforks
    13. 26.13. Conjugation of loops
    14. 26.14. Dependent cocones under spans
    15. 26.15. Dependent coforks
    16. 26.16. The dependent pullback property of pushouts
    17. 26.17. Dependent suspension structures
    18. 26.18. The dependent universal property of coequalizers
    19. 26.19. The dependent universal property of pushouts
    20. 26.20. Dependent universal property of suspensions
    21. 26.21. The descent property of the circle
    22. 26.22. Descent data for constant type families over the circle
    23. 26.23. Descent data for families of dependent pair types over the circle
    24. 26.24. Descent data for families of equivalence types over the circle
    25. 26.25. Descent data for families of function types over the circle
    26. 26.26. Subtypes of descent data for the circle
    27. 26.27. Double loop spaces
    28. 26.28. The flattening lemma for coequalizers
    29. 26.29. The flattening lemma for pushouts
    30. 26.30. Free loops
    31. 26.31. Functoriality of the loop space operation
    32. 26.32. Groups of loops in 1-types
    33. 26.33. Hatcher's acyclic type
    34. 26.34. The induction principle of pushouts
    35. 26.35. The infinite complex projective space
    36. 26.36. Infinite cyclic types
    37. 26.37. The interval
    38. 26.38. Iterated loop spaces
    39. 26.39. Join powers of types
    40. 26.40. Joins of types
    41. 26.41. Loop spaces
    42. 26.42. The multiplication operation on the circle
    43. 26.43. The plus-principle
    44. 26.44. Powers of loops
    45. 26.45. Prespectra
    46. 26.46. The pullback property of pushouts
    47. 26.47. Pushouts
    48. 26.48. Pushouts of pointed types
    49. 26.49. Sections of families over the circle
    50. 26.50. Smash products of pointed types
    51. 26.51. Spectra
    52. 26.52. Spheres
    53. 26.53. Suspension Structures
    54. 26.54. Suspensions of pointed types
    55. 26.55. Suspensions of types
    56. 26.56. Triple loop spaces
    57. 26.57. The universal cover of the circle
    58. 26.58. The universal property of the circle
    59. 26.59. The universal property of coequalizers
    60. 26.60. The universal property of pushouts
    61. 26.61. Universal property of suspensions
    62. 26.62. Universal Property of suspensions of pointed types
    63. 26.63. 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

Repetitions of values in sequences

Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-04-08.
Last modified on 2023-05-01.

module univalent-combinatorics.repetitions-of-values-sequences where
Imports

Properties

{-
is-decidable-is-ordered-repetition-of-values-ℕ-Fin :
  (k : ℕ) (f : ℕ → Fin k) (x : ℕ) →
  is-decidable (is-ordered-repetition-of-values-ℕ f x)
is-decidable-is-ordered-repetition-of-values-ℕ-Fin k f x = {!!}
-}

{-
  is-decidable-strictly-bounded-Σ-ℕ' x
    ( λ y → Id (f y) (f x))
    ( λ y → has-decidable-equality-Fin k (f y) (f x))
-}

{-
is-decidable-is-ordered-repetition-of-values-ℕ-count :
  {l : Level} {A : UU l} (e : count A) (f : ℕ → A) (x : ℕ) →
  is-decidable (is-ordered-repetition-of-values-ℕ f x)
is-decidable-is-ordered-repetition-of-values-ℕ-count e f x = {!!}
-}

{-
  is-decidable-strictly-bounded-Σ-ℕ' x
    ( λ y → Id (f y) (f x))
    ( λ y → has-decidable-equality-count e (f y) (f x))
  -}

Recent changes

  • 2023-05-01. Fredrik Bakke. Refactor 2, the sequel to refactor (#581).
  • 2023-04-08. Egbert Rijke. Refactoring elementary number theory files (#546).