1. Overview
  2. 1. Overview
    ❱
    1. 1.1. Home
    2. 1.2. Community
      ❱
      1. 1.2.1. Maintainers
      2. 1.2.2. Contributors
      3. 1.2.3. Statement of inclusivity
      4. 1.2.4. Projects using Agda-Unimath
      5. 1.2.5. Grant acknowledgements
    3. 1.3. Guides
      ❱
      1. 1.3.1. Installing the library
      2. 1.3.2. Design principles
      3. 1.3.3. Contributing to the library
      4. 1.3.4. Structuring your file
        ❱
        1. 1.3.4.1. File template
      5. 1.3.5. The library coding style
      6. 1.3.6. Guidelines for mixfix operators
      7. 1.3.7. Citing the library
    4. 1.4. Library contents
    5. 1.5. Art
  3. The agda-unimath library
  4. 2. Category theory
    ❱
    1. 2.1. Adjunctions between large categories
    2. 2.2. Adjunctions between large precategories
    3. 2.3. Anafunctors between categories
    4. 2.4. Anafunctors between precategories
    5. 2.5. The augmented simplex category
    6. 2.6. Categories
    7. 2.7. The category of functors and natural transformations between two categories
    8. 2.8. The category of functors and natural transformations from small to large categories
    9. 2.9. The category of maps and natural transformations between two categories
    10. 2.10. The category of maps and natural transformations from small to large categories
    11. 2.11. Commuting squares of morphisms in large precategories
    12. 2.12. Commuting squares of morphisms in precategories
    13. 2.13. Commuting squares of morphisms in set-magmoids
    14. 2.14. Composition operations on binary families of sets
    15. 2.15. Conservative functors between precategories
    16. 2.16. Constant functors
    17. 2.17. Copresheaf categories
    18. 2.18. Coproducts in precategories
    19. 2.19. Cores of categories
    20. 2.20. Cores of precategories
    21. 2.21. Dependent products of categories
    22. 2.22. Dependent products of large categories
    23. 2.23. Dependent products of large precategories
    24. 2.24. Dependent products of precategories
    25. 2.25. Discrete categories
    26. 2.26. Embedding maps between precategories
    27. 2.27. Embeddings between precategories
    28. 2.28. Endomorphisms in categories
    29. 2.29. Endomorphisms in precategories
    30. 2.30. Epimorphism in large precategories
    31. 2.31. Equivalences between categories
    32. 2.32. Equivalences between large precategories
    33. 2.33. Equivalences between precategories
    34. 2.34. Essential fibers of functors between precategories
    35. 2.35. Essentially injective functors between precategories
    36. 2.36. Essentially surjective functors between precategories
    37. 2.37. Exponential objects in precategories
    38. 2.38. Faithful functors between precategories
    39. 2.39. Faithful maps between precategories
    40. 2.40. Full functors between precategories
    41. 2.41. Full large subcategories
    42. 2.42. Full large subprecategories
    43. 2.43. Full maps between precategories
    44. 2.44. Full subcategories
    45. 2.45. Full subprecategories
    46. 2.46. Fully faithful functors between precategories
    47. 2.47. Fully faithful maps between precategories
    48. 2.48. Function categories
    49. 2.49. Function precategories
    50. 2.50. Functors between categories
    51. 2.51. Functors from small to large categories
    52. 2.52. Functors from small to large precategories
    53. 2.53. Functors between large categories
    54. 2.54. Functors between large precategories
    55. 2.55. Functors between nonunital precategories
    56. 2.56. Functors between precategories
    57. 2.57. Functors between set-magmoids
    58. 2.58. Gaunt categories
    59. 2.59. Groupoids
    60. 2.60. Homotopies of natural transformations in large precategories
    61. 2.61. Indiscrete precategories
    62. 2.62. The initial category
    63. 2.63. Initial objects of large categories
    64. 2.64. Initial objects of large precategories
    65. 2.65. Initial objects in a precategory
    66. 2.66. Isomorphism induction in categories
    67. 2.67. Isomorphism induction in precategories
    68. 2.68. Isomorphisms in categories
    69. 2.69. Isomorphisms in large categories
    70. 2.70. Isomorphisms in large precategories
    71. 2.71. Isomorphisms in precategories
    72. 2.72. Isomorphisms in subprecategories
    73. 2.73. Large categories
    74. 2.74. Large function categories
    75. 2.75. Large function precategories
    76. 2.76. Large precategories
    77. 2.77. Large subcategories
    78. 2.78. Large subprecategories
    79. 2.79. Maps between categories
    80. 2.80. Maps from small to large categories
    81. 2.81. Maps from small to large precategories
    82. 2.82. Maps between precategories
    83. 2.83. Maps between set-magmoids
    84. 2.84. Monomorphisms in large precategories
    85. 2.85. Natural isomorphisms between functors between categories
    86. 2.86. Natural isomorphisms between functors between large precategories
    87. 2.87. Natural isomorphisms between functors between precategories
    88. 2.88. Natural isomorphisms between maps between categories
    89. 2.89. Natural isomorphisms between maps between precategories
    90. 2.90. Natural numbers object in a precategory
    91. 2.91. Natural transformations between functors between categories
    92. 2.92. Natural transformations between functors from small to large categories
    93. 2.93. Natural transformations between functors from small to large precategories
    94. 2.94. Natural transformations between functors between large categories
    95. 2.95. Natural transformations between functors between large precategories
    96. 2.96. Natural transformations between functors between precategories
    97. 2.97. Natural transformations between maps between categories
    98. 2.98. Natural transformations between maps from small to large precategories
    99. 2.99. Natural transformations between maps between precategories
    100. 2.100. Nonunital precategories
    101. 2.101. One object precategories
    102. 2.102. Opposite categories
    103. 2.103. Opposite large precategories
    104. 2.104. Opposite precategories
    105. 2.105. Opposite preunivalent categories
    106. 2.106. Precategories
    107. 2.107. Precategory of elements of a presheaf
    108. 2.108. The precategory of functors and natural transformations between two precategories
    109. 2.109. The precategory of functors and natural transformations from small to large precategories
    110. 2.110. The precategory of maps and natural transformations from a small to a large precategory
    111. 2.111. The precategory of maps and natural transformations between two precategories
    112. 2.112. Pregroupoids
    113. 2.113. Presheaf categories
    114. 2.114. Preunivalent categories
    115. 2.115. Products in precategories
    116. 2.116. Products of precategories
    117. 2.117. Pseudomonic functors between precategories
    118. 2.118. Pullbacks in precategories
    119. 2.119. Replete subprecategories
    120. 2.120. Representable functors between categories
    121. 2.121. Representable functors between large precategories
    122. 2.122. Representable functors between precategories
    123. 2.123. The representing arrow category
    124. 2.124. Restrictions of functors to cores of precategories
    125. 2.125. Rigid objects in a category
    126. 2.126. Rigid objects in a precategory
    127. 2.127. Set-magmoids
    128. 2.128. Sieves in categories
    129. 2.129. The simplex category
    130. 2.130. Slice precategories
    131. 2.131. Split essentially surjective functors between precategories
    132. 2.132. Strict categories
    133. 2.133. Structure equivalences between set-magmoids
    134. 2.134. Subcategories
    135. 2.135. Subprecategories
    136. 2.136. Subterminal precategories
    137. 2.137. The terminal category
    138. 2.138. Terminal objects in a precategory
    139. 2.139. Wide subcategories
    140. 2.140. Wide subprecategories
    141. 2.141. The Yoneda lemma for categories
    142. 2.142. The Yoneda lemma for precategories
  5. 3. Commutative algebra
    ❱
    1. 3.1. The binomial theorem in commutative rings
    2. 3.2. The binomial theorem in commutative semirings
    3. 3.3. Boolean rings
    4. 3.4. The category of commutative rings
    5. 3.5. Commutative rings
    6. 3.6. Commutative semirings
    7. 3.7. Dependent products of commutative rings
    8. 3.8. Dependent products of commutative semirings
    9. 3.9. Discrete fields
    10. 3.10. The Eisenstein integers
    11. 3.11. Euclidean domains
    12. 3.12. Full ideals of commutative rings
    13. 3.13. Function commutative rings
    14. 3.14. Function commutative semirings
    15. 3.15. The Gaussian integers
    16. 3.16. The group of multiplicative units of a commutative ring
    17. 3.17. Homomorphisms of commutative rings
    18. 3.18. Homomorphisms of commutative semirings
    19. 3.19. Ideals of commutative rings
    20. 3.20. Ideals of commutative semirings
    21. 3.21. Ideals generated by subsets of commutative rings
    22. 3.22. Integer multiples of elements of commutative rings
    23. 3.23. Integral domains
    24. 3.24. Intersections of ideals of commutative rings
    25. 3.25. Intersections of radical ideals of commutative rings
    26. 3.26. Invertible elements in commutative rings
    27. 3.27. Isomorphisms of commutative rings
    28. 3.28. Joins of ideals of commutative rings
    29. 3.29. Joins of radical ideals of commutative rings
    30. 3.30. Local commutative rings
    31. 3.31. Maximal ideals of commutative rings
    32. 3.32. Multiples of elements in commutative rings
    33. 3.33. Nilradical of a commutative ring
    34. 3.34. The nilradical of a commutative semiring
    35. 3.35. The poset of ideals of a commutative ring
    36. 3.36. The poset of radical ideals of a commutative ring
    37. 3.37. Powers of elements in commutative rings
    38. 3.38. Powers of elements in commutative semirings
    39. 3.39. The precategory of commutative rings
    40. 3.40. The precategory of commutative semirings
    41. 3.41. Prime ideals of commutative rings
    42. 3.42. Products of commutative rings
    43. 3.43. Products of ideals of commutative rings
    44. 3.44. Products of radical ideals of a commutative ring
    45. 3.45. Products of subsets of commutative rings
    46. 3.46. Radical ideals of commutative rings
    47. 3.47. Radical ideals generated by subsets of commutative rings
    48. 3.48. Radicals of ideals of commutative rings
    49. 3.49. Subsets of commutative rings
    50. 3.50. Subsets of commutative semirings
    51. 3.51. Sums in commutative rings
    52. 3.52. Sums in commutative semirings
    53. 3.53. Transporting commutative ring structures along isomorphisms of abelian groups
    54. 3.54. Trivial commutative rings
    55. 3.55. The Zariski locale
    56. 3.56. The Zariski topology on the set of prime ideals of a commutative ring
  6. 4. Elementary number theory
    ❱
    1. 4.1. The absolute value function on the integers
    2. 4.2. The Ackermann function
    3. 4.3. Addition on integer fractions
    4. 4.4. Addition on the integers
    5. 4.5. Addition on the natural numbers
    6. 4.6. Addition on the rational numbers
    7. 4.7. Arithmetic functions
    8. 4.8. The based induction principle of the natural numbers
    9. 4.9. Based strong induction for the natural numbers
    10. 4.10. Bezout's lemma in the integers
    11. 4.11. Bezout's lemma on the natural numbers
    12. 4.12. The binomial coefficients
    13. 4.13. The binomial theorem for the integers
    14. 4.14. The binomial theorem for the natural numbers
    15. 4.15. Bounded sums of arithmetic functions
    16. 4.16. Catalan numbers
    17. 4.17. The cofibonacci sequence
    18. 4.18. The Collatz bijection
    19. 4.19. The Collatz conjecture
    20. 4.20. The commutative semiring of natural numbers
    21. 4.21. The congruence relations on the integers
    22. 4.22. The congruence relations on the natural numbers
    23. 4.23. Decidable dependent function types
    24. 4.24. The decidable total order of natural numbers
    25. 4.25. The decidable total order of a standard finite type
    26. 4.26. Decidable types in elementary number theory
    27. 4.27. The difference between integers
    28. 4.28. Dirichlet convolution
    29. 4.29. The distance between integers
    30. 4.30. The distance between natural numbers
    31. 4.31. Divisibility of integers
    32. 4.32. Divisibility in modular arithmetic
    33. 4.33. Divisibility of natural numbers
    34. 4.34. The divisibility relation on the standard finite types
    35. 4.35. Equality of integers
    36. 4.36. Equality of natural numbers
    37. 4.37. Euclidean division on the natural numbers
    38. 4.38. Euler's totient function
    39. 4.39. Exponentiation of natural numbers
    40. 4.40. Factorials of natural numbers
    41. 4.41. Falling factorials
    42. 4.42. The Fibonacci sequence
    43. 4.43. The natural numbers base k
    44. 4.44. Finitely cyclic maps
    45. 4.45. The fundamental theorem of arithmetic
    46. 4.46. The Goldbach conjecture
    47. 4.47. The greatest common divisor of integers
    48. 4.48. The greatest common divisor of natural numbers
    49. 4.49. The group of integers
    50. 4.50. The half-integers
    51. 4.51. Inequality on integer fractions
    52. 4.52. Inequality on the integers
    53. 4.53. Inequality of natural numbers
    54. 4.54. Inequality on the rational numbers
    55. 4.55. Inequality on the standard finite types
    56. 4.56. The infinitude of primes
    57. 4.57. Initial segments of the natural numbers
    58. 4.58. Integer fractions
    59. 4.59. Integer partitions
    60. 4.60. The integers
    61. 4.61. The Jacobi symbol
    62. 4.62. The Kolakoski sequence
    63. 4.63. The Legendre symbol
    64. 4.64. Lower bounds of type families over the natural numbers
    65. 4.65. Maximum on the natural numbers
    66. 4.66. Maximum on the standard finite types
    67. 4.67. Mersenne primes
    68. 4.68. Minimum on the natural numbers
    69. 4.69. Minimum on the standard finite types
    70. 4.70. Modular arithmetic
    71. 4.71. Modular arithmetic on the standard finite types
    72. 4.72. The monoid of natural numbers with addition
    73. 4.73. The monoid of the natural numbers with maximum
    74. 4.74. Multiplication on integer fractions
    75. 4.75. Multiplication of integers
    76. 4.76. Multiplication of the elements of a list of natural numbers
    77. 4.77. Multiplication of natural numbers
    78. 4.78. Multiplication on the rational numbers
    79. 4.79. The multiplicative monoid of natural numbers
    80. 4.80. Multiplicative units in the integers
    81. 4.81. Multiplicative units in modular arithmetic
    82. 4.82. Multiset coefficients
    83. 4.83. The type of natural numbers
    84. 4.84. Nonzero integers
    85. 4.85. Nonzero natural numbers
    86. 4.86. The ordinal induction principle for the natural numbers
    87. 4.87. Parity of the natural numbers
    88. 4.88. Peano arithmetic
    89. 4.89. Pisano periods
    90. 4.90. The poset of natural numbers ordered by divisibility
    91. 4.91. Powers of integers
    92. 4.92. Powers of two
    93. 4.93. Prime numbers
    94. 4.94. Products of natural numbers
    95. 4.95. Proper divisors of natural numbers
    96. 4.96. Pythagorean triples
    97. 4.97. The rational numbers
    98. 4.98. Reduced integer fractions
    99. 4.99. Relatively prime integers
    100. 4.100. Relatively prime natural numbers
    101. 4.101. Repeating an element in a standard finite type
    102. 4.102. Retracts of the type of natural numbers
    103. 4.103. The ring of integers
    104. 4.104. The sieve of Eratosthenes
    105. 4.105. Square-free natural numbers
    106. 4.106. Squares in the integers
    107. 4.107. Squares in ℤₚ
    108. 4.108. Squares in the natural numbers
    109. 4.109. The standard cyclic groups
    110. 4.110. The standard cyclic rings
    111. 4.111. Stirling numbers of the second kind
    112. 4.112. Strict inequality natural numbers
    113. 4.113. Strictly ordered pairs of natural numbers
    114. 4.114. The strong induction principle for the natural numbers
    115. 4.115. Sums of natural numbers
    116. 4.116. Telephone numbers
    117. 4.117. The triangular numbers
    118. 4.118. The Twin Prime conjecture
    119. 4.119. Type arithmetic with natural numbers
    120. 4.120. Unit elements in the standard finite types
    121. 4.121. Unit similarity on the standard finite types
    122. 4.122. The universal property of the integers
    123. 4.123. The universal property of the natural numbers
    124. 4.124. Upper bounds for type families over the natural numbers
    125. 4.125. The Well-Ordering Principle of the natural numbers
    126. 4.126. The well-ordering principle of the standard finite types
  7. 5. Finite algebra
    ❱
    1. 5.1. Commutative finite rings
    2. 5.2. Dependent products of commutative finit rings
    3. 5.3. Dependent products of finite rings
    4. 5.4. Abelian groups
    5. 5.5. Finite Commutative monoids
    6. 5.6. Finite fields
    7. 5.7. Abstract finite groups
    8. 5.8. Finite monoids
    9. 5.9. Finite rings
    10. 5.10. Finite semigroups
    11. 5.11. Homomorphisms of commutative finite rings
    12. 5.12. Homomorphisms of finite rings
    13. 5.13. Products of commutative finite rings
    14. 5.14. Products of finite rings
    15. 5.15. Semisimple commutative finite rings
  8. 6. Finite group theory
    ❱
    1. 6.1. The abstract quaternion group of order 8
    2. 6.2. Alternating concrete groups
    3. 6.3. Alternating groups
    4. 6.4. Cartier's delooping of the sign homomorphism
    5. 6.5. The concrete quaternion group
    6. 6.6. Deloopings of the sign homomorphism
    7. 6.7. Finite groups
    8. 6.8. Finite monoids
    9. 6.9. Finite semigroups
    10. 6.10. The group of n-element types
    11. 6.11. Groups of order 2
    12. 6.12. Orbits of permutations
    13. 6.13. Permutations
    14. 6.14. Permutations of standard finite types
    15. 6.15. The sign homomorphism
    16. 6.16. Simpson's delooping of the sign homomorphism
    17. 6.17. Subgroups of finite groups
    18. 6.18. Tetrahedra in 3-dimensional space
    19. 6.19. Transpositions
    20. 6.20. Transpositions of standard finite types
  9. 7. Foundation
    ❱
    1. 7.1. 0-Connected types
    2. 7.2. 0-Images of maps
    3. 7.3. 0-Maps
    4. 7.4. 1-Types
    5. 7.5. 2-Types
    6. 7.6. Action on equivalences of functions
    7. 7.7. The action on equivalences of functions out of subuniverses
    8. 7.8. Action on equivalences of type families
    9. 7.9. Action on equivalences in type families over subuniverses
    10. 7.10. The binary action on identifications of binary functions
    11. 7.11. The action on identifications of dependent functions
    12. 7.12. The action on identifications of functions
    13. 7.13. Apartness relations
    14. 7.14. Arithmetic law for coproduct decomposition and Σ-decomposition
    15. 7.15. Arithmetic law for product decomposition and Π-decomposition
    16. 7.16. Automorphisms
    17. 7.17. The axiom of choice
    18. 7.18. Bands
    19. 7.19. Binary embeddings
    20. 7.20. Binary equivalences
    21. 7.21. Binary equivalences on unordered pairs of types
    22. 7.22. Binary functoriality of set quotients
    23. 7.23. Homotopies of binary operations
    24. 7.24. Binary operations on unordered pairs of types
    25. 7.25. Binary reflecting maps of equivalence relations
    26. 7.26. Binary relations
    27. 7.27. Binary transport
    28. 7.28. The booleans
    29. 7.29. The Cantor–Schröder–Bernstein–Escardó theorem
    30. 7.30. Cantor's diagonal argument
    31. 7.31. Cartesian product types
    32. 7.32. Cartesian products of set quotients
    33. 7.33. The category of families of sets
    34. 7.34. The category of sets
    35. 7.35. Choice of representatives for an equivalence relation
    36. 7.36. Codiagonal maps of types
    37. 7.37. Coherently invertible maps
    38. 7.38. Commuting 3-simplices of homotopies
    39. 7.39. Commuting 3-simplices of maps
    40. 7.40. Commuting cubes of maps
    41. 7.41. Commuting hexagons of identifications
    42. 7.42. Commuting pentagons of identifications
    43. 7.43. Commuting squares of homotopies
    44. 7.44. Commuting squares of identifications
    45. 7.45. Commuting squares of maps
    46. 7.46. Commuting triangles of homotopies
    47. 7.47. Commuting triangles of identifications
    48. 7.48. Commuting triangles of maps
    49. 7.49. Complements of type families
    50. 7.50. Complements of subtypes
    51. 7.51. Composite maps in towers
    52. 7.52. Cones over cospans
    53. 7.53. Cones over towers
    54. 7.54. Conjunction of propositions
    55. 7.55. Connected components of types
    56. 7.56. Connected components of universes
    57. 7.57. Connected maps
    58. 7.58. Connected types
    59. 7.59. Constant maps
    60. 7.60. Constant type families
    61. 7.61. Contractible maps
    62. 7.62. Contractible types
    63. 7.63. Coproduct decompositions
    64. 7.64. Coproduct decompositions in a subuniverse
    65. 7.65. Coproduct types
    66. 7.66. Morphisms in the coslice category of types
    67. 7.67. Cospans of types
    68. 7.68. Decidability of dependent function types
    69. 7.69. Decidability of dependent pair types
    70. 7.70. Decidable embeddings
    71. 7.71. Decidable equality
    72. 7.72. Decidable equivalence relations
    73. 7.73. Decidable maps
    74. 7.74. Decidable propositions
    75. 7.75. Decidable relations on types
    76. 7.76. Decidable subtypes
    77. 7.77. Decidable types
    78. 7.78. Dependent binary homotopies
    79. 7.79. The dependent binomial theorem for types (distributivity of dependent function types over coproduct types)
    80. 7.80. Dependent epimorphisms
    81. 7.81. Dependent epimorphisms with respect to truncated types
    82. 7.82. Dependent homotopies
    83. 7.83. Dependent identifications
    84. 7.84. Dependent pair types
    85. 7.85. Dependent sequences
    86. 7.86. Dependent telescopes
    87. 7.87. Dependent towers of types
    88. 7.88. The dependent universal property of equivalences
    89. 7.89. Descent for coproduct types
    90. 7.90. Descent for dependent pair types
    91. 7.91. Descent for the empty type
    92. 7.92. Descent for equivalences
    93. 7.93. Diagonal maps of types
    94. 7.94. Diagonals of maps
    95. 7.95. Diagonals of morphisms of arrows
    96. 7.96. Discrete reflexive relations
    97. 7.97. Discrete relaxed Σ-decompositions
    98. 7.98. Discrete Σ-decompositions
    99. 7.99. Discrete types
    100. 7.100. Disjunction of propositions
    101. 7.101. Double negation
    102. 7.102. The double negation modality
    103. 7.103. Double powersets
    104. 7.104. Dubuc-Penon compact types
    105. 7.105. Effective maps for equivalence relations
    106. 7.106. Embeddings
    107. 7.107. Empty types
    108. 7.108. Endomorphisms
    109. 7.109. Epimorphisms
    110. 7.110. Epimorphisms with respect to maps into sets
    111. 7.111. Epimorphisms with respect to truncated types
    112. 7.112. Equality of cartesian product types
    113. 7.113. Equality of coproduct types
    114. 7.114. Equality on dependent function types
    115. 7.115. Equality of dependent pair types
    116. 7.116. Equality in the fibers of a map
    117. 7.117. Equivalence classes
    118. 7.118. Equivalence extensionality
    119. 7.119. Equivalence induction
    120. 7.120. Equivalence relations
    121. 7.121. Equivalences
    122. 7.122. Equivalences on Maybe
    123. 7.123. Equivalences of towers of types
    124. 7.124. Exclusive disjunction of propositions
    125. 7.125. Existential quantification
    126. 7.126. Exponents of set quotients
    127. 7.127. Faithful maps
    128. 7.128. Families of equivalences
    129. 7.129. Families of maps
    130. 7.130. Fiber inclusions
    131. 7.131. Fibered equivalences
    132. 7.132. Fibered involutions
    133. 7.133. Maps fibered over a map
    134. 7.134. Fibers of maps
    135. 7.135. Full subtypes of types
    136. 7.136. Function extensionality
    137. 7.137. Function types
    138. 7.138. Functional correspondences
    139. 7.139. Functoriality of cartesian product types
    140. 7.140. Functoriality of coproduct types
    141. 7.141. Functoriality of dependent function types
    142. 7.142. Functoriality of dependent pair types
    143. 7.143. Functoriality of fibers of maps
    144. 7.144. Functoriality of function types
    145. 7.145. Functoriality of propositional truncations
    146. 7.146. Functorialty of pullbacks
    147. 7.147. Functoriality of sequential limits
    148. 7.148. Functoriality of set quotients
    149. 7.149. Functoriality of set truncation
    150. 7.150. Functoriality of truncations
    151. 7.151. The fundamental theorem of identity types
    152. 7.152. Global choice
    153. 7.153. Global subuniverses
    154. 7.154. Hilbert's ε-operators
    155. 7.155. Homotopies
    156. 7.156. Homotopy induction
    157. 7.157. Identity systems
    158. 7.158. Identity types of truncated types
    159. 7.159. Identity types
    160. 7.160. The image of a map
    161. 7.161. Images of subtypes
    162. 7.162. Implicit function types
    163. 7.163. Impredicative encodings of the logical operations
    164. 7.164. Impredicative universes
    165. 7.165. The induction principle for propositional truncation
    166. 7.166. Inhabited subtypes
    167. 7.167. Inhabited types
    168. 7.168. Injective maps
    169. 7.169. The interchange law
    170. 7.170. Intersections of subtypes
    171. 7.171. Invertible maps
    172. 7.172. Involutions
    173. 7.173. Isolated elements
    174. 7.174. Isomorphisms of sets
    175. 7.175. Iterated cartesian product types
    176. 7.176. Iterated dependent pair types
    177. 7.177. Iterated dependent product types
    178. 7.178. Iterating automorphisms
    179. 7.179. Iterating functions
    180. 7.180. Iterating involutions
    181. 7.181. Large binary relations
    182. 7.182. Large dependent pair types
    183. 7.183. Large homotopies
    184. 7.184. Large identity types
    185. 7.185. The large locale of propositions
    186. 7.186. The large locale of subtypes
    187. 7.187. The law of excluded middle
    188. 7.188. Lawvere's fixed point theorem
    189. 7.189. The lesser limited principle of omniscience
    190. 7.190. The limited principle of omniscience
    191. 7.191. Locally small types
    192. 7.192. Logical equivalences
    193. 7.193. The maybe modality
    194. 7.194. Mere embeddings
    195. 7.195. Mere equality
    196. 7.196. Mere equivalences
    197. 7.197. Monomorphisms
    198. 7.198. Morphisms of arrows
    199. 7.199. Morphisms of binary relations
    200. 7.200. Morphisms of cospans
    201. 7.201. Morphisms of towers of types
    202. 7.202. Morphisms of twisted arrows
    203. 7.203. Multisubsets
    204. 7.204. Multivariable correspondences
    205. 7.205. Multivariable decidable relations
    206. 7.206. Multivariable functoriality of set quotients
    207. 7.207. Multivariable homotopies
    208. 7.208. Multivariable operations
    209. 7.209. Multivariable relations
    210. 7.210. Multivariable sections
    211. 7.211. Negated equality
    212. 7.212. Negation
    213. 7.213. Non-contractible types
    214. 7.214. Pairs of distinct elements
    215. 7.215. Partial elements
    216. 7.216. Partitions
    217. 7.217. Path algebra
    218. 7.218. Path-split maps
    219. 7.219. Perfect images
    220. 7.220. Π-decompositions of types
    221. 7.221. Π-decompositions of types into types in a subuniverse
    222. 7.222. Pointed torsorial type families
    223. 7.223. Postcomposition
    224. 7.224. Powersets
    225. 7.225. Precomposition of dependent functions
    226. 7.226. Precomposition of functions
    227. 7.227. Precomposition of functions into subuniverses
    228. 7.228. Preidempotent maps
    229. 7.229. Preimages of subtypes
    230. 7.230. The preunivalence axiom
    231. 7.231. The principle of omniscience
    232. 7.232. Product decompositions
    233. 7.233. Product decompositions of types in a subuniverse
    234. 7.234. Products of binary relations
    235. 7.235. Products of equivalence relataions
    236. 7.236. Products of tuples of types
    237. 7.237. Products of unordered pairs of types
    238. 7.238. Products of unordered tuples of types
    239. 7.239. Projective types
    240. 7.240. Proper subsets
    241. 7.241. Propositional extensionality
    242. 7.242. Propositional maps
    243. 7.243. Propositional resizing
    244. 7.244. Propositional truncations
    245. 7.245. Propositions
    246. 7.246. Pullback squares
    247. 7.247. Pullbacks
    248. 7.248. Pullbacks of subtypes
    249. 7.249. Raising universe levels
    250. 7.250. Reflecting maps for equivalence relations
    251. 7.251. Reflexive relations
    252. 7.252. The Regensburg extension of the fundamental theorem of identity types
    253. 7.253. Relaxed Σ-decompositions of types
    254. 7.254. Repetitions of values of maps
    255. 7.255. Repetitions in sequences
    256. 7.256. The type theoretic replacement axiom
    257. 7.257. Retractions
    258. 7.258. Retracts of maps
    259. 7.259. Retracts of types
    260. 7.260. Russell's paradox
    261. 7.261. Sections
    262. 7.262. Separated types
    263. 7.263. Sequences
    264. 7.264. Sequential limits
    265. 7.265. Set presented types
    266. 7.266. Set quotients
    267. 7.267. Set truncations
    268. 7.268. Sets
    269. 7.269. Shifting sequences
    270. 7.270. Σ-closed subuniverses
    271. 7.271. Σ-decompositions of types into types in a subuniverse
    272. 7.272. Σ-decompositions of types
    273. 7.273. Singleton induction
    274. 7.274. Singleton subtypes
    275. 7.275. Morphisms in the slice category of types
    276. 7.276. Small maps
    277. 7.277. Small types
    278. 7.278. Small universes
    279. 7.279. Sorial type families
    280. 7.280. Spans of types
    281. 7.281. Split surjective maps
    282. 7.282. Standard apartness relations
    283. 7.283. Strongly extensional maps
    284. 7.284. Structure
    285. 7.285. The structure identity principle
    286. 7.286. Structured type duality
    287. 7.287. Subsingleton induction
    288. 7.288. Subterminal types
    289. 7.289. Subtype duality
    290. 7.290. The subtype identity principle
    291. 7.291. Subtypes
    292. 7.292. Subuniverses
    293. 7.293. Surjective maps
    294. 7.294. Symmetric binary relations
    295. 7.295. Symmetric cores of binary relations
    296. 7.296. Symmetric difference of subtypes
    297. 7.297. The symmetric identity types
    298. 7.298. Symmetric operations
    299. 7.299. Telescopes
    300. 7.300. Tight apartness relations
    301. 7.301. Torsorial type families
    302. 7.302. Towers of types
    303. 7.303. Transfinite cocomposition of maps
    304. 7.304. Transport along equivalences
    305. 7.305. Transport along higher identifications
    306. 7.306. Transport along homotopies
    307. 7.307. Transport along identifications
    308. 7.308. Trivial relaxed Σ-decompositions
    309. 7.309. Trivial Σ-decompositions
    310. 7.310. Truncated equality
    311. 7.311. Truncated maps
    312. 7.312. Truncated types
    313. 7.313. k-Equivalences
    314. 7.314. Truncation images of maps
    315. 7.315. Truncation levels
    316. 7.316. The truncation modalities
    317. 7.317. Truncations
    318. 7.318. Tuples of types
    319. 7.319. Type arithmetic with the booleans
    320. 7.320. Type arithmetic for cartesian product types
    321. 7.321. Type arithmetic for coproduct types
    322. 7.322. Type arithmetic with dependent function types
    323. 7.323. Type arithmetic for dependent pair types
    324. 7.324. Type arithmetic with the empty type
    325. 7.325. Type arithmetic with the unit type
    326. 7.326. Type duality
    327. 7.327. The type theoretic principle of choice
    328. 7.328. Unions of subtypes
    329. 7.329. Unique existence
    330. 7.330. Uniqueness of the image of a map
    331. 7.331. The uniqueness of set quotients
    332. 7.332. Uniqueness of set truncations
    333. 7.333. Uniqueness of the truncations
    334. 7.334. The unit type
    335. 7.335. Unital binary operations
    336. 7.336. The univalence axiom
    337. 7.337. The univalence axiom implies function extensionality
    338. 7.338. Univalent type families
    339. 7.339. The universal property of booleans
    340. 7.340. The universal propert of cartesian product types
    341. 7.341. The universal property of coproduct types
    342. 7.342. The universal property of dependent pair types
    343. 7.343. The universal property of the empty type
    344. 7.344. The universal property of equivalences
    345. 7.345. The universal property of fiber products
    346. 7.346. The universal property of identity systems
    347. 7.347. The universal property of identity types
    348. 7.348. The universal property of the image of a map
    349. 7.349. The universal property of maybe
    350. 7.350. The universal property of propositional truncations
    351. 7.351. The universal property of propositional truncations with respect to sets
    352. 7.352. The universal property of pullbacks
    353. 7.353. The universal property of sequential limits
    354. 7.354. The universal property of set quotients
    355. 7.355. The universal property of set truncations
    356. 7.356. The universal property of truncations
    357. 7.357. The universal property of the unit type
    358. 7.358. Universe levels
    359. 7.359. Unordered pairs of elements in a type
    360. 7.360. Unordered pairs of types
    361. 7.361. Unordered n-tuples of elements in a type
    362. 7.362. Unordered tuples of types
    363. 7.363. Vectors of set quotients
    364. 7.364. Weak function extensionality
    365. 7.365. The weak limited principle of omniscience
    366. 7.366. Weakly constant maps
    367. 7.367. Whiskering homotopies
  10. 8. Foundation core
    ❱
    1. 8.1. 1-Types
    2. 8.2. Cartesian product types
    3. 8.3. Coherently invertible maps
    4. 8.4. Commuting squares of maps
    5. 8.5. Commuting triangles of maps
    6. 8.6. Constant maps
    7. 8.7. Contractible maps
    8. 8.8. Contractible types
    9. 8.9. Coproduct types
    10. 8.10. Decidable propositions
    11. 8.11. Dependent identifications
    12. 8.12. Diagonal maps of types
    13. 8.13. Discrete types
    14. 8.14. Embeddings
    15. 8.15. Empty types
    16. 8.16. Endomorphisms
    17. 8.17. Equality of dependent pair types
    18. 8.18. Equivalence relations
    19. 8.19. Equivalences
    20. 8.20. Fibers of maps
    21. 8.21. Function types
    22. 8.22. Functoriality of dependent function types
    23. 8.23. Functoriality of dependent pair types
    24. 8.24. Functoriality of function types
    25. 8.25. Homotopies
    26. 8.26. Identity types
    27. 8.27. Injective maps
    28. 8.28. Invertible maps
    29. 8.29. Negation
    30. 8.30. Path-split maps
    31. 8.31. Precomposition of dependent functions
    32. 8.32. Precomposition of functions
    33. 8.33. Propositional maps
    34. 8.34. Propositions
    35. 8.35. Pullbacks
    36. 8.36. Retractions
    37. 8.37. Sections
    38. 8.38. Sets
    39. 8.39. Singleton induction
    40. 8.40. Small types
    41. 8.41. Subtypes
    42. 8.42. Torsorial type families
    43. 8.43. Transport along identifications
    44. 8.44. Truncated maps
    45. 8.45. Truncated types
    46. 8.46. Truncation levels
    47. 8.47. The type theoretic principle of choice
    48. 8.48. The univalence axiom
    49. 8.49. The universal property of pullbacks
    50. 8.50. The universal property of truncations
    51. 8.51. Whiskering homotopies
  11. 9. Graph theory
    ❱
    1. 9.1. Acyclic undirected graphs
    2. 9.2. Circuits in undirected graphs
    3. 9.3. Closed walks in undirected graphs
    4. 9.4. Complete bipartite graphs
    5. 9.5. Complete multipartite graphs
    6. 9.6. Complete undirected graphs
    7. 9.7. Connected graphs
    8. 9.8. Cycles in undirected graphs
    9. 9.9. Directed graph structures on standard finite sets
    10. 9.10. Directed graphs
    11. 9.11. Edge-coloured undirected graphs
    12. 9.12. Embeddings of directed graphs
    13. 9.13. Embeddings of undirected graphs
    14. 9.14. Enriched undirected graphs
    15. 9.15. Equivalences of directed graphs
    16. 9.16. Equivalences of enriched undirected graphs
    17. 9.17. Equivalences of undirected graphs
    18. 9.18. Eulerian circuits in undirected graphs
    19. 9.19. Faithful morphisms of undirected graphs
    20. 9.20. Fibers of directed graphs
    21. 9.21. Finite graphs
    22. 9.22. Geometric realizations of undirected graphs
    23. 9.23. Hypergraphs
    24. 9.24. Matchings
    25. 9.25. Mere equivalences of undirected graphs
    26. 9.26. Morphisms of directed graphs
    27. 9.27. Morphisms of undirected graphs
    28. 9.28. Incidence in undirected graphs
    29. 9.29. Orientations of undirected graphs
    30. 9.30. Paths in undirected graphs
    31. 9.31. Polygons
    32. 9.32. Raising universe levels of directed graphs
    33. 9.33. Reflecting maps of undirected graphs
    34. 9.34. Reflexive graphs
    35. 9.35. Regular undirected graph
    36. 9.36. Simple undirected graphs
    37. 9.37. Stereoisomerism for enriched undirected graphs
    38. 9.38. Totally faithful morphisms of undirected graphs
    39. 9.39. Trails in directed graphs
    40. 9.40. Trails in undirected graphs
    41. 9.41. Undirected graph structures on standard finite sets
    42. 9.42. Undirected graphs
    43. 9.43. Vertex covers
    44. 9.44. Voltage graphs
    45. 9.45. Walks in directed graphs
    46. 9.46. Walks in undirected graphs
  12. 10. Group theory
    ❱
    1. 10.1. Abelian groups
    2. 10.2. Abelianization of groups
    3. 10.3. Pointwise addition of morphisms of abelian groups
    4. 10.4. Automorphism groups
    5. 10.5. Cartesian products of abelian groups
    6. 10.6. Cartesian products of concrete groups
    7. 10.7. Cartesian products of groups
    8. 10.8. Cartesian products of monoids
    9. 10.9. Cartesian products of semigroups
    10. 10.10. The category of abelian groups
    11. 10.11. The category of concrete groups
    12. 10.12. The category of group actions
    13. 10.13. The category of groups
    14. 10.14. The orbit category of a group
    15. 10.15. The category of semigroups
    16. 10.16. Cayley's theorem
    17. 10.17. The center of a group
    18. 10.18. Center of a monoid
    19. 10.19. Center of a semigroup
    20. 10.20. Central elements of groups
    21. 10.21. Central elements of monoids
    22. 10.22. Central elements of semirings
    23. 10.23. Centralizer subgroups
    24. 10.24. Characteristic subgroups
    25. 10.25. Commutative monoids
    26. 10.26. Commutator subgroups
    27. 10.27. Commutators of elements in groups
    28. 10.28. Commuting elements of groups
    29. 10.29. Commuting elements of monoids
    30. 10.30. Commuting elements of semigroups
    31. 10.31. Commuting squares of group homomorphisms
    32. 10.32. Concrete group actions
    33. 10.33. Concrete groups
    34. 10.34. Concrete monoids
    35. 10.35. Congruence relations on abelian groups
    36. 10.36. Congruence relations on commutative monoids
    37. 10.37. Congruence relations on groups
    38. 10.38. Congruence relations on monoids
    39. 10.39. Congruence relations on semigroups
    40. 10.40. Conjugation in groups
    41. 10.41. Conjugation on concrete groups
    42. 10.42. Contravariant pushforwards of concrete group actions
    43. 10.43. Cores of monoids
    44. 10.44. Cyclic groups
    45. 10.45. Decidable subgroups of groups
    46. 10.46. Dependent products of abelian groups
    47. 10.47. Dependent products of commutative monoids
    48. 10.48. Dependent products of groups
    49. 10.49. Dependent products of monoids
    50. 10.50. Dependent products of semigroups
    51. 10.51. The dihedral group construction
    52. 10.52. The dihedral groups
    53. 10.53. The E₈-lattice
    54. 10.54. Elements of finite order
    55. 10.55. Embeddings of abelian groups
    56. 10.56. Embeddings of groups
    57. 10.57. The endomorphism rings of abelian groups
    58. 10.58. Epimorphisms in groups
    59. 10.59. Equivalences of concrete group actions
    60. 10.60. Equivalences of concrete groups
    61. 10.61. Equivalences of group actions
    62. 10.62. Equivalences between semigroups
    63. 10.63. Exponents of abelian groups
    64. 10.64. Exponents of groups
    65. 10.65. Free concrete group actions
    66. 10.66. Free groups with one generator
    67. 10.67. The full subgroup of a group
    68. 10.68. The full subsemigroup of a semigroup
    69. 10.69. Function groups of abelian groups
    70. 10.70. Function commutative monoids
    71. 10.71. Function groups
    72. 10.72. Function monoids
    73. 10.73. Function semigroups
    74. 10.74. Functoriality of quotient groups
    75. 10.75. Furstenberg groups
    76. 10.76. Generating elements of groups
    77. 10.77. Generating sets of groups
    78. 10.78. Group actions
    79. 10.79. Abstract groups
    80. 10.80. Homomorphisms of abelian groups
    81. 10.81. Homomorphisms of commutative monoids
    82. 10.82. Morphisms of concrete group actions
    83. 10.83. Homomorphisms of concrete groups
    84. 10.84. Homomorphisms of generated subgroups
    85. 10.85. Homomorphisms of group actions
    86. 10.86. Homomorphisms of groups
    87. 10.87. Homomorphisms of groups equipped with normal subgroups
    88. 10.88. Homomorphisms of monoids
    89. 10.89. Homomorphisms of semigroups
    90. 10.90. Images of group homomorphisms
    91. 10.91. Images of semigroup homomorphisms
    92. 10.92. Integer multiples of elements in abelian groups
    93. 10.93. Integer powers of elements of groups
    94. 10.94. Intersections of subgroups of abelian groups
    95. 10.95. Intersections of subgroups of groups
    96. 10.96. Inverse semigroups
    97. 10.97. Invertible elements in monoids
    98. 10.98. Isomorphisms of abelian groups
    99. 10.99. Isomorphisms of concrete groups
    100. 10.100. Isomorphisms of group actions
    101. 10.101. Isomorphisms of groups
    102. 10.102. Isomorphisms of monoids
    103. 10.103. Isomorphisms of semigroups
    104. 10.104. Iterated cartesian products of concrete groups
    105. 10.105. Kernels of homomorphisms between abelian groups
    106. 10.106. Kernels of homomorphisms of concrete groups
    107. 10.107. Kernels of homomorphisms of groups
    108. 10.108. Large semigroups
    109. 10.109. Concrete automorphism groups on sets
    110. 10.110. Mere equivalences of concrete group actions
    111. 10.111. Mere equivalences of group actions
    112. 10.112. Monoid actions
    113. 10.113. Monoids
    114. 10.114. Monomorphisms of concrete groups
    115. 10.115. Monomorphisms in the category of groups
    116. 10.116. Multiples of elements in abelian groups
    117. 10.117. Nontrivial groups
    118. 10.118. Normal closures of subgroups
    119. 10.119. Normal cores of subgroups
    120. 10.120. Normal subgroups
    121. 10.121. Normal subgroups of concrete groups
    122. 10.122. Normal submonoids
    123. 10.123. Normal submonoids of commutative monoids
    124. 10.124. Normalizer subgroups
    125. 10.125. Nullifying group homomorphisms
    126. 10.126. The opposite of a group
    127. 10.127. The opposite of a semigroup
    128. 10.128. The orbit-stabilizer theorem for concrete groups
    129. 10.129. Orbits of concrete group actions
    130. 10.130. Orbits of group actions
    131. 10.131. The precategory of orbits of a monoid action
    132. 10.132. The order of an element in a group
    133. 10.133. Perfect cores
    134. 10.134. Perfect groups
    135. 10.135. Perfect subgroups
    136. 10.136. Powers of elements in commutative monoids
    137. 10.137. Powers of elements in groups
    138. 10.138. Powers of elements in monoids
    139. 10.139. The precategory of commutative monoids
    140. 10.140. The precategory of concrete groups
    141. 10.141. The precategory of group actions
    142. 10.142. The precategory of groups
    143. 10.143. The precategory of monoids
    144. 10.144. The precategory of semigroups
    145. 10.145. Principal group actions
    146. 10.146. Principal torsors of concrete groups
    147. 10.147. Products of elements in a monoid
    148. 10.148. Products of tuples of elements in commutative monoids
    149. 10.149. Pullbacks of subgroups
    150. 10.150. Pullbacks of subsemigroups
    151. 10.151. Quotient groups
    152. 10.152. Quotient groups of concrete groups
    153. 10.153. Quotients of abelian groups
    154. 10.154. Rational commutative monoids
    155. 10.155. Representations of monoids in precategories
    156. 10.156. Saturated congruence relations on commutative monoids
    157. 10.157. Saturated congruence relations on monoids
    158. 10.158. Semigroups
    159. 10.159. Sheargroups
    160. 10.160. Shriek of concrete group homomorphisms
    161. 10.161. Stabilizer groups
    162. 10.162. Stabilizers of concrete group actions
    163. 10.163. Subgroups
    164. 10.164. Subgroups of abelian groups
    165. 10.165. Subgroups of concrete groups
    166. 10.166. Subgroups generated by elements of a group
    167. 10.167. Subgroups generated by families of elements
    168. 10.168. Subgroups generated by subsets of groups
    169. 10.169. Submonoids
    170. 10.170. Submonoids of commutative monoids
    171. 10.171. Subsemigroups
    172. 10.172. Subsets of abelian groups
    173. 10.173. Subsets of commutative monoids
    174. 10.174. Subsets of groups
    175. 10.175. Subsets of monoids
    176. 10.176. Subsets of semigroups
    177. 10.177. The substitution functor of concrete group actions
    178. 10.178. The substitution functor of group actions
    179. 10.179. Surjective group homomorphisms
    180. 10.180. Surjective semigroup homomorphisms
    181. 10.181. Symmetric concrete groups
    182. 10.182. Symmetric groups
    183. 10.183. Torsion elements of groups
    184. 10.184. Torsion-free groups
    185. 10.185. Torsors of abstract groups
    186. 10.186. Transitive concrete group actions
    187. 10.187. Transitive group actions
    188. 10.188. Trivial concrete groups
    189. 10.189. Trivial group homomorphisms
    190. 10.190. Trivial groups
    191. 10.191. Trivial subgroups
    192. 10.192. Unordered tuples of elements in commutative monoids
    193. 10.193. Wild representations of monoids
  13. 11. Higher group theory
    ❱
    1. 11.1. Cartesian products of higher groups
    2. 11.2. Conjugation in higher groups
    3. 11.3. Cyclic higher groups
    4. 11.4. Equivalences of higher groups
    5. 11.5. Fixed points of higher group actions
    6. 11.6. Free higher group actions
    7. 11.7. Higher group actions
    8. 11.8. Higher groups
    9. 11.9. Homomorphisms of higher group actions
    10. 11.10. Homomorphisms of higher groups
    11. 11.11. The higher group of integers
    12. 11.12. Iterated cartesian products of higher groups
    13. 11.13. Orbits of higher group actions
    14. 11.14. Subgroups of higher groups
    15. 11.15. Symmetric higher groups
    16. 11.16. Transitive higher group actions
    17. 11.17. Trivial higher groups
  14. 12. Linear algebra
    ❱
    1. 12.1. Constant matrices
    2. 12.2. Diagonal vectors
    3. 12.3. Diagonal matrices on rings
    4. 12.4. Functoriality of matrices
    5. 12.5. Functoriality of the type of vectors
    6. 12.6. Matrices
    7. 12.7. Matrices on rings
    8. 12.8. Multiplication of matrices
    9. 12.9. Scalar multiplication on matrices
    10. 12.10. Scalar multiplication of vectors
    11. 12.11. Scalar multiplication of vectors on rings
    12. 12.12. Transposition of matrices
    13. 12.13. Vectors
    14. 12.14. Vectors on commutative rings
    15. 12.15. Vectors on commutative semirings
    16. 12.16. Vectors on euclidean domains
    17. 12.17. Vectors on rings
    18. 12.18. Vectors on semirings
  15. 13. Lists
    ❱
    1. 13.1. Arrays
    2. 13.2. Concatenation of lists
    3. 13.3. Flattening of lists
    4. 13.4. Functoriality of the list operation
    5. 13.5. Lists
    6. 13.6. Lists of elements in discrete types
    7. 13.7. Permutations of lists
    8. 13.8. Permutations of vectors
    9. 13.9. Predicates on lists
    10. 13.10. Quicksort for lists
    11. 13.11. Reversing lists
    12. 13.12. Sort by insertion for lists
    13. 13.13. Sort by insertion for vectors
    14. 13.14. Sorted lists
    15. 13.15. Sorted vectors
    16. 13.16. Sorting algorithms for lists
    17. 13.17. Sorting algorithms for vectors
    18. 13.18. The universal property of lists with respect to wild monoids
  16. 14. Modal type theory
    ❱
    1. 14.1. Crisp identity types
    2. 14.2. The crisp law of excluded middle
    3. 14.3. Flat dependent function types
    4. 14.4. Flat dependent pair types
    5. 14.5. Flat discrete types
    6. 14.6. The flat modality
    7. 14.7. The flat-sharp adjunction
    8. 14.8. Sharp codiscrete maps
    9. 14.9. Sharp codiscrete types
    10. 14.10. The sharp modality
  17. 15. Online encyclopedia of integer sequences
    ❱
    1. 15.1. Sequences of the online encyclopedia of integer sequences
  18. 16. Order theory
    ❱
    1. 16.1. Accessible elements with respect to relations
    2. 16.2. Bottom elements in posets
    3. 16.3. Bottom elements in preorders
    4. 16.4. Chains in posets
    5. 16.5. Chains in preorders
    6. 16.6. Closure operators on large locales
    7. 16.7. Closure operators on large posets
    8. 16.8. Commuting squares of Galois connections between large posets
    9. 16.9. Commuting squares of order preserving maps of large posets
    10. 16.10. Coverings in locales
    11. 16.11. Decidable posets
    12. 16.12. Decidable preorders
    13. 16.13. Decidable subposets
    14. 16.14. Decidable subpreorders
    15. 16.15. Decidable total orders
    16. 16.16. Decidable total preorders
    17. 16.17. Dependent products of large frames
    18. 16.18. Dependent products of large locales
    19. 16.19. Dependent products of large meet-semilattices
    20. 16.20. Dependent products of large posets
    21. 16.21. Dependent products large preorders
    22. 16.22. Dependent products of large suplattices
    23. 16.23. Directed complete posets
    24. 16.24. Directed families in posets
    25. 16.25. Distributive lattices
    26. 16.26. Finite coverings in locales
    27. 16.27. Finite posets
    28. 16.28. Finite preorders
    29. 16.29. Finite total orders
    30. 16.30. Finitely graded posets
    31. 16.31. Frames
    32. 16.32. Galois connections
    33. 16.33. Galois connections between large posets
    34. 16.34. Greatest lower bounds in large posets
    35. 16.35. Greatest lower bounds in posets
    36. 16.36. Homomorphisms of frames
    37. 16.37. Homomorphisms of large frames
    38. 16.38. Homomorphisms of large locales
    39. 16.39. Homomorphisms of large meet-semilattices
    40. 16.40. Homomorphisms of large suplattices
    41. 16.41. Homomorphisms of meet-semilattices
    42. 16.42. Homomorphisms of meet sup lattices
    43. 16.43. Homomorphisms of suplattices
    44. 16.44. Ideals in preorders
    45. 16.45. Inhabited finite total orders
    46. 16.46. Interval subposets
    47. 16.47. Join-semilattices
    48. 16.48. Large frames
    49. 16.49. Large locales
    50. 16.50. Large meet-semilattices
    51. 16.51. Large meet-subsemilattices
    52. 16.52. Large posets
    53. 16.53. Large preorders
    54. 16.54. Large quotient locales
    55. 16.55. Large subframes
    56. 16.56. Large subposets
    57. 16.57. Large subpreorders
    58. 16.58. Large subsuplattices
    59. 16.59. Large suplattices
    60. 16.60. Lattices
    61. 16.61. Least upper bounds in large posets
    62. 16.62. Least upper bounds in posets
    63. 16.63. Locales
    64. 16.64. Locally finite posets
    65. 16.65. Lower bounds in large posets
    66. 16.66. Lower bounds in posets
    67. 16.67. Lower sets in large posets
    68. 16.68. Lower types in preorders
    69. 16.69. Maximal chains in posets
    70. 16.70. Maximal chains in preorders
    71. 16.71. Meet-semilattices
    72. 16.72. Meet-suplattices
    73. 16.73. Nuclei on large locales
    74. 16.74. Order preserving maps between large posets
    75. 16.75. Order preserving maps between large preorders
    76. 16.76. Order preserving maps on posets
    77. 16.77. Order preserving maps on preorders
    78. 16.78. Posets
    79. 16.79. Powers of large locales
    80. 16.80. The precategory of decidable total orders
    81. 16.81. The precategory of finite posets
    82. 16.82. The precategory of finite total orders
    83. 16.83. The precategory of inhabited finite total orders
    84. 16.84. The precategory of posets
    85. 16.85. The precategory of total orders
    86. 16.86. Preorders
    87. 16.87. Principal lower sets of large posets
    88. 16.88. Principal upper sets of large posets
    89. 16.89. Reflective Galois connections between large posets
    90. 16.90. Similarity of elements in large posets
    91. 16.91. Similarity of elements in large preorders
    92. 16.92. Similarity of order preserving maps between large posets
    93. 16.93. Similarity of order preserving maps between large preorders
    94. 16.94. Subposets
    95. 16.95. Subpreorders
    96. 16.96. Suplattices
    97. 16.97. Top elements in large posets
    98. 16.98. Top elements in posets
    99. 16.99. Top elements in preorders
    100. 16.100. Total orders
    101. 16.101. Total preorders
    102. 16.102. Upper bounds in large posets
    103. 16.103. Upper bounds in posets
    104. 16.104. Upper sets of large posets
    105. 16.105. Well-founded orders
    106. 16.106. Well-founded relations
  19. 17. Organic Chemistry
    ❱
    1. 17.1. Alcohols
    2. 17.2. Alkanes
    3. 17.3. Alkenes
    4. 17.4. Alkynes
    5. 17.5. Ethane
    6. 17.6. Hydrocarbons
    7. 17.7. Methane
    8. 17.8. Saturated carbons
  20. 18. Orthogonal factorization systems
    ❱
    1. 18.1. Cd-structures
    2. 18.2. Cellular maps
    3. 18.3. The closed modalities
    4. 18.4. Extensions of maps
    5. 18.5. Factorization operations
    6. 18.6. Factorization operations into function classes
    7. 18.7. Factorization operations into global function classes
    8. 18.8. Factorizations of maps
    9. 18.9. Factorizations of maps into function classes
    10. 18.10. Factorizations of maps into global function classes
    11. 18.11. Function classes
    12. 18.12. Functoriality of higher modalities
    13. 18.13. Functoriality of the pullback-hom
    14. 18.14. Global function classes
    15. 18.15. Higher modalities
    16. 18.16. The identity modality
    17. 18.17. Lifting operations
    18. 18.18. Lifting squares
    19. 18.19. Lifts of maps
    20. 18.20. Local families
    21. 18.21. Local maps
    22. 18.22. Local types
    23. 18.23. Localizations at maps
    24. 18.24. Localizations at subuniverses
    25. 18.25. Locally small modal-operators
    26. 18.26. Mere lifting properties
    27. 18.27. Modal induction
    28. 18.28. Modal operators
    29. 18.29. Modal subuniverse induction
    30. 18.30. Null types
    31. 18.31. The open modalities
    32. 18.32. Orthogonal factorization systems
    33. 18.33. Orthogonal maps
    34. 18.34. The pullback-hom
    35. 18.35. The raise modalities
    36. 18.36. Reflective modalities
    37. 18.37. Reflective subuniverses
    38. 18.38. Regular cd-structures
    39. 18.39. Separated types
    40. 18.40. Σ-closed modalities
    41. 18.41. Σ-closed reflective modalities
    42. 18.42. Σ-closed reflective subuniverses
    43. 18.43. Stable orthogonal factorization systems
    44. 18.44. Uniquely eliminating modalities
    45. 18.45. Wide function classes
    46. 18.46. Wide global function classes
    47. 18.47. The zero modality
  21. 19. Polytopes
    ❱
    1. 19.1. Abstract polytopes
  22. 20. Primitives
    ❱
    1. 20.1. Characters
    2. 20.2. Floats
    3. 20.3. Machine integers
    4. 20.4. Strings
  23. 21. Real numbers
    ❱
    1. 21.1. Dedekind real numbers
  24. 22. Reflection
    ❱
    1. 22.1. Abstractions
    2. 22.2. Arguments
    3. 22.3. Boolean reflection
    4. 22.4. Definitions
    5. 22.5. Fixity
    6. 22.6. Group solver
    7. 22.7. Literals
    8. 22.8. Metavariables
    9. 22.9. Names
    10. 22.10. Precategory solver
    11. 22.11. Terms
    12. 22.12. The type checking monad
  25. 23. Ring theory
    ❱
    1. 23.1. Additive orders of elements of rings
    2. 23.2. Algebras over rings
    3. 23.3. The binomial theorem for rings
    4. 23.4. The binomial theorem for semirings
    5. 23.5. The category of cyclic rings
    6. 23.6. The category of rings
    7. 23.7. Central elements of rings
    8. 23.8. Central elements of semirings
    9. 23.9. Characteristics of rings
    10. 23.10. Commuting elements of rings
    11. 23.11. Congruence relations on rings
    12. 23.12. Congruence relations on semirings
    13. 23.13. Cyclic rings
    14. 23.14. Dependent products of rings
    15. 23.15. Dependent products of semirings
    16. 23.16. Division rings
    17. 23.17. The free ring with one generator
    18. 23.18. Full ideals of rings
    19. 23.19. Function rings
    20. 23.20. Function semirings
    21. 23.21. Generating elements of rings
    22. 23.22. The group of multiplicative units of a ring
    23. 23.23. Homomorphisms of cyclic rings
    24. 23.24. Homomorphisms of rings
    25. 23.25. Homomorphisms of semirings
    26. 23.26. Ideals generated by subsets of rings
    27. 23.27. Ideals of rings
    28. 23.28. Ideals of semirings
    29. 23.29. Idempotent elements in rings
    30. 23.30. Initial rings
    31. 23.31. Integer multiples of elements of rings
    32. 23.32. Intersections of ideals of rings
    33. 23.33. Intersections of ideals of semirings
    34. 23.34. The invariant basis property of rings
    35. 23.35. Invertible elements in rings
    36. 23.36. Isomorphisms of rings
    37. 23.37. Joins of ideals of rings
    38. 23.38. Joins of left ideals of rings
    39. 23.39. Joins of right ideals of rings
    40. 23.40. Kernels of ring homomorphisms
    41. 23.41. Left ideals generated by subsets of rings
    42. 23.42. Left ideals of rings
    43. 23.43. Local rings
    44. 23.44. Localizations of rings
    45. 23.45. Maximal ideals of rings
    46. 23.46. Modules over rings
    47. 23.47. Multiples of elements in rings
    48. 23.48. Multiplicative orders of elements of rings
    49. 23.49. Nil ideals of rings
    50. 23.50. Nilpotent elements in rings
    51. 23.51. Nilpotent elements in semirings
    52. 23.52. Opposite rings
    53. 23.53. The poset of cyclic rings
    54. 23.54. The poset of ideals of a ring
    55. 23.55. The poset of left ideals of a ring
    56. 23.56. The poset of right ideals of a ring
    57. 23.57. Powers of elements in rings
    58. 23.58. Powers of elements in semirings
    59. 23.59. The precategory of rings
    60. 23.60. The precategory of semirings
    61. 23.61. Products of ideals of rings
    62. 23.62. Products of left ideals of rings
    63. 23.63. Products of right ideals of rings
    64. 23.64. Products of rings
    65. 23.65. Products of subsets of rings
    66. 23.66. Quotient rings
    67. 23.67. Radical ideals of rings
    68. 23.68. Right ideals generated by subsets of rings
    69. 23.69. Right ideals of rings
    70. 23.70. Rings
    71. 23.71. Semirings
    72. 23.72. Subsets of rings
    73. 23.73. Subsets of semirings
    74. 23.74. Sums of elements in rings
    75. 23.75. Sums of elements in semirings
    76. 23.76. Transporting ring structures along isomorphisms of abelian groups
    77. 23.77. Trivial rings
  26. 24. Set theory
    ❱
    1. 24.1. Baire space
    2. 24.2. Cantor space
    3. 24.3. Cardinalities of sets
    4. 24.4. Countable sets
    5. 24.5. Cumulative hierarchy
    6. 24.6. Infinite sets
    7. 24.7. Uncountable sets
  27. 25. Species
    ❱
    1. 25.1. Cartesian exponents of species
    2. 25.2. Cartesian products of species of types
    3. 25.3. Cauchy composition of species of types
    4. 25.4. Cauchy composition of species of types in a subuniverse
    5. 25.5. Cauchy exponentials of species of types
    6. 25.6. Cauchy exponentials of species of types in a subuniverse
    7. 25.7. Cauchy products of species of types
    8. 25.8. Cauchy products of species of types in a subuniverse
    9. 25.9. Cauchy series of species of types
    10. 25.10. Cauchy series of species of types in a subuniverse
    11. 25.11. Composition of Cauchy series of species of types
    12. 25.12. Composition of Cauchy series of species of types in subuniverses
    13. 25.13. Coproducts of species of types
    14. 25.14. Coproducts of species of types in subuniverses
    15. 25.15. Cycle index series of species
    16. 25.16. Derivatives of species
    17. 25.17. Dirichlet exponentials of a species of types
    18. 25.18. Dirichlet exponentials of species of types in a subuniverse
    19. 25.19. Dirichlet products of species of types
    20. 25.20. Dirichlet products of species of types in subuniverses
    21. 25.21. Dirichlet series of species of finite inhabited types
    22. 25.22. Dirichlet series of species of types
    23. 25.23. Dirichlet series of species of types in subuniverses
    24. 25.24. Equivalences of species of types
    25. 25.25. Equivalences of species of types in subuniverses
    26. 25.26. Exponential of Cauchy series of species of types
    27. 25.27. Exponential of Cauchy series of species of types in subuniverses
    28. 25.28. Hasse-Weil species
    29. 25.29. Morphisms of finite species
    30. 25.30. Morphisms of species of types
    31. 25.31. Pointing of species of types
    32. 25.32. The precategory of finite species
    33. 25.33. Products of Cauchy series of species of types
    34. 25.34. Products of Cauchy series of species of types in subuniverses
    35. 25.35. Products of Dirichlet series of species of finite inhabited types
    36. 25.36. Products of Dirichlet series of species of types
    37. 25.37. Products of Dirichlet series of species of types in subuniverses
    38. 25.38. Small Composition of species of finite inhabited types
    39. 25.39. Small Cauchy composition of species types in subuniverses
    40. 25.40. Species of finite inhabited types
    41. 25.41. Species of finite types
    42. 25.42. Species of inhabited types
    43. 25.43. Species of types
    44. 25.44. Species of types in subuniverses
    45. 25.45. The unit of Cauchy composition of types
    46. 25.46. The unit of Cauchy composition of species of types in subuniverses
    47. 25.47. Unlabeled structures of finite species
  28. 26. Structured types
    ❱
    1. 26.1. Cartesian products of types equipped with endomorphisms
    2. 26.2. Central H-spaces
    3. 26.3. Commuting squares of pointed maps
    4. 26.4. Conjugation of pointed types
    5. 26.5. Constant maps of pointed types
    6. 26.6. Contractible pointed types
    7. 26.7. Cyclic types
    8. 26.8. Dependent products of H-spaces
    9. 26.9. Dependent products of pointed types
    10. 26.10. Dependent products of wild monoids
    11. 26.11. Dependent types equipped with automorphisms
    12. 26.12. Equivalences of types equipped with automorphisms
    13. 26.13. Equivalences of types equipped with endomorphisms
    14. 26.14. Faithful pointed maps
    15. 26.15. Fibers of pointed maps
    16. 26.16. Finite multiplication in magmas
    17. 26.17. Function H-spaces
    18. 26.18. Function magmas
    19. 26.19. Function wild monoids
    20. 26.20. H-spaces
    21. 26.21. The initial pointed type equipped with an automorphism
    22. 26.22. The involutive type of H-space structures on a pointed type
    23. 26.23. Involutive types
    24. 26.24. Iterated cartesian products of types equipped with endomorphisms
    25. 26.25. Iterated cartesian products of pointed types
    26. 26.26. Magmas
    27. 26.27. Mere equivalences of types equipped with endomorphisms
    28. 26.28. Morphisms of H-spaces
    29. 26.29. Morphisms of magmas
    30. 26.30. Morphisms of types equipped with automorphisms
    31. 26.31. Morphisms of types equipped with endomorphisms
    32. 26.32. Morphisms of wild monoids
    33. 26.33. Non-coherent H-spaces
    34. 26.34. Pointed cartesian product types
    35. 26.35. Pointed dependent functions
    36. 26.36. Pointed dependent pair types
    37. 26.37. Pointed equivalences
    38. 26.38. Pointed families of types
    39. 26.39. Pointed homotopies
    40. 26.40. Pointed maps
    41. 26.41. Pointed sections of pointed maps
    42. 26.42. Pointed types
    43. 26.43. Pointed types equipped with automorphisms
    44. 26.44. The pointed unit type
    45. 26.45. Sets equipped with automorphisms
    46. 26.46. Symmetric elements of involutive types
    47. 26.47. Symmetric H-spaces
    48. 26.48. Types equipped with automorphisms
    49. 26.49. Types equipped with endomorphisms
    50. 26.50. Unpointed maps between pointed types
    51. 26.51. Wild groups
    52. 26.52. Wild loops
    53. 26.53. Wild monoids
    54. 26.54. Wild quasigroups
    55. 26.55. Wild semigroups
  29. 27. Synthetic homotopy theory
    ❱
    1. 27.1. 0-acyclic maps
    2. 27.2. 0-acyclic types
    3. 27.3. 1-acyclic types
    4. 27.4. Formalization of the Symmetry book - 26 descent
    5. 27.5. Formalization of the Symmetry book - 26 id pushout
    6. 27.6. Acyclic maps
    7. 27.7. Acyclic types
    8. 27.8. The category of connected set bundles over the circle
    9. 27.9. Cavallo's trick
    10. 27.10. The circle
    11. 27.11. Cocartesian morphisms of arrows
    12. 27.12. Cocones under sequential diagrams
    13. 27.13. Cocones under spans
    14. 27.14. Cocones under spans of pointed types
    15. 27.15. Codiagonals of maps
    16. 27.16. Coequalizers
    17. 27.17. Cofibers
    18. 27.18. Coforks
    19. 27.19. Conjugation of loops
    20. 27.20. Connected set bundles over the circle
    21. 27.21. Dependent cocones under sequential diagrams
    22. 27.22. Dependent cocones under spans
    23. 27.23. Dependent coforks
    24. 27.24. Dependent descent for the circle
    25. 27.25. The dependent pullback property of pushouts
    26. 27.26. Dependent pushout-products
    27. 27.27. Dependent sequential diagrams
    28. 27.28. Dependent suspension structures
    29. 27.29. The dependent universal property of coequalizers
    30. 27.30. The dependent universal property of pushouts
    31. 27.31. The dependent universal property of sequential colimits
    32. 27.32. Dependent universal property of suspensions
    33. 27.33. The descent property of the circle
    34. 27.34. Descent data for constant type families over the circle
    35. 27.35. Descent data for families of dependent pair types over the circle
    36. 27.36. Descent data for families of equivalence types over the circle
    37. 27.37. Descent data for families of function types over the circle
    38. 27.38. Subtypes of descent data for the circle
    39. 27.39. Double loop spaces
    40. 27.40. The Eckmann-Hilton Argument
    41. 27.41. Equivalences of sequential diagrams
    42. 27.42. The flattening lemma for coequalizers
    43. 27.43. The flattening lemma for pushouts
    44. 27.44. Free loops
    45. 27.45. Functoriality of the loop space operation
    46. 27.46. Functoriality of suspensions
    47. 27.47. Groups of loops in 1-types
    48. 27.48. Hatcher's acyclic type
    49. 27.49. The induction principle of pushouts
    50. 27.50. The infinite complex projective space
    51. 27.51. Infinite cyclic types
    52. 27.52. The interval
    53. 27.53. Iterated loop spaces
    54. 27.54. Iterated suspensions of pointed types
    55. 27.55. Join powers of types
    56. 27.56. Joins of maps
    57. 27.57. Joins of types
    58. 27.58. Loop spaces
    59. 27.59. Maps of prespectra
    60. 27.60. Mere spheres
    61. 27.61. Morphisms of descent data of the circle
    62. 27.62. Morphisms of sequential diagrams
    63. 27.63. The multiplication operation on the circle
    64. 27.64. The plus-principle
    65. 27.65. Powers of loops
    66. 27.66. Premanifolds
    67. 27.67. Prespectra
    68. 27.68. The pullback property of pushouts
    69. 27.69. Pushout-products
    70. 27.70. Pushouts
    71. 27.71. Pushouts of pointed types
    72. 27.72. Sections of families over the circle
    73. 27.73. Sequential diagrams
    74. 27.74. Sequentially compact types
    75. 27.75. Smash products of pointed types
    76. 27.76. Spectra
    77. 27.77. The sphere prespectrum
    78. 27.78. Spheres
    79. 27.79. Suspension prespectra
    80. 27.80. Suspension Structures
    81. 27.81. Suspensions of pointed types
    82. 27.82. Suspensions of types
    83. 27.83. Tangent spheres
    84. 27.84. Triple loop spaces
    85. 27.85. k-acyclic maps
    86. 27.86. k-acyclic types
    87. 27.87. The universal cover of the circle
    88. 27.88. The universal property of the circle
    89. 27.89. The universal property of coequalizers
    90. 27.90. The universal property of pushouts
    91. 27.91. The universal property of sequential colimits
    92. 27.92. Universal property of suspensions
    93. 27.93. Universal Property of suspensions of pointed types
    94. 27.94. Wedges of pointed types
  30. 28. Trees
    ❱
    1. 28.1. Algebras for polynomial endofunctors
    2. 28.2. Bases of directed trees
    3. 28.3. Bases of enriched directed trees
    4. 28.4. Bounded multisets
    5. 28.5. The coalgebra of directed trees
    6. 28.6. The coalgebra of enriched directed trees
    7. 28.7. Coalgebras of polynomial endofunctors
    8. 28.8. The combinator of directed trees
    9. 28.9. Combinators of enriched directed trees
    10. 28.10. Directed trees
    11. 28.11. The elementhood relation on coalgebras of polynomial endofunctors
    12. 28.12. The elementhood relation on W-types
    13. 28.13. Empty multisets
    14. 28.14. Enriched directed trees
    15. 28.15. Equivalences of directed trees
    16. 28.16. Equivalences of enriched directed trees
    17. 28.17. Extensional W-types
    18. 28.18. Fibers of directed trees
    19. 28.19. Fibers of enriched directed trees
    20. 28.20. Functoriality of the combinator of directed trees
    21. 28.21. Functoriality of the fiber operation on directed trees
    22. 28.22. Functoriality of W-types
    23. 28.23. Indexed W-types
    24. 28.24. Induction principles on W-types
    25. 28.25. Inequality on W-types
    26. 28.26. Lower types of elements in W-types
    27. 28.27. Morphisms of algebras of polynomial endofunctors
    28. 28.28. Morphisms of coalgebras of polynomial endofunctors
    29. 28.29. Morphisms of directed trees
    30. 28.30. Morphisms of enriched directed trees
    31. 28.31. Multiset-indexed dependent products of types
    32. 28.32. Multisets
    33. 28.33. Planar binary trees
    34. 28.34. Polynomial endofunctors
    35. 28.35. Raising universe levels of directed trees
    36. 28.36. Ranks of elements in W-types
    37. 28.37. Rooted morphisms of directed trees
    38. 28.38. Rooted morphisms of enriched directed trees
    39. 28.39. Rooted quasitrees
    40. 28.40. Rooted undirected trees
    41. 28.41. Small multisets
    42. 28.42. Submultisets
    43. 28.43. Transitive multisets
    44. 28.44. The underlying trees of elements of coalgebras of polynomial endofunctors
    45. 28.45. The underlying trees of elements of W-types
    46. 28.46. Undirected rees
    47. 28.47. The universal multiset
    48. 28.48. The universal tree
    49. 28.49. The W-type of natural numbers
    50. 28.50. The W-type of the type of propositions
    51. 28.51. W-types
  31. 29. Type theories
    ❱
    1. 29.1. Comprehension of fibered type theories
    2. 29.2. Dependent type theories
    3. 29.3. Fibered dependent type theories
    4. 29.4. Π-types in precategories with attributes
    5. 29.5. Π-types in precategories with families
    6. 29.6. Precategories with attributes
    7. 29.7. Precategories with families
    8. 29.8. Sections of dependent type theories
    9. 29.9. Simple type theories
    10. 29.10. Unityped type theories
  32. 30. Univalent combinatorics
    ❱
    1. 30.1. 2-element decidable subtypes
    2. 30.2. 2-element subtypes
    3. 30.3. 2-element types
    4. 30.4. The binomial types
    5. 30.5. Bracelets
    6. 30.6. Cartesian products of finite types
    7. 30.7. The classical definition of the standard finite types
    8. 30.8. Complements of isolated elements of finite types
    9. 30.9. Coproducts of finite types
    10. 30.10. Counting in type theory
    11. 30.11. Counting the elements of decidable subtypes
    12. 30.12. Counting the elements of dependent pair types
    13. 30.13. Counting the elements of the fiber of a map
    14. 30.14. Counting the elements in Maybe
    15. 30.15. Cubes
    16. 30.16. Cycle partitions of finite types
    17. 30.17. Cycle prime decompositions of natural numbers
    18. 30.18. Cyclic finite types
    19. 30.19. Decidable dependent function types
    20. 30.20. Decidability of dependent pair types
    21. 30.21. Decidable equivalence relations on finite types
    22. 30.22. Decidable propositions
    23. 30.23. Decidable subtypes of finite types
    24. 30.24. Dedekind finite sets
    25. 30.25. Counting the elements of dependent function types
    26. 30.26. Dependent pair types of finite types
    27. 30.27. Finite discrete Σ-decompositions
    28. 30.28. Distributivity of set truncation over finite products
    29. 30.29. Double counting
    30. 30.30. Injective maps
    31. 30.31. Embeddings between standard finite types
    32. 30.32. Equality in finite types
    33. 30.33. Equality in the standard finite types
    34. 30.34. Equivalences between finite types
    35. 30.35. Equivalences of cubes
    36. 30.36. Equivalences between standard finite types
    37. 30.37. Ferrers diagrams (unlabeled partitions)
    38. 30.38. Fibers of maps between finite types
    39. 30.39. Finite choice
    40. 30.40. Finiteness of the type of connected components
    41. 30.41. Finite presentations of types
    42. 30.42. Finite types
    43. 30.43. Finitely presented types
    44. 30.44. Finite function types
    45. 30.45. The image of a map
    46. 30.46. Inequality on types equipped with a counting
    47. 30.47. Inhabited finite types
    48. 30.48. Injective maps between finite types
    49. 30.49. An involution on the standard finite types
    50. 30.50. Isotopies of Latin squares
    51. 30.51. Kuratowsky finite sets
    52. 30.52. Latin squares
    53. 30.53. The groupoid of main classes of Latin hypercubes
    54. 30.54. The groupoid of main classes of Latin squares
    55. 30.55. The maybe modality on finite types
    56. 30.56. Necklaces
    57. 30.57. Orientations of the complete undirected graph
    58. 30.58. Orientations of cubes
    59. 30.59. Partitions of finite types
    60. 30.60. Petri-nets
    61. 30.61. π-finite types
    62. 30.62. The pigeonhole principle
    63. 30.63. Finitely π-presented types
    64. 30.64. Quotients of finite types
    65. 30.65. Ramsey theory
    66. 30.66. Repetitions of values
    67. 30.67. Repetitions of values in sequences
    68. 30.68. Retracts of finite types
    69. 30.69. Sequences of elements in finite types
    70. 30.70. Set quotients of index 2
    71. 30.71. Finite Σ-decompositions of finite types
    72. 30.72. Skipping elements in standard finite types
    73. 30.73. Small types
    74. 30.74. Standard finite pruned trees
    75. 30.75. Standard finite trees
    76. 30.76. The standard finite types
    77. 30.77. Steiner systems
    78. 30.78. Steiner triple systems
    79. 30.79. Combinatorial identities of sums of natural numbers
    80. 30.80. Surjective maps between finite types
    81. 30.81. Symmetric difference of finite subtypes
    82. 30.82. Finite trivial Σ-decompositions
    83. 30.83. Type duality of finite types
    84. 30.84. Unions of finite subtypes
    85. 30.85. The universal property of the standard finite types
    86. 30.86. Unlabeled partitions
    87. 30.87. Unlabeled rooted trees
    88. 30.88. Unlabeled trees
  33. 31. Universal Algebra
    ❱
    1. 31.1. Abstract equations over signatures
    2. 31.2. Algebraic theories
    3. 31.3. Algebraic theory of groups
    4. 31.4. Algebras
    5. 31.5. Congruences
    6. 31.6. Homomorphisms of algebras
    7. 31.7. Kernels of homomorphisms of algebras
    8. 31.8. Models of signatures
    9. 31.9. Quotient algebras
    10. 31.10. Signatures
    11. 31.11. Terms over signatures

agda-unimath

Commuting squares of morphisms in large precategories

Content created by Fredrik Bakke.

Created on 2023-09-27.
Last modified on 2023-09-27.

module category-theory.commuting-squares-of-morphisms-in-large-precategories where
Imports
open import category-theory.large-precategories

open import foundation.identity-types
open import foundation.universe-levels

Idea

A square of morphisms

  x ------> y
  |         |
  |         |
  V         V
  z ------> w

in a large precategory C is said to commute if there is an identification between both composites.

Definitions

coherence-square-hom-Large-Precategory :
  {l1 l2 l3 l4 : Level}
  {α : Level → Level}
  {β : Level → Level → Level}
  (C : Large-Precategory α β)
  {x : obj-Large-Precategory C l1}
  {y : obj-Large-Precategory C l2}
  {z : obj-Large-Precategory C l3}
  {w : obj-Large-Precategory C l4}
  (top : hom-Large-Precategory C x y)
  (left : hom-Large-Precategory C x z)
  (right : hom-Large-Precategory C y w)
  (bottom : hom-Large-Precategory C z w) →
  UU (β l1 l4)
coherence-square-hom-Large-Precategory C top left right bottom =
  ( comp-hom-Large-Precategory C bottom left) =
  ( comp-hom-Large-Precategory C right top)

Recent changes

  • 2023-09-27. Fredrik Bakke. Presheaf categories (#801).