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

The principle of omniscience

Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.

Created on 2022-04-09.
Last modified on 2023-06-08.

module foundation.principle-of-omniscience where
Imports
open import foundation.decidable-subtypes
open import foundation.propositional-truncations
open import foundation.universe-levels

open import foundation-core.decidable-propositions
open import foundation-core.propositions

Idea

A type X is said to satisfy the principle of omniscience if every decidable subtype of X is either inhabited or empty.

Definition

is-omniscient-Prop : {l : Level} → UU l → Prop (lsuc lzero ⊔ l)
is-omniscient-Prop X =
  Π-Prop
    ( decidable-subtype lzero X)
    ( λ P → is-decidable-Prop (trunc-Prop (type-decidable-subtype P)))

is-omniscient : {l : Level} → UU l → UU (lsuc lzero ⊔ l)
is-omniscient X = type-Prop (is-omniscient-Prop X)

See also

  • The limited principle of omniscience
  • The lesser limited principle of omniscience
  • The weak limited principle of omniscience

Recent changes

  • 2023-06-08. Fredrik Bakke. Examples of modalities and various fixes (#639).
  • 2023-06-08. Fredrik Bakke. Remove empty foundation modules and replace them by their core counterparts (#644).
  • 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
  • 2023-03-13. Jonathan Prieto-Cubides. More maintenance (#506).
  • 2023-03-07. Fredrik Bakke. Add blank lines between <details> tags and markdown syntax (#490).