1. Overview
  2. 1. Home
  3. 2. Community
    ❱
    1. 2.1. Maintainers
    2. 2.2. Contributors
    3. 2.3. Statement of inclusivity
    4. 2.4. Projects using agda-unimath
    5. 2.5. Grant acknowledgments
  4. 3. Guides
    ❱
    1. 3.1. Installing the library
    2. 3.2. Design principles
    3. 3.3. Contributing to the library
    4. 3.4. Structuring your file
      ❱
      1. 3.4.1. File template
    5. 3.5. The library coding style
    6. 3.6. Guidelines for mixfix operators
    7. 3.7. Citing sources
    8. 3.8. Citing the library
  5. 4. Library explorer
  6. 5. Art
  7. 6. Full list of library contents
  8. 7. Formalization of results from the literature
    ❱
    1. 7.1. Wiedijk's 100 Theorems
    2. 7.2. Idempotents in Intensional Type Theory
    3. 7.3. Introduction to homotopy type theory
    4. 7.4. Sequences of the online encyclopedia of integer sequences
    5. 7.5. Sequential Colimits in Homotopy Type Theory
    6. 7.6. Wikipedia's list of theorems
  9. The agda-unimath library
  10. 8. Analysis
    ❱
    1. 8.1. Convergent series in metric abelian groups
    2. 8.2. Metric abelian groups
    3. 8.3. Series in metric abelian groups
  11. 9. Category theory
    ❱
    1. 9.1. Adjunctions between large categories
    2. 9.2. Adjunctions between large precategories
    3. 9.3. Adjunctions between precategories
    4. 9.4. Algebras over monads on precategories
    5. 9.5. Anafunctors between categories
    6. 9.6. Anafunctors between precategories
    7. 9.7. The augmented simplex category
    8. 9.8. Categories
    9. 9.9. The category of functors and natural transformations between two categories
    10. 9.10. The category of functors and natural transformations from small to large categories
    11. 9.11. The category of maps and natural transformations between two categories
    12. 9.12. The category of maps and natural transformations from small to large categories
    13. 9.13. The category of simplicial sets
    14. 9.14. Coalgebras over comonads on precategories
    15. 9.15. Cocones in precategories
    16. 9.16. Codensity monads on precategories
    17. 9.17. Colimits in precategories
    18. 9.18. Commuting squares of morphisms in large precategories
    19. 9.19. Commuting squares of morphisms in precategories
    20. 9.20. Commuting squares of morphisms in set-magmoids
    21. 9.21. Commuting triangles of morphisms in precategories
    22. 9.22. Commuting triangles of morphisms in set-magmoids
    23. 9.23. Comonads on precategories
    24. 9.24. Complete precategories
    25. 9.25. Composition operations on binary families of sets
    26. 9.26. Cones in precategories
    27. 9.27. Conservative functors between precategories
    28. 9.28. Constant functors
    29. 9.29. Copointed endofunctors on precategories
    30. 9.30. Copresheaf categories
    31. 9.31. Coproducts in precategories
    32. 9.32. Cores of categories
    33. 9.33. Cores of precategories
    34. 9.34. Coslice precategories
    35. 9.35. Density comonads on precategories
    36. 9.36. Dependent composition operations over precategories
    37. 9.37. Dependent products of categories
    38. 9.38. Dependent products of large categories
    39. 9.39. Dependent products of large precategories
    40. 9.40. Dependent products of precategories
    41. 9.41. Discrete categories
    42. 9.42. Displayed precategories
    43. 9.43. Embedding maps between precategories
    44. 9.44. Embeddings between precategories
    45. 9.45. Endomorphisms in categories
    46. 9.46. Endomorphisms in precategories
    47. 9.47. Epimorphism in large precategories
    48. 9.48. Equivalences between categories
    49. 9.49. Equivalences between large precategories
    50. 9.50. Equivalences between precategories
    51. 9.51. Essential fibers of functors between precategories
    52. 9.52. Essentially injective functors between precategories
    53. 9.53. Essentially surjective functors between precategories
    54. 9.54. Exponential objects in precategories
    55. 9.55. Extensions of functors between precategories
    56. 9.56. Faithful functors between precategories
    57. 9.57. Faithful maps between precategories
    58. 9.58. Full functors between precategories
    59. 9.59. Full large subcategories
    60. 9.60. Full large subprecategories
    61. 9.61. Full maps between precategories
    62. 9.62. Full subcategories
    63. 9.63. Full subprecategories
    64. 9.64. Fully faithful functors between precategories
    65. 9.65. Fully faithful maps between precategories
    66. 9.66. Function categories
    67. 9.67. Function precategories
    68. 9.68. Functors between categories
    69. 9.69. Functors from small to large categories
    70. 9.70. Functors from small to large precategories
    71. 9.71. Functors between large categories
    72. 9.72. Functors between large precategories
    73. 9.73. Functors between nonunital precategories
    74. 9.74. Functors between precategories
    75. 9.75. Functors between set-magmoids
    76. 9.76. Gaunt categories
    77. 9.77. Groupoids
    78. 9.78. Homotopies of natural transformations in large precategories
    79. 9.79. Indiscrete precategories
    80. 9.80. The initial category
    81. 9.81. Initial objects of large categories
    82. 9.82. Initial objects of large precategories
    83. 9.83. Initial objects in a precategory
    84. 9.84. Isomorphism induction in categories
    85. 9.85. Isomorphism induction in precategories
    86. 9.86. Isomorphisms in categories
    87. 9.87. Isomorphisms in large categories
    88. 9.88. Isomorphisms in large precategories
    89. 9.89. Isomorphisms in precategories
    90. 9.90. Isomorphisms in subprecategories
    91. 9.91. Large categories
    92. 9.92. Large function categories
    93. 9.93. Large function precategories
    94. 9.94. Large precategories
    95. 9.95. Large subcategories
    96. 9.96. Large subprecategories
    97. 9.97. Left extensions in precategories
    98. 9.98. Left Kan extensions in precategories
    99. 9.99. Limits in precategories
    100. 9.100. Maps between categories
    101. 9.101. Maps from small to large categories
    102. 9.102. Maps from small to large precategories
    103. 9.103. Maps between precategories
    104. 9.104. Maps between set-magmoids
    105. 9.105. Monads on categories
    106. 9.106. Monads on precategories
    107. 9.107. Monomorphisms in large precategories
    108. 9.108. Morphisms of algebras over monads on precategories
    109. 9.109. Morphisms of coalgebras over comonads on precategories
    110. 9.110. Natural isomorphisms between functors between categories
    111. 9.111. Natural isomorphisms between functors between large precategories
    112. 9.112. Natural isomorphisms between functors between precategories
    113. 9.113. Natural isomorphisms between maps between categories
    114. 9.114. Natural isomorphisms between maps between precategories
    115. 9.115. Natural numbers object in a precategory
    116. 9.116. Natural transformations between functors between categories
    117. 9.117. Natural transformations between functors from small to large categories
    118. 9.118. Natural transformations between functors from small to large precategories
    119. 9.119. Natural transformations between functors between large categories
    120. 9.120. Natural transformations between functors between large precategories
    121. 9.121. Natural transformations between functors between precategories
    122. 9.122. Natural transformations between maps between categories
    123. 9.123. Natural transformations between maps from small to large precategories
    124. 9.124. Natural transformations between maps between precategories
    125. 9.125. Nonunital precategories
    126. 9.126. One object precategories
    127. 9.127. Opposite categories
    128. 9.128. Opposite large precategories
    129. 9.129. Opposite precategories
    130. 9.130. Opposite preunivalent categories
    131. 9.131. Opposite strongly preunivalent categories
    132. 9.132. Pointed endofunctors on categories
    133. 9.133. Pointed endofunctors on precategories
    134. 9.134. Precategories
    135. 9.135. The precategory of algebras over a monad
    136. 9.136. The precategory of coalgebras over a comonad
    137. 9.137. Precategory of elements of a presheaf
    138. 9.138. The precategory of free algebras of a monad
    139. 9.139. The precategory of functors and natural transformations between two precategories
    140. 9.140. The precategory of functors and natural transformations from small to large precategories
    141. 9.141. The precategory of maps and natural transformations from a small to a large precategory
    142. 9.142. The precategory of maps and natural transformations between two precategories
    143. 9.143. Pregroupoids
    144. 9.144. Presheaf categories
    145. 9.145. Preunivalent categories
    146. 9.146. Products in precategories
    147. 9.147. Products of precategories
    148. 9.148. Pseudomonic functors between precategories
    149. 9.149. Pullbacks in precategories
    150. 9.150. Replete subprecategories
    151. 9.151. Representable functors between categories
    152. 9.152. Representable functors between large precategories
    153. 9.153. Representable functors between precategories
    154. 9.154. The representing arrow category
    155. 9.155. Restrictions of functors to cores of precategories
    156. 9.156. Right extensions in precategories
    157. 9.157. Right Kan extensions in precategories
    158. 9.158. Rigid objects in a category
    159. 9.159. Rigid objects in a precategory
    160. 9.160. Set-magmoids
    161. 9.161. Sieves in categories
    162. 9.162. The simplex category
    163. 9.163. Slice precategories
    164. 9.164. Split essentially surjective functors between precategories
    165. 9.165. Strict categories
    166. 9.166. Strongly preunivalent categories
    167. 9.167. Structure equivalences between set-magmoids
    168. 9.168. Subcategories
    169. 9.169. Subprecategories
    170. 9.170. Subterminal precategories
    171. 9.171. The terminal category
    172. 9.172. Terminal objects in a precategory
    173. 9.173. Wide subcategories
    174. 9.174. Wide subprecategories
    175. 9.175. The Yoneda lemma for categories
    176. 9.176. The Yoneda lemma for precategories
  12. 10. Commutative algebra
    ❱
    1. 10.1. The binomial theorem in commutative rings
    2. 10.2. The binomial theorem in commutative semirings
    3. 10.3. Boolean rings
    4. 10.4. The category of commutative rings
    5. 10.5. Commutative rings
    6. 10.6. Commutative semirings
    7. 10.7. Convolution of sequences in commutative rings
    8. 10.8. Convolution of sequences in commutative semirings
    9. 10.9. Dependent products of commutative rings
    10. 10.10. Dependent products of commutative semirings
    11. 10.11. Discrete fields
    12. 10.12. The Eisenstein integers
    13. 10.13. Euclidean domains
    14. 10.14. Formal power series in commutative rings
    15. 10.15. Formal power series in commutative semirings
    16. 10.16. Full ideals of commutative rings
    17. 10.17. Function commutative rings
    18. 10.18. Function commutative semirings
    19. 10.19. The Gaussian integers
    20. 10.20. The group of multiplicative units of a commutative ring
    21. 10.21. Homomorphisms of commutative rings
    22. 10.22. Homomorphisms of commutative semirings
    23. 10.23. Ideals of commutative rings
    24. 10.24. Ideals of commutative semirings
    25. 10.25. Ideals generated by subsets of commutative rings
    26. 10.26. Integer multiples of elements of commutative rings
    27. 10.27. Integral domains
    28. 10.28. Intersections of ideals of commutative rings
    29. 10.29. Intersections of radical ideals of commutative rings
    30. 10.30. Invertible elements in commutative rings
    31. 10.31. Isomorphisms of commutative rings
    32. 10.32. Joins of ideals of commutative rings
    33. 10.33. Joins of radical ideals of commutative rings
    34. 10.34. Local commutative rings
    35. 10.35. Maximal ideals of commutative rings
    36. 10.36. Multiples of elements in commutative rings
    37. 10.37. Nilradical of a commutative ring
    38. 10.38. The nilradical of a commutative semiring
    39. 10.39. Polynomials in commutative rings
    40. 10.40. Polynomials in commutative semirings
    41. 10.41. The poset of ideals of a commutative ring
    42. 10.42. The poset of radical ideals of a commutative ring
    43. 10.43. Powers of elements in commutative rings
    44. 10.44. Powers of elements in commutative semirings
    45. 10.45. The precategory of commutative rings
    46. 10.46. The precategory of commutative semirings
    47. 10.47. Prime ideals of commutative rings
    48. 10.48. Products of commutative rings
    49. 10.49. Products of ideals of commutative rings
    50. 10.50. Products of radical ideals of a commutative ring
    51. 10.51. Products of subsets of commutative rings
    52. 10.52. Radical ideals of commutative rings
    53. 10.53. Radical ideals generated by subsets of commutative rings
    54. 10.54. Radicals of ideals of commutative rings
    55. 10.55. Subsets of commutative rings
    56. 10.56. Subsets of commutative semirings
    57. 10.57. Sums of finite families in commutative rings
    58. 10.58. Sums of finite families of elements in commutative semirings
    59. 10.59. Sums of finite sequences in commutative rings
    60. 10.60. Sums of finite sequences in commutative semirings
    61. 10.61. Transporting commutative ring structures along isomorphisms of abelian groups
    62. 10.62. Trivial commutative rings
    63. 10.63. The Zariski locale
    64. 10.64. The Zariski topology on the set of prime ideals of a commutative ring
  13. 11. Domain theory
    ❱
    1. 11.1. Directed complete posets
    2. 11.2. Directed families in posets
    3. 11.3. Kleene's fixed point theorem for ω-complete posets
    4. 11.4. Kleene's fixed point theorem for posets
    5. 11.5. ω-Complete posets
    6. 11.6. ω-Continuous maps between ω-complete posets
    7. 11.7. ω-Continuous maps between posets
    8. 11.8. Reindexing directed families in posets
    9. 11.9. Scott-continuous maps between posets
  14. 12. Elementary number theory
    ❱
    1. 12.1. The absolute value function on the integers
    2. 12.2. The absolute value function on the rational numbers
    3. 12.3. The Ackermann function
    4. 12.4. Addition on closed intervals in the rational numbers
    5. 12.5. Addition on integer fractions
    6. 12.6. Addition on the integers
    7. 12.7. Addition on the natural numbers
    8. 12.8. Addition on nonnegative rational numbers
    9. 12.9. Addition of positive, negative, nonnegative and nonpositive integers
    10. 12.10. Addition of positive rational numbers
    11. 12.11. Addition on the rational numbers
    12. 12.12. The additive group of rational numbers
    13. 12.13. The Archimedean property of integer fractions
    14. 12.14. The Archimedean property of the integers
    15. 12.15. The Archimedean property of the natural numbers
    16. 12.16. The Archimedean property of the positive rational numbers
    17. 12.17. The Archimedean property of ℚ
    18. 12.18. Arithmetic functions
    19. 12.19. Arithmetic sequences of positive rational numbers
    20. 12.20. The based induction principle of the natural numbers
    21. 12.21. Based strong induction for the natural numbers
    22. 12.22. The Bell numbers
    23. 12.23. Bernoulli's inequality on the positive rational numbers
    24. 12.24. Bezout's lemma in the integers
    25. 12.25. Bezout's lemma on the natural numbers
    26. 12.26. Binary sum decompositions of natural numbers
    27. 12.27. The binomial coefficients
    28. 12.28. The binomial theorem for the integers
    29. 12.29. The binomial theorem for the natural numbers
    30. 12.30. Bounded sums of arithmetic functions
    31. 12.31. Catalan numbers
    32. 12.32. Closed intervals in the rational numbers
    33. 12.33. The cofibonacci sequence
    34. 12.34. The Collatz bijection
    35. 12.35. The Collatz conjecture
    36. 12.36. The commutative semiring of natural numbers
    37. 12.37. Conatural numbers
    38. 12.38. The congruence relations on the integers
    39. 12.39. The congruence relations on the natural numbers
    40. 12.40. The cross-multiplication difference of two integer fractions
    41. 12.41. The cross-multiplication difference of two rational numbers
    42. 12.42. Cubes of natural numbers
    43. 12.43. Decidable dependent function types
    44. 12.44. The decidable total order of integers
    45. 12.45. The decidable total order of natural numbers
    46. 12.46. The decidable total order of rational numbers
    47. 12.47. The decidable total order of a standard finite type
    48. 12.48. Decidable types in elementary number theory
    49. 12.49. The difference between integers
    50. 12.50. The difference between rational numbers
    51. 12.51. Dirichlet convolution
    52. 12.52. The distance between integers
    53. 12.53. The distance between natural numbers
    54. 12.54. The distance between rational numbers
    55. 12.55. Divisibility of integers
    56. 12.56. Divisibility in modular arithmetic
    57. 12.57. Divisibility of natural numbers
    58. 12.58. The divisibility relation on the standard finite types
    59. 12.59. Equality of conatural numbers
    60. 12.60. Equality of integers
    61. 12.61. Equality of natural numbers
    62. 12.62. Equality of rational numbers
    63. 12.63. The Euclid–Mullin sequence
    64. 12.64. Euclidean division on the natural numbers
    65. 12.65. Euler's totient function
    66. 12.66. Exponentiation of natural numbers
    67. 12.67. Factorials of natural numbers
    68. 12.68. Falling factorials
    69. 12.69. Fermat numbers
    70. 12.70. The Fibonacci sequence
    71. 12.71. The field of rational numbers
    72. 12.72. The natural numbers base k
    73. 12.73. Finitely cyclic maps
    74. 12.74. The fundamental theorem of arithmetic
    75. 12.75. Geometric sequences of positive rational numbers
    76. 12.76. The Goldbach conjecture
    77. 12.77. The greatest common divisor of integers
    78. 12.78. The greatest common divisor of natural numbers
    79. 12.79. The group of integers
    80. 12.80. The half-integers
    81. 12.81. The Hardy-Ramanujan number
    82. 12.82. The inclusion of the natural numbers into the conatural numbers
    83. 12.83. Inequality of arithmetic and geometric means on the integers
    84. 12.84. Inequality of arithmetic and geometric means on the rational numbers
    85. 12.85. Inequality of conatural numbers
    86. 12.86. Inequality on integer fractions
    87. 12.87. Inequality on the integers
    88. 12.88. Inequality of natural numbers
    89. 12.89. Inequality on the nonnegative rational numbers
    90. 12.90. Inequality on the positive rational numbers
    91. 12.91. Inequality on the rational numbers
    92. 12.92. Inequality on the standard finite types
    93. 12.93. Infinite conatural numbers
    94. 12.94. The infinitude of primes
    95. 12.95. Initial segments of the natural numbers
    96. 12.96. Integer fractions
    97. 12.97. Integer partitions
    98. 12.98. The integers
    99. 12.99. Intersections of closed intervals of rational numbers
    100. 12.100. The Jacobi symbol
    101. 12.101. The Kolakoski sequence
    102. 12.102. The Legendre symbol
    103. 12.103. Lower bounds of type families over the natural numbers
    104. 12.104. Maximum on the natural numbers
    105. 12.105. The maximum of positive rational numbers
    106. 12.106. Maximum on the rational numbers
    107. 12.107. Maximum on the standard finite types
    108. 12.108. The mediant fraction of two integer fractions
    109. 12.109. Mersenne primes
    110. 12.110. Minimum on the natural numbers
    111. 12.111. The minimum of positive rational numbers
    112. 12.112. Minimum on the rational numbers
    113. 12.113. Minimum on the standard finite types
    114. 12.114. Modular arithmetic
    115. 12.115. Modular arithmetic on the standard finite types
    116. 12.116. The monoid of natural numbers with addition
    117. 12.117. The monoid of the natural numbers with maximum
    118. 12.118. Multiplication on closed intervals in the rational numbers
    119. 12.119. Multiplication on integer fractions
    120. 12.120. Multiplication of integers
    121. 12.121. Multiplication of the elements of a list of natural numbers
    122. 12.122. Multiplication of natural numbers
    123. 12.123. Multiplication of nonnegative rational numbers
    124. 12.124. Multiplication of positive, negative, nonnegative and nonpositive integers
    125. 12.125. Multiplication of positive rational numbers
    126. 12.126. Multiplication on the rational numbers
    127. 12.127. The multiplicative group of positive rational numbers
    128. 12.128. The multiplicative group of rational numbers
    129. 12.129. Multiplicative inverses of positive integer fractions
    130. 12.130. The multiplicative monoid of natural numbers
    131. 12.131. The multiplicative monoid of rational numbers
    132. 12.132. Multiplicative units in the integers
    133. 12.133. Multiplicative units in modular arithmetic
    134. 12.134. Multiset coefficients
    135. 12.135. The type of natural numbers
    136. 12.136. Negative integer fractions
    137. 12.137. The negative integers
    138. 12.138. Negative rational numbers
    139. 12.139. Nonnegative integer fractions
    140. 12.140. The nonnegative integers
    141. 12.141. Nonnegative rational numbers
    142. 12.142. The nonpositive integers
    143. 12.143. Nonzero integers
    144. 12.144. Nonzero natural numbers
    145. 12.145. Nonzero rational numbers
    146. 12.146. The ordinal induction principle for the natural numbers
    147. 12.147. Parity of the natural numbers
    148. 12.148. Peano arithmetic
    149. 12.149. Pisano periods
    150. 12.150. The poset of closed intervals of rational numbers
    151. 12.151. The poset of natural numbers ordered by divisibility
    152. 12.152. The positive, negative, nonnegative and nonpositive integers
    153. 12.153. The positive, negative, and nonnegative rational numbers
    154. 12.154. Positive conatural numbers
    155. 12.155. Positive integer fractions
    156. 12.156. The positive integers
    157. 12.157. Positive rational numbers
    158. 12.158. Powers of integers
    159. 12.159. Powers of two
    160. 12.160. Prime numbers
    161. 12.161. Products of natural numbers
    162. 12.162. Proper divisors of natural numbers
    163. 12.163. Pythagorean triples
    164. 12.164. The rational numbers
    165. 12.165. Reduced integer fractions
    166. 12.166. Relatively prime integers
    167. 12.167. Relatively prime natural numbers
    168. 12.168. Repeating an element in a standard finite type
    169. 12.169. Retracts of the type of natural numbers
    170. 12.170. The ring extension of rational numbers of the ring of rational numbers
    171. 12.171. The ring of integers
    172. 12.172. The ring of rational numbers
    173. 12.173. The sieve of Eratosthenes
    174. 12.174. Square-free natural numbers
    175. 12.175. Squares in the integers
    176. 12.176. Squares in ℤₚ
    177. 12.177. Squares in the natural numbers
    178. 12.178. Squares in the rational numbers
    179. 12.179. The standard cyclic groups
    180. 12.180. The standard cyclic rings
    181. 12.181. Stirling numbers of the second kind
    182. 12.182. Strict inequality on the integer fractions
    183. 12.183. Strict inequality on the integers
    184. 12.184. Strict inequality on the natural numbers
    185. 12.185. Strict inequality on nonnegative rational numbers
    186. 12.186. Strict inequality on positive rational numbers
    187. 12.187. Strict inequality on the rational numbers
    188. 12.188. Strict inequality on the standard finite types
    189. 12.189. Strictly ordered pairs of natural numbers
    190. 12.190. The strong induction principle for the natural numbers
    191. 12.191. Sums of natural numbers
    192. 12.192. Sylvester's sequence
    193. 12.193. Taxicab numbers
    194. 12.194. Telephone numbers
    195. 12.195. The triangular numbers
    196. 12.196. The Twin Prime conjecture
    197. 12.197. Type arithmetic with natural numbers
    198. 12.198. Unit elements in the standard finite types
    199. 12.199. Unit fractions in the rational numbers types
    200. 12.200. Unit similarity on the standard finite types
    201. 12.201. The universal property of the conatural numbers
    202. 12.202. The universal property of the integers
    203. 12.203. The universal property of the natural numbers
    204. 12.204. Upper bounds for type families over the natural numbers
    205. 12.205. The well-ordering principle of the natural numbers
    206. 12.206. The well-ordering principle of the standard finite types
    207. 12.207. The zero conatural number
  15. 13. Finite algebra
    ❱
    1. 13.1. Commutative finite rings
    2. 13.2. Dependent products of commutative finit rings
    3. 13.3. Dependent products of finite rings
    4. 13.4. Finite fields
    5. 13.5. Finite rings
    6. 13.6. Homomorphisms of commutative finite rings
    7. 13.7. Homomorphisms of finite rings
    8. 13.8. Products of commutative finite rings
    9. 13.9. Products of finite rings
    10. 13.10. Semisimple commutative finite rings
  16. 14. Finite group theory
    ❱
    1. 14.1. The abstract quaternion group of order 8
    2. 14.2. Alternating concrete groups
    3. 14.3. Alternating groups
    4. 14.4. Cartier's delooping of the sign homomorphism
    5. 14.5. The concrete quaternion group
    6. 14.6. Deloopings of the sign homomorphism
    7. 14.7. Abelian groups
    8. 14.8. Finite Commutative monoids
    9. 14.9. Finite groups
    10. 14.10. Finite monoids
    11. 14.11. Finite semigroups
    12. 14.12. The group of n-element types
    13. 14.13. Groups of order 2
    14. 14.14. Orbits of permutations
    15. 14.15. Permutations
    16. 14.16. Permutations of standard finite types
    17. 14.17. The sign homomorphism
    18. 14.18. Simpson's delooping of the sign homomorphism
    19. 14.19. Subgroups of finite groups
    20. 14.20. Tetrahedra in 3-dimensional space
    21. 14.21. Transpositions
    22. 14.22. Transpositions of standard finite types
  17. 15. Foundation
    ❱
    1. 15.1. 0-Connected types
    2. 15.2. 0-Images of maps
    3. 15.3. 0-Maps
    4. 15.4. 1-Types
    5. 15.5. 2-Types
    6. 15.6. Action on equivalences of functions
    7. 15.7. The action on equivalences of functions out of subuniverses
    8. 15.8. Action on equivalences of type families
    9. 15.9. Action on equivalences in type families over subuniverses
    10. 15.10. The action of functions on higher identifications
    11. 15.11. The action on homotopies of functions
    12. 15.12. The binary action on identifications of binary dependent functions
    13. 15.13. The binary action on identifications of binary functions
    14. 15.14. The action on identifications of dependent functions
    15. 15.15. The action on identifications of functions
    16. 15.16. Apartness relations
    17. 15.17. Arithmetic law for coproduct decomposition and Σ-decomposition
    18. 15.18. Arithmetic law for product decomposition and Π-decomposition
    19. 15.19. Automorphisms
    20. 15.20. The axiom of choice
    21. 15.21. The axiom of countable choice
    22. 15.22. The axiom of dependent choice
    23. 15.23. Bands
    24. 15.24. Base changes of span diagrams
    25. 15.25. Bicomposition of functions
    26. 15.26. Binary dependent identifications
    27. 15.27. Binary embeddings
    28. 15.28. Binary equivalences
    29. 15.29. Binary equivalences on unordered pairs of types
    30. 15.30. Binary functoriality of set quotients
    31. 15.31. Homotopies of binary operations
    32. 15.32. Binary operations on unordered pairs of types
    33. 15.33. Binary reflecting maps of equivalence relations
    34. 15.34. Binary relations
    35. 15.35. Binary relations with extensions
    36. 15.36. Binary relations with lifts
    37. 15.37. Binary transport
    38. 15.38. Binary type duality
    39. 15.39. The booleans
    40. 15.40. The Cantor–Schröder–Bernstein–Escardó theorem
    41. 15.41. Cantor's theorem
    42. 15.42. Cartesian morphisms of arrows
    43. 15.43. Cartesian morphisms of span diagrams
    44. 15.44. Cartesian product types
    45. 15.45. Cartesian products of set quotients
    46. 15.46. Cartesian products of subtypes
    47. 15.47. The category of families of sets
    48. 15.48. The category of sets
    49. 15.49. Choice of representatives for an equivalence relation
    50. 15.50. Coalgebras of the maybe monad
    51. 15.51. Codiagonal maps of types
    52. 15.52. Coherently constant maps
    53. 15.53. Coherently idempotent maps
    54. 15.54. Coherently invertible maps
    55. 15.55. Coinhabited pairs of types
    56. 15.56. Commuting cubes of maps
    57. 15.57. Commuting hexagons of identifications
    58. 15.58. Commuting pentagons of identifications
    59. 15.59. Commuting prisms of maps
    60. 15.60. Commuting squares of homotopies
    61. 15.61. Commuting squares of identifications
    62. 15.62. Commuting squares of maps
    63. 15.63. Commuting tetrahedra of homotopies
    64. 15.64. Commuting tetrahedra of maps
    65. 15.65. Commuting triangles of homotopies
    66. 15.66. Commuting triangles of identifications
    67. 15.67. Commuting triangles of maps
    68. 15.68. Commuting triangles of morphisms of arrows
    69. 15.69. Complements of type families
    70. 15.70. Complements of subtypes
    71. 15.71. Composite maps in inverse sequential diagrams
    72. 15.72. Composition algebra
    73. 15.73. Composition of spans
    74. 15.74. Computational identity types
    75. 15.75. Cones over cospan diagrams
    76. 15.76. Cones over inverse sequential diagrams
    77. 15.77. Conjunction
    78. 15.78. Connected components of types
    79. 15.79. Connected components of universes
    80. 15.80. Connected maps
    81. 15.81. Connected types
    82. 15.82. Constant maps
    83. 15.83. Constant span diagrams
    84. 15.84. Constant type families
    85. 15.85. The continuation monad
    86. 15.86. Contractible maps
    87. 15.87. Contractible types
    88. 15.88. Copartial elements
    89. 15.89. Copartial functions
    90. 15.90. Coproduct decompositions
    91. 15.91. Coproduct decompositions in a subuniverse
    92. 15.92. Coproduct types
    93. 15.93. Coproducts of pullbacks
    94. 15.94. Morphisms in the coslice category of types
    95. 15.95. Cospan diagrams
    96. 15.96. Cospans of types
    97. 15.97. Decidability of dependent function types
    98. 15.98. Decidability of dependent pair types
    99. 15.99. Decidable embeddings
    100. 15.100. Decidable equality
    101. 15.101. Decidable equivalence relations
    102. 15.102. Decidable maps
    103. 15.103. Decidable propositions
    104. 15.104. Decidable relations on types
    105. 15.105. Decidable subtypes
    106. 15.106. Decidable type families
    107. 15.107. Decidable types
    108. 15.108. Dependent binary homotopies
    109. 15.109. The dependent binomial theorem for types (distributivity of dependent function types over coproduct types)
    110. 15.110. Dependent epimorphisms
    111. 15.111. Dependent epimorphisms with respect to truncated types
    112. 15.112. Dependent function types
    113. 15.113. Dependent homotopies
    114. 15.114. Dependent identifications
    115. 15.115. Dependent inverse sequential diagrams of types
    116. 15.116. Dependent pair types
    117. 15.117. Dependent products of pullbacks
    118. 15.118. Dependent products of subtypes
    119. 15.119. Dependent sums of pullbacks
    120. 15.120. Dependent telescopes
    121. 15.121. The dependent universal property of equivalences
    122. 15.122. Descent for coproduct types
    123. 15.123. Descent for dependent pair types
    124. 15.124. Descent for the empty type
    125. 15.125. Descent for equivalences
    126. 15.126. Diaconescu's theorem
    127. 15.127. Diagonal maps into cartesian products of types
    128. 15.128. Diagonal maps of types
    129. 15.129. Diagonal span diagrams
    130. 15.130. Diagonals of maps
    131. 15.131. Diagonals of morphisms of arrows
    132. 15.132. Discrete binary relations
    133. 15.133. Discrete reflexive relations
    134. 15.134. Discrete relaxed Σ-decompositions
    135. 15.135. Discrete Σ-decompositions
    136. 15.136. Discrete types
    137. 15.137. Disjoint subtypes
    138. 15.138. Disjunction
    139. 15.139. Double arrows
    140. 15.140. Double negation
    141. 15.141. Double negation dense equality
    142. 15.142. Maps with double negation dense equality
    143. 15.143. The double negation image of a map
    144. 15.144. The double negation modality
    145. 15.145. Double negation stable equality
    146. 15.146. Double negation stable propositions
    147. 15.147. Double powersets
    148. 15.148. Dubuc-Penon compact types
    149. 15.149. Effective maps for equivalence relations
    150. 15.150. Embeddings
    151. 15.151. Empty subtypes
    152. 15.152. Empty types
    153. 15.153. Endomorphisms
    154. 15.154. Epimorphisms
    155. 15.155. Epimorphisms with respect to maps into sets
    156. 15.156. Epimorphisms with respect to truncated types
    157. 15.157. Equality of cartesian product types
    158. 15.158. Equality of coproduct types
    159. 15.159. Equality on dependent function types
    160. 15.160. Equality of dependent pair types
    161. 15.161. Equality in the fibers of a map
    162. 15.162. Equality of truncation levels
    163. 15.163. Equivalence classes
    164. 15.164. Equivalence extensionality
    165. 15.165. Equivalence induction
    166. 15.166. Equivalence injective type families
    167. 15.167. Equivalence relations
    168. 15.168. Equivalences
    169. 15.169. Equivalences of arrows
    170. 15.170. Equivalences of cospans
    171. 15.171. Equivalences of double arrows
    172. 15.172. Equivalences of inverse sequential diagrams of types
    173. 15.173. Equivalences on Maybe
    174. 15.174. Equivalences of span diagrams
    175. 15.175. Equivalences of span diagrams on families of types
    176. 15.176. Equivalences of spans
    177. 15.177. Equivalences of spans of families of types
    178. 15.178. Evaluation of functions
    179. 15.179. Exclusive disjunctions
    180. 15.180. Exclusive sums
    181. 15.181. Existential quantification
    182. 15.182. Exponents of set quotients
    183. 15.183. Extensions of types
    184. 15.184. Extensions of types in a global subuniverse
    185. 15.185. Extensions of types in a subuniverse
    186. 15.186. Faithful maps
    187. 15.187. Families of equivalences
    188. 15.188. Families of maps
    189. 15.189. Families of types over telescopes
    190. 15.190. Fiber inclusions
    191. 15.191. Fibered equivalences
    192. 15.192. Fibered involutions
    193. 15.193. Maps fibered over a map
    194. 15.194. Fibers of maps
    195. 15.195. Finite sequences of set quotients
    196. 15.196. Finitely coherent equivalences
    197. 15.197. Finitely coherently invertible maps
    198. 15.198. Finitely truncated types
    199. 15.199. Fixed points of endofunctions
    200. 15.200. Freely generated equivalence relations
    201. 15.201. Full subtypes of types
    202. 15.202. Function extensionality
    203. 15.203. Function types
    204. 15.204. Functional correspondences
    205. 15.205. Functoriality of the action on identifications of functions
    206. 15.206. Functoriality of cartesian product types
    207. 15.207. Functoriality of coproduct types
    208. 15.208. Functoriality of dependent function types
    209. 15.209. Functoriality of dependent pair types
    210. 15.210. Functoriality of disjunction
    211. 15.211. Functoriality of fibers of maps
    212. 15.212. Functoriality of function types
    213. 15.213. Functoriality of morphisms of arrows
    214. 15.214. Functoriality of propositional truncations
    215. 15.215. Functorialty of pullbacks
    216. 15.216. Functoriality of sequential limits
    217. 15.217. Functoriality of set quotients
    218. 15.218. Functoriality of set truncation
    219. 15.219. Functoriality of truncations
    220. 15.220. Fundamental theorem of equivalence relations
    221. 15.221. The fundamental theorem of identity types
    222. 15.222. Global choice
    223. 15.223. Global subuniverses
    224. 15.224. The globular type of dependent functions
    225. 15.225. The globular type of functions
    226. 15.226. Higher homotopies of morphisms of arrows
    227. 15.227. Hilbert ε-operators on maps
    228. 15.228. Hilbert's ε-operators
    229. 15.229. Homotopies
    230. 15.230. Homotopies of morphisms of arrows
    231. 15.231. Homotopies of morphisms of cospan diagrams
    232. 15.232. Homotopy algebra
    233. 15.233. Homotopy induction
    234. 15.234. The homotopy preorder of types
    235. 15.235. Horizontal composition of spans of spans
    236. 15.236. Idempotent maps
    237. 15.237. Identity systems
    238. 15.238. Identity types of truncated types
    239. 15.239. Identity types
    240. 15.240. The image of a map
    241. 15.241. Images of subtypes
    242. 15.242. Implicit function types
    243. 15.243. Impredicative encodings of the logical operations
    244. 15.244. Impredicative universes
    245. 15.245. The induction principle for propositional truncation
    246. 15.246. The standard inequality relation on booleans
    247. 15.247. Inequality of truncation levels
    248. 15.248. Infinitely coherent equivalences
    249. 15.249. ∞-connected maps
    250. 15.250. ∞-connected types
    251. 15.251. Inhabited subtypes
    252. 15.252. Inhabited types
    253. 15.253. Injective maps
    254. 15.254. The interchange law
    255. 15.255. Intersections of subtypes
    256. 15.256. Inverse sequential diagrams of types
    257. 15.257. Invertible maps
    258. 15.258. Involutions
    259. 15.259. Irrefutable equality
    260. 15.260. Irrefutable propositions
    261. 15.261. Isolated elements
    262. 15.262. Isomorphisms of sets
    263. 15.263. Iterated cartesian product types
    264. 15.264. Iterated dependent pair types
    265. 15.265. Iterated dependent product types
    266. 15.266. Iterated successors of truncation levels
    267. 15.267. Iterating automorphisms
    268. 15.268. Iterating families of maps over a map
    269. 15.269. Iterating functions
    270. 15.270. Iterating involutions
    271. 15.271. Kernel span diagrams of maps
    272. 15.272. Large apartness relations
    273. 15.273. Large binary relations
    274. 15.274. Large dependent pair types
    275. 15.275. Large homotopies
    276. 15.276. Large identity types
    277. 15.277. The large locale of propositions
    278. 15.278. The large locale of subtypes
    279. 15.279. The law of excluded middle
    280. 15.280. Lawvere's fixed point theorem
    281. 15.281. The lesser limited principle of omniscience
    282. 15.282. Lifts of types
    283. 15.283. The limited principle of omniscience
    284. 15.284. The locale of propositions
    285. 15.285. Locally small types
    286. 15.286. Logical equivalences
    287. 15.287. Logical operations on the booleans
    288. 15.288. Maps in global subuniverses
    289. 15.289. Maps in subuniverses
    290. 15.290. The maximum of truncation levels
    291. 15.291. The maybe monad
    292. 15.292. Mere embeddings
    293. 15.293. Mere equality
    294. 15.294. Mere equivalences
    295. 15.295. Mere functions
    296. 15.296. Mere logical equivalences
    297. 15.297. Mere path-cosplit maps
    298. 15.298. Monomorphisms
    299. 15.299. Morphisms of arrows
    300. 15.300. Morphisms of binary relations
    301. 15.301. Morphisms of coalgebras of the maybe monad
    302. 15.302. Morphisms of cospan diagrams
    303. 15.303. Morphisms of cospans
    304. 15.304. Morphisms of double arrows
    305. 15.305. Morphisms of inverse sequential diagrams of types
    306. 15.306. Morphisms of span diagrams
    307. 15.307. Morphisms of spans
    308. 15.308. Morphisms of spans on families of types
    309. 15.309. Morphisms of twisted arrows
    310. 15.310. Multisubsets
    311. 15.311. Multivariable correspondences
    312. 15.312. Multivariable decidable relations
    313. 15.313. Multivariable functoriality of set quotients
    314. 15.314. Multivariable homotopies
    315. 15.315. Multivariable operations
    316. 15.316. Multivariable relations
    317. 15.317. Multivariable sections
    318. 15.318. Negated equality
    319. 15.319. Negation
    320. 15.320. Noncontractible types
    321. 15.321. Noninjective maps
    322. 15.322. Null-homotopic maps
    323. 15.323. Operations on span diagrams
    324. 15.324. Operations on spans
    325. 15.325. Operations on spans of families of types
    326. 15.326. Opposite spans
    327. 15.327. Pairs of distinct elements
    328. 15.328. Partial elements
    329. 15.329. Partial functions
    330. 15.330. Partitions
    331. 15.331. Path algebra
    332. 15.332. Path-cosplit maps
    333. 15.333. Path-split maps
    334. 15.334. Path-split type families
    335. 15.335. Perfect images
    336. 15.336. Permutations of spans of families of types
    337. 15.337. Π-decompositions of types
    338. 15.338. Π-decompositions of types into types in a subuniverse
    339. 15.339. Pointed torsorial type families
    340. 15.340. Postcomposition of dependent functions
    341. 15.341. Postcomposition of functions
    342. 15.342. Postcomposition of pullbacks
    343. 15.343. Powersets
    344. 15.344. Precomposition of dependent functions
    345. 15.345. Precomposition of functions
    346. 15.346. Precomposition of functions into subuniverses
    347. 15.347. Precomposition of type families
    348. 15.348. The preunivalence axiom
    349. 15.349. Preunivalent type families
    350. 15.350. The principle of omniscience
    351. 15.351. Product decompositions
    352. 15.352. Product decompositions of types in a subuniverse
    353. 15.353. Products of binary relations
    354. 15.354. Products of equivalence relataions
    355. 15.355. Products of tuples of types
    356. 15.356. Products of pullbacks
    357. 15.357. Products of unordered pairs of types
    358. 15.358. Products of unordered tuples of types
    359. 15.359. Projective types
    360. 15.360. Proper subsets
    361. 15.361. Propositional extensionality
    362. 15.362. Propositional maps
    363. 15.363. Propositional resizing
    364. 15.364. Propositional truncations
    365. 15.365. Propositions
    366. 15.366. Pullback cones
    367. 15.367. Pullbacks
    368. 15.368. Pullbacks of subtypes
    369. 15.369. Quasicoherently idempotent maps
    370. 15.370. Raising universe levels
    371. 15.371. Reflecting maps for equivalence relations
    372. 15.372. Reflexive relations
    373. 15.373. The Regensburg extension of the fundamental theorem of identity types
    374. 15.374. Relaxed Σ-decompositions of types
    375. 15.375. Repetitions of values of maps
    376. 15.376. The type theoretic replacement axiom
    377. 15.377. Retractions
    378. 15.378. Retracts of maps
    379. 15.379. Retracts of types
    380. 15.380. Sections
    381. 15.381. Types separated at subuniverses
    382. 15.382. Sequential limits
    383. 15.383. Set coequalizers
    384. 15.384. Set presented types
    385. 15.385. Set quotients
    386. 15.386. Set truncations
    387. 15.387. Sets
    388. 15.388. Σ-closed subuniverses
    389. 15.389. Σ-decompositions of types into types in a subuniverse
    390. 15.390. Σ-decompositions of types
    391. 15.391. Singleton induction
    392. 15.392. Singleton subtypes
    393. 15.393. Morphisms in the slice category of types
    394. 15.394. Small maps
    395. 15.395. Small types
    396. 15.396. Small universes
    397. 15.397. Sorial type families
    398. 15.398. Span diagrams
    399. 15.399. Span diagrams on families of types
    400. 15.400. Spans of types
    401. 15.401. Spans of families of types
    402. 15.402. Spans of spans
    403. 15.403. Split idempotent maps
    404. 15.404. Split surjective maps
    405. 15.405. Standard apartness relations
    406. 15.406. Standard pullbacks
    407. 15.407. Standard ternary pullbacks
    408. 15.408. Strict symmetrization of binary relations
    409. 15.409. Strictly involutive identity types
    410. 15.410. The strictly right unital concatenation operation on identifications
    411. 15.411. The strong preunivalence axiom
    412. 15.412. Strongly extensional maps
    413. 15.413. Structure
    414. 15.414. The structure identity principle
    415. 15.415. Structured equality duality
    416. 15.416. Structured type duality
    417. 15.417. Subsingleton induction
    418. 15.418. Subterminal types
    419. 15.419. Subtype duality
    420. 15.420. The subtype identity principle
    421. 15.421. Subtypes
    422. 15.422. Subuniverses
    423. 15.423. Surjective maps
    424. 15.424. Symmetric binary relations
    425. 15.425. Symmetric cores of binary relations
    426. 15.426. Symmetric difference of subtypes
    427. 15.427. The symmetric identity types
    428. 15.428. Symmetric operations
    429. 15.429. Telescopes
    430. 15.430. Terminal spans on families of types
    431. 15.431. Tight apartness relations
    432. 15.432. Torsorial type families
    433. 15.433. Total partial elements
    434. 15.434. Total partial functions
    435. 15.435. Transfinite cocomposition of maps
    436. 15.436. Transport along equivalences
    437. 15.437. Transport along higher identifications
    438. 15.438. Transport along homotopies
    439. 15.439. Transport along identifications
    440. 15.440. Transport-split type families
    441. 15.441. Transposing identifications along equivalences
    442. 15.442. Transposing identifications along retractions
    443. 15.443. Transposing identifications along sections
    444. 15.444. Transposition of span diagrams
    445. 15.445. Trivial relaxed Σ-decompositions
    446. 15.446. Trivial Σ-decompositions
    447. 15.447. Truncated addition of truncation levels
    448. 15.448. Truncated equality
    449. 15.449. Truncated maps
    450. 15.450. Truncated types
    451. 15.451. k-Equivalences
    452. 15.452. Truncation images of maps
    453. 15.453. Truncation levels
    454. 15.454. The truncation modalities
    455. 15.455. Truncations
    456. 15.456. Tuples of types
    457. 15.457. Type arithmetic with the booleans
    458. 15.458. Type arithmetic for cartesian product types
    459. 15.459. Type arithmetic for coproduct types
    460. 15.460. Type arithmetic with dependent function types
    461. 15.461. Type arithmetic for dependent pair types
    462. 15.462. Type arithmetic with the empty type
    463. 15.463. Type arithmetic with standard pullbacks
    464. 15.464. Type arithmetic with the unit type
    465. 15.465. Type duality
    466. 15.466. The type theoretic principle of choice
    467. 15.467. Uniformly decidable type families
    468. 15.468. Unions of subtypes
    469. 15.469. Uniqueness of the image of a map
    470. 15.470. Uniqueness quantification
    471. 15.471. The uniqueness of set quotients
    472. 15.472. Uniqueness of set truncations
    473. 15.473. Uniqueness of the truncations
    474. 15.474. The unit type
    475. 15.475. Unital binary operations
    476. 15.476. The univalence axiom
    477. 15.477. The univalence axiom implies function extensionality
    478. 15.478. Univalent type families
    479. 15.479. The universal property of booleans
    480. 15.480. The universal properties of cartesian product types
    481. 15.481. Universal property of contractible types
    482. 15.482. The universal property of coproduct types
    483. 15.483. The universal property of dependent function types
    484. 15.484. The universal property of dependent pair types
    485. 15.485. The universal property of the empty type
    486. 15.486. The universal property of equivalences
    487. 15.487. The universal property of the family of fibers of maps
    488. 15.488. The universal property of fiber products
    489. 15.489. The universal property of identity systems
    490. 15.490. The universal property of identity types
    491. 15.491. The universal property of the image of a map
    492. 15.492. The universal property of the maybe monad
    493. 15.493. The universal property of propositional truncations
    494. 15.494. The universal property of propositional truncations with respect to sets
    495. 15.495. The universal property of pullbacks
    496. 15.496. The universal property of sequential limits
    497. 15.497. The universal property of set quotients
    498. 15.498. The universal property of set truncations
    499. 15.499. The universal property of truncations
    500. 15.500. The universal property of the unit type
    501. 15.501. Universal quantification
    502. 15.502. Universe levels
    503. 15.503. Unordered pairs of elements in a type
    504. 15.504. Unordered pairs of types
    505. 15.505. Unordered n-tuples of elements in a type
    506. 15.506. Unordered tuples of types
    507. 15.507. Vertical composition of spans of spans
    508. 15.508. Weak function extensionality
    509. 15.509. The weak limited principle of omniscience
    510. 15.510. Weakly constant maps
    511. 15.511. Whiskering higher homotopies with respect to composition
    512. 15.512. Whiskering homotopies with respect to composition
    513. 15.513. Whiskering homotopies with respect to concatenation
    514. 15.514. Whiskering identifications with respect to concatenation
    515. 15.515. Whiskering operations
    516. 15.516. The wild category of types
    517. 15.517. Yoneda identity types
  18. 16. Foundation core
    ❱
    1. 16.1. 1-Types
    2. 16.2. Cartesian product types
    3. 16.3. Coherently invertible maps
    4. 16.4. Commuting prisms of maps
    5. 16.5. Commuting squares of homotopies
    6. 16.6. Commuting squares of identifications
    7. 16.7. Commuting squares of maps
    8. 16.8. Commuting triangles of maps
    9. 16.9. Constant maps
    10. 16.10. Contractible maps
    11. 16.11. Contractible types
    12. 16.12. Coproduct types
    13. 16.13. Decidable propositions
    14. 16.14. Dependent identifications
    15. 16.15. Diagonal maps into cartesian products of types
    16. 16.16. Discrete types
    17. 16.17. Embeddings
    18. 16.18. Empty types
    19. 16.19. Endomorphisms
    20. 16.20. Equality of dependent pair types
    21. 16.21. Equivalence relations
    22. 16.22. Equivalences
    23. 16.23. Families of equivalences
    24. 16.24. Fibers of maps
    25. 16.25. Function types
    26. 16.26. Functoriality of dependent function types
    27. 16.27. Functoriality of dependent pair types
    28. 16.28. Homotopies
    29. 16.29. Identity types
    30. 16.30. Injective maps
    31. 16.31. Invertible maps
    32. 16.32. Iterating functions
    33. 16.33. Negation
    34. 16.34. Operations on span diagrams
    35. 16.35. Operations on spans
    36. 16.36. Path-split maps
    37. 16.37. Postcomposition of dependent functions
    38. 16.38. Postcomposition of functions
    39. 16.39. Precomposition of dependent functions
    40. 16.40. Precomposition of functions
    41. 16.41. Propositional maps
    42. 16.42. Propositions
    43. 16.43. Pullbacks
    44. 16.44. Retractions
    45. 16.45. Retracts of types
    46. 16.46. Sections
    47. 16.47. Sets
    48. 16.48. Small types
    49. 16.49. Subtypes
    50. 16.50. Torsorial type families
    51. 16.51. Transport along identifications
    52. 16.52. Truncated maps
    53. 16.53. Truncated types
    54. 16.54. Truncation levels
    55. 16.55. The type theoretic principle of choice
    56. 16.56. The univalence axiom
    57. 16.57. The universal property of pullbacks
    58. 16.58. The universal property of truncations
    59. 16.59. Whiskering homotopies with respect to concatenation
    60. 16.60. Whiskering identifications with respect to concatenation
  19. 17. Globular types
    ❱
    1. 17.1. Base change of dependent globular types
    2. 17.2. Base change of dependent reflexive globular types
    3. 17.3. Binary dependent globular types
    4. 17.4. Binary dependent reflexive globular types
    5. 17.5. Binary globular maps
    6. 17.6. Colax reflexive globular maps
    7. 17.7. Colax transitive globular maps
    8. 17.8. Composition structure on globular types
    9. 17.9. Constant globular types
    10. 17.10. Dependent globular types
    11. 17.11. Dependent reflexive globular types
    12. 17.12. Dependent sums of globular types
    13. 17.13. Discrete dependent reflexive globular types
    14. 17.14. Discrete globular types
    15. 17.15. Discrete reflexive globular types
    16. 17.16. Empty globular types
    17. 17.17. Equality of globular types
    18. 17.18. Exponentials of globular types
    19. 17.19. Fibers of globular maps
    20. 17.20. Equivalences between globular types
    21. 17.21. Maps between globular types
    22. 17.22. Globular types
    23. 17.23. Large colax reflexive globular maps
    24. 17.24. Large colax transitive globular maps
    25. 17.25. Maps between large globular types
    26. 17.26. Large globular types
    27. 17.27. Large lax reflexive globular maps
    28. 17.28. Large lax transitive globular maps
    29. 17.29. Large reflexive globular maps
    30. 17.30. Large reflexive globular types
    31. 17.31. Large symmetric globular types
    32. 17.32. Large transitive globular maps
    33. 17.33. Large transitive globular types
    34. 17.34. Lax reflexive globular maps
    35. 17.35. Lax transitive globular maps
    36. 17.36. Points of globular types
    37. 17.37. Points of reflexive globular types
    38. 17.38. Pointwise extensions of binary families of globular types
    39. 17.39. Pointwise extensions of binary families of reflexive globular types
    40. 17.40. Pointwise extensions of families of globular types
    41. 17.41. Pointwise extensions of families of reflexive globular types
    42. 17.42. Products of families of globular types
    43. 17.43. Reflexive globular equivalences
    44. 17.44. Reflexive globular maps
    45. 17.45. Reflexive globular types
    46. 17.46. Sections of dependent globular types
    47. 17.47. Superglobular types
    48. 17.48. Symmetric globular types
    49. 17.49. Terminal globular types
    50. 17.50. Transitive globular maps
    51. 17.51. Transitive globular types
    52. 17.52. The unit globular type
    53. 17.53. The unit reflexive globular type
    54. 17.54. The universal globular type
    55. 17.55. The universal reflexive globular type
  20. 18. Graph theory
    ❱
    1. 18.1. Acyclic undirected graphs
    2. 18.2. Base change of dependent directed graphs
    3. 18.3. Base change of dependent reflexive graphs
    4. 18.4. Cartesian products of directed graphs
    5. 18.5. Cartesian products of reflexive graphs
    6. 18.6. Circuits in undirected graphs
    7. 18.7. Closed walks in undirected graphs
    8. 18.8. Complete bipartite graphs
    9. 18.9. Complete multipartite graphs
    10. 18.10. Complete undirected graphs
    11. 18.11. Connected graphs
    12. 18.12. Cycles in undirected graphs
    13. 18.13. Dependent directed graphs
    14. 18.14. Dependent products of directed graphs
    15. 18.15. Dependent products of reflexive graphs
    16. 18.16. Dependent reflexive graphs
    17. 18.17. Dependent sums directed graphs
    18. 18.18. Dependent sums reflexive graphs
    19. 18.19. Directed graph duality
    20. 18.20. Directed graph structures on standard finite sets
    21. 18.21. Directed graphs
    22. 18.22. Discrete dependent reflexive graphs
    23. 18.23. Discrete directed graphs
    24. 18.24. Discrete reflexive graphs
    25. 18.25. Displayed large reflexive graphs
    26. 18.26. Edge-colored undirected graphs
    27. 18.27. Embeddings of directed graphs
    28. 18.28. Embeddings of undirected graphs
    29. 18.29. Enriched undirected graphs
    30. 18.30. Equivalences of dependent directed graphs
    31. 18.31. Equivalences of dependent reflexive graphs
    32. 18.32. Equivalences of directed graphs
    33. 18.33. Equivalences of enriched undirected graphs
    34. 18.34. Equivalences of reflexive graphs
    35. 18.35. Equivalences of undirected graphs
    36. 18.36. Eulerian circuits in undirected graphs
    37. 18.37. Faithful morphisms of undirected graphs
    38. 18.38. Fibers of directed graphs
    39. 18.39. Fibers of morphisms into directed graphs
    40. 18.40. Fibers of morphisms into reflexive graphs
    41. 18.41. Finite graphs
    42. 18.42. Geometric realizations of undirected graphs
    43. 18.43. Higher directed graphs
    44. 18.44. Hypergraphs
    45. 18.45. Internal homs of directed graphs
    46. 18.46. Large higher directed graphs
    47. 18.47. Large reflexive graphs
    48. 18.48. Matchings
    49. 18.49. Mere equivalences of undirected graphs
    50. 18.50. Morphisms of dependent directed graphs
    51. 18.51. Morphisms of directed graphs
    52. 18.52. Morphisms of reflexive graphs
    53. 18.53. Morphisms of undirected graphs
    54. 18.54. Incidence in undirected graphs
    55. 18.55. Orientations of undirected graphs
    56. 18.56. Paths in undirected graphs
    57. 18.57. Polygons
    58. 18.58. Raising universe levels of directed graphs
    59. 18.59. Reflecting maps of undirected graphs
    60. 18.60. Reflexive graphs
    61. 18.61. Regular undirected graph
    62. 18.62. Sections of dependent directed graphs
    63. 18.63. Sections of dependent reflexive graphs
    64. 18.64. Simple undirected graphs
    65. 18.65. Stereoisomerism for enriched undirected graphs
    66. 18.66. Terminal directed graphs
    67. 18.67. Terminal reflexive graphs
    68. 18.68. Totally faithful morphisms of undirected graphs
    69. 18.69. Trails in directed graphs
    70. 18.70. Trails in undirected graphs
    71. 18.71. Undirected graph structures on standard finite sets
    72. 18.72. Undirected graphs
    73. 18.73. The universal directed graph
    74. 18.74. The universal reflexive graph
    75. 18.75. Vertex covers
    76. 18.76. Voltage graphs
    77. 18.77. Walks in directed graphs
    78. 18.78. Walks in undirected graphs
    79. 18.79. Wide displayed large reflexive graphs
  21. 19. Group theory
    ❱
    1. 19.1. Abelian groups
    2. 19.2. Abelianization of groups
    3. 19.3. Pointwise addition of morphisms of abelian groups
    4. 19.4. Arithmetic sequences in semigroups
    5. 19.5. Automorphism groups
    6. 19.6. Cartesian products of abelian groups
    7. 19.7. Cartesian products of commutative monoids
    8. 19.8. Cartesian products of concrete groups
    9. 19.9. Cartesian products of groups
    10. 19.10. Cartesian products of monoids
    11. 19.11. Cartesian products of semigroups
    12. 19.12. The category of abelian groups
    13. 19.13. The category of concrete groups
    14. 19.14. The category of group actions
    15. 19.15. The category of groups
    16. 19.16. The orbit category of a group
    17. 19.17. The category of semigroups
    18. 19.18. Cayley's theorem
    19. 19.19. The center of a group
    20. 19.20. Center of a monoid
    21. 19.21. Center of a semigroup
    22. 19.22. Central elements of groups
    23. 19.23. Central elements of monoids
    24. 19.24. Central elements of semirings
    25. 19.25. Centralizer subgroups
    26. 19.26. Characteristic subgroups
    27. 19.27. Commutative monoids
    28. 19.28. Commutative semigroups
    29. 19.29. Commutator subgroups
    30. 19.30. Commutators of elements in groups
    31. 19.31. Commuting elements of groups
    32. 19.32. Commuting elements of monoids
    33. 19.33. Commuting elements of semigroups
    34. 19.34. Commuting squares of group homomorphisms
    35. 19.35. Concrete group actions
    36. 19.36. Concrete groups
    37. 19.37. Concrete monoids
    38. 19.38. Congruence relations on abelian groups
    39. 19.39. Congruence relations on commutative monoids
    40. 19.40. Congruence relations on groups
    41. 19.41. Congruence relations on monoids
    42. 19.42. Congruence relations on semigroups
    43. 19.43. Conjugation in groups
    44. 19.44. Conjugation on concrete groups
    45. 19.45. Contravariant pushforwards of concrete group actions
    46. 19.46. Cores of monoids
    47. 19.47. Cyclic groups
    48. 19.48. Decidable subgroups of groups
    49. 19.49. Dependent products of abelian groups
    50. 19.50. Dependent products of commutative monoids
    51. 19.51. Dependent products of groups
    52. 19.52. Dependent products of monoids
    53. 19.53. Dependent products of semigroups
    54. 19.54. The dihedral group construction
    55. 19.55. The dihedral groups
    56. 19.56. The E₈-lattice
    57. 19.57. Elements of finite order
    58. 19.58. Embeddings of abelian groups
    59. 19.59. Embeddings of groups
    60. 19.60. The endomorphism rings of abelian groups
    61. 19.61. Epimorphisms in groups
    62. 19.62. Equivalences of concrete group actions
    63. 19.63. Equivalences of concrete groups
    64. 19.64. Equivalences of group actions
    65. 19.65. Equivalences between semigroups
    66. 19.66. Exponents of abelian groups
    67. 19.67. Exponents of groups
    68. 19.68. Free concrete group actions
    69. 19.69. Free groups with one generator
    70. 19.70. The full subgroup of a group
    71. 19.71. The full subsemigroup of a semigroup
    72. 19.72. Function groups of abelian groups
    73. 19.73. Function commutative monoids
    74. 19.74. Function groups
    75. 19.75. Function monoids
    76. 19.76. Function semigroups
    77. 19.77. Functoriality of quotient groups
    78. 19.78. Furstenberg groups
    79. 19.79. Generating elements of groups
    80. 19.80. Generating sets of groups
    81. 19.81. Grothendieck groups
    82. 19.82. Group actions
    83. 19.83. Abstract groups
    84. 19.84. Homomorphisms of abelian groups
    85. 19.85. Homomorphisms of commutative monoids
    86. 19.86. Morphisms of concrete group actions
    87. 19.87. Homomorphisms of concrete groups
    88. 19.88. Homomorphisms of generated subgroups
    89. 19.89. Homomorphisms of group actions
    90. 19.90. Homomorphisms of groups
    91. 19.91. Homomorphisms of groups equipped with normal subgroups
    92. 19.92. Homomorphisms of monoids
    93. 19.93. Homomorphisms of semigroups
    94. 19.94. Homotopy automorphism groups
    95. 19.95. Images of group homomorphisms
    96. 19.96. Images of semigroup homomorphisms
    97. 19.97. Integer multiples of elements in abelian groups
    98. 19.98. Integer powers of elements of groups
    99. 19.99. Intersections of subgroups of abelian groups
    100. 19.100. Intersections of subgroups of groups
    101. 19.101. Inverse semigroups
    102. 19.102. Invertible elements in monoids
    103. 19.103. Isomorphisms of abelian groups
    104. 19.104. Isomorphisms of concrete groups
    105. 19.105. Isomorphisms of group actions
    106. 19.106. Isomorphisms of groups
    107. 19.107. Isomorphisms of monoids
    108. 19.108. Isomorphisms of semigroups
    109. 19.109. Iterated cartesian products of concrete groups
    110. 19.110. Kernels of homomorphisms between abelian groups
    111. 19.111. Kernels of homomorphisms of concrete groups
    112. 19.112. Kernels of homomorphisms of groups
    113. 19.113. Large semigroups
    114. 19.114. Concrete automorphism groups on sets
    115. 19.115. Mere equivalences of concrete group actions
    116. 19.116. Mere equivalences of group actions
    117. 19.117. Minkowski multiplication of subsets of a commutative monoid
    118. 19.118. Minkowski multiplication on subsets of a monoid
    119. 19.119. Minkowski multiplication on subsets of a semigroup
    120. 19.120. Monoid actions
    121. 19.121. Monoids
    122. 19.122. Monomorphisms of concrete groups
    123. 19.123. Monomorphisms in the category of groups
    124. 19.124. Multiples of elements in abelian groups
    125. 19.125. Nontrivial groups
    126. 19.126. Normal closures of subgroups
    127. 19.127. Normal cores of subgroups
    128. 19.128. Normal subgroups
    129. 19.129. Normal subgroups of concrete groups
    130. 19.130. Normal submonoids
    131. 19.131. Normal submonoids of commutative monoids
    132. 19.132. Normalizer subgroups
    133. 19.133. Nullifying group homomorphisms
    134. 19.134. The opposite of a group
    135. 19.135. The opposite of a semigroup
    136. 19.136. The orbit-stabilizer theorem for concrete groups
    137. 19.137. Orbits of concrete group actions
    138. 19.138. Orbits of group actions
    139. 19.139. The order of an element in a group
    140. 19.140. Perfect cores
    141. 19.141. Perfect groups
    142. 19.142. Perfect subgroups
    143. 19.143. Powers of elements in commutative monoids
    144. 19.144. Powers of elements in groups
    145. 19.145. Powers of elements in monoids
    146. 19.146. The precategory of commutative monoids
    147. 19.147. The precategory of concrete groups
    148. 19.148. The precategory of group actions
    149. 19.149. The precategory of groups
    150. 19.150. The precategory of monoids
    151. 19.151. The precategory of orbits of a monoid action
    152. 19.152. The precategory of semigroups
    153. 19.153. Principal group actions
    154. 19.154. Principal torsors of concrete groups
    155. 19.155. Products of elements in a monoid
    156. 19.156. Pullbacks of subgroups
    157. 19.157. Pullbacks of subsemigroups
    158. 19.158. Quotient groups
    159. 19.159. Quotient groups of concrete groups
    160. 19.160. Quotients of abelian groups
    161. 19.161. Rational commutative monoids
    162. 19.162. Representations of monoids in precategories
    163. 19.163. Saturated congruence relations on commutative monoids
    164. 19.164. Saturated congruence relations on monoids
    165. 19.165. Semigroups
    166. 19.166. Sheargroups
    167. 19.167. Shriek of concrete group homomorphisms
    168. 19.168. Stabilizer groups
    169. 19.169. Stabilizers of concrete group actions
    170. 19.170. Subgroups
    171. 19.171. Subgroups of abelian groups
    172. 19.172. Subgroups of concrete groups
    173. 19.173. Subgroups generated by elements of a group
    174. 19.174. Subgroups generated by families of elements
    175. 19.175. Subgroups generated by subsets of groups
    176. 19.176. Submonoids
    177. 19.177. Submonoids of commutative monoids
    178. 19.178. Subsemigroups
    179. 19.179. Subsets of abelian groups
    180. 19.180. Subsets of commutative monoids
    181. 19.181. Subsets of groups
    182. 19.182. Subsets of monoids
    183. 19.183. Subsets of semigroups
    184. 19.184. The substitution functor of concrete group actions
    185. 19.185. The substitution functor of group actions
    186. 19.186. Sums of finite families of elements in abelian groups
    187. 19.187. Sums of finite families of elements in commutative monoids
    188. 19.188. Sums of finite families of elements in commutative semigroups
    189. 19.189. Sums of finite sequences of elements in abelian groups
    190. 19.190. Sums of finite sequences of elements in commutative monoids
    191. 19.191. Sums of finite sequences of elements in commutative semigroups
    192. 19.192. Sums of finite sequences of elements in groups
    193. 19.193. Sums of finite sequences of elements in monoids
    194. 19.194. Sums of finite sequences of elements in semigroups
    195. 19.195. Surjective group homomorphisms
    196. 19.196. Surjective semigroup homomorphisms
    197. 19.197. Symmetric concrete groups
    198. 19.198. Symmetric groups
    199. 19.199. Torsion elements of groups
    200. 19.200. Torsion-free groups
    201. 19.201. Torsors of abstract groups
    202. 19.202. Transitive concrete group actions
    203. 19.203. Transitive group actions
    204. 19.204. Trivial concrete groups
    205. 19.205. Trivial group homomorphisms
    206. 19.206. Trivial groups
    207. 19.207. Trivial subgroups
    208. 19.208. Unordered tuples of elements in commutative monoids
    209. 19.209. Wild representations of monoids
  22. 20. Higher group theory
    ❱
    1. 20.1. Abelian higher groups
    2. 20.2. Automorphism groups
    3. 20.3. Cartesian products of higher groups
    4. 20.4. Conjugation in higher groups
    5. 20.5. Cyclic higher groups
    6. 20.6. Deloopable groups
    7. 20.7. Deloopable H-spaces
    8. 20.8. Deloopable types
    9. 20.9. Eilenberg-Mac Lane spaces
    10. 20.10. Equivalences of higher groups
    11. 20.11. Fixed points of higher group actions
    12. 20.12. Free higher group actions
    13. 20.13. Higher group actions
    14. 20.14. Higher groups
    15. 20.15. Homomorphisms of higher group actions
    16. 20.16. Homomorphisms of higher groups
    17. 20.17. The higher group of integers
    18. 20.18. Iterated cartesian products of higher groups
    19. 20.19. Iterated deloopings of pointed types
    20. 20.20. Orbits of higher group actions
    21. 20.21. Small ∞-groups
    22. 20.22. Subgroups of higher groups
    23. 20.23. Symmetric higher groups
    24. 20.24. Transitive higher group actions
    25. 20.25. Trivial higher groups
  23. 21. Linear algebra
    ❱
    1. 21.1. Constant matrices
    2. 21.2. Diagonal tuples
    3. 21.3. Dependent products of left modules over commutative rings
    4. 21.4. Dependent products of left modules over rings
    5. 21.5. Diagonal matrices on rings
    6. 21.6. Finite sequences in abelian groups
    7. 21.7. Finite sequences in commutative monoids
    8. 21.8. Finite sequences in commutative rings
    9. 21.9. Finite sequences in commutative semigroups
    10. 21.10. Finite sequences in commutative semirings
    11. 21.11. Finite sequences in euclidean domains
    12. 21.12. Finite sequences in groups
    13. 21.13. Finite sequences in monoids
    14. 21.14. Finite sequences in rings
    15. 21.15. Finite sequences in semigroups
    16. 21.16. Finite sequences in semirings
    17. 21.17. Functoriality of the type of matrices
    18. 21.18. Left modules over commutative rings
    19. 21.19. Left modules over rings
    20. 21.20. Left submodules over rings
    21. 21.21. Linear combinations of tuples of vectors in left modules over rings
    22. 21.22. Linear maps between left modules over rings
    23. 21.23. Linear spans in left modules over rings
    24. 21.24. Matrices
    25. 21.25. Matrices on rings
    26. 21.26. Multiplication of matrices
    27. 21.27. Preimages of left module structures along homomorphisms of rings
    28. 21.28. Rational modules
    29. 21.29. Right modules over rings
    30. 21.30. Scalar multiplication on matrices
    31. 21.31. Scalar multiplication of tuples
    32. 21.32. Scalar multiplication of tuples on rings
    33. 21.33. Subsets of left modules over rings
    34. 21.34. Transposition of matrices
    35. 21.35. Tuples on commutative monoids
    36. 21.36. Tuples on commutative rings
    37. 21.37. Tuples on commutative semirings
    38. 21.38. Tuples on euclidean domains
    39. 21.39. Tuples on monoids
    40. 21.40. Tuples on rings
    41. 21.41. Tuples on semirings
  24. 22. Lists
    ❱
    1. 22.1. Arrays
    2. 22.2. Concatenation of lists
    3. 22.3. Concatenation of tuples
    4. 22.4. Dependent sequences
    5. 22.5. The equivalence between tuples and finite sequences
    6. 22.6. Finite sequences
    7. 22.7. Flattening of lists
    8. 22.8. Functoriality of the type of finite sequences
    9. 22.9. Functoriality of the list operation
    10. 22.10. Functoriality of the type of tuples
    11. 22.11. Relationship between functoriality of tuples and finite sequences
    12. 22.12. Lists
    13. 22.13. Lists of elements in discrete types
    14. 22.14. Partial sequences
    15. 22.15. Permutations of lists
    16. 22.16. Permutations of tuples
    17. 22.17. Predicates on lists
    18. 22.18. Quicksort for lists
    19. 22.19. Repetitions in sequences
    20. 22.20. Reversing lists
    21. 22.21. Sequences
    22. 22.22. Shifting sequences
    23. 22.23. Sort by insertion for lists
    24. 22.24. Sort by insertion for tuples
    25. 22.25. Sorted lists
    26. 22.26. Sorted tuples
    27. 22.27. Sorting algorithms for lists
    28. 22.28. Sorting algorithms for tuples
    29. 22.29. Subsequences
    30. 22.30. Tuples
    31. 22.31. The universal property of lists with respect to wild monoids
  25. 23. Logic
    ❱
    1. 23.1. Complements of De Morgan subtypes
    2. 23.2. Complements of decidable subtypes
    3. 23.3. Complements of double negation stable subtypes
    4. 23.4. De Morgan embeddings
    5. 23.5. De Morgan maps
    6. 23.6. De Morgan propositions
    7. 23.7. De Morgan subtypes
    8. 23.8. De Morgan types
    9. 23.9. De Morgan's law
    10. 23.10. Dirk Gently's principle
    11. 23.11. Double negation dense maps
    12. 23.12. Double negation dense subtypes of types
    13. 23.13. Double negation eliminating maps
    14. 23.14. Double negation elimination
    15. 23.15. Double negation stable embeddings
    16. 23.16. Double negation stable subtypes
    17. 23.17. Functoriality of existential quantification
    18. 23.18. Irrefutable types
    19. 23.19. Markovian types
    20. 23.20. Markov's principle
    21. 23.21. Propositional double negation elimination
    22. 23.22. Propositionally decidable maps
    23. 23.23. Propositionally decidable types
    24. 23.24. Propositionally double negation eliminating maps
  26. 24. Metric spaces
    ❱
    1. 24.1. Approximations in located metric spaces
    2. 24.2. Approximations in metric spaces
    3. 24.3. The bounded distance decomposition of metric spaces
    4. 24.4. Cartesian products of metric spaces
    5. 24.5. The category of metric spaces and isometries
    6. 24.6. The category of metric spaces and short maps
    7. 24.7. Cauchy approximations in metric spaces
    8. 24.8. Cauchy approximations in pseudometric spaces
    9. 24.9. Cauchy sequences in complete metric spaces
    10. 24.10. Cauchy sequences in metric spaces
    11. 24.11. Closed subsets of located metric spaces
    12. 24.12. Closed subsets of metric spaces
    13. 24.13. The closure of subsets of metric spaces
    14. 24.14. Compact metric spaces
    15. 24.15. Complete metric spaces
    16. 24.16. Continuous functions between metric spaces
    17. 24.17. Convergent Cauchy approximations in metric spaces
    18. 24.18. Convergent sequences in metric spaces
    19. 24.19. Dense subsets of metric spaces
    20. 24.20. Dependent products of metric spaces
    21. 24.21. Discrete metric spaces
    22. 24.22. Elements at bounded distance in metric spaces
    23. 24.23. Equality of metric spaces
    24. 24.24. Equality of pseudometric spaces
    25. 24.25. Extensionality of pseudometric spaces
    26. 24.26. Functions between metric spaces
    27. 24.27. Functions between pseudometric spaces
    28. 24.28. The functor from the precategory of metric spaces and isometries to the precategory of sets
    29. 24.29. The inclusion of isometries into the category of metric spaces and short maps
    30. 24.30. Images of metric spaces under isometries
    31. 24.31. Images of metric spaces
    32. 24.32. Images of metric spaces under short functions
    33. 24.33. Images of metric spaces under uniformly continuous functions
    34. 24.34. Indexed sums of metric spaces
    35. 24.35. Inhabited, totally bounded subspaces of metric spaces
    36. 24.36. The interior of subsets of metric spaces
    37. 24.37. Isometries between metric spaces
    38. 24.38. Isometries between pseudometric spaces
    39. 24.39. Limits of Cauchy approximations in metric spaces
    40. 24.40. Limits of Cauchy approximations in pseudometric spaces
    41. 24.41. Limits of functions between metric spaces
    42. 24.42. Limits of sequences in metric spaces
    43. 24.43. Lipschitz functions between metric spaces
    44. 24.44. Locally constant functions in metric spaces
    45. 24.45. Located metric spaces
    46. 24.46. The metric space of Cauchy approximations in a complete metric space
    47. 24.47. The metric space of Cauchy approximations in a metric space
    48. 24.48. The metric space of convergent Cauchy approximations in a metric space
    49. 24.49. The metric space of convergent sequences in metric spaces
    50. 24.50. The metric space of functions between metric spaces
    51. 24.51. The metric space of isometries between metric spaces
    52. 24.52. The metric space of Lipschitz functions between metric spaces
    53. 24.53. The standard metric space of rational numbers
    54. 24.54. The metric space of short functions between metric spaces
    55. 24.55. Metric spaces
    56. 24.56. Metrics
    57. 24.57. Metrics of metric spaces
    58. 24.58. Metrics of metric spaces are uniformly continuous
    59. 24.59. Monotonic rational neighborhood relations
    60. 24.60. Nets in located metric spaces
    61. 24.61. Nets in metric spaces
    62. 24.62. Open subsets of located metric spaces
    63. 24.63. Open subsets of metric spaces
    64. 24.64. The poset of rational neighborhood relations on a type
    65. 24.65. The precategory of metric spaces and functions
    66. 24.66. The precategory of metric spaces and isometries
    67. 24.67. The precategory of metric spaces and short functions
    68. 24.68. Preimages of rational neighborhood relations along maps
    69. 24.69. Pseudometric spaces
    70. 24.70. Rational approximations of zero
    71. 24.71. Rational Cauchy approximations
    72. 24.72. Rational neighborhood relations
    73. 24.73. Rational sequences approximating zero
    74. 24.74. Reflexive rational neighborhood relations
    75. 24.75. Saturated rational neighborhood relations
    76. 24.76. Sequences in metric spaces
    77. 24.77. Short functions between metric spaces
    78. 24.78. Short functions between pseudometric spaces
    79. 24.79. Similarity of elements in pseudometric spaces
    80. 24.80. Subspaces of metric spaces
    81. 24.81. Symmetric rational neighborhood relations
    82. 24.82. Totally bounded metric spaces
    83. 24.83. Totally bounded subspaces of metric spaces
    84. 24.84. Triangular rational neighborhood relations
    85. 24.85. Uniformly continuous functions between metric spaces
  27. 25. Modal type theory
    ❱
    1. 25.1. The action on homotopies of the flat modality
    2. 25.2. The action on identifications of crisp functions
    3. 25.3. The action on identifications of the flat modality
    4. 25.4. Crisp cartesian product types
    5. 25.5. Crisp coproduct types
    6. 25.6. Crisp dependent function types
    7. 25.7. Crisp dependent pair types
    8. 25.8. Crisp function types
    9. 25.9. Crisp identity types
    10. 25.10. The crisp law of excluded middle
    11. 25.11. Crisp pullbacks
    12. 25.12. Crisp types
    13. 25.13. Dependent universal property of flat discrete crisp types
    14. 25.14. Flat discrete crisp types
    15. 25.15. The flat modality
    16. 25.16. The flat-sharp adjunction
    17. 25.17. Functoriality of the flat modality
    18. 25.18. Functoriality of the sharp modality
    19. 25.19. Sharp codiscrete maps
    20. 25.20. Sharp codiscrete types
    21. 25.21. The sharp modality
    22. 25.22. Transport along crisp identifications
    23. 25.23. The universal property of flat discrete crisp types
  28. 26. Order theory
    ❱
    1. 26.1. Accessible elements with respect to relations
    2. 26.2. Bottom elements in large posets
    3. 26.3. Bottom elements in posets
    4. 26.4. Bottom elements in preorders
    5. 26.5. Chains in posets
    6. 26.6. Chains in preorders
    7. 26.7. Closed interval preserving maps between posets
    8. 26.8. Closed interval preserving maps between total orders
    9. 26.9. Closed intervals in posets
    10. 26.10. Closed intervals in total orders
    11. 26.11. Closure operators on large locales
    12. 26.12. Closure operators on large posets
    13. 26.13. Commuting squares of Galois connections between large posets
    14. 26.14. Commuting squares of order preserving maps of large posets
    15. 26.15. Coverings in locales
    16. 26.16. Decidable posets
    17. 26.17. Decidable preorders
    18. 26.18. Decidable subposets
    19. 26.19. Decidable subpreorders
    20. 26.20. Decidable total orders
    21. 26.21. Decidable total preorders
    22. 26.22. Deflationary maps on a poset
    23. 26.23. Deflationary maps on a preorder
    24. 26.24. Dependent products of large frames
    25. 26.25. Dependent products of large inflattices
    26. 26.26. Dependent products of large locales
    27. 26.27. Dependent products of large meet-semilattices
    28. 26.28. Dependent products of large posets
    29. 26.29. Dependent products of large preorders
    30. 26.30. Dependent products of large suplattices
    31. 26.31. Distributive lattices
    32. 26.32. Finite coverings in locales
    33. 26.33. Finite posets
    34. 26.34. Finite preorders
    35. 26.35. Finite total orders
    36. 26.36. Finitely graded posets
    37. 26.37. Frames
    38. 26.38. Galois connections
    39. 26.39. Galois connections between large posets
    40. 26.40. Greatest lower bounds in large posets
    41. 26.41. Greatest lower bounds in posets
    42. 26.42. Homomorphisms of frames
    43. 26.43. Homomorphisms of large frames
    44. 26.44. Homomorphisms of large locales
    45. 26.45. Homomorphisms of large meet-semilattices
    46. 26.46. Homomorphisms of large suplattices
    47. 26.47. Homomorphisms of meet-semilattices
    48. 26.48. Homomorphisms of meet-suplattices
    49. 26.49. Homomorphisms of suplattices
    50. 26.50. Ideals in preorders
    51. 26.51. Incidence algebras
    52. 26.52. Increasing sequences in partially ordered sets
    53. 26.53. Inflationary maps on a poset
    54. 26.54. Inflationary maps on a preorder
    55. 26.55. Inflattices
    56. 26.56. Inhabited chains in posets
    57. 26.57. Inhabited chains in preorders
    58. 26.58. Inhabited finite total orders
    59. 26.59. Intersections of closed intervals in total orders
    60. 26.60. Interval subposets
    61. 26.61. Join preserving maps between posets
    62. 26.62. Join-semilattices
    63. 26.63. Joins of finite families of elements in join-semilattices
    64. 26.64. The Knaster–Tarski fixed point theorem
    65. 26.65. Large frames
    66. 26.66. Large inflattices
    67. 26.67. Large join-semilattices
    68. 26.68. Large locales
    69. 26.69. Large meet-semilattices
    70. 26.70. Large meet-subsemilattices
    71. 26.71. Large posets
    72. 26.72. Large preorders
    73. 26.73. Large quotient locales
    74. 26.74. Large strict orders
    75. 26.75. Large strict preorders
    76. 26.76. Large subframes
    77. 26.77. Large subposets
    78. 26.78. Large subpreorders
    79. 26.79. Large subsuplattices
    80. 26.80. Large suplattices
    81. 26.81. Lattices
    82. 26.82. Least upper bounds in large posets
    83. 26.83. Least upper bounds in posets
    84. 26.84. Locales
    85. 26.85. Locally finite posets
    86. 26.86. Lower bounds in large posets
    87. 26.87. Lower bounds in posets
    88. 26.88. Lower sets in large posets
    89. 26.89. Lower types in preorders
    90. 26.90. Maximal chains in posets
    91. 26.91. Maximal chains in preorders
    92. 26.92. Meet-semilattices
    93. 26.93. Meet-suplattices
    94. 26.94. Meets of finite families of elements in meet-semilattices
    95. 26.95. Nuclei on large locales
    96. 26.96. Opposite large posets
    97. 26.97. Opposite large preorders
    98. 26.98. Opposite posets
    99. 26.99. Opposite preorders
    100. 26.100. Order preserving maps between large posets
    101. 26.101. Order preserving maps between large preorders
    102. 26.102. Order preserving maps between posets
    103. 26.103. Order preserving maps between preorders
    104. 26.104. Ordinals
    105. 26.105. The poset of closed intervals in posets
    106. 26.106. The poset of closed intervals in total orders
    107. 26.107. Posets
    108. 26.108. Powers of large locales
    109. 26.109. The precategory of decidable total orders
    110. 26.110. The precategory of finite posets
    111. 26.111. The precategory of finite total orders
    112. 26.112. The precategory of inhabited finite total orders
    113. 26.113. The precategory of posets
    114. 26.114. The precategory of total orders
    115. 26.115. Preorders
    116. 26.116. Principal lower sets of large posets
    117. 26.117. Principal upper sets of large posets
    118. 26.118. Reflective Galois connections between large posets
    119. 26.119. Resizing posets
    120. 26.120. Resizing preorders
    121. 26.121. Resizing suplattices
    122. 26.122. Sequences in partially ordered sets
    123. 26.123. Sequences in preorders
    124. 26.124. Sequences in strictly preordered sets
    125. 26.125. Similarity of elements in large posets
    126. 26.126. Similarity of elements in large preorders
    127. 26.127. Similarity of elements in large strict orders
    128. 26.128. Similarity of elements in large strict preorders
    129. 26.129. Similarity of elements in strict orders
    130. 26.130. Similarity of elements in strict preorders
    131. 26.131. Similarity of order preserving maps between large posets
    132. 26.132. Similarity of order preserving maps between large preorders
    133. 26.133. Spans of closed intervals in total orders
    134. 26.134. Strict order preserving maps
    135. 26.135. Strict orders
    136. 26.136. Strict preorders
    137. 26.137. Strictly increasing sequences in strictly preordered sets
    138. 26.138. Strictly inflationary maps on a strictly preordered type
    139. 26.139. Strictly preordered sets
    140. 26.140. Subposets
    141. 26.141. Subpreorders
    142. 26.142. Suplattices
    143. 26.143. Supremum preserving maps between posets
    144. 26.144. Top elements in large posets
    145. 26.145. Top elements in posets
    146. 26.146. Top elements in preorders
    147. 26.147. Total orders
    148. 26.148. Total preorders
    149. 26.149. Transitive well-founded relations
    150. 26.150. Transposing inequalities in posets along order-preserving retractions
    151. 26.151. Transposing inequalities in posets along sections of order-preserving maps
    152. 26.152. Upper bounds of chains in posets
    153. 26.153. Upper bounds in large posets
    154. 26.154. Upper bounds in posets
    155. 26.155. Upper sets of large posets
    156. 26.156. Well-founded relations
    157. 26.157. Zorn's lemma
  29. 27. Organic chemistry
    ❱
    1. 27.1. Alcohols
    2. 27.2. Alkanes
    3. 27.3. Alkenes
    4. 27.4. Alkynes
    5. 27.5. Ethane
    6. 27.6. Hydrocarbons
    7. 27.7. Methane
    8. 27.8. Saturated carbons
  30. 28. Orthogonal factorization systems
    ❱
    1. 28.1. Anodyne maps
    2. 28.2. Cd-structures
    3. 28.3. Cellular maps
    4. 28.4. The closed modalities
    5. 28.5. Continuation modalities
    6. 28.6. Double lifts of families of elements
    7. 28.7. Double negation sheaves
    8. 28.8. Extensions of double lifts of families of elements
    9. 28.9. Extensions of families of elements
    10. 28.10. Extensions of maps
    11. 28.11. Factorization operations
    12. 28.12. Factorization operations into function classes
    13. 28.13. Factorization operations into global function classes
    14. 28.14. Factorizations of maps
    15. 28.15. Factorizations of maps into function classes
    16. 28.16. Factorizations of maps into global function classes
    17. 28.17. Families of types local at a map
    18. 28.18. Fiberwise orthogonal maps
    19. 28.19. Function classes
    20. 28.20. Functoriality of higher modalities
    21. 28.21. Functoriality of localizations at global subuniverses
    22. 28.22. Functoriality of the pullback-hom
    23. 28.23. Functoriality of reflective global subuniverses
    24. 28.24. Global function classes
    25. 28.25. Higher modalities
    26. 28.26. The identity modality
    27. 28.27. Large Lawvere–Tierney topologies
    28. 28.28. Lawvere–Tierney topologies
    29. 28.29. Lifting operations
    30. 28.30. Lifting structures on commuting squares of maps
    31. 28.31. Lifts of families of elements
    32. 28.32. Lifts of maps
    33. 28.33. Localizations at global subuniverses
    34. 28.34. Localizations at maps
    35. 28.35. Localizations at subuniverses
    36. 28.36. Locally small modal-operators
    37. 28.37. Maps local at maps
    38. 28.38. Mere lifting properties
    39. 28.39. Modal induction
    40. 28.40. Modal operators
    41. 28.41. Modal subuniverse induction
    42. 28.42. Null families of types
    43. 28.43. Null maps
    44. 28.44. Null types
    45. 28.45. The open modalities
    46. 28.46. Orthogonal factorization systems
    47. 28.47. Orthogonal maps
    48. 28.48. Precomposition of lifts of families of elements by maps
    49. 28.49. The pullback-hom
    50. 28.50. The raise modalities
    51. 28.51. Reflective global subuniverses
    52. 28.52. Reflective modalities
    53. 28.53. Reflective subuniverses
    54. 28.54. Regular cd-structures
    55. 28.55. Σ-closed modalities
    56. 28.56. Σ-closed reflective modalities
    57. 28.57. Σ-closed reflective subuniverses
    58. 28.58. Stable orthogonal factorization systems
    59. 28.59. Types colocal at maps
    60. 28.60. Types local at maps
    61. 28.61. Types separated at maps
    62. 28.62. Uniquely eliminating modalities
    63. 28.63. The universal property of localizations at global subuniverses
    64. 28.64. Weakly anodyne maps
    65. 28.65. Wide function classes
    66. 28.66. Wide global function classes
    67. 28.67. The zero modality
  31. 29. Polytopes
    ❱
    1. 29.1. Abstract polytopes
  32. 30. Primitives
    ❱
    1. 30.1. Characters
    2. 30.2. Floats
    3. 30.3. Machine integers
    4. 30.4. Strings
  33. 31. Real numbers
    ❱
    1. 31.1. The absolute value of real numbers
    2. 31.2. Addition of lower Dedekind real numbers
    3. 31.3. Addition of Dedekind real numbers
    4. 31.4. Addition of upper Dedekind real numbers
    5. 31.5. Apartness of real numbers
    6. 31.6. Arithmetically located Dedekind cuts
    7. 31.7. The binary maximum of real numbers
    8. 31.8. The binary minimum of real numbers
    9. 31.9. Cauchy completeness of the Dedekind real numbers
    10. 31.10. Dedekind real numbers
    11. 31.11. The difference between real numbers
    12. 31.12. The distance between real numbers
    13. 31.13. Finitely enumerable subsets of the real numbers
    14. 31.14. Inequality on the lower Dedekind real numbers
    15. 31.15. Inequality on the real numbers
    16. 31.16. Inequality on the upper Dedekind real numbers
    17. 31.17. Infima of families of real numbers
    18. 31.18. Inhabited finitely enumerable subsets of the real numbers
    19. 31.19. Inhabited totally bounded subsets of the real numbers
    20. 31.20. The addition isometry on real numbers
    21. 31.21. The negation isometry on real numbers
    22. 31.22. Lower Dedekind real numbers
    23. 31.23. The maximum of finite families of real numbers
    24. 31.24. The maximum of inhabited, finitely enumerable subsets of real numbers
    25. 31.25. The maximum of lower Dedekind real numbers
    26. 31.26. The maximum of upper Dedekind real numbers
    27. 31.27. The metric space of real numbers
    28. 31.28. The minimum of finite families of real numbers
    29. 31.29. The minimum of inhabited, finitely enumerable subsets of real numbers
    30. 31.30. The minimum of lower Dedekind real numbers
    31. 31.31. The minimum of upper Dedekind real numbers
    32. 31.32. Negation of lower and upper Dedekind real numbers
    33. 31.33. Negation of real numbers
    34. 31.34. Nonnegative real numbers
    35. 31.35. Positive real numbers
    36. 31.36. Raising the universe levels of real numbers
    37. 31.37. Rational lower Dedekind real numbers
    38. 31.38. Rational real numbers
    39. 31.39. Rational upper Dedekind real numbers
    40. 31.40. Real numbers from lower Dedekind real numbers
    41. 31.41. Real numbers from upper Dedekind real numbers
    42. 31.42. Saturation of inequality of real numbers
    43. 31.43. Similarity of real numbers
    44. 31.44. Strict inequality of real numbers
    45. 31.45. Subsets of the real numbers
    46. 31.46. Suprema of families of real numbers
    47. 31.47. Totally bounded subsets of the real numbers
    48. 31.48. Transposition of addition and subtraction through cuts of Dedekind real numbers
    49. 31.49. Upper Dedekind real numbers
  34. 32. Reflection
    ❱
    1. 32.1. Abstractions
    2. 32.2. Arguments
    3. 32.3. Boolean reflection
    4. 32.4. Definitions
    5. 32.5. Erasing equality
    6. 32.6. Fixity
    7. 32.7. Group solver
    8. 32.8. Literals
    9. 32.9. Metavariables
    10. 32.10. Names
    11. 32.11. Precategory solver
    12. 32.12. Rewriting
    13. 32.13. Terms
    14. 32.14. The type checking monad
  35. 33. Ring theory
    ❱
    1. 33.1. Additive orders of elements of rings
    2. 33.2. Algebras over rings
    3. 33.3. Arithmetic sequences in semirings
    4. 33.4. Arithmetic series in semirings
    5. 33.5. The binomial theorem for rings
    6. 33.6. The binomial theorem for semirings
    7. 33.7. The category of cyclic rings
    8. 33.8. The category of rings
    9. 33.9. Central elements of rings
    10. 33.10. Central elements of semirings
    11. 33.11. Characteristics of rings
    12. 33.12. Commuting elements of rings
    13. 33.13. Congruence relations on rings
    14. 33.14. Congruence relations on semirings
    15. 33.15. Cyclic rings
    16. 33.16. Dependent products of ring extensions of the rational numbers
    17. 33.17. Dependent products of rings
    18. 33.18. Dependent products of semirings
    19. 33.19. Division rings
    20. 33.20. The free ring with one generator
    21. 33.21. Full ideals of rings
    22. 33.22. Function rings
    23. 33.23. Function semirings
    24. 33.24. Generating elements of rings
    25. 33.25. Geometric sequences in semirings
    26. 33.26. The group of multiplicative units of a ring
    27. 33.27. Homomorphisms of cyclic rings
    28. 33.28. Homomorphisms of ring extensions of the rational numbers
    29. 33.29. Homomorphisms of rings
    30. 33.30. Homomorphisms of semirings
    31. 33.31. Ideals generated by subsets of rings
    32. 33.32. Ideals of rings
    33. 33.33. Ideals of semirings
    34. 33.34. Idempotent elements in rings
    35. 33.35. Initial rings
    36. 33.36. Integer multiples of elements of rings
    37. 33.37. Intersections of ideals of rings
    38. 33.38. Intersections of ideals of semirings
    39. 33.39. The invariant basis property of rings
    40. 33.40. Invertible elements in rings
    41. 33.41. Isomorphisms of rings
    42. 33.42. Joins of ideals of rings
    43. 33.43. Joins of left ideals of rings
    44. 33.44. Joins of right ideals of rings
    45. 33.45. Kernels of ring homomorphisms
    46. 33.46. Left ideals generated by subsets of rings
    47. 33.47. Left ideals of rings
    48. 33.48. Local rings
    49. 33.49. Localizations of rings
    50. 33.50. Maximal ideals of rings
    51. 33.51. Multiples of elements in rings
    52. 33.52. Multiplicative orders of elements of rings
    53. 33.53. Nil ideals of rings
    54. 33.54. Nilpotent elements in rings
    55. 33.55. Nilpotent elements in semirings
    56. 33.56. Opposite ring extensions of the rational numbers
    57. 33.57. Opposite rings
    58. 33.58. Partial sums of sequences in semirings
    59. 33.59. The poset of cyclic rings
    60. 33.60. The poset of ideals of a ring
    61. 33.61. The poset of left ideals of a ring
    62. 33.62. The poset of right ideals of a ring
    63. 33.63. Powers of elements in rings
    64. 33.64. Powers of elements in semirings
    65. 33.65. The precategory of rings
    66. 33.66. The precategory of semirings
    67. 33.67. Products of ideals of rings
    68. 33.68. Products of left ideals of rings
    69. 33.69. Products of right ideals of rings
    70. 33.70. Products of rings
    71. 33.71. Products of subsets of rings
    72. 33.72. Quotient rings
    73. 33.73. Radical ideals of rings
    74. 33.74. Right ideals generated by subsets of rings
    75. 33.75. Right ideals of rings
    76. 33.76. Ring extensions of the rational numbers
    77. 33.77. Rings
    78. 33.78. Semirings
    79. 33.79. Subsets of rings
    80. 33.80. Subsets of semirings
    81. 33.81. Sums of finite families of elements in rings
    82. 33.82. Sums of finite families of elements in semirings
    83. 33.83. Sums of finite sequences in rings
    84. 33.84. Sums of finite sequences in semirings
    85. 33.85. Transporting ring structures along isomorphisms of abelian groups
    86. 33.86. Trivial rings
  36. 34. Set theory
    ❱
    1. 34.1. Baire space
    2. 34.2. Cantor space
    3. 34.3. Cantor's diagonal argument
    4. 34.4. Cardinalities of sets
    5. 34.5. Countable sets
    6. 34.6. Cumulative hierarchy
    7. 34.7. Infinite sets
    8. 34.8. Russell's paradox
    9. 34.9. Uncountable sets
  37. 35. Species
    ❱
    1. 35.1. Cartesian exponents of species of types
    2. 35.2. Cartesian products of species of types
    3. 35.3. Cauchy composition of species of types
    4. 35.4. Cauchy composition of species of types in subuniverses
    5. 35.5. Cauchy exponentials of species of types
    6. 35.6. Cauchy exponentials of species of types in subuniverses
    7. 35.7. Cauchy products of species of types
    8. 35.8. Cauchy products of species of types in subuniverses
    9. 35.9. Cauchy series of species of types
    10. 35.10. Cauchy series of species of types in subuniverses
    11. 35.11. Composition of Cauchy series of species of types
    12. 35.12. Composition of Cauchy series of species of types in subuniverses
    13. 35.13. Coproducts of species of types
    14. 35.14. Coproducts of species of types in subuniverses
    15. 35.15. Cycle index series of species
    16. 35.16. Derivatives of species
    17. 35.17. Dirichlet exponentials of a species of types
    18. 35.18. Dirichlet exponentials of species of types in subuniverses
    19. 35.19. Dirichlet products of species of types
    20. 35.20. Dirichlet products of species of types in subuniverses
    21. 35.21. Dirichlet series of species of finite inhabited types
    22. 35.22. Dirichlet series of species of types
    23. 35.23. Dirichlet series of species of types in subuniverses
    24. 35.24. Equivalences of species of types
    25. 35.25. Equivalences of species of types in subuniverses
    26. 35.26. Exponential of Cauchy series of species of types
    27. 35.27. Exponential of Cauchy series of species of types in subuniverses
    28. 35.28. Hasse-Weil species
    29. 35.29. Morphisms of finite species
    30. 35.30. Morphisms of species of types
    31. 35.31. Pointing of species of types
    32. 35.32. The precategory of finite species
    33. 35.33. Products of Cauchy series of species of types
    34. 35.34. Products of Cauchy series of species of types in subuniverses
    35. 35.35. Products of Dirichlet series of species of finite inhabited types
    36. 35.36. Products of Dirichlet series of species of types
    37. 35.37. Products of Dirichlet series of species of types in subuniverses
    38. 35.38. Small Composition of species of finite inhabited types
    39. 35.39. Small Cauchy composition of species types in subuniverses
    40. 35.40. Species of finite inhabited types
    41. 35.41. Species of finite types
    42. 35.42. Species of inhabited types
    43. 35.43. Species of types
    44. 35.44. Species of types in subuniverses
    45. 35.45. The unit of Cauchy composition of species of types
    46. 35.46. The unit of Cauchy composition of species of types in subuniverses
    47. 35.47. Unlabeled structures of finite species
  38. 36. Structured types
    ❱
    1. 36.1. Cartesian products of types equipped with endomorphisms
    2. 36.2. Central H-spaces
    3. 36.3. Commuting squares of pointed homotopies
    4. 36.4. Commuting squares of pointed maps
    5. 36.5. Commuting triangles of pointed maps
    6. 36.6. Conjugation of pointed types
    7. 36.7. Constant pointed maps
    8. 36.8. Contractible pointed types
    9. 36.9. Cyclic types
    10. 36.10. Dependent products of H-spaces
    11. 36.11. Dependent products of pointed types
    12. 36.12. Dependent products of wild monoids
    13. 36.13. Dependent types equipped with automorphisms
    14. 36.14. Equivalences of H-spaces
    15. 36.15. Equivalences of pointed arrows
    16. 36.16. Equivalences of types equipped with automorphisms
    17. 36.17. Equivalences of types equipped with endomorphisms
    18. 36.18. Faithful pointed maps
    19. 36.19. Fibers of pointed maps
    20. 36.20. Finite multiplication in magmas
    21. 36.21. Function H-spaces
    22. 36.22. Function magmas
    23. 36.23. Function wild monoids
    24. 36.24. H-spaces
    25. 36.25. The initial pointed type equipped with an automorphism
    26. 36.26. The involutive type of H-space structures on a pointed type
    27. 36.27. Involutive types
    28. 36.28. Iterated cartesian products of types equipped with endomorphisms
    29. 36.29. Iterated cartesian products of pointed types
    30. 36.30. Magmas
    31. 36.31. Medial magmas
    32. 36.32. Mere equivalences of types equipped with endomorphisms
    33. 36.33. Morphisms of H-spaces
    34. 36.34. Morphisms of magmas
    35. 36.35. Morphisms of pointed arrows
    36. 36.36. Morphisms of twisted pointed arrows
    37. 36.37. Morphisms of types equipped with automorphisms
    38. 36.38. Morphisms of types equipped with endomorphisms
    39. 36.39. Morphisms of wild monoids
    40. 36.40. Noncoherent H-spaces
    41. 36.41. Opposite pointed spans
    42. 36.42. Pointed 2-homotopies
    43. 36.43. Pointed cartesian product types
    44. 36.44. Pointed dependent functions
    45. 36.45. Pointed dependent pair types
    46. 36.46. Pointed equivalences
    47. 36.47. Pointed families of types
    48. 36.48. Pointed homotopies
    49. 36.49. Pointed isomorphisms
    50. 36.50. Pointed maps
    51. 36.51. Pointed retractions of pointed maps
    52. 36.52. Pointed sections of pointed maps
    53. 36.53. Pointed span diagrams
    54. 36.54. Pointed spans
    55. 36.55. Pointed types
    56. 36.56. Pointed types equipped with automorphisms
    57. 36.57. The pointed unit type
    58. 36.58. Universal property of contractible types with respect to pointed types and maps
    59. 36.59. Postcomposition of pointed maps
    60. 36.60. Precomposition of pointed maps
    61. 36.61. Products of magmas
    62. 36.62. Sets equipped with automorphisms
    63. 36.63. Small pointed types
    64. 36.64. Symmetric elements of involutive types
    65. 36.65. Symmetric H-spaces
    66. 36.66. Transposition of pointed span diagrams
    67. 36.67. Types equipped with automorphisms
    68. 36.68. Types equipped with endomorphisms
    69. 36.69. Uniform pointed homotopies
    70. 36.70. The universal property of pointed equivalences
    71. 36.71. Unpointed maps between pointed types
    72. 36.72. Whiskering pointed homotopies with respect to concatenation
    73. 36.73. Whiskering of pointed homotopies with respect to composition of pointed maps
    74. 36.74. The wild category of pointed types
    75. 36.75. Wild groups
    76. 36.76. Wild loops
    77. 36.77. Wild monoids
    78. 36.78. Wild quasigroups
    79. 36.79. Wild semigroups
  39. 37. Synthetic category theory
    ❱
    1. 37.1. Cone diagrams of synthetic categories
    2. 37.2. Cospans of synthetic categories
    3. 37.3. Equivalences between synthetic categories
    4. 37.4. Invertible functors between synthetic categories
    5. 37.5. Pullbacks of synthetic categories
    6. 37.6. Retractions of functors between synthetic categories
    7. 37.7. Sections of functor between synthetic categories
    8. 37.8. Synthetic categories
  40. 38. Synthetic homotopy theory
    ❱
    1. 38.1. 0-acyclic maps
    2. 38.2. 0-acyclic types
    3. 38.3. 1-acyclic types
    4. 38.4. Acyclic maps
    5. 38.5. Acyclic types
    6. 38.6. The category of connected set bundles over the circle
    7. 38.7. Cavallo's trick
    8. 38.8. The circle
    9. 38.9. Cocartesian morphisms of arrows
    10. 38.10. Cocones under pointed span diagrams
    11. 38.11. Cocones under sequential diagrams
    12. 38.12. Cocones under spans
    13. 38.13. Codiagonals of maps
    14. 38.14. Coequalizers
    15. 38.15. Cofibers of maps
    16. 38.16. Cofibers of pointed maps
    17. 38.17. Coforks
    18. 38.18. Correspondence between cocones under sequential diagrams and certain coforks
    19. 38.19. Conjugation of loops
    20. 38.20. Connected set bundles over the circle
    21. 38.21. Connective prespectra
    22. 38.22. Connective spectra
    23. 38.23. Dependent cocones under sequential diagrams
    24. 38.24. Dependent cocones under spans
    25. 38.25. Dependent coforks
    26. 38.26. Dependent descent for the circle
    27. 38.27. The dependent pullback property of pushouts
    28. 38.28. Dependent pushout-products
    29. 38.29. Dependent sequential diagrams
    30. 38.30. Dependent suspension structures
    31. 38.31. The dependent universal property of coequalizers
    32. 38.32. The dependent universal property of pushouts
    33. 38.33. The dependent universal property of sequential colimits
    34. 38.34. Dependent universal property of suspensions
    35. 38.35. The descent property of the circle
    36. 38.36. Descent data for constant type families over the circle
    37. 38.37. Descent data for families of dependent pair types over the circle
    38. 38.38. Descent data for families of equivalence types over the circle
    39. 38.39. Descent data for families of function types over the circle
    40. 38.40. Subtypes of descent data for the circle
    41. 38.41. Descent data for type families of equivalence types over pushouts
    42. 38.42. Descent data for type families of function types over pushouts
    43. 38.43. Descent data for type families of identity types over pushouts
    44. 38.44. Descent data for pushouts
    45. 38.45. Descent data for sequential colimits
    46. 38.46. Descent property of pushouts
    47. 38.47. Descent property of sequential colimits
    48. 38.48. Double loop spaces
    49. 38.49. The Eckmann-Hilton argument
    50. 38.50. Equifibered sequential diagrams
    51. 38.51. Equifibered span diagrams
    52. 38.52. Equivalences of cocones under sequential diagrams
    53. 38.53. Equivalences of coforks
    54. 38.54. Equivalances of dependent sequential diagrams
    55. 38.55. Equivalences of descent data for pushouts
    56. 38.56. Equivalences of equifibered span diagrams
    57. 38.57. Equivalences of sequential diagrams
    58. 38.58. Families with descent data for pushouts
    59. 38.59. Families with descent data for sequential colimits
    60. 38.60. The flattening lemma for coequalizers
    61. 38.61. The flattening lemma for pushouts
    62. 38.62. The flattening lemma for sequential colimits
    63. 38.63. Free loops
    64. 38.64. Functoriality of the loop space operation
    65. 38.65. Functoriality of sequential colimits
    66. 38.66. Functoriality of suspensions
    67. 38.67. Groups of loops in 1-types
    68. 38.68. Hatcher's acyclic type
    69. 38.69. Homotopy groups
    70. 38.70. Identity systems of descent data for pushouts
    71. 38.71. The induction principle of pushouts
    72. 38.72. The infinite dimensional complex projective space
    73. 38.73. Infinite cyclic types
    74. 38.74. The infinite dimensional real projective space
    75. 38.75. The interval
    76. 38.76. Iterated loop spaces
    77. 38.77. Iterated suspensions of pointed types
    78. 38.78. Join powers of types
    79. 38.79. Joins of maps
    80. 38.80. Joins of types
    81. 38.81. Left half-smash products
    82. 38.82. The loop homotopy on the circle
    83. 38.83. Loop spaces
    84. 38.84. Maps of prespectra
    85. 38.85. Mather's second cube theorem
    86. 38.86. Mere spheres
    87. 38.87. Morphisms of cocones under morphisms of sequential diagrams
    88. 38.88. Morphisms of coforks
    89. 38.89. Morphisms of dependent sequential diagrams
    90. 38.90. Morphisms of descent data of the circle
    91. 38.91. Morphisms of descent data for pushouts
    92. 38.92. Morphisms of sequential diagrams
    93. 38.93. The multiplication operation on the circle
    94. 38.94. Null cocones under pointed span diagrams
    95. 38.95. The plus-principle
    96. 38.96. Powers of loops
    97. 38.97. Premanifolds
    98. 38.98. Prespectra
    99. 38.99. The pullback property of pushouts
    100. 38.100. Pushout-products
    101. 38.101. Pushouts
    102. 38.102. Pushouts of pointed types
    103. 38.103. The recursion principle of pushouts
    104. 38.104. Retracts of sequential diagrams
    105. 38.105. Rewriting rules for pushouts
    106. 38.106. Sections of families over the circle
    107. 38.107. Sections of descent data for pushouts
    108. 38.108. Sequential colimits
    109. 38.109. Sequential diagrams
    110. 38.110. Sequentially compact types
    111. 38.111. Shifts of sequential diagrams
    112. 38.112. Smash products of pointed types
    113. 38.113. Spectra
    114. 38.114. The sphere prespectrum
    115. 38.115. Spheres
    116. 38.116. Suspension prespectra
    117. 38.117. Suspension Structures
    118. 38.118. Suspensions of pointed types
    119. 38.119. Suspensions of propositions
    120. 38.120. Suspensions of types
    121. 38.121. Tangent spheres
    122. 38.122. Total cocones of type families over cocones under sequential diagrams
    123. 38.123. Total sequential diagrams of dependent sequential diagrams
    124. 38.124. Triple loop spaces
    125. 38.125. k-acyclic maps
    126. 38.126. k-acyclic types
    127. 38.127. The universal cover of the circle
    128. 38.128. The universal property of the circle
    129. 38.129. The universal property of coequalizers
    130. 38.130. The universal property of pushouts
    131. 38.131. The universal property of sequential colimits
    132. 38.132. Universal property of suspensions
    133. 38.133. Universal Property of suspensions of pointed types
    134. 38.134. Wedges of pointed types
    135. 38.135. The Whitehead principle for maps
    136. 38.136. The Whitehead principle for types
    137. 38.137. Zigzags between sequential diagrams
  41. 39. Trees
    ❱
    1. 39.1. Algebras for polynomial endofunctors
    2. 39.2. Bases of directed trees
    3. 39.3. Bases of enriched directed trees
    4. 39.4. Binary W-types
    5. 39.5. Bounded multisets
    6. 39.6. The coalgebra of directed trees
    7. 39.7. The coalgebra of enriched directed trees
    8. 39.8. Coalgebras of polynomial endofunctors
    9. 39.9. The combinator of directed trees
    10. 39.10. Combinators of enriched directed trees
    11. 39.11. Directed trees
    12. 39.12. The elementhood relation on coalgebras of polynomial endofunctors
    13. 39.13. The elementhood relation on W-types
    14. 39.14. Empty multisets
    15. 39.15. Enriched directed trees
    16. 39.16. Equivalences of directed trees
    17. 39.17. Equivalences of enriched directed trees
    18. 39.18. Extensional W-types
    19. 39.19. Fibers of directed trees
    20. 39.20. Fibers of enriched directed trees
    21. 39.21. Full binary trees
    22. 39.22. Functoriality of the combinator of directed trees
    23. 39.23. Functoriality of the fiber operation on directed trees
    24. 39.24. Functoriality of W-types
    25. 39.25. Hereditary W-types
    26. 39.26. Indexed W-types
    27. 39.27. Induction principles on W-types
    28. 39.28. Inequality on W-types
    29. 39.29. Lower types of elements in W-types
    30. 39.30. Morphisms of algebras of polynomial endofunctors
    31. 39.31. Morphisms of coalgebras of polynomial endofunctors
    32. 39.32. Morphisms of directed trees
    33. 39.33. Morphisms of enriched directed trees
    34. 39.34. Multiset-indexed dependent products of types
    35. 39.35. Multisets
    36. 39.36. Multivariable polynomial functors
    37. 39.37. Planar binary trees
    38. 39.38. Plane trees
    39. 39.39. Polynomial endofunctors
    40. 39.40. Raising universe levels of directed trees
    41. 39.41. Ranks of elements in W-types
    42. 39.42. Rooted morphisms of directed trees
    43. 39.43. Rooted morphisms of enriched directed trees
    44. 39.44. Rooted quasitrees
    45. 39.45. Rooted undirected trees
    46. 39.46. Small multisets
    47. 39.47. Submultisets
    48. 39.48. Transitive multisets
    49. 39.49. The underlying trees of elements of coalgebras of polynomial endofunctors
    50. 39.50. The underlying trees of elements of W-types
    51. 39.51. Undirected trees
    52. 39.52. The universal multiset
    53. 39.53. The universal tree
    54. 39.54. The W-type of natural numbers
    55. 39.55. The W-type of the type of propositions
    56. 39.56. W-types
  42. 40. Type theories
    ❱
    1. 40.1. Comprehension of fibered type theories
    2. 40.2. Dependent type theories
    3. 40.3. Fibered dependent type theories
    4. 40.4. Π-types in precategories with attributes
    5. 40.5. Π-types in precategories with families
    6. 40.6. Precategories with attributes
    7. 40.7. Precategories with families
    8. 40.8. Sections of dependent type theories
    9. 40.9. Simple type theories
    10. 40.10. Unityped type theories
  43. 41. Univalent combinatorics
    ❱
    1. 41.1. 2-element decidable subtypes
    2. 41.2. 2-element subtypes
    3. 41.3. 2-element types
    4. 41.4. The binomial types
    5. 41.5. Bracelets
    6. 41.6. Cartesian products of finite types
    7. 41.7. The classical definition of the standard finite types
    8. 41.8. Complements of decidable subtypes of finite types
    9. 41.9. Complements of isolated elements of finite types
    10. 41.10. Coproducts of finite types
    11. 41.11. Coproducts of inhabited finite types
    12. 41.12. Counting in type theory
    13. 41.13. Counting the elements of decidable subtypes
    14. 41.14. Counting the elements of dependent pair types
    15. 41.15. Counting the elements in Maybe
    16. 41.16. Cubes
    17. 41.17. Cycle partitions of finite types
    18. 41.18. Cycle prime decompositions of natural numbers
    19. 41.19. Cyclic finite types
    20. 41.20. De Morgan's law for finite families of propositions
    21. 41.21. Decidable dependent function types
    22. 41.22. Decidability of dependent pair types
    23. 41.23. Decidable equivalence relations on finite types
    24. 41.24. Decidable propositions
    25. 41.25. Decidable subtypes of finite types
    26. 41.26. Dedekind finite sets
    27. 41.27. Dedekind finite types
    28. 41.28. Counting the elements of dependent function types
    29. 41.29. Dependent pair types of finite types
    30. 41.30. Finite discrete Σ-decompositions
    31. 41.31. Disjunctions
    32. 41.32. Distributivity of set truncation over finite products
    33. 41.33. Double counting
    34. 41.34. Dual Dedekind finite types
    35. 41.35. Embeddings
    36. 41.36. Embeddings between standard finite types
    37. 41.37. Equality in finite types
    38. 41.38. Equality in the standard finite types
    39. 41.39. Equivalences between finite types
    40. 41.40. Equivalences of cubes
    41. 41.41. Equivalences between standard finite types
    42. 41.42. Ferrers diagrams (unlabeled partitions)
    43. 41.43. Fibers of maps between finite types
    44. 41.44. Finite choice
    45. 41.45. Finite subtypes
    46. 41.46. Finite types
    47. 41.47. Finitely enumerable subtypes
    48. 41.48. Finitely enumerable types
    49. 41.49. Finiteness of the type of connected components
    50. 41.50. Finitely presented types
    51. 41.51. Finite function types
    52. 41.52. The image of a map
    53. 41.53. Inequality on types equipped with a counting
    54. 41.54. Inhabited finite types
    55. 41.55. Inhabited finitely enumerable subtypes
    56. 41.56. Inhabited finitely enumerable types
    57. 41.57. Injective maps between finite types
    58. 41.58. An involution on the standard finite types
    59. 41.59. Isotopies of Latin squares
    60. 41.60. Kuratowski finite sets
    61. 41.61. Latin squares
    62. 41.62. Locally finite types
    63. 41.63. The groupoid of main classes of Latin hypercubes
    64. 41.64. The groupoid of main classes of Latin squares
    65. 41.65. The maybe monad on finite types
    66. 41.66. Necklaces
    67. 41.67. Orientations of the complete undirected graph
    68. 41.68. Orientations of cubes
    69. 41.69. Partitions of finite types
    70. 41.70. Petri-nets
    71. 41.71. π-finite types
    72. 41.72. The pigeonhole principle
    73. 41.73. Finitely π-presented types
    74. 41.74. Quotients of finite types
    75. 41.75. Ramsey theory
    76. 41.76. Repetitions of values
    77. 41.77. Repetitions of values in sequences
    78. 41.78. Retracts of finite types
    79. 41.79. Riffle shuffles
    80. 41.80. Sequences of elements in finite types
    81. 41.81. Set quotients of index 2
    82. 41.82. Finite Σ-decompositions of finite types
    83. 41.83. Skipping elements in standard finite types
    84. 41.84. Small types
    85. 41.85. Standard finite pruned trees
    86. 41.86. Standard finite trees
    87. 41.87. The standard finite types
    88. 41.88. Steiner systems
    89. 41.89. Steiner triple systems
    90. 41.90. Subcounting
    91. 41.91. Subfinite indexing
    92. 41.92. Subfinite types
    93. 41.93. Subfinitely enumerable types
    94. 41.94. Combinatorial identities of sums of natural numbers
    95. 41.95. Surjective maps between finite types
    96. 41.96. Symmetric difference of finite subtypes
    97. 41.97. Finite trivial Σ-decompositions
    98. 41.98. Truncated π-finite types
    99. 41.99. Type duality of finite types
    100. 41.100. Unbounded π-finite types
    101. 41.101. Unions of finite subtypes
    102. 41.102. The universal property of the standard finite types
    103. 41.103. Unlabeled partitions
    104. 41.104. Unlabeled rooted trees
    105. 41.105. Unlabeled trees
    106. 41.106. Untruncated π-finite types
  44. 42. Universal algebra
    ❱
    1. 42.1. Abstract equations over signatures
    2. 42.2. Algebraic theories
    3. 42.3. Algebraic theory of groups
    4. 42.4. Algebras
    5. 42.5. The category of algebras of theories
    6. 42.6. Congruences
    7. 42.7. Equivalences of models of signatures
    8. 42.8. Homomorphisms of algebras
    9. 42.9. Isomorphisms of algebras of theories
    10. 42.10. Kernels of homomorphisms of algebras
    11. 42.11. Models of signatures
    12. 42.12. Morphisms of models of signatures
    13. 42.13. The precategory of algebras of an equational theory
    14. 42.14. Quotient algebras
    15. 42.15. Signatures
    16. 42.16. Terms over signatures
  45. 43. Wild category theory
    ❱
    1. 43.1. Coinductive isomorphisms in noncoherent large ω-precategories
    2. 43.2. Coinductive isomorphisms in noncoherent ω-precategories
    3. 43.3. Colax functors between large noncoherent ω-precategories
    4. 43.4. Colax functors between noncoherent ω-precategories
    5. 43.5. Maps between noncoherent large ω-precategories
    6. 43.6. Maps between noncoherent ω-precategories
    7. 43.7. Noncoherent large ω-precategories
    8. 43.8. Noncoherent ω-precategories

agda-unimath

Mere equivalences of group actions

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

Created on 2022-03-17.
Last modified on 2023-11-24.

module group-theory.mere-equivalences-group-actions where
Imports
open import foundation.propositional-truncations
open import foundation.propositions
open import foundation.universe-levels

open import group-theory.equivalences-group-actions
open import group-theory.group-actions
open import group-theory.groups

Idea

A mere equivalence of group actions is an element of the propositional truncation of the type of equivalences of group actions.

Definition

module _
  {l1 l2 l3 : Level} (G : Group l1)
  (X : action-Group G l2) (Y : action-Group G l3)
  where

  mere-equiv-prop-action-Group : Prop (l1 ⊔ l2 ⊔ l3)
  mere-equiv-prop-action-Group = trunc-Prop (equiv-action-Group G X Y)

  mere-equiv-action-Group : UU (l1 ⊔ l2 ⊔ l3)
  mere-equiv-action-Group = type-Prop mere-equiv-prop-action-Group

Recent changes

  • 2023-11-24. Egbert Rijke. Abelianization (#877).
  • 2023-03-10. Fredrik Bakke. Additions to fix-import (#497).
  • 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).
  • 2023-03-07. Fredrik Bakke. Add blank lines between <details> tags and markdown syntax (#490).
  • 2023-03-07. Jonathan Prieto-Cubides. Show module declarations (#488).