Overview
1.
Home
2.
Community
❱
2.1.
Maintainers
2.2.
Contributors
2.3.
Statement of inclusivity
2.4.
Projects using agda-unimath
2.5.
Grant acknowledgments
3.
Guides
❱
3.1.
Installing the library
3.2.
Design principles
3.3.
Contributing to the library
3.4.
Structuring your file
❱
3.4.1.
File template
3.5.
The library coding style
3.6.
Guidelines for mixfix operators
3.7.
Citing sources
3.8.
Citing the library
4.
Library explorer
5.
Art
6.
Full list of contents
7.
Formalization of results from the literature
❱
7.1.
Wiedijk's 100 Theorems
7.2.
Idempotents in Intensional Type Theory
7.3.
Introduction to homotopy type theory
7.4.
Sequences of the online encyclopedia of integer sequences
7.5.
Sequential Colimits in Homotopy Type Theory
7.6.
Wikipedia's list of theorems
The agda-unimath library
8.
Analysis
❱
8.1.
Absolute convergence of series in the real numbers
8.2.
Addition of differentiable functions on proper closed intervals in the real numbers
8.3.
The alternation of sequences in metric abelian groups
8.4.
Comparison test for series in the real numbers
8.5.
Complete metric abelian groups
8.6.
The composition of differentiable real functions on proper closed intervals in the real numbers
8.7.
The constructive intermediate value theorem
8.8.
Convergent series in complete metric abelian groups
8.9.
Convergent series in metric abelian groups
8.10.
Convergent series in the real numbers
8.11.
Differentiability of constant functions on proper closed intervals in the real numbers
8.12.
Differentiability of the identity map on proper closed intervals in the real numbers
8.13.
The differentiability of the reciprocal function on proper closed intervals in the real numbers
8.14.
Differentiable real functions on proper closed intervals in the real numbers
8.15.
The intermediate value theorem
8.16.
Limits of sequences in metric abelian groups
8.17.
Metric abelian groups
8.18.
Metric abelian groups of normed real vector spaces
8.19.
Metric abelian groups of uniformly continuous maps into metric abelian groups
8.20.
Monotone convergence theorem for increasing sequences of real numbers
8.21.
Nonnegative series in the real numbers
8.22.
The ratio test for series in the real numbers
8.23.
Scalar multiplication of differentiable functions on proper closed intervals in the real numbers
8.24.
Sequences in metric abelian groups
8.25.
Series in complete metric abelian groups
8.26.
Series in metric abelian groups
8.27.
Series in the real numbers
9.
Category theory
❱
9.1.
Adjunctions between large categories
9.2.
Adjunctions between large precategories
9.3.
Adjunctions between precategories
9.4.
Algebras over monads on precategories
9.5.
Anafunctors between categories
9.6.
Anafunctors between precategories
9.7.
The augmented simplex category
9.8.
Categories
9.9.
The category of functors and natural transformations between two categories
9.10.
The category of functors and natural transformations from small to large categories
9.11.
The category of maps and natural transformations between two categories
9.12.
The category of maps and natural transformations from small to large categories
9.13.
The category of simplicial sets
9.14.
Coalgebras over comonads on precategories
9.15.
Cocones in precategories
9.16.
Codensity monads on precategories
9.17.
Colimits in precategories
9.18.
Commuting squares of morphisms in large precategories
9.19.
Commuting squares of morphisms in precategories
9.20.
Commuting squares of morphisms in set-magmoids
9.21.
Commuting triangles of morphisms in precategories
9.22.
Commuting triangles of morphisms in set-magmoids
9.23.
Comonads on precategories
9.24.
Complete precategories
9.25.
Composition operations on binary families of sets
9.26.
Cones in precategories
9.27.
Conservative functors between precategories
9.28.
Constant functors
9.29.
Copointed endofunctors on precategories
9.30.
Copresheaf categories
9.31.
Coproducts in precategories
9.32.
Cores of categories
9.33.
Cores of precategories
9.34.
Coslice precategories
9.35.
Density comonads on precategories
9.36.
Dependent composition operations over precategories
9.37.
Dependent products of categories
9.38.
Dependent products of large categories
9.39.
Dependent products of large precategories
9.40.
Dependent products of precategories
9.41.
Discrete categories
9.42.
Displayed precategories
9.43.
Embedding maps between precategories
9.44.
Embeddings between precategories
9.45.
Endomorphisms in categories
9.46.
Endomorphisms in precategories
9.47.
Epimorphism in large precategories
9.48.
Equivalences between categories
9.49.
Equivalences between large precategories
9.50.
Equivalences between precategories
9.51.
Essential fibers of functors between precategories
9.52.
Essentially injective functors between precategories
9.53.
Essentially surjective functors between precategories
9.54.
Exponential objects in precategories
9.55.
Extensions of functors between precategories
9.56.
Faithful functors between precategories
9.57.
Faithful maps between precategories
9.58.
Full functors between precategories
9.59.
Full large subcategories
9.60.
Full large subprecategories
9.61.
Full maps between precategories
9.62.
Full subcategories
9.63.
Full subprecategories
9.64.
Fully faithful functors between precategories
9.65.
Fully faithful maps between precategories
9.66.
Function categories
9.67.
Function precategories
9.68.
Functors between categories
9.69.
Functors from small to large categories
9.70.
Functors from small to large precategories
9.71.
Functors between large categories
9.72.
Functors between large precategories
9.73.
Functors between nonunital precategories
9.74.
Functors between precategories
9.75.
Functors between set-magmoids
9.76.
Gaunt categories
9.77.
Groupoids
9.78.
Homotopies of natural transformations in large precategories
9.79.
Indiscrete precategories
9.80.
The initial category
9.81.
Initial objects of large categories
9.82.
Initial objects of large precategories
9.83.
Initial objects in a precategory
9.84.
Isomorphism induction in categories
9.85.
Isomorphism induction in precategories
9.86.
Isomorphisms in categories
9.87.
Isomorphisms in large categories
9.88.
Isomorphisms in large precategories
9.89.
Isomorphisms in precategories
9.90.
Isomorphisms in subprecategories
9.91.
Large categories
9.92.
Large function categories
9.93.
Large function precategories
9.94.
Large precategories
9.95.
Large subcategories
9.96.
Large subprecategories
9.97.
Left extensions in precategories
9.98.
Left Kan extensions in precategories
9.99.
Limits in precategories
9.100.
Maps between categories
9.101.
Maps from small to large categories
9.102.
Maps from small to large precategories
9.103.
Maps between precategories
9.104.
Maps between set-magmoids
9.105.
Monads on categories
9.106.
Monads on precategories
9.107.
Monomorphisms in large precategories
9.108.
Morphisms of algebras over monads on precategories
9.109.
Morphisms of coalgebras over comonads on precategories
9.110.
Natural isomorphisms between functors between categories
9.111.
Natural isomorphisms between functors between large precategories
9.112.
Natural isomorphisms between functors between precategories
9.113.
Natural isomorphisms between maps between categories
9.114.
Natural isomorphisms between maps between precategories
9.115.
Natural numbers object in a precategory
9.116.
Natural transformations between functors between categories
9.117.
Natural transformations between functors from small to large categories
9.118.
Natural transformations between functors from small to large precategories
9.119.
Natural transformations between functors between large categories
9.120.
Natural transformations between functors between large precategories
9.121.
Natural transformations between functors between precategories
9.122.
Natural transformations between maps between categories
9.123.
Natural transformations between maps from small to large precategories
9.124.
Natural transformations between maps between precategories
9.125.
Nonunital precategories
9.126.
One object precategories
9.127.
Opposite categories
9.128.
Opposite large precategories
9.129.
Opposite precategories
9.130.
Opposite preunivalent categories
9.131.
Opposite strongly preunivalent categories
9.132.
Pointed endofunctors on categories
9.133.
Pointed endofunctors on precategories
9.134.
Precategories
9.135.
The precategory of algebras over a monad
9.136.
The precategory of coalgebras over a comonad
9.137.
Precategory of elements of a presheaf
9.138.
The precategory of free algebras of a monad
9.139.
The precategory of functors and natural transformations between two precategories
9.140.
The precategory of functors and natural transformations from small to large precategories
9.141.
The precategory of maps and natural transformations from a small to a large precategory
9.142.
The precategory of maps and natural transformations between two precategories
9.143.
Pregroupoids
9.144.
Presheaf categories
9.145.
Preunivalent categories
9.146.
Products in precategories
9.147.
Products of precategories
9.148.
Pseudomonic functors between precategories
9.149.
Pullbacks in precategories
9.150.
Replete subprecategories
9.151.
Representable functors between categories
9.152.
Representable functors between large precategories
9.153.
Representable functors between precategories
9.154.
The representing arrow category
9.155.
Restrictions of functors to cores of precategories
9.156.
Right extensions in precategories
9.157.
Right Kan extensions in precategories
9.158.
Rigid objects in a category
9.159.
Rigid objects in a precategory
9.160.
Set-magmoids
9.161.
Sieves in categories
9.162.
The simplex category
9.163.
Slice precategories
9.164.
Split essentially surjective functors between precategories
9.165.
Strict categories
9.166.
Strongly preunivalent categories
9.167.
Structure equivalences between set-magmoids
9.168.
Subcategories
9.169.
Subprecategories
9.170.
Subterminal precategories
9.171.
The terminal category
9.172.
Terminal objects in a precategory
9.173.
Wide subcategories
9.174.
Wide subprecategories
9.175.
The Yoneda lemma for categories
9.176.
The Yoneda lemma for precategories
10.
Commutative algebra
❱
10.1.
Algebras over commutative rings
10.2.
Associative algebras over commutative rings
10.3.
The binomial theorem in commutative rings
10.4.
The binomial theorem in commutative semirings
10.5.
Boolean rings
10.6.
The category of commutative rings
10.7.
The center of a ring
10.8.
Commutative rings
10.9.
Commutative semirings
10.10.
Convolution of sequences in commutative rings
10.11.
Convolution of sequences in commutative semirings
10.12.
Dependent products of algebras over commutative rings
10.13.
Dependent products of associative algebras over commutative rings
10.14.
Dependent products of commutative rings
10.15.
Dependent products of commutative semirings
10.16.
Dependent products of unital algebras over commutative rings
10.17.
Dependent products of unital associative algebras over commutative rings
10.18.
Discrete fields
10.19.
Euclidean domains
10.20.
Formal power series in commutative rings
10.21.
Formal power series in commutative semirings
10.22.
Full ideals of commutative rings
10.23.
Function algebras on commutative rings
10.24.
Function commutative rings
10.25.
Function commutative semirings
10.26.
Geometric sequences in commutative rings
10.27.
Geometric sequences in commutative semirings
10.28.
The group of multiplicative units of a commutative ring
10.29.
Heyting fields
10.30.
Homomorphisms of commutative rings
10.31.
Homomorphisms of commutative semirings
10.32.
Homomorphisms of Heyting fields
10.33.
Ideals of commutative rings
10.34.
Ideals of commutative semirings
10.35.
Ideals generated by subsets of commutative rings
10.36.
Integer multiples of elements of commutative rings
10.37.
Integral domains
10.38.
Intersections of ideals of commutative rings
10.39.
Intersections of radical ideals of commutative rings
10.40.
Invertible elements in commutative rings
10.41.
Isomorphisms of commutative rings
10.42.
Joins of ideals of commutative rings
10.43.
Joins of radical ideals of commutative rings
10.44.
Large commutative rings
10.45.
Large function commutative rings
10.46.
Local commutative rings
10.47.
Maximal ideals of commutative rings
10.48.
Multiples of elements in commutative rings
10.49.
Multiples of elements in commutative semirings
10.50.
Multiples of elements in Euclidean domains
10.51.
Multiples of elements in integral domains
10.52.
Nilradical of a commutative ring
10.53.
The nilradical of a commutative semiring
10.54.
Polynomials in commutative rings
10.55.
Polynomials in commutative semirings
10.56.
The poset of ideals in a commutative ring
10.57.
The poset of radical ideals in a commutative ring
10.58.
Powers of elements in commutative rings
10.59.
Powers of elements in commutative semirings
10.60.
Powers of elements in large commutative rings
10.61.
The precategory of commutative rings
10.62.
The precategory of commutative semirings
10.63.
Prime ideals of commutative rings
10.64.
Products of commutative rings
10.65.
Products of ideals of commutative rings
10.66.
Products of radical ideals in a commutative ring
10.67.
Products of subsets of commutative rings
10.68.
Radical ideals of commutative rings
10.69.
Radical ideals generated by subsets of commutative rings
10.70.
Radicals of ideals of commutative rings
10.71.
Subalgebras over commutative rings
10.72.
Subsets of algebras over commutative rings
10.73.
Subsets of commutative rings
10.74.
Subsets of commutative semirings
10.75.
Sums of finite families in commutative rings
10.76.
Sums of finite families of elements in commutative semirings
10.77.
Sums of finite sequences in commutative rings
10.78.
Sums of finite sequences in commutative semirings
10.79.
Transporting commutative ring structures along isomorphisms of abelian groups
10.80.
Trivial commutative rings
10.81.
Unital algebras over commutative rings
10.82.
Unital associative algebras over commutative rings
10.83.
The Zariski locale
10.84.
The Zariski topology on the set of prime ideals in a commutative ring
11.
Complex numbers
❱
11.1.
Addition of complex numbers
11.2.
Addition of nonzero complex numbers
11.3.
Apartness of complex numbers
11.4.
Complex numbers
11.5.
Conjugation of complex numbers
11.6.
The Eisenstein integers
11.7.
The field of complex numbers
11.8.
The Gaussian integers
11.9.
The large additive group of complex numbers
11.10.
The large ring of complex numbers
11.11.
The local ring of complex numbers
11.12.
Magnitude of complex numbers
11.13.
Multiplication of complex numbers
11.14.
Multiplicative inverses of complex numbers
11.15.
Nonzero complex numbers
11.16.
Raising the universe level of complex numbers
11.17.
Real complex numbers
11.18.
Similarity of complex numbers
12.
Domain theory
❱
12.1.
Directed complete posets
12.2.
Directed families in posets
12.3.
Kleene's fixed point theorem for ω-complete posets
12.4.
Kleene's fixed point theorem for posets
12.5.
ω-Complete posets
12.6.
ω-Continuous maps between ω-complete posets
12.7.
ω-Continuous maps between posets
12.8.
Reindexing directed families in posets
12.9.
Scott-continuous maps between posets
13.
Elementary number theory
❱
13.1.
Absolute value on closed intervals in the rational numbers
13.2.
The absolute value function on the integers
13.3.
The absolute value function on the rational numbers
13.4.
The Ackermann function
13.5.
Addition on closed intervals in the rational numbers
13.6.
Addition on integer fractions
13.7.
Addition on the integers
13.8.
Addition on the natural numbers
13.9.
Addition on nonnegative rational numbers
13.10.
Addition of positive, negative, nonnegative and nonpositive integers
13.11.
Addition of positive rational numbers
13.12.
Addition on the rational numbers
13.13.
The additive group of rational numbers
13.14.
The Archimedean property of integer fractions
13.15.
The Archimedean property of the integers
13.16.
The Archimedean property of the natural numbers
13.17.
The Archimedean property of the positive rational numbers
13.18.
The Archimedean property of ℚ
13.19.
Arithmetic functions
13.20.
Arithmetic sequences of positive rational numbers
13.21.
The based induction principle of the natural numbers
13.22.
Based strong induction for the natural numbers
13.23.
The Bell numbers
13.24.
Bernoulli's inequality on the positive rational numbers
13.25.
Bezout's lemma in the integers
13.26.
Bezout's lemma on the natural numbers
13.27.
Binary sum decompositions of natural numbers
13.28.
The binomial coefficients
13.29.
The binomial theorem for the integers
13.30.
The binomial theorem for the natural numbers
13.31.
Bounded sums of arithmetic functions
13.32.
Catalan numbers
13.33.
Closed interval preserving endomaps on the rational numbers
13.34.
Closed intervals in the rational numbers
13.35.
The cofibonacci sequence
13.36.
The Collatz bijection
13.37.
The Collatz conjecture
13.38.
Conatural numbers
13.39.
The congruence relations on the integers
13.40.
The congruence relations on the natural numbers
13.41.
The cross-multiplication difference of two integer fractions
13.42.
The cross-multiplication difference of two rational numbers
13.43.
Cubes of natural numbers
13.44.
Decidable dependent function types
13.45.
The decidable total order of integers
13.46.
The decidable total order of natural numbers
13.47.
The decidable total order of rational numbers
13.48.
The decidable total order of a standard finite type
13.49.
Decidable types in elementary number theory
13.50.
The difference between integers
13.51.
The difference of natural numbers
13.52.
The difference between rational numbers
13.53.
Dirichlet convolution
13.54.
The distance between integers
13.55.
The distance between natural numbers
13.56.
The distance between rational numbers
13.57.
Divisibility of integers
13.58.
Divisibility in modular arithmetic
13.59.
Divisibility of natural numbers
13.60.
The divisibility relation on the standard finite types
13.61.
Equality of conatural numbers
13.62.
Equality of integers
13.63.
Equality of natural numbers
13.64.
Equality of rational numbers
13.65.
The Euclid–Mullin sequence
13.66.
Euclidean division on the natural numbers
13.67.
Euler's totient function
13.68.
Exponentiation of natural numbers
13.69.
Factorials of natural numbers
13.70.
Falling factorials
13.71.
Fermat numbers
13.72.
The Fibonacci sequence
13.73.
The field of rational numbers
13.74.
The natural numbers base k
13.75.
Finitely cyclic maps
13.76.
The floor of nonnegative integer fractions
13.77.
The floor of nonnegative rational numbers
13.78.
The fundamental theorem of arithmetic
13.79.
Geometric sequences of positive rational numbers
13.80.
Geometric sequences of rational numbers
13.81.
The Goldbach conjecture
13.82.
The greatest common divisor of integers
13.83.
The greatest common divisor of natural numbers
13.84.
The group of integers
13.85.
The half-integers
13.86.
The Hardy-Ramanujan number
13.87.
The harmonic series of rational numbers
13.88.
The inclusion of the natural numbers into the conatural numbers
13.89.
Inequalities between positive, negative, nonnegative, and nonpositive rational numbers
13.90.
Inequality of arithmetic and geometric means on the integers
13.91.
Inequality of arithmetic and geometric means on the rational numbers
13.92.
Inequality of conatural numbers
13.93.
Inequality on integer fractions
13.94.
Inequality on the integers
13.95.
Inequality of natural numbers
13.96.
Inequality on the nonnegative rational numbers
13.97.
Inequality on the positive rational numbers
13.98.
Inequality on the rational numbers
13.99.
Inequality on the standard finite types
13.100.
Infinite conatural numbers
13.101.
The infinitude of primes
13.102.
Initial segments of the natural numbers
13.103.
Integer fractions
13.104.
Integer partitions
13.105.
The integers
13.106.
Interior closed intervals in the rational numbers
13.107.
Intersections of closed intervals of rational numbers
13.108.
The Jacobi symbol
13.109.
The Kolakoski sequence
13.110.
The Legendre symbol
13.111.
Lower bounds of type families over the natural numbers
13.112.
Maximum on the natural numbers
13.113.
The maximum of nonnegative rational numbers
13.114.
The maximum of positive rational numbers
13.115.
Maximum on the rational numbers
13.116.
Maximum on the standard finite types
13.117.
The mediant fraction of two integer fractions
13.118.
Mersenne primes
13.119.
The metric additive group of rational numbers
13.120.
Minima and maxima on the rational numbers
13.121.
Minimum on the natural numbers
13.122.
The minimum of positive rational numbers
13.123.
Minimum on the rational numbers
13.124.
Minimum on the standard finite types
13.125.
Modular arithmetic
13.126.
Modular arithmetic on the standard finite types
13.127.
The monoid of natural numbers with addition
13.128.
The monoid of the natural numbers with maximum
13.129.
Multiplication on closed intervals in the rational numbers
13.130.
Multiplication on integer fractions
13.131.
Multiplication of integers
13.132.
Multiplication of interior intervals of closed intervals of rational numbers
13.133.
Multiplication of the elements of a list of natural numbers
13.134.
Multiplication of natural numbers
13.135.
Multiplication by negative rational numbers
13.136.
Multiplication by nonnegative rational numbers
13.137.
Multiplication by nonpositive rational numbers
13.138.
Multiplication of positive, negative, nonnegative and nonpositive integers
13.139.
Multiplication by positive, negative, and nonnegative rational numbers
13.140.
Multiplication by positive rational numbers
13.141.
Multiplication on the rational numbers
13.142.
The multiplicative group of positive rational numbers
13.143.
The multiplicative group of rational numbers
13.144.
Multiplicative inverses of positive integer fractions
13.145.
The multiplicative monoid of natural numbers
13.146.
The multiplicative monoid of nonnegative rational numbers
13.147.
The multiplicative monoid of rational numbers
13.148.
Multiplicative units in the integers
13.149.
Multiplicative units in modular arithmetic
13.150.
Multiset coefficients
13.151.
The type of natural numbers
13.152.
Negation of closed intervals in the rational numbers
13.153.
Negative closed intervals in the rational numbers
13.154.
Negative integer fractions
13.155.
The negative integers
13.156.
Negative rational numbers
13.157.
Nonnegative integer fractions
13.158.
The nonnegative integers
13.159.
Nonnegative rational numbers
13.160.
The nonpositive integers
13.161.
The nonpositive rational numbers
13.162.
Nonzero integers
13.163.
Nonzero natural numbers
13.164.
Nonzero rational numbers
13.165.
The ordinal induction principle for the natural numbers
13.166.
Parity of the natural numbers
13.167.
Peano arithmetic
13.168.
Pisano periods
13.169.
The poset of closed intervals of rational numbers
13.170.
The poset of natural numbers ordered by divisibility
13.171.
The positive, negative, nonnegative and nonpositive integers
13.172.
The positive, negative, and nonnegative rational numbers
13.173.
Positive closed intervals in the rational numbers
13.174.
Positive conatural numbers
13.175.
Positive integer fractions
13.176.
The positive integers
13.177.
Positive rational numbers
13.178.
Powers of integers
13.179.
Powers of nonnegative rational numbers
13.180.
Powers of two
13.181.
Powers of positive rational numbers
13.182.
Powers of rational numbers
13.183.
Prime numbers
13.184.
Products of natural numbers
13.185.
Proper closed intervals in the rational numbers
13.186.
Proper divisors of natural numbers
13.187.
Pythagorean triples
13.188.
The rational numbers
13.189.
Reduced integer fractions
13.190.
Relatively prime integers
13.191.
Relatively prime natural numbers
13.192.
Repeating an element in a standard finite type
13.193.
Retracts of the type of natural numbers
13.194.
The ring extension of rational numbers of the ring of rational numbers
13.195.
The ring of integers
13.196.
The ring of rational numbers
13.197.
The semiring of natural numbers
13.198.
Series of rational numbers
13.199.
The sieve of Eratosthenes
13.200.
Square-free natural numbers
13.201.
Square roots of positive rational numbers
13.202.
Squares in the integers
13.203.
Squares in ℤₚ
13.204.
Squares in the natural numbers
13.205.
Squares in the rational numbers
13.206.
The standard cyclic groups
13.207.
The standard cyclic rings
13.208.
Stirling numbers of the second kind
13.209.
Strict inequality on the integer fractions
13.210.
Strict inequality on the integers
13.211.
Strict inequality on the natural numbers
13.212.
Strict inequality on nonnegative rational numbers
13.213.
Strict inequality on positive rational numbers
13.214.
Strict inequality on the rational numbers
13.215.
Strict inequality on the standard finite types
13.216.
Strictly ordered pairs of natural numbers
13.217.
The strong induction principle for the natural numbers
13.218.
Sums of natural numbers
13.219.
Sums of finite sequences of rational numbers
13.220.
Sylvester's sequence
13.221.
Taxicab numbers
13.222.
Telephone numbers
13.223.
The triangular numbers
13.224.
The Twin Prime conjecture
13.225.
Type arithmetic with natural numbers
13.226.
The unit closed interval in the rational numbers
13.227.
Unit elements in the standard finite types
13.228.
Unit fractions in the rational numbers types
13.229.
Unit similarity on the standard finite types
13.230.
The universal property of the conatural numbers
13.231.
The universal property of the integers
13.232.
The universal property of the natural numbers
13.233.
Unsolvability of squaring to two in the rational numbers
13.234.
Upper bounds for type families over the natural numbers
13.235.
The well-ordering principle of the natural numbers
13.236.
The well-ordering principle of the standard finite types
13.237.
The zero conatural number
14.
Finite algebra
❱
14.1.
Commutative finite rings
14.2.
Dependent products of commutative finit rings
14.3.
Dependent products of finite rings
14.4.
Finite fields
14.5.
Finite rings
14.6.
Homomorphisms of commutative finite rings
14.7.
Homomorphisms of finite rings
14.8.
Products of commutative finite rings
14.9.
Products of finite rings
14.10.
Semisimple commutative finite rings
15.
Finite group theory
❱
15.1.
The abstract quaternion group of order 8
15.2.
Alternating concrete groups
15.3.
Alternating groups
15.4.
Cartier's delooping of the sign homomorphism
15.5.
The concrete quaternion group
15.6.
Deloopings of the sign homomorphism
15.7.
Finite abelian groups
15.8.
Finite commutative monoids
15.9.
Finite groups
15.10.
Finite monoids
15.11.
Finite semigroups
15.12.
The group of n-element types
15.13.
Groups of order 2
15.14.
Orbits of permutations
15.15.
Permutations
15.16.
Permutations of standard finite types
15.17.
The sign homomorphism
15.18.
Simpson's delooping of the sign homomorphism
15.19.
Subgroups of finite groups
15.20.
Tetrahedra in 3-dimensional space
15.21.
Transpositions
15.22.
Transpositions of standard finite types
16.
Foundation
❱
16.1.
0-Connected types
16.2.
0-Images of maps
16.3.
0-Maps
16.4.
1-Types
16.5.
2-Types
16.6.
Action on equivalences of functions
16.7.
The action on equivalences of functions out of subuniverses
16.8.
Action on equivalences of type families
16.9.
Action on equivalences in type families over subuniverses
16.10.
The action of functions on higher identifications
16.11.
The action on homotopies of functions
16.12.
The binary action on identifications of binary dependent functions
16.13.
The binary action on identifications of binary functions
16.14.
The action on identifications of dependent functions
16.15.
The action on identifications of functions
16.16.
The ternary action on identifications of ternary functions
16.17.
Apartness relations
16.18.
Arithmetic law for coproduct decomposition and Σ-decomposition
16.19.
Arithmetic law for product decomposition and Π-decomposition
16.20.
Automorphisms
16.21.
The axiom of choice
16.22.
The axiom of countable choice
16.23.
The axiom of dependent choice
16.24.
Bands
16.25.
Base changes of span diagrams
16.26.
Bicomposition of functions
16.27.
Binary dependent identifications
16.28.
Binary embeddings
16.29.
Binary equivalences
16.30.
Binary equivalences on unordered pairs of types
16.31.
Binary functoriality of set quotients
16.32.
Homotopies of binary operations
16.33.
Binary operations on unordered pairs of types
16.34.
Binary reflecting maps of equivalence relations
16.35.
Binary relations
16.36.
Binary relations with extensions
16.37.
Binary relations with lifts
16.38.
Binary transport
16.39.
Binary type duality
16.40.
The booleans
16.41.
The Cantor–Schröder–Bernstein theorem for decidable embeddings
16.42.
The Cantor–Schröder–Bernstein–Escardó theorem
16.43.
Cantor's theorem
16.44.
Cartesian morphisms of arrows
16.45.
Cartesian morphisms of span diagrams
16.46.
Cartesian product types
16.47.
Cartesian products of set quotients
16.48.
Cartesian products of subtypes
16.49.
The category of families of sets
16.50.
The category of sets
16.51.
Choice of representatives for an equivalence relation
16.52.
Coalgebras of the maybe monad
16.53.
Codiagonal maps of types
16.54.
Coherently constant maps
16.55.
Coherently idempotent maps
16.56.
Coherently invertible maps
16.57.
Coinhabited pairs of types
16.58.
Commuting cubes of maps
16.59.
Commuting hexagons of identifications
16.60.
Commuting pentagons of identifications
16.61.
Commuting prisms of maps
16.62.
Commuting squares of homotopies
16.63.
Commuting squares of identifications
16.64.
Commuting squares of maps
16.65.
Commuting tetrahedra of homotopies
16.66.
Commuting tetrahedra of maps
16.67.
Commuting triangles of homotopies
16.68.
Commuting triangles of identifications
16.69.
Commuting triangles of maps
16.70.
Commuting triangles of morphisms of arrows
16.71.
Complements of type families
16.72.
The complement of the image of a map
16.73.
Complements of subtypes
16.74.
Composite maps in inverse sequential diagrams
16.75.
Composition algebra
16.76.
Composition of spans
16.77.
Computational identity types
16.78.
Cones over cospan diagrams
16.79.
Cones over inverse sequential diagrams
16.80.
Conjunction
16.81.
Connected components of types
16.82.
Connected components of universes
16.83.
Connected maps
16.84.
Connected types
16.85.
Constant maps
16.86.
Constant span diagrams
16.87.
Constant type families
16.88.
The continuation monad
16.89.
Contractible maps
16.90.
Contractible types
16.91.
Copartial elements
16.92.
Copartial functions
16.93.
Coproduct decompositions
16.94.
Coproduct decompositions in a subuniverse
16.95.
Coproduct types
16.96.
Coproducts of pullbacks
16.97.
Morphisms in the coslice category of types
16.98.
Cospan diagrams
16.99.
Cospans of types
16.100.
Cumulative large sets
16.101.
Decidability of dependent function types
16.102.
Decidability of dependent pair types
16.103.
Decidable embeddings
16.104.
Decidable equality
16.105.
Decidable equivalence relations
16.106.
Decidable maps
16.107.
Decidable propositions
16.108.
Decidable relations on types
16.109.
Decidable subtypes
16.110.
Decidable type families
16.111.
Decidable types
16.112.
Dependent binary homotopies
16.113.
The dependent binomial theorem for types (distributivity of dependent function types over coproduct types)
16.114.
Dependent epimorphisms
16.115.
Dependent epimorphisms with respect to truncated types
16.116.
Dependent function types
16.117.
Apartness relations on dependent function types
16.118.
Dependent homotopies
16.119.
Dependent identifications
16.120.
Dependent inverse sequential diagrams of types
16.121.
Dependent pair types
16.122.
Dependent products of cumulative large sets
16.123.
Dependent products of large binary relations
16.124.
Dependent products of large equivalence relations
16.125.
Dependent products of large similarity relations
16.126.
Dependent products of pullbacks
16.127.
Dependent products of subtypes
16.128.
Dependent sums of pullbacks
16.129.
Dependent telescopes
16.130.
The dependent universal property of equivalences
16.131.
Descent for coproduct types
16.132.
Descent for dependent pair types
16.133.
Descent for the empty type
16.134.
Descent for equivalences
16.135.
Descent for surjective maps
16.136.
Diaconescu's theorem
16.137.
Diagonal maps into cartesian products of types
16.138.
Diagonal maps of types
16.139.
Diagonal span diagrams
16.140.
Diagonals of maps
16.141.
Diagonals of morphisms of arrows
16.142.
Discrete binary relations
16.143.
Discrete reflexive relations
16.144.
Discrete relaxed Σ-decompositions
16.145.
Discrete Σ-decompositions
16.146.
Discrete types
16.147.
Disjoint subtypes
16.148.
Disjunction
16.149.
Double arrows
16.150.
Double negation
16.151.
Double negation dense equality
16.152.
Maps with double negation dense equality
16.153.
The double negation image of a map
16.154.
The double negation modality
16.155.
Double negation stable equality
16.156.
Double negation stable propositions
16.157.
Double powersets
16.158.
Dubuc-Penon compact types
16.159.
Effective maps for equivalence relations
16.160.
Embeddings
16.161.
Empty subtypes
16.162.
Empty types
16.163.
Endomorphisms
16.164.
Epimorphisms
16.165.
Epimorphisms with respect to maps into sets
16.166.
Epimorphisms with respect to truncated types
16.167.
Equality of cartesian product types
16.168.
Equality of coproduct types
16.169.
Equality on dependent function types
16.170.
Equality of dependent pair types
16.171.
Equality in the fibers of a map
16.172.
Equality of equality of cartesian product types
16.173.
Equality of truncation levels
16.174.
Equivalence classes
16.175.
Equivalence extensionality
16.176.
Equivalence induction
16.177.
Equivalence injective type families
16.178.
Equivalence relations
16.179.
Equivalences
16.180.
Equivalences of arrows
16.181.
Equivalences of cospan diagrams
16.182.
Equivalences of cospans
16.183.
Equivalences of double arrows
16.184.
Equivalences of forks over equivalences of double arrows
16.185.
Equivalences of inverse sequential diagrams of types
16.186.
Equivalences on Maybe
16.187.
Equivalences of span diagrams
16.188.
Equivalences of span diagrams on families of types
16.189.
Equivalences of spans
16.190.
Equivalences of spans of families of types
16.191.
Evaluation of functions
16.192.
Exclusive disjunctions
16.193.
Exclusive sums
16.194.
Existential quantification
16.195.
Exponents of set quotients
16.196.
Extensional binary functions on apartness relations
16.197.
Extensions of types
16.198.
Extensions of types in a global subuniverse
16.199.
Extensions of types in a subuniverse
16.200.
Faithful maps
16.201.
Families of equivalences
16.202.
Families of maps
16.203.
Families of types over telescopes
16.204.
Fiber inclusions
16.205.
Fibered equivalences
16.206.
Fibered involutions
16.207.
Maps fibered over a map
16.208.
Fibers of maps
16.209.
Finite sequences of set quotients
16.210.
Finitely coherent equivalences
16.211.
Finitely coherently invertible maps
16.212.
Finitely truncated types
16.213.
Fixed points of endofunctions
16.214.
Forks
16.215.
Freely generated equivalence relations
16.216.
Full subtypes of types
16.217.
Full subuniverses
16.218.
Function cumulative large sets
16.219.
Function extensionality
16.220.
Function large binary relations
16.221.
Function large equivalence relations
16.222.
Function large similarity relations
16.223.
Function types
16.224.
Apartness relations on function types
16.225.
Functional correspondences
16.226.
Functoriality of the action on identifications of functions
16.227.
Functoriality of cartesian product types
16.228.
Functoriality of coproduct types
16.229.
Functoriality of dependent function types
16.230.
Functoriality of dependent pair types
16.231.
Functoriality of disjunction
16.232.
Functoriality of fibers of maps
16.233.
Functoriality of function types
16.234.
Functoriality of morphisms of arrows
16.235.
Functoriality of propositional truncations
16.236.
Functorialty of pullbacks
16.237.
Functoriality of sequential limits
16.238.
Functoriality of set quotients
16.239.
Functoriality of set truncation
16.240.
Functoriality of truncations
16.241.
Fundamental theorem of equivalence relations
16.242.
The fundamental theorem of identity types
16.243.
Global choice
16.244.
Global subuniverses
16.245.
The globular type of dependent functions
16.246.
The globular type of functions
16.247.
Higher homotopies of morphisms of arrows
16.248.
Hilbert ε-operators on maps
16.249.
Hilbert's ε-operators
16.250.
Homotopies
16.251.
Homotopies of morphisms of arrows
16.252.
Homotopies of morphisms of cospan diagrams
16.253.
Homotopy algebra
16.254.
Homotopy induction
16.255.
The homotopy preorder of types
16.256.
Horizontal composition of spans of spans
16.257.
Idempotent maps
16.258.
Identity systems
16.259.
Identity types of truncated types
16.260.
Identity types
16.261.
The image of a map
16.262.
Images of subtypes
16.263.
Implicit function types
16.264.
Impredicative encodings of the logical operations
16.265.
Impredicative universes
16.266.
The induction principle for propositional truncation
16.267.
The standard inequality relation on booleans
16.268.
Inequality of truncation levels
16.269.
Infinitely coherent equivalences
16.270.
∞-connected maps
16.271.
∞-connected types
16.272.
Inhabited subtypes
16.273.
Inhabited types
16.274.
Injective maps
16.275.
The interchange law
16.276.
Intersections of subtypes
16.277.
Inverse sequential diagrams of types
16.278.
Invertible maps
16.279.
Involutions
16.280.
Irrefutable equality
16.281.
Irrefutable propositions
16.282.
Isolated elements
16.283.
Isomorphisms of sets
16.284.
Iterated cartesian product types
16.285.
Iterated dependent pair types
16.286.
Iterated dependent product types
16.287.
Iterated successors of truncation levels
16.288.
Iterating automorphisms
16.289.
Iterating families of maps over a map
16.290.
Iterating functions
16.291.
Iterating involutions
16.292.
Kernel span diagrams of maps
16.293.
Large apartness relations
16.294.
Large binary relations
16.295.
Large dependent pair types
16.296.
Large equivalence relations
16.297.
Large homotopies
16.298.
Large identity types
16.299.
The large locale of propositions
16.300.
The large locale of subtypes
16.301.
Large similarity relations
16.302.
The law of excluded middle
16.303.
Lawvere's fixed point theorem
16.304.
The lesser limited principle of omniscience
16.305.
Lifts of morphisms of arrows
16.306.
Lifts of types
16.307.
The limited principle of omniscience
16.308.
The locale of propositions
16.309.
Locally small types
16.310.
Logical equivalences
16.311.
Logical operations on the booleans
16.312.
Maps in global subuniverses
16.313.
Maps in subuniverses
16.314.
The maximum of truncation levels
16.315.
The maybe monad
16.316.
Mere decidable embeddings
16.317.
Mere embeddings
16.318.
Mere equality
16.319.
Mere equivalences
16.320.
Mere functions
16.321.
Mere logical equivalences
16.322.
Mere path-cosplit maps
16.323.
Monomorphisms
16.324.
Morphisms of arrows
16.325.
Morphisms of binary relations
16.326.
Morphisms of coalgebras of the maybe monad
16.327.
Morphisms of cospan diagrams
16.328.
Morphisms of cospans
16.329.
Morphisms of double arrows
16.330.
Morphisms of forks over morphisms of double arrows
16.331.
Morphisms of inverse sequential diagrams of types
16.332.
Morphisms of span diagrams
16.333.
Morphisms of spans
16.334.
Morphisms of spans on families of types
16.335.
Morphisms of twisted arrows
16.336.
Multisubsets
16.337.
Multivariable correspondences
16.338.
Multivariable decidable relations
16.339.
Multivariable functoriality of set quotients
16.340.
Multivariable homotopies
16.341.
Multivariable operations
16.342.
Multivariable relations
16.343.
Multivariable sections
16.344.
Negated equality
16.345.
Negation
16.346.
Noncontractible types
16.347.
Noninjective maps
16.348.
Nonsurjective maps
16.349.
Null-homotopic maps
16.350.
Operations on cospan diagrams
16.351.
Operations on cospans
16.352.
Operations on span diagrams
16.353.
Operations on spans
16.354.
Operations on spans of families of types
16.355.
Opposite cospans
16.356.
Opposite spans
16.357.
Pairs of distinct elements
16.358.
Parametric types
16.359.
The parametricity axiom
16.360.
Partial elements
16.361.
Partial functions
16.362.
Partitions
16.363.
Path algebra
16.364.
Path-cosplit maps
16.365.
Path-split maps
16.366.
Path-split type families
16.367.
Perfect images
16.368.
Permutations of spans of families of types
16.369.
Π-decompositions of types
16.370.
Π-decompositions of types into types in a subuniverse
16.371.
Pointed torsorial type families
16.372.
Postcomposition of dependent functions
16.373.
Postcomposition of functions
16.374.
Postcomposition of pullbacks
16.375.
Powersets
16.376.
Precomposition of dependent functions
16.377.
Precomposition of functions
16.378.
Precomposition of functions into subuniverses
16.379.
Precomposition of type families
16.380.
The preunivalence axiom
16.381.
Preunivalent type families
16.382.
The principle of omniscience
16.383.
Product decompositions
16.384.
Product decompositions of types in a subuniverse
16.385.
Products of binary relations
16.386.
Products of equivalence relataions
16.387.
Products of tuples of types
16.388.
Products of pullbacks
16.389.
Products of unordered pairs of types
16.390.
Products of unordered tuples of types
16.391.
Projective types
16.392.
Proper subsets
16.393.
Propositional extensionality
16.394.
Propositional maps
16.395.
Propositional resizing
16.396.
Propositional truncations
16.397.
Propositions
16.398.
Pullback cones
16.399.
Pullbacks
16.400.
Pullbacks of subtypes
16.401.
Quasicoherently idempotent maps
16.402.
Raising universe levels
16.403.
Reflecting maps for equivalence relations
16.404.
Reflexive relations
16.405.
The Regensburg extension of the fundamental theorem of identity types
16.406.
Relaxed Σ-decompositions of types
16.407.
Repetitions of values of maps
16.408.
The type theoretic replacement axiom
16.409.
Retractions
16.410.
Retracts of arrows
16.411.
Retracts of types
16.412.
Sections
16.413.
Types separated at subuniverses
16.414.
Sequential limits
16.415.
Set coequalizers
16.416.
Set presented types
16.417.
Set quotients
16.418.
Set truncations
16.419.
Sets
16.420.
Σ-closed subuniverses
16.421.
Σ-decompositions of types into types in a subuniverse
16.422.
Σ-decompositions of types
16.423.
Similarity preserving binary maps on cumulative large sets
16.424.
Similarity preserving binary maps over large similarity relations
16.425.
Similarity-preserving maps on cumulative large sets
16.426.
Large similarity preserving maps
16.427.
Similarity of subtypes
16.428.
Singleton induction
16.429.
Singleton subtypes
16.430.
Morphisms in the slice category of types
16.431.
Small maps
16.432.
Small types
16.433.
Small universes
16.434.
Smallness in cumulative large sets
16.435.
Smallness relative to large similarity relations
16.436.
Sorial type families
16.437.
Span diagrams
16.438.
Span diagrams on families of types
16.439.
Spans of types
16.440.
Spans of families of types
16.441.
Spans of spans
16.442.
Split idempotent maps
16.443.
Split surjective maps
16.444.
Standard apartness relations
16.445.
Standard pullbacks
16.446.
Standard ternary pullbacks
16.447.
Strict symmetrization of binary relations
16.448.
Strictly involutive identity types
16.449.
The strictly right unital concatenation operation on identifications
16.450.
The strong preunivalence axiom
16.451.
Strongly extensional maps
16.452.
Structure
16.453.
The structure identity principle
16.454.
Structured equality duality
16.455.
Structured type duality
16.456.
Subsingleton induction
16.457.
Subterminal types
16.458.
Subtype duality
16.459.
The subtype identity principle
16.460.
Subtypes
16.461.
Subuniverse parametric types
16.462.
Subuniverses
16.463.
Surjective maps
16.464.
Symmetric binary relations
16.465.
Symmetric cores of binary relations
16.466.
Symmetric difference of subtypes
16.467.
The symmetric identity types
16.468.
Symmetric operations
16.469.
Telescopes
16.470.
Terminal spans on families of types
16.471.
Tight apartness relations
16.472.
Tight large apartness relations
16.473.
Torsorial type families
16.474.
Total partial elements
16.475.
Total partial functions
16.476.
Transfinite cocomposition of maps
16.477.
Transport along equivalences
16.478.
Transport along higher identifications
16.479.
Transport along homotopies
16.480.
Transport along identifications
16.481.
Transport-split type families
16.482.
Transposition of cospan diagrams
16.483.
Transposing identifications along equivalences
16.484.
Transposing identifications along retractions
16.485.
Transposing identifications along sections
16.486.
Transposition of span diagrams
16.487.
Trivial relaxed Σ-decompositions
16.488.
Trivial Σ-decompositions
16.489.
Truncated addition of truncation levels
16.490.
Truncated equality
16.491.
Truncated maps
16.492.
Truncated types
16.493.
k-Equivalences
16.494.
Truncation images of maps
16.495.
Truncation levels
16.496.
The truncation modalities
16.497.
Truncations
16.498.
Tuples of types
16.499.
Type arithmetic with the booleans
16.500.
Type arithmetic for cartesian product types
16.501.
Type arithmetic for coproduct types
16.502.
Type arithmetic with dependent function types
16.503.
Type arithmetic for dependent pair types
16.504.
Type arithmetic with the empty type
16.505.
Type arithmetic with standard pullbacks
16.506.
Type arithmetic with the unit type
16.507.
Type duality
16.508.
The type theoretic principle of choice
16.509.
Types with decidable Σ-types
16.510.
Types with decidable Π-types
16.511.
Types with decidable universal quantifications
16.512.
Uniformly decidable type families
16.513.
Unions of subtypes
16.514.
Uniqueness of the image of a map
16.515.
Uniqueness quantification
16.516.
The uniqueness of set quotients
16.517.
Uniqueness of set truncations
16.518.
Uniqueness of the truncations
16.519.
The unit type
16.520.
Unital binary operations
16.521.
The univalence axiom
16.522.
The univalence axiom implies function extensionality
16.523.
Univalent type families
16.524.
The universal property of booleans
16.525.
The universal property of cartesian morphisms of arrows
16.526.
The universal properties of cartesian product types
16.527.
Universal property of contractible types
16.528.
The universal property of coproduct types
16.529.
The universal property of dependent function types
16.530.
The universal property of dependent pair types
16.531.
The universal property of the empty type
16.532.
The universal property of equivalences
16.533.
The universal property of the family of fibers of maps
16.534.
The universal property of fiber products
16.535.
The universal property of identity systems
16.536.
The universal property of identity types
16.537.
The universal property of the image of a map
16.538.
The universal property of the maybe monad
16.539.
The universal property of propositional truncations
16.540.
The universal property of propositional truncations with respect to sets
16.541.
The universal property of pullbacks
16.542.
The universal property of sequential limits
16.543.
The universal property of set quotients
16.544.
The universal property of set truncations
16.545.
The universal property of truncations
16.546.
The universal property of the unit type
16.547.
Universal quantification
16.548.
Universe levels
16.549.
Unordered pairs of elements in a type
16.550.
Unordered pairs of types
16.551.
Unordered n-tuples of elements in a type
16.552.
Unordered tuples of types
16.553.
Vertical composition of spans of spans
16.554.
Weak function extensionality
16.555.
The weak limited principle of omniscience
16.556.
Weakly constant maps
16.557.
Whiskering higher homotopies with respect to composition
16.558.
Whiskering homotopies with respect to composition
16.559.
Whiskering homotopies with respect to concatenation
16.560.
Whiskering identifications with respect to concatenation
16.561.
Whiskering operations
16.562.
The wild category of types
16.563.
Yoneda identity types
17.
Foundation core
❱
17.1.
1-Types
17.2.
Cartesian product types
17.3.
Coherently invertible maps
17.4.
Commuting prisms of maps
17.5.
Commuting squares of homotopies
17.6.
Commuting squares of identifications
17.7.
Commuting squares of maps
17.8.
Commuting triangles of maps
17.9.
Constant maps
17.10.
Contractible maps
17.11.
Contractible types
17.12.
Coproduct types
17.13.
Decidable propositions
17.14.
Dependent identifications
17.15.
Diagonal maps into cartesian products of types
17.16.
Discrete types
17.17.
Double negation stable equality
17.18.
Embeddings
17.19.
Empty types
17.20.
Endomorphisms
17.21.
Equality of dependent pair types
17.22.
Equivalence relations
17.23.
Equivalences
17.24.
Equivalences of arrows
17.25.
Families of equivalences
17.26.
Fibers of maps
17.27.
Function types
17.28.
Functoriality of dependent function types
17.29.
Functoriality of dependent pair types
17.30.
Homotopies
17.31.
Identity types
17.32.
Injective maps
17.33.
Invertible maps
17.34.
Iterating functions
17.35.
The law of excluded middle
17.36.
Monomorphisms
17.37.
Negation
17.38.
Operations on cospan diagrams
17.39.
Operations on cospans
17.40.
Operations on span diagrams
17.41.
Operations on spans
17.42.
Path-split maps
17.43.
Postcomposition of dependent functions
17.44.
Postcomposition of functions
17.45.
Precomposition of dependent functions
17.46.
Precomposition of functions
17.47.
Propositional maps
17.48.
Propositions
17.49.
Pullbacks
17.50.
Retractions
17.51.
Retracts of types
17.52.
Sections
17.53.
Sets
17.54.
Small types
17.55.
Subtypes
17.56.
Torsorial type families
17.57.
Transport along identifications
17.58.
Truncated maps
17.59.
Truncated types
17.60.
Truncation levels
17.61.
The type theoretic principle of choice
17.62.
The univalence axiom
17.63.
The universal property of pullbacks
17.64.
The universal property of truncations
17.65.
Whiskering homotopies with respect to concatenation
17.66.
Whiskering identifications with respect to concatenation
18.
Functional analysis
❱
18.1.
Absolute convergence of series in real Banach spaces
18.2.
The underlying additive complete metric abelian groups of real Banach spaces
18.3.
Convergent series in real Banach spaces
18.4.
The ratio test for series in real Banach spaces
18.5.
Real Banach spaces
18.6.
Real Hilbert spaces
18.7.
Series in real Banach spaces
18.8.
The standard Euclidean Hilbert spaces
18.9.
Sums of finite sequences of elements in real Banach spaces
19.
Globular types
❱
19.1.
Base change of dependent globular types
19.2.
Base change of dependent reflexive globular types
19.3.
Binary dependent globular types
19.4.
Binary dependent reflexive globular types
19.5.
Binary globular maps
19.6.
Colax reflexive globular maps
19.7.
Colax transitive globular maps
19.8.
Composition structure on globular types
19.9.
Constant globular types
19.10.
Dependent globular types
19.11.
Dependent reflexive globular types
19.12.
Dependent sums of globular types
19.13.
Discrete dependent reflexive globular types
19.14.
Discrete globular types
19.15.
Discrete reflexive globular types
19.16.
Empty globular types
19.17.
Equality of globular types
19.18.
Exponentials of globular types
19.19.
Fibers of globular maps
19.20.
Equivalences between globular types
19.21.
Maps between globular types
19.22.
Globular types
19.23.
Large colax reflexive globular maps
19.24.
Large colax transitive globular maps
19.25.
Maps between large globular types
19.26.
Large globular types
19.27.
Large lax reflexive globular maps
19.28.
Large lax transitive globular maps
19.29.
Large reflexive globular maps
19.30.
Large reflexive globular types
19.31.
Large symmetric globular types
19.32.
Large transitive globular maps
19.33.
Large transitive globular types
19.34.
Lax reflexive globular maps
19.35.
Lax transitive globular maps
19.36.
Points of globular types
19.37.
Points of reflexive globular types
19.38.
Pointwise extensions of binary families of globular types
19.39.
Pointwise extensions of binary families of reflexive globular types
19.40.
Pointwise extensions of families of globular types
19.41.
Pointwise extensions of families of reflexive globular types
19.42.
Products of families of globular types
19.43.
Reflexive globular equivalences
19.44.
Reflexive globular maps
19.45.
Reflexive globular types
19.46.
Sections of dependent globular types
19.47.
Superglobular types
19.48.
Symmetric globular types
19.49.
Terminal globular types
19.50.
Transitive globular maps
19.51.
Transitive globular types
19.52.
The unit globular type
19.53.
The unit reflexive globular type
19.54.
The universal globular type
19.55.
The universal reflexive globular type
20.
Graph theory
❱
20.1.
Acyclic undirected graphs
20.2.
Base change of dependent directed graphs
20.3.
Base change of dependent reflexive graphs
20.4.
Cartesian products of directed graphs
20.5.
Cartesian products of reflexive graphs
20.6.
Circuits in undirected graphs
20.7.
Closed walks in undirected graphs
20.8.
Complete bipartite graphs
20.9.
Complete multipartite graphs
20.10.
Complete undirected graphs
20.11.
Connected graphs
20.12.
Cycles in undirected graphs
20.13.
Dependent directed graphs
20.14.
Dependent products of directed graphs
20.15.
Dependent products of reflexive graphs
20.16.
Dependent reflexive graphs
20.17.
Dependent sums directed graphs
20.18.
Dependent sums reflexive graphs
20.19.
Directed graph duality
20.20.
Directed graph structures on standard finite sets
20.21.
Directed graphs
20.22.
Discrete dependent reflexive graphs
20.23.
Discrete directed graphs
20.24.
Discrete reflexive graphs
20.25.
Displayed large reflexive graphs
20.26.
Edge-colored undirected graphs
20.27.
Embeddings of directed graphs
20.28.
Embeddings of undirected graphs
20.29.
Enriched undirected graphs
20.30.
Equivalences of dependent directed graphs
20.31.
Equivalences of dependent reflexive graphs
20.32.
Equivalences of directed graphs
20.33.
Equivalences of enriched undirected graphs
20.34.
Equivalences of reflexive graphs
20.35.
Equivalences of undirected graphs
20.36.
Eulerian circuits in undirected graphs
20.37.
Faithful morphisms of undirected graphs
20.38.
Fibers of directed graphs
20.39.
Fibers of morphisms into directed graphs
20.40.
Fibers of morphisms into reflexive graphs
20.41.
Finite graphs
20.42.
Geometric realizations of undirected graphs
20.43.
Higher directed graphs
20.44.
Hypergraphs
20.45.
Internal homs of directed graphs
20.46.
Large higher directed graphs
20.47.
Large reflexive graphs
20.48.
Matchings
20.49.
Mere equivalences of undirected graphs
20.50.
Morphisms of dependent directed graphs
20.51.
Morphisms of directed graphs
20.52.
Morphisms of reflexive graphs
20.53.
Morphisms of undirected graphs
20.54.
Incidence in undirected graphs
20.55.
Orientations of undirected graphs
20.56.
Paths in undirected graphs
20.57.
Polygons
20.58.
Raising universe levels of directed graphs
20.59.
Reflecting maps of undirected graphs
20.60.
Reflexive graphs
20.61.
Regular undirected graph
20.62.
Sections of dependent directed graphs
20.63.
Sections of dependent reflexive graphs
20.64.
Simple undirected graphs
20.65.
Stereoisomerism for enriched undirected graphs
20.66.
Terminal directed graphs
20.67.
Terminal reflexive graphs
20.68.
Totally faithful morphisms of undirected graphs
20.69.
Trails in directed graphs
20.70.
Trails in undirected graphs
20.71.
Undirected graph structures on standard finite sets
20.72.
Undirected graphs
20.73.
The universal directed graph
20.74.
The universal reflexive graph
20.75.
Vertex covers
20.76.
Voltage graphs
20.77.
Walks in directed graphs
20.78.
Walks in undirected graphs
20.79.
Wide displayed large reflexive graphs
21.
Group theory
❱
21.1.
Abelian groups
21.2.
Abelianization of groups
21.3.
Pointwise addition of morphisms of abelian groups
21.4.
Arithmetic sequences in semigroups
21.5.
Automorphism groups
21.6.
Cartesian products of abelian groups
21.7.
Cartesian products of commutative monoids
21.8.
Cartesian products of concrete groups
21.9.
Cartesian products of groups
21.10.
Cartesian products of monoids
21.11.
Cartesian products of semigroups
21.12.
The category of abelian groups
21.13.
The category of concrete groups
21.14.
The category of group actions
21.15.
The category of groups
21.16.
The orbit category of a group
21.17.
The category of semigroups
21.18.
Cayley's theorem
21.19.
The center of a group
21.20.
Center of a monoid
21.21.
Center of a semigroup
21.22.
Central elements of groups
21.23.
Central elements of monoids
21.24.
Central elements of semirings
21.25.
Centralizer subgroups
21.26.
Characteristic subgroups
21.27.
Commutative monoids
21.28.
Commutative semigroups
21.29.
Commutator subgroups
21.30.
Commutators of elements in groups
21.31.
Commuting elements of groups
21.32.
Commuting elements of monoids
21.33.
Commuting elements of semigroups
21.34.
Commuting squares of group homomorphisms
21.35.
Concrete group actions
21.36.
Concrete groups
21.37.
Concrete monoids
21.38.
Congruence relations on abelian groups
21.39.
Congruence relations on commutative monoids
21.40.
Congruence relations on groups
21.41.
Congruence relations on monoids
21.42.
Congruence relations on semigroups
21.43.
Conjugation in groups
21.44.
Conjugation on concrete groups
21.45.
Contravariant pushforwards of concrete group actions
21.46.
Cores of monoids
21.47.
Cyclic groups
21.48.
Decidable subgroups of groups
21.49.
Dependent products of abelian groups
21.50.
Dependent products of commutative monoids
21.51.
Dependent products of groups
21.52.
Dependent products of large monoids
21.53.
Dependent products of large semigroups
21.54.
Dependent products of monoids
21.55.
Dependent products of semigroups
21.56.
The dihedral group construction
21.57.
The dihedral groups
21.58.
The E₈-lattice
21.59.
Elements of finite order
21.60.
Embeddings of abelian groups
21.61.
Embeddings of groups
21.62.
The endomorphism rings of abelian groups
21.63.
Epimorphisms in groups
21.64.
Equivalences of concrete group actions
21.65.
Equivalences of concrete groups
21.66.
Equivalences of group actions
21.67.
Equivalences between semigroups
21.68.
Exponents of abelian groups
21.69.
Exponents of groups
21.70.
Free concrete group actions
21.71.
Free groups with one generator
21.72.
The full subgroup of a group
21.73.
The full subsemigroup of a semigroup
21.74.
Function groups of abelian groups
21.75.
Function commutative monoids
21.76.
Function groups
21.77.
Function monoids
21.78.
Function semigroups
21.79.
Functoriality of quotient groups
21.80.
Furstenberg groups
21.81.
Generating elements of groups
21.82.
Generating sets of groups
21.83.
Grothendieck groups
21.84.
Group actions
21.85.
Abstract groups
21.86.
Homomorphisms of abelian groups
21.87.
Homomorphisms of commutative monoids
21.88.
Morphisms of concrete group actions
21.89.
Homomorphisms of concrete groups
21.90.
Homomorphisms of generated subgroups
21.91.
Homomorphisms of group actions
21.92.
Homomorphisms of groups
21.93.
Homomorphisms of groups equipped with normal subgroups
21.94.
Homomorphisms of monoids
21.95.
Homomorphisms of semigroups
21.96.
Homotopy automorphism groups
21.97.
Images of group homomorphisms
21.98.
Images of semigroup homomorphisms
21.99.
Integer multiples of elements in abelian groups
21.100.
Integer multiples of elements in large abelian groups
21.101.
Integer powers of elements of groups
21.102.
Integer powers of elements in large groups
21.103.
Intersections of subgroups of abelian groups
21.104.
Intersections of subgroups of groups
21.105.
Inverse semigroups
21.106.
Invertible elements in large monoids
21.107.
Invertible elements in monoids
21.108.
Isomorphisms of abelian groups
21.109.
Isomorphisms of concrete groups
21.110.
Isomorphisms of group actions
21.111.
Isomorphisms of groups
21.112.
Isomorphisms of monoids
21.113.
Isomorphisms of semigroups
21.114.
Iterated cartesian products of concrete groups
21.115.
Kernels of homomorphisms between abelian groups
21.116.
Kernels of homomorphisms of concrete groups
21.117.
Kernels of homomorphisms of groups
21.118.
Large abelian groups
21.119.
Large commutative monoids
21.120.
Large function abelian groups
21.121.
Large function commutative monoids
21.122.
Large function groups
21.123.
Large function monoids
21.124.
Large function semigroups
21.125.
Large groups
21.126.
Large monoids
21.127.
Large semigroups
21.128.
Concrete automorphism groups on sets
21.129.
Mere equivalences of concrete group actions
21.130.
Mere equivalences of group actions
21.131.
Minkowski multiplication of subsets of a commutative monoid
21.132.
Minkowski multiplication on subsets of a monoid
21.133.
Minkowski multiplication on subsets of a semigroup
21.134.
Monoid actions
21.135.
Monoids
21.136.
Monomorphisms of concrete groups
21.137.
Monomorphisms in the category of groups
21.138.
Multiples of elements in abelian groups
21.139.
Multiples of elements in large abelian groups
21.140.
Nontrivial groups
21.141.
Normal closures of subgroups
21.142.
Normal cores of subgroups
21.143.
Normal subgroups
21.144.
Normal subgroups of concrete groups
21.145.
Normal submonoids
21.146.
Normal submonoids of commutative monoids
21.147.
Normalizer subgroups
21.148.
Nullifying group homomorphisms
21.149.
The opposite of a group
21.150.
The opposite of a semigroup
21.151.
The orbit-stabilizer theorem for concrete groups
21.152.
Orbits of concrete group actions
21.153.
Orbits of group actions
21.154.
The order of an element in a group
21.155.
Perfect cores
21.156.
Perfect groups
21.157.
Perfect subgroups
21.158.
Powers of elements in commutative monoids
21.159.
Powers of elements in groups
21.160.
Powers of elements in large commutative monoids
21.161.
Powers of elements in large groups
21.162.
Powers of elements in large monoids
21.163.
Powers of elements in monoids
21.164.
The precategory of commutative monoids
21.165.
The precategory of concrete groups
21.166.
The precategory of group actions
21.167.
The precategory of groups
21.168.
The precategory of monoids
21.169.
The precategory of orbits of a monoid action
21.170.
The precategory of semigroups
21.171.
Principal group actions
21.172.
Principal torsors of concrete groups
21.173.
Products of elements in a monoid
21.174.
Pullbacks of subgroups
21.175.
Pullbacks of subsemigroups
21.176.
Quotient groups
21.177.
Quotient groups of concrete groups
21.178.
Quotients of abelian groups
21.179.
Rational commutative monoids
21.180.
Representations of monoids in precategories
21.181.
Saturated congruence relations on commutative monoids
21.182.
Saturated congruence relations on monoids
21.183.
Semigroups
21.184.
Sheargroups
21.185.
Shriek of concrete group homomorphisms
21.186.
Stabilizer groups
21.187.
Stabilizers of concrete group actions
21.188.
Subgroups
21.189.
Subgroups of abelian groups
21.190.
Subgroups of concrete groups
21.191.
Subgroups generated by elements of a group
21.192.
Subgroups generated by families of elements
21.193.
Subgroups generated by subsets of groups
21.194.
Submonoids
21.195.
Submonoids of commutative monoids
21.196.
Subsemigroups
21.197.
Subsets of abelian groups
21.198.
Subsets of commutative monoids
21.199.
Subsets of groups
21.200.
Subsets of monoids
21.201.
Subsets of semigroups
21.202.
The substitution functor of concrete group actions
21.203.
The substitution functor of group actions
21.204.
Sums of finite families of elements in abelian groups
21.205.
Sums of finite families of elements in commutative monoids
21.206.
Sums of finite families of elements in commutative semigroups
21.207.
Sums of finite sequences of elements in abelian groups
21.208.
Sums of finite sequences of elements in commutative monoids
21.209.
Sums of finite sequences of elements in commutative semigroups
21.210.
Sums of finite sequences of elements in groups
21.211.
Sums of finite sequences of elements in monoids
21.212.
Sums of finite sequences of elements in semigroups
21.213.
Surjective group homomorphisms
21.214.
Surjective semigroup homomorphisms
21.215.
Symmetric concrete groups
21.216.
Symmetric groups
21.217.
Torsion elements of groups
21.218.
Torsion-free groups
21.219.
Torsors of abstract groups
21.220.
Transitive concrete group actions
21.221.
Transitive group actions
21.222.
Trivial concrete groups
21.223.
Trivial group homomorphisms
21.224.
Trivial groups
21.225.
Trivial subgroups
21.226.
Unordered tuples of elements in commutative monoids
21.227.
Wild representations of monoids
22.
Higher group theory
❱
22.1.
Abelian higher groups
22.2.
Automorphism groups
22.3.
Cartesian products of higher groups
22.4.
Conjugation in higher groups
22.5.
Cyclic higher groups
22.6.
Deloopable groups
22.7.
Deloopable H-spaces
22.8.
Deloopable types
22.9.
Eilenberg-Mac Lane spaces
22.10.
Equivalences of higher groups
22.11.
Fixed points of higher group actions
22.12.
Free higher group actions
22.13.
Higher group actions
22.14.
Higher groups
22.15.
Homomorphisms of higher group actions
22.16.
Homomorphisms of higher groups
22.17.
The higher group of integers
22.18.
Iterated cartesian products of higher groups
22.19.
Iterated deloopings of pointed types
22.20.
Orbits of higher group actions
22.21.
Small ∞-groups
22.22.
Subgroups of higher groups
22.23.
Symmetric higher groups
22.24.
Transitive higher group actions
22.25.
Trivial higher groups
23.
Linear algebra
❱
23.1.
Addition of linear maps between left modules over commutative rings
23.2.
Addition of linear maps between left modules over rings
23.3.
Bilinear forms in real vector spaces
23.4.
Bilinear maps on vector spaces
23.5.
Bilinear maps on left modules over rings
23.6.
The Cauchy-Schwarz inequality for complex inner product spaces
23.7.
The Cauchy-Schwarz inequality on real inner product spaces
23.8.
Complex inner product spaces
23.9.
Complex vector spaces
23.10.
Conjugate symmetric sesquilinear forms in complex vector spaces
23.11.
Constant matrices
23.12.
Diagonal tuples
23.13.
Dependent products of left modules over commutative rings
23.14.
Dependent products of left modules over rings
23.15.
Diagonal matrices on rings
23.16.
The difference of linear maps between left modules over commutative rings
23.17.
The difference of linear maps between left modules over rings
23.18.
The dot product in standard Euclidean vector spaces
23.19.
Duals of left modules over commutative rings
23.20.
Finite sequences in abelian groups
23.21.
Finite sequences in commutative monoids
23.22.
Finite sequences in commutative rings
23.23.
Finite sequences in commutative semigroups
23.24.
Finite sequences in commutative semirings
23.25.
Finite sequences in euclidean domains
23.26.
Finite sequences in groups
23.27.
Finite sequences in monoids
23.28.
Finite sequences in rings
23.29.
Finite sequences in semigroups
23.30.
Finite sequences in semirings
23.31.
Functoriality of the type of matrices
23.32.
Kernels of linear maps between left modules over commutative rings
23.33.
Kernels of linear maps between left modules over rings
23.34.
Kernels of linear maps between vector spaces
23.35.
Large left modules over large rings
23.36.
The left module of linear maps between left modules over commutative rings
23.37.
Left modules over commutative rings
23.38.
Left modules over rings
23.39.
Left submodules over commutative rings
23.40.
Left submodules over rings
23.41.
Linear combinations of tuples of vectors in left modules over rings
23.42.
Linear endomaps on left modules over commutative rings
23.43.
Linear endomaps on left modules of rings
23.44.
Linear endomaps on vector spaces
23.45.
Linear forms in left modules over commutative rings
23.46.
Linear forms in vector spaces
23.47.
Linear maps on left modules over commutative rings
23.48.
Linear maps between left modules over rings
23.49.
Linear maps on vector spaces
23.50.
Linear spans in left modules over rings
23.51.
Matrices
23.52.
Matrices on rings
23.53.
Multiplication of matrices
23.54.
Negation of linear maps between left modules over rings
23.55.
Normed complex vector spaces
23.56.
Normed real vector spaces
23.57.
Orthogonality relative to a bilinear form in a real vector space
23.58.
Orthogonality in real inner product spaces
23.59.
The precategory of left modules over commutative rings
23.60.
The precategory of left modules over a ring
23.61.
The precategory of vector spaces
23.62.
Preimages of left module structures along homomorphisms of rings
23.63.
Rational modules
23.64.
Real inner product spaces
23.65.
Real inner product spaces are normed
23.66.
Real vector spaces
23.67.
Right modules over rings
23.68.
Scalar multiplication of linear maps between left modules over commutative rings
23.69.
Scalar multiplication of linear maps between vector spaces
23.70.
Scalar multiplication on matrices
23.71.
Scalar multiplication of tuples
23.72.
Scalar multiplication of tuples on rings
23.73.
Seminormed complex vector spaces
23.74.
Seminormed real vector spaces
23.75.
Sesquilinear forms in complex vector spaces
23.76.
The standard Euclidean inner product spaces
23.77.
The standard Euclidean vector space
23.78.
Subsets of left modules over commutative rings
23.79.
Subsets of left modules over rings
23.80.
Subspaces of vector spaces
23.81.
Sums of finite sequences of elements in normed real vector spaces
23.82.
Symmetric bilinear forms in real vector spaces
23.83.
Transposition of matrices
23.84.
Tuples on commutative monoids
23.85.
Tuples on commutative rings
23.86.
Tuples on commutative semirings
23.87.
Tuples on euclidean domains
23.88.
Tuples on monoids
23.89.
Tuples on rings
23.90.
Tuples on semirings
23.91.
Vector spaces
24.
Lists
❱
24.1.
Arrays
24.2.
Concatenation of lists
24.3.
Concatenation of tuples
24.4.
Dependent sequences
24.5.
Equivalence relations on tuples
24.6.
The equivalence between tuples and finite sequences
24.7.
Finite sequences
24.8.
Flattening of lists
24.9.
Functoriality of the type of finite sequences
24.10.
Functoriality of the list operation
24.11.
Functoriality of the type of tuples
24.12.
Relationship between functoriality of tuples and finite sequences
24.13.
Lists
24.14.
Lists of elements in discrete types
24.15.
Partial sequences
24.16.
Permutations of lists
24.17.
Permutations of tuples
24.18.
Predicates on lists
24.19.
Quicksort for lists
24.20.
Repetitions in sequences
24.21.
Reversing lists
24.22.
Sequences
24.23.
Set quotients of tuples
24.24.
Shifting sequences
24.25.
Sort by insertion for lists
24.26.
Sort by insertion for tuples
24.27.
Sorted lists
24.28.
Sorted tuples
24.29.
Sorting algorithms for lists
24.30.
Sorting algorithms for tuples
24.31.
Subsequences
24.32.
Tuples
24.33.
The universal property of lists with respect to wild monoids
25.
Logic
❱
25.1.
Cartesian products of double negation stable subtypes
25.2.
Complements of De Morgan subtypes
25.3.
Complements of decidable subtypes
25.4.
Complements of double negation stable subtypes
25.5.
De Morgan embeddings
25.6.
De Morgan maps
25.7.
De Morgan propositions
25.8.
De Morgan subtypes
25.9.
De Morgan types
25.10.
De Morgan's law
25.11.
Dirk Gently's principle
25.12.
Double negation dense maps
25.13.
Double negation dense subtypes of types
25.14.
Double negation eliminating maps
25.15.
Double negation elimination
25.16.
Double negation stable embeddings
25.17.
Double negation stable subtypes
25.18.
Functoriality of existential quantification
25.19.
The impredicative encoding of oracle modalities
25.20.
Intersections of double negation stable subtypes
25.21.
Irrefutable types
25.22.
Markovian types
25.23.
Markov's principle
25.24.
Oracle modalities
25.25.
Oracle reflections
25.26.
Propositional double negation elimination
25.27.
Propositionally decidable maps
25.28.
Propositionally decidable types
25.29.
Propositionally double negation eliminating maps
26.
Metric spaces
❱
26.1.
Accumulation points of subsets of located metric spaces
26.2.
The action on Cauchy sequences of short maps between metric spaces
26.3.
The action on Cauchy sequences of uniformly continuous maps between metric spaces
26.4.
The action on convergent sequences of modulated uniformly continuous maps between metric spaces
26.5.
The action on convergent sequences of short maps between metric spaces
26.6.
The action on convergent sequences of uniformly continuous maps between metric spaces
26.7.
The action on modulated Cauchy sequences of modulated uniformly continuous maps between metric spaces
26.8.
Apartness in located metric spaces
26.9.
Approximations in located metric spaces
26.10.
Approximations in metric spaces
26.11.
The bounded distance decomposition of metric spaces
26.12.
Cartesian products of metric spaces
26.13.
The category of metric spaces and isometries
26.14.
The category of metric spaces and short maps
26.15.
Cauchy approximations in the Cauchy pseudocompletion of a pseudometric space
26.16.
Cauchy approximations in metric quotients of pseudometric spaces
26.17.
Cauchy approximations in metric spaces
26.18.
Cauchy approximations in pseudometric spaces
26.19.
Cauchy pseudocompletions of complete metric space
26.20.
The Cauchy pseudocompletion of a metric space
26.21.
The Cauchy pseudocompletion of a pseudometric space
26.22.
Cauchy sequences in complete metric spaces
26.23.
Cauchy sequences in metric spaces
26.24.
Closed subsets of located metric spaces
26.25.
Closed subsets of metric spaces
26.26.
The closure of subsets of metric spaces
26.27.
Compact metric spaces
26.28.
Complete metric spaces
26.29.
Continuity of maps at points in metric spaces
26.30.
Convergent Cauchy approximations in metric spaces
26.31.
Convergent sequences in metric spaces
26.32.
Dense subsets of metric spaces
26.33.
Dependent products of complete metric spaces
26.34.
Dependent products of metric spaces
26.35.
Discrete metric spaces
26.36.
Distances in located metric spaces
26.37.
Elements at bounded distance in metric spaces
26.38.
ε-δ limits of maps between metric spaces
26.39.
Equality of metric spaces
26.40.
Equality of pseudometric spaces
26.41.
Expansive maps between metric spaces
26.42.
Expansive maps between pseudometric spaces
26.43.
Extensionality of pseudometric spaces
26.44.
The functor from the precategory of metric spaces and isometries to the precategory of sets
26.45.
The inclusion of isometries into the category of metric spaces and short maps
26.46.
Functorial action on isometries of Cauchy pseudocompletions of metric spaces
26.47.
Functorial action on isometries of Cauchy pseudocompletions of pseudometric spaces
26.48.
Functorial action on isometries of metric quotients of pseudometric spaces
26.49.
Functorial action on short maps of Cauchy pseudocompletions of metric spaces
26.50.
Functorial action on short maps of Cauchy pseudocompletions of pseudometric spaces
26.51.
Functorial action on short maps of metric quotients of pseudometric spaces
26.52.
Images of metric spaces under isometries
26.53.
Images of metric spaces
26.54.
Images of metric spaces under short maps
26.55.
Images of metric spaces under uniformly continuous maps
26.56.
Indexed sums of metric spaces
26.57.
Inhabited, totally bounded subspaces of metric spaces
26.58.
The interior of subsets of metric spaces
26.59.
Isometries between metric spaces
26.60.
Isometries between pseudometric spaces
26.61.
Limits of Cauchy approximations in metric spaces
26.62.
Limits of Cauchy approximations in pseudometric spaces
26.63.
Limits of Cauchy sequences in metric spaces
26.64.
Limits of maps between metric spaces
26.65.
Limits of modulated Cauchy sequences in metric spaces
26.66.
Limits of sequences in metric spaces
26.67.
Lipschitz maps between metric spaces
26.68.
Locally constant maps in metric spaces
26.69.
Located metric spaces
26.70.
Maps between metric spaces
26.71.
Maps between pseudometric spaces
26.72.
Metric quotients of metric spaces
26.73.
Metric quotients of pseudometric spaces
26.74.
The metric space of Cauchy approximations in a complete metric space
26.75.
The metric space of Cauchy approximations in a metric space
26.76.
The metric space of convergent Cauchy approximations in a metric space
26.77.
The metric space of convergent sequences in metric spaces
26.78.
The metric space of isometries between metric spaces
26.79.
The metric space of Lipschitz maps between metric spaces
26.80.
The metric space of maps between metric spaces
26.81.
The standard metric space of rational numbers
26.82.
The metric space of sequences in a metric space
26.83.
The metric space of short maps between metric spaces
26.84.
The metric space of uniformly continuous maps between metric spaces
26.85.
Metric spaces
26.86.
Metrics
26.87.
Metrics of metric spaces
26.88.
Metrics of metric spaces are uniformly continuous
26.89.
Modulated Cauchy sequences in complete metric spaces
26.90.
Modulated Cauchy sequences in metric spaces
26.91.
Modulated uniformly continuous maps between metric spaces
26.92.
Monotonic rational neighborhood relations
26.93.
Nets in located metric spaces
26.94.
Nets in metric spaces
26.95.
Open subsets of located metric spaces
26.96.
Open subsets of metric spaces
26.97.
Pointwise continuous maps between metric spaces
26.98.
Pointwise ε-δ continuous maps between metric spaces
26.99.
The poset of rational neighborhood relations on a type
26.100.
The precategory of metric spaces and isometries
26.101.
The precategory of metric spaces and maps
26.102.
The precategory of metric spaces and short maps
26.103.
Preimages of rational neighborhood relations along maps
26.104.
Pseudometric spaces
26.105.
Rational approximations of zero
26.106.
Rational Cauchy approximations
26.107.
Rational neighborhood relations
26.108.
Rational sequences approximating zero
26.109.
Reflexive rational neighborhood relations
26.110.
Saturated rational neighborhood relations
26.111.
Sequences in metric spaces
26.112.
Short maps between metric spaces
26.113.
Short maps between pseudometric spaces
26.114.
Similarity of elements in pseudometric spaces
26.115.
Subspaces of metric spaces
26.116.
Symmetric rational neighborhood relations
26.117.
Totally bounded metric spaces
26.118.
Totally bounded subspaces of metric spaces
26.119.
Triangular rational neighborhood relations
26.120.
Uniform homeomorphisms between metric spaces
26.121.
The uniform limit theorem for pointwise continuous maps between metric spaces
26.122.
The uniform limit theorem for uniformly continuous maps between metric spaces
26.123.
Uniformly continuous maps between metric spaces
26.124.
The unit map of metric quotients of pseudometric spaces
26.125.
Universal property of metric quotients of pseudometric spaces and isometries
26.126.
Universal property of metric quotients of pseudometric spaces and short maps
27.
Modal type theory
❱
27.1.
The action on homotopies of the flat modality
27.2.
The action on identifications of crisp functions
27.3.
The action on identifications of the flat modality
27.4.
Crisp cartesian product types
27.5.
Crisp coproduct types
27.6.
Crisp dependent function types
27.7.
Crisp dependent pair types
27.8.
Crisp function types
27.9.
Crisp identity types
27.10.
The crisp law of excluded middle
27.11.
Crisp pullbacks
27.12.
Crisp types
27.13.
Dependent universal property of flat discrete crisp types
27.14.
Flat discrete crisp types
27.15.
The flat modality
27.16.
The flat-sharp adjunction
27.17.
Functoriality of the flat modality
27.18.
Functoriality of the sharp modality
27.19.
Sharp codiscrete maps
27.20.
Sharp codiscrete types
27.21.
The sharp modality
27.22.
Transport along crisp identifications
27.23.
The universal property of flat discrete crisp types
28.
Order theory
❱
28.1.
Accessible elements with respect to relations
28.2.
Bottom elements in large posets
28.3.
Bottom elements in posets
28.4.
Bottom elements in preorders
28.5.
Chains in posets
28.6.
Chains in preorders
28.7.
Closed interval preserving maps between posets
28.8.
Closed interval preserving maps between total orders
28.9.
Closed intervals in large posets
28.10.
Closed intervals in lattices
28.11.
Closed intervals in posets
28.12.
Closed intervals in total orders
28.13.
Closure operators on large locales
28.14.
Closure operators on large posets
28.15.
Cofinal maps in posets
28.16.
Coinitial maps in posets
28.17.
Commuting squares of Galois connections between large posets
28.18.
Commuting squares of order preserving maps of large posets
28.19.
Coverings in locales
28.20.
Decidable posets
28.21.
Decidable preorders
28.22.
Decidable subposets
28.23.
Decidable subpreorders
28.24.
Decidable total orders
28.25.
Decidable total preorders
28.26.
Decreasing sequences in posets
28.27.
Deflationary maps on a poset
28.28.
Deflationary maps on a preorder
28.29.
Dependent products of large frames
28.30.
Dependent products of large inflattices
28.31.
Dependent products of large locales
28.32.
Dependent products of large meet-semilattices
28.33.
Dependent products of large posets
28.34.
Dependent products of large preorders
28.35.
Dependent products of large suplattices
28.36.
Distributive lattices
28.37.
Filters on posets
28.38.
Finite coverings in locales
28.39.
Finite posets
28.40.
Finite preorders
28.41.
Finite total orders
28.42.
Finitely graded posets
28.43.
Frames
28.44.
Galois connections
28.45.
Galois connections between large posets
28.46.
Greatest lower bounds in large posets
28.47.
Greatest lower bounds in posets
28.48.
Homomorphisms of frames
28.49.
Homomorphisms of large frames
28.50.
Homomorphisms of large locales
28.51.
Homomorphisms of large meet-semilattices
28.52.
Homomorphisms of large suplattices
28.53.
Homomorphisms of meet-semilattices
28.54.
Homomorphisms of meet-suplattices
28.55.
Homomorphisms of suplattices
28.56.
Ideals in preorders
28.57.
Incidence algebras
28.58.
Increasing sequences in partially ordered sets
28.59.
Inflationary maps on a poset
28.60.
Inflationary maps on a preorder
28.61.
Inflattices
28.62.
Inhabited chains in posets
28.63.
Inhabited chains in preorders
28.64.
Inhabited finite total orders
28.65.
Intersections of closed intervals in lattices
28.66.
Intersections of closed intervals in total orders
28.67.
Interval subposets
28.68.
Join preserving maps between posets
28.69.
Join-semilattices
28.70.
Joins of finite families of elements in join-semilattices
28.71.
Joins of finite families in large join semilattices
28.72.
The Knaster–Tarski fixed point theorem
28.73.
Large frames
28.74.
Large inflattices
28.75.
Large join-semilattices
28.76.
Large locales
28.77.
Large meet-semilattices
28.78.
Large meet-subsemilattices
28.79.
Large posets
28.80.
Large preorders
28.81.
Large quotient locales
28.82.
Large strict orders
28.83.
Large strict preorders
28.84.
Large subframes
28.85.
Large subposets
28.86.
Large subpreorders
28.87.
Large subsuplattices
28.88.
Large suplattices
28.89.
Lattices
28.90.
Least upper bounds in large posets
28.91.
Least upper bounds in posets
28.92.
Locales
28.93.
Locally finite posets
28.94.
Lower bounds in large posets
28.95.
Lower bounds in posets
28.96.
Lower sets in large posets
28.97.
Lower types in preorders
28.98.
Maximal chains in posets
28.99.
Maximal chains in preorders
28.100.
Meet-semilattices
28.101.
Meet-suplattices
28.102.
Meets of finite families of elements in meet-semilattices
28.103.
Nuclei on large locales
28.104.
Opposite large posets
28.105.
Opposite large preorders
28.106.
Opposite posets
28.107.
Opposite preorders
28.108.
Order preserving maps between large posets
28.109.
Order preserving maps between large preorders
28.110.
Order preserving maps between posets
28.111.
Order preserving maps between preorders
28.112.
Order preserving maps between total orders
28.113.
Ordinals
28.114.
The poset of closed intervals in lattices
28.115.
The poset of closed intervals in posets
28.116.
The poset of closed intervals in total orders
28.117.
Posets
28.118.
Powers of large locales
28.119.
The precategory of decidable total orders
28.120.
The precategory of finite posets
28.121.
The precategory of finite total orders
28.122.
The precategory of inhabited finite total orders
28.123.
The precategory of posets
28.124.
The precategory of total orders
28.125.
Preorders
28.126.
Principal lower sets of large posets
28.127.
Principal upper sets of large posets
28.128.
Reflective Galois connections between large posets
28.129.
Resizing posets
28.130.
Resizing preorders
28.131.
Resizing suplattices
28.132.
Sequences in partially ordered sets
28.133.
Sequences in preorders
28.134.
Sequences in strictly preordered sets
28.135.
Similarity of elements in large posets
28.136.
Similarity of elements in large preorders
28.137.
Similarity of elements in large strict orders
28.138.
Similarity of elements in large strict preorders
28.139.
Similarity of elements in posets
28.140.
Similarity of elements in preorders
28.141.
Similarity of elements in strict orders
28.142.
Similarity of elements in strict preorders
28.143.
Similarity of order preserving maps between large posets
28.144.
Similarity of order preserving maps between large preorders
28.145.
Spans of closed intervals in total orders
28.146.
Strict order preserving maps
28.147.
Strict orders
28.148.
Strict preorders
28.149.
Strict subpreorders
28.150.
Strictly increasing sequences in strictly preordered sets
28.151.
Strictly inflationary maps on a strictly preordered type
28.152.
Strictly preordered sets
28.153.
Subposets
28.154.
Subpreorders
28.155.
Suplattices
28.156.
Supremum preserving maps between posets
28.157.
Top elements in large posets
28.158.
Top elements in posets
28.159.
Top elements in preorders
28.160.
Total orders
28.161.
Total preorders
28.162.
Transitive well-founded relations
28.163.
Transposing inequalities in posets along order-preserving retractions
28.164.
Transposing inequalities in posets along sections of order-preserving maps
28.165.
Upper bounds of chains in posets
28.166.
Upper bounds in large posets
28.167.
Upper bounds in posets
28.168.
Upper sets of large posets
28.169.
Well-founded relations
28.170.
Zorn's lemma
29.
Organic chemistry
❱
29.1.
Alcohols
29.2.
Alkanes
29.3.
Alkenes
29.4.
Alkynes
29.5.
Ethane
29.6.
Hydrocarbons
29.7.
Methane
29.8.
Saturated carbons
30.
Orthogonal factorization systems
❱
30.1.
Anodyne maps
30.2.
Cd-structures
30.3.
Cellular maps
30.4.
The closed modalities
30.5.
K-Connected maps, with respect to a subuniverse K
30.6.
K-connected maps over a type, with respect to a subuniverse K
30.7.
K-Connected types, with respect to a subuniverse K
30.8.
Continuation modalities
30.9.
Coproducts of null types
30.10.
Double lifts of families of elements
30.11.
Double negation sheaves
30.12.
Equality of extensions of dependent maps
30.13.
Equality of extensions of maps
30.14.
K-Equivalences, with respect to a subuniverse K
30.15.
Extensions of dependent maps
30.16.
Extensions of double lifts of families of elements
30.17.
Extensions of families of elements
30.18.
Extensions of maps
30.19.
Factorization operations
30.20.
Factorization operations into function classes
30.21.
Factorization operations into global function classes
30.22.
Factorizations of maps
30.23.
Factorizations of maps into function classes
30.24.
Factorizations of maps into global function classes
30.25.
Families of types local at a map
30.26.
Fiberwise orthogonal maps
30.27.
Function classes
30.28.
Functoriality of higher modalities
30.29.
Functoriality of localizations at global subuniverses
30.30.
Functoriality of the pullback-hom
30.31.
Functoriality of reflective global subuniverses
30.32.
Global function classes
30.33.
Higher modalities
30.34.
The identity modality
30.35.
Large Lawvere–Tierney topologies
30.36.
Lawvere–Tierney topologies
30.37.
Lifting operations
30.38.
Lifting structures on commuting squares of maps
30.39.
Lifts of families of elements
30.40.
Lifts of maps
30.41.
Localizations at global subuniverses
30.42.
Localizations at maps
30.43.
Localizations at subuniverses
30.44.
Locally small modal-operators
30.45.
Maps local at maps
30.46.
Mere lifting properties
30.47.
Modal induction
30.48.
Modal operators
30.49.
Modal subuniverse induction
30.50.
Null families of types
30.51.
Null maps
30.52.
Null types
30.53.
The open modalities
30.54.
Orthogonal factorization systems
30.55.
Orthogonal maps
30.56.
Postcomposition of extensions of maps
30.57.
Precomposition of lifts of families of elements by maps
30.58.
The pullback-hom
30.59.
The raise modalities
30.60.
Reflective global subuniverses
30.61.
Reflective modalities
30.62.
Reflective subuniverses
30.63.
Regular cd-structures
30.64.
Σ-closed modalities
30.65.
Σ-closed reflective modalities
30.66.
Σ-closed reflective subuniverses
30.67.
Stable orthogonal factorization systems
30.68.
Types colocal at maps
30.69.
Types local at maps
30.70.
Types separated at maps
30.71.
Uniquely eliminating modalities
30.72.
The universal property of localizations at global subuniverses
30.73.
Weakly anodyne maps
30.74.
Wide function classes
30.75.
Wide global function classes
30.76.
The zero modality
31.
Polytopes
❱
31.1.
Abstract polytopes
32.
Primitives
❱
32.1.
Characters
32.2.
Floats
32.3.
Machine integers
32.4.
Strings
33.
Real numbers
❱
33.1.
Absolute value on closed intervals in the real numbers
33.2.
The absolute value of real numbers
33.3.
Accumulation points of subsets of the real numbers
33.4.
Addition of lower Dedekind real numbers
33.5.
Addition of negative real numbers
33.6.
Addition of nonnegative real numbers
33.7.
Addition of nonzero real numbers
33.8.
Addition of positive, negative, and nonnegative real numbers
33.9.
Addition of positive real numbers
33.10.
Addition of Dedekind real numbers
33.11.
Addition of upper Dedekind real numbers
33.12.
Alternation of sequences of real numbers
33.13.
Apartness of real numbers
33.14.
Arithmetically located Dedekind cuts
33.15.
The binary maximum of nonnegative real numbers
33.16.
The binary maximum of real numbers
33.17.
The binary mean of real numbers
33.18.
The binary minimum of nonnegative real numbers
33.19.
The binary minimum of real numbers
33.20.
Cauchy completeness of the Dedekind real numbers
33.21.
Cauchy sequences in the real numbers
33.22.
Closed intervals in the real numbers
33.23.
Cofinal and coinitial endomaps on the real numbers
33.24.
Cofinal and coinitial, strictly increasing, pointwise ε-δ continuous endomaps on the real numbers
33.25.
Decreasing sequences in the real numbers
33.26.
Dedekind real numbers
33.27.
Dense subsets of the real numbers
33.28.
The density of rational numbers in proper closed intervals of real numbers
33.29.
The difference between real numbers
33.30.
The distance between real numbers
33.31.
Enclosing closed rational intervals of Dedekind real numbers
33.32.
Equality of real numbers
33.33.
Extensionality of multiplication of real numbers as a bilinear form
33.34.
The field of real numbers
33.35.
Finitely enumerable subsets of the real numbers
33.36.
Geometric sequences of real numbers
33.37.
Increasing endomaps on the real numbers
33.38.
Increasing pointwise ε-δ continuous endomaps on the real numbers
33.39.
Increasing sequences in the real numbers
33.40.
Inequalities about addition and subtraction on the real numbers
33.41.
Inequality on the lower Dedekind real numbers
33.42.
Inequality on the MacNeille real numbers
33.43.
Inequality of nonnegative real numbers
33.44.
Inequality of positive real numbers
33.45.
Inequality on the real numbers
33.46.
Inequality on the upper Dedekind real numbers
33.47.
Infima and suprema of families of real numbers
33.48.
Infima of families of real numbers
33.49.
Inhabited finitely enumerable subsets of the real numbers
33.50.
Inhabited totally bounded subsets of the real numbers
33.51.
Integer powers of positive real numbers
33.52.
Irrational real numbers
33.53.
The irrationality of the square root of two
33.54.
The addition isometry on real numbers
33.55.
The difference isometry on real numbers
33.56.
The negation isometry on real numbers
33.57.
Iterated halving of the difference between real numbers
33.58.
The large additive group of Dedekind real numbers
33.59.
The large multiplicative group of positive real numbers
33.60.
The large multiplicative monoid of Dedekind real numbers
33.61.
The large ring of Dedekind real numbers
33.62.
Limits of endomaps on the real numbers
33.63.
Limits of sequences in the real numbers
33.64.
Multiplication of real numbers is Lipschitz continuous
33.65.
The local ring of Dedekind real numbers
33.66.
The located metric space of real numbers
33.67.
Lower Dedekind real numbers
33.68.
MacNeille real numbers
33.69.
The maximum of finite families of nonnegative real numbers
33.70.
The maximum of finite families of real numbers
33.71.
The maximum of inhabited, finitely enumerable subsets of real numbers
33.72.
The maximum of lower Dedekind real numbers
33.73.
The maximum of upper Dedekind real numbers
33.74.
The metric abelian group of real numbers
33.75.
The metric space of functions into the real numbers
33.76.
The metric space of nonnegative real numbers
33.77.
The metric space of real numbers
33.78.
The minimum of finite families of real numbers
33.79.
The minimum of inhabited, finitely enumerable subsets of real numbers
33.80.
The minimum of lower Dedekind real numbers
33.81.
The minimum of upper Dedekind real numbers
33.82.
Modulated Cauchy sequences in the real numbers
33.83.
Modulated suprema of families of real numbers
33.84.
Multiplication of negative real numbers
33.85.
Multiplication of nonnegative real numbers
33.86.
Multiplication of nonzero real numbers
33.87.
Multiplication by positive, negative, and nonnegative real numbers
33.88.
Multiplication of positive real numbers
33.89.
Multiplication of real numbers
33.90.
Multiplicative inverses of negative real numbers
33.91.
Multiplicative inverses of nonzero real numbers
33.92.
Multiplicative inverses of positive real numbers
33.93.
Negation of lower and upper Dedekind real numbers
33.94.
Negation of real numbers
33.95.
Negative real numbers
33.96.
Nonnegative real numbers
33.97.
Nonpositive real numbers
33.98.
Nonzero real numbers
33.99.
Nonzero roots of nonnegative real numbers
33.100.
Odd roots of real numbers
33.101.
Pointwise continuous endomaps on the real numbers
33.102.
Pointwise ε-δ continuous endomaps on the real numbers
33.103.
Positive and negative real numbers
33.104.
Positive proper closed intervals in the real numbers
33.105.
Positive real numbers
33.106.
Powers of real numbers
33.107.
Proper closed intervals in the real numbers
33.108.
Raising universe levels of lower Dedekind real numbers
33.109.
Raising the universe levels of real numbers
33.110.
Raising universe levels of upper Dedekind real numbers
33.111.
Rational approximates of real numbers
33.112.
Rational lower Dedekind real numbers
33.113.
Rational real numbers
33.114.
Rational upper Dedekind real numbers
33.115.
Real numbers from lower Dedekind real numbers
33.116.
Real numbers from upper Dedekind real numbers
33.117.
Real sequences approximating zero
33.118.
Saturation of inequality of nonnegative real numbers
33.119.
Saturation of inequality of real numbers
33.120.
Sequences with alternating signs in the real numbers
33.121.
The binary maximum of real numbers is a short map
33.122.
The binary minimum of real numbers is a short map
33.123.
Similarity of nonnegative real numbers
33.124.
Similarity of positive real numbers
33.125.
Similarity of real numbers
33.126.
Square roots of nonnegative real numbers
33.127.
Squares of real numbers
33.128.
Strict inequalities about addition and subtraction on the real numbers
33.129.
Strict inequality of nonnegative real numbers
33.130.
Strict inequality of positive real numbers
33.131.
Strict inequality of real numbers
33.132.
Strictly increasing endomaps on the real numbers
33.133.
Strictly increasing pointwise ε-δ continuous endomaps on the real numbers
33.134.
Subsets of the real numbers
33.135.
Sums of finite sequences of nonnegative real numbers
33.136.
Sums of finite sequences of real numbers
33.137.
Suprema of families of real numbers
33.138.
Totally bounded subsets of the real numbers
33.139.
Transposition of addition and subtraction through cuts of Dedekind real numbers
33.140.
A uniform homeomorphism between the unit interval and a proper closed interval in the real numbers
33.141.
Uniformly continuous endomaps on the real numbers
33.142.
Uniformly continuous real functions on proper closed intervals of real numbers
33.143.
The unit closed interval in the real numbers
33.144.
Upper Dedekind real numbers
33.145.
Zero nonnegative real numbers
33.146.
Zero real numbers
34.
Reflection
❱
34.1.
Abstractions
34.2.
Arguments
34.3.
Boolean reflection
34.4.
Definitions
34.5.
Erasing equality
34.6.
Fixity
34.7.
Group solver
34.8.
Literals
34.9.
Metavariables
34.10.
Names
34.11.
Precategory solver
34.12.
Rewriting
34.13.
Terms
34.14.
The type checking monad
35.
Ring theory
❱
35.1.
Additive orders of elements of rings
35.2.
Arithmetic sequences in semirings
35.3.
Arithmetic series in semirings
35.4.
The binomial theorem for rings
35.5.
The binomial theorem for semirings
35.6.
The category of cyclic rings
35.7.
The category of rings
35.8.
Central elements of rings
35.9.
Central elements of semirings
35.10.
Characteristics of rings
35.11.
Commuting elements of rings
35.12.
Congruence relations on rings
35.13.
Congruence relations on semirings
35.14.
Cyclic rings
35.15.
Dependent products of ring extensions of the rational numbers
35.16.
Dependent products of rings
35.17.
Dependent products of semirings
35.18.
Division rings
35.19.
The free ring with one generator
35.20.
Full ideals of rings
35.21.
Function rings
35.22.
Function semirings
35.23.
Generating elements of rings
35.24.
Geometric sequences in rings
35.25.
Geometric sequences in semirings
35.26.
The group of multiplicative units of a ring
35.27.
Homomorphisms of cyclic rings
35.28.
Homomorphisms of ring extensions of the rational numbers
35.29.
Homomorphisms of rings
35.30.
Homomorphisms of semirings
35.31.
Ideals generated by subsets of rings
35.32.
Ideals of rings
35.33.
Ideals of semirings
35.34.
Idempotent elements in rings
35.35.
Initial rings
35.36.
Integer multiples of elements of rings
35.37.
Intersections of ideals of rings
35.38.
Intersections of ideals of semirings
35.39.
The invariant basis property of rings
35.40.
Invertible elements in rings
35.41.
Isomorphisms of rings
35.42.
Joins of ideals of rings
35.43.
Joins of left ideals of rings
35.44.
Joins of right ideals of rings
35.45.
Kernels of ring homomorphisms
35.46.
Large function rings
35.47.
Large rings
35.48.
Left ideals generated by subsets of rings
35.49.
Left ideals of rings
35.50.
Local rings
35.51.
Localizations of rings
35.52.
Maximal ideals of rings
35.53.
Multiples of elements in rings
35.54.
Multiples of elements in semirings
35.55.
Multiplicative orders of elements of rings
35.56.
Nil ideals of rings
35.57.
Nilpotent elements in rings
35.58.
Nilpotent elements in semirings
35.59.
Nontrivial rings
35.60.
Nonunital left algebras over rings
35.61.
Opposite ring extensions of the rational numbers
35.62.
Opposite rings
35.63.
Partial sums of sequences in semirings
35.64.
The poset of cyclic rings
35.65.
The poset of ideals of a ring
35.66.
The poset of left ideals of a ring
35.67.
The poset of right ideals of a ring
35.68.
Powers of elements in large rings
35.69.
Powers of elements in rings
35.70.
Powers of elements in semirings
35.71.
The precategory of rings
35.72.
The precategory of semirings
35.73.
Products of ideals of rings
35.74.
Products of left ideals of rings
35.75.
Products of right ideals of rings
35.76.
Products of rings
35.77.
Products of subsets of rings
35.78.
Quotient rings
35.79.
Radical ideals of rings
35.80.
Right ideals generated by subsets of rings
35.81.
Right ideals of rings
35.82.
Ring extensions of the rational numbers
35.83.
Rings
35.84.
Semirings
35.85.
Subrings
35.86.
Subsets of rings
35.87.
Subsets of semirings
35.88.
Sums of finite families of elements in rings
35.89.
Sums of finite families of elements in semirings
35.90.
Sums of finite sequences in rings
35.91.
Sums of finite sequences in semirings
35.92.
Transporting ring structures along isomorphisms of abelian groups
35.93.
Trivial rings
36.
Set theory
❱
36.1.
Baire space
36.2.
Bounded increasing binary sequences
36.3.
Cantor space
36.4.
Cantor's diagonal argument
36.5.
Cardinality-projective sets
36.6.
Cardinality-recursive sets
36.7.
Cardinals
36.8.
Complemented inequality on cardinals
36.9.
Countable sets
36.10.
Cumulative hierarchy
36.11.
Dependent products of cardinals
36.12.
Dependent sums of cardinals
36.13.
Equality of cardinals
36.14.
Finite elements in the type of increasing binary sequences
36.15.
The canonical inclusion of natural numbers into increasing binary sequences
36.16.
The type of increasing binary sequences
36.17.
Inequality on cardinals
36.18.
Inequality of increasing binary sequences
36.19.
Infinite sets
36.20.
Inhabited cardinals
36.21.
Positive elements in the type of increasing binary sequences
36.22.
Russell's paradox
36.23.
Strict lower bounds on increasing binary sequences
36.24.
Uncountable sets
36.25.
The zero cardinal
37.
Species
❱
37.1.
Cartesian exponents of species of types
37.2.
Cartesian products of species of types
37.3.
Cauchy composition of species of types
37.4.
Cauchy composition of species of types in subuniverses
37.5.
Cauchy exponentials of species of types
37.6.
Cauchy exponentials of species of types in subuniverses
37.7.
Cauchy products of species of types
37.8.
Cauchy products of species of types in subuniverses
37.9.
Cauchy series of species of types
37.10.
Cauchy series of species of types in subuniverses
37.11.
Composition of Cauchy series of species of types
37.12.
Composition of Cauchy series of species of types in subuniverses
37.13.
Coproducts of species of types
37.14.
Coproducts of species of types in subuniverses
37.15.
Cycle index series of species
37.16.
Derivatives of species
37.17.
Dirichlet exponentials of a species of types
37.18.
Dirichlet exponentials of species of types in subuniverses
37.19.
Dirichlet products of species of types
37.20.
Dirichlet products of species of types in subuniverses
37.21.
Dirichlet series of species of finite inhabited types
37.22.
Dirichlet series of species of types
37.23.
Dirichlet series of species of types in subuniverses
37.24.
Equivalences of species of types
37.25.
Equivalences of species of types in subuniverses
37.26.
Exponential of Cauchy series of species of types
37.27.
Exponential of Cauchy series of species of types in subuniverses
37.28.
Hasse-Weil species
37.29.
Morphisms of finite species
37.30.
Morphisms of species of types
37.31.
Pointing of species of types
37.32.
The precategory of finite species
37.33.
Products of Cauchy series of species of types
37.34.
Products of Cauchy series of species of types in subuniverses
37.35.
Products of Dirichlet series of species of finite inhabited types
37.36.
Products of Dirichlet series of species of types
37.37.
Products of Dirichlet series of species of types in subuniverses
37.38.
Small Composition of species of finite inhabited types
37.39.
Small Cauchy composition of species types in subuniverses
37.40.
Species of finite inhabited types
37.41.
Species of finite types
37.42.
Species of inhabited types
37.43.
Species of types
37.44.
Species of types in subuniverses
37.45.
The unit of Cauchy composition of species of types
37.46.
The unit of Cauchy composition of species of types in subuniverses
37.47.
Unlabeled structures of finite species
38.
Spectral theory
❱
38.1.
Eigenmodules of linear endomaps of left modules over commutative rings
38.2.
Eigenspaces of linear endomaps of vector spaces
38.3.
Eigenvalues and eigenelements of linear endomaps of left modules over commutative rings
38.4.
Eigenvalues and eigenvectors of linear endomaps of vector spaces
39.
Structured types
❱
39.1.
Cartesian products of types equipped with endomorphisms
39.2.
Central H-spaces
39.3.
Commuting squares of pointed homotopies
39.4.
Commuting squares of pointed maps
39.5.
Commuting triangles of pointed maps
39.6.
Conjugation of pointed types
39.7.
Constant pointed maps
39.8.
Contractible pointed types
39.9.
Cyclic types
39.10.
Dependent products of H-spaces
39.11.
Dependent products of pointed types
39.12.
Dependent products of wild monoids
39.13.
Dependent types equipped with automorphisms
39.14.
Equivalences of H-spaces
39.15.
Equivalences of pointed arrows
39.16.
Equivalences of retractive types
39.17.
Equivalences of types equipped with automorphisms
39.18.
Equivalences of types equipped with endomorphisms
39.19.
Faithful pointed maps
39.20.
Fibers of pointed maps
39.21.
Finite multiplication in magmas
39.22.
Function H-spaces
39.23.
Function magmas
39.24.
Function wild monoids
39.25.
H-spaces
39.26.
The initial pointed type equipped with an automorphism
39.27.
The involutive type of H-space structures on a pointed type
39.28.
Involutive types
39.29.
Iterated cartesian products of types equipped with endomorphisms
39.30.
Iterated cartesian products of pointed types
39.31.
Magmas
39.32.
Medial magmas
39.33.
Mere equivalences of types equipped with endomorphisms
39.34.
Morphisms of H-spaces
39.35.
Morphisms of magmas
39.36.
Morphisms of pointed arrows
39.37.
Morphisms of retractive types
39.38.
Morphisms of twisted pointed arrows
39.39.
Morphisms of types equipped with automorphisms
39.40.
Morphisms of types equipped with endomorphisms
39.41.
Morphisms of wild monoids
39.42.
Noncoherent H-spaces
39.43.
Opposite pointed spans
39.44.
Pointed 2-homotopies
39.45.
Pointed cartesian product types
39.46.
Pointed dependent functions
39.47.
Pointed dependent pair types
39.48.
Pointed equivalences
39.49.
Pointed families of types
39.50.
Pointed homotopies
39.51.
Pointed isomorphisms
39.52.
Pointed maps
39.53.
Pointed retractions of pointed maps
39.54.
Pointed sections of pointed maps
39.55.
Pointed span diagrams
39.56.
Pointed spans
39.57.
Pointed type duality
39.58.
Pointed types
39.59.
Pointed types equipped with automorphisms
39.60.
The pointed unit type
39.61.
Universal property of contractible types with respect to pointed types and maps
39.62.
Postcomposition of pointed maps
39.63.
Precomposition of pointed maps
39.64.
Products of magmas
39.65.
Retractive types
39.66.
Sets equipped with automorphisms
39.67.
Small pointed types
39.68.
Symmetric elements of involutive types
39.69.
Symmetric H-spaces
39.70.
Transposition of pointed span diagrams
39.71.
Types equipped with automorphisms
39.72.
Types equipped with endomorphisms
39.73.
Uniform pointed homotopies
39.74.
The universal property of pointed equivalences
39.75.
Unpointed maps between pointed types
39.76.
Whiskering pointed homotopies with respect to concatenation
39.77.
Whiskering of pointed homotopies with respect to composition of pointed maps
39.78.
The wild category of pointed types
39.79.
Wild groups
39.80.
Wild loops
39.81.
Wild monoids
39.82.
Wild quasigroups
39.83.
Wild semigroups
40.
Synthetic category theory
❱
40.1.
Cone diagrams of synthetic categories
40.2.
Cospans of synthetic categories
40.3.
Equivalences between synthetic categories
40.4.
Invertible functors between synthetic categories
40.5.
Pullbacks of synthetic categories
40.6.
Retractions of functors between synthetic categories
40.7.
Sections of functor between synthetic categories
40.8.
Synthetic categories
41.
Synthetic homotopy theory
❱
41.1.
0-acyclic maps
41.2.
0-acyclic types
41.3.
1-acyclic types
41.4.
Acyclic maps
41.5.
Acyclic types
41.6.
The category of connected set bundles over the circle
41.7.
Cavallo's trick
41.8.
The circle
41.9.
Cocartesian morphisms of arrows
41.10.
Cocones under pointed span diagrams
41.11.
Cocones under sequential diagrams
41.12.
Cocones under spans
41.13.
Codiagonals of maps
41.14.
Coequalizers
41.15.
Cofibers of maps
41.16.
Cofibers of pointed maps
41.17.
Coforks
41.18.
Correspondence between cocones under sequential diagrams and certain coforks
41.19.
Composition of cospans
41.20.
Conjugation of loops
41.21.
Connected set bundles over the circle
41.22.
Connective prespectra
41.23.
Connective spectra
41.24.
Dependent cocones under sequential diagrams
41.25.
Dependent cocones under spans
41.26.
Dependent coforks
41.27.
Dependent descent for the circle
41.28.
The dependent pullback property of pushouts
41.29.
Dependent pushout-products
41.30.
Dependent sequential diagrams
41.31.
Dependent suspension structures
41.32.
The dependent universal property of coequalizers
41.33.
The dependent universal property of pushouts
41.34.
The dependent universal property of sequential colimits
41.35.
Dependent universal property of suspensions
41.36.
Descent for the circle
41.37.
Descent data for constant type families over the circle
41.38.
Descent data for families of dependent pair types over the circle
41.39.
Descent data for families of equivalence types over the circle
41.40.
Descent data for families of function types over the circle
41.41.
Subtypes of descent data for the circle
41.42.
Descent data for type families of equivalence types over pushouts
41.43.
Descent data for type families of function types over pushouts
41.44.
Descent data for type families of identity types over pushouts
41.45.
Descent data for pushouts
41.46.
Descent data for sequential colimits
41.47.
Descent for pushouts
41.48.
Descent for sequential colimits
41.49.
Double loop spaces
41.50.
The Eckmann-Hilton argument
41.51.
Equifibered sequential diagrams
41.52.
Equifibered span diagrams
41.53.
Equivalences of cocones under sequential diagrams
41.54.
Equivalences of coforks under equivalences of double arrows
41.55.
Equivalances of dependent sequential diagrams
41.56.
Equivalences of descent data for pushouts
41.57.
Equivalences of equifibered span diagrams
41.58.
Equivalences of sequential diagrams
41.59.
Families with descent data for pushouts
41.60.
Families with descent data for sequential colimits
41.61.
The flattening lemma for coequalizers
41.62.
The flattening lemma for pushouts
41.63.
The flattening lemma for sequential colimits
41.64.
Free loops
41.65.
Functoriality of the loop space operation
41.66.
Functoriality of sequential colimits
41.67.
Functoriality of suspensions
41.68.
Groups of loops in 1-types
41.69.
Hatcher's acyclic type
41.70.
Homotopy groups
41.71.
Identity systems of descent data for pushouts
41.72.
The induction principle of pushouts
41.73.
The infinite dimensional complex projective space
41.74.
Infinite cyclic types
41.75.
The infinite dimensional real projective space
41.76.
The interval
41.77.
Iterated loop spaces
41.78.
Iterated suspensions of pointed types
41.79.
Join powers of types
41.80.
Joins of maps
41.81.
Joins of types
41.82.
Left half-smash products
41.83.
The loop homotopy on the circle
41.84.
Loop spaces
41.85.
Maps of prespectra
41.86.
Mather's second cube theorem
41.87.
Mere spheres
41.88.
Morphisms of cocones under morphisms of sequential diagrams
41.89.
Morphisms of coforks under morphisms of double arrows
41.90.
Morphisms of dependent sequential diagrams
41.91.
Morphisms of descent data of the circle
41.92.
Morphisms of descent data for pushouts
41.93.
Morphisms of sequential diagrams
41.94.
The multiplication operation on the circle
41.95.
Null cocones under pointed span diagrams
41.96.
The plus-principle
41.97.
Powers of loops
41.98.
Premanifolds
41.99.
Prespectra
41.100.
The pullback property of pushouts
41.101.
Pushout-products
41.102.
Pushouts
41.103.
Pushouts of pointed types
41.104.
The recursion principle of pushouts
41.105.
Retracts of sequential diagrams
41.106.
Rewriting rules for pushouts
41.107.
Sections of families over the circle
41.108.
Sections of descent data for pushouts
41.109.
Sequential colimits
41.110.
Sequential diagrams
41.111.
Sequentially compact types
41.112.
Shifts of sequential diagrams
41.113.
Smash products of pointed types
41.114.
Spectra
41.115.
The sphere prespectrum
41.116.
Spheres
41.117.
Suspension prespectra
41.118.
Suspension Structures
41.119.
Suspensions of pointed types
41.120.
Suspensions of propositions
41.121.
Suspensions of types
41.122.
Tangent spheres
41.123.
Total cocones of type families over cocones under sequential diagrams
41.124.
Total sequential diagrams of dependent sequential diagrams
41.125.
Triple loop spaces
41.126.
k-acyclic maps
41.127.
k-acyclic types
41.128.
The universal cover of the circle
41.129.
The universal property of the circle
41.130.
The universal property of coequalizers
41.131.
The universal property of pushouts
41.132.
The universal property of sequential colimits
41.133.
Universal property of suspensions
41.134.
Universal Property of suspensions of pointed types
41.135.
Wedges of pointed types
41.136.
The Whitehead principle for maps
41.137.
The Whitehead principle for types
41.138.
Zigzags between sequential diagrams
42.
Trees
❱
42.1.
Algebras for polynomial endofunctors
42.2.
Bases of directed trees
42.3.
Bases of enriched directed trees
42.4.
Binary W-types
42.5.
Bounded multisets
42.6.
Cartesian morphisms of polynomial endofunctors
42.7.
Cartesian natural transformations between polynomial endofunctors
42.8.
Cartesian product polynomial endofunctors
42.9.
The coalgebra of directed trees
42.10.
The coalgebra of enriched directed trees
42.11.
Coalgebras of polynomial endofunctors
42.12.
The combinator of directed trees
42.13.
Combinators of enriched directed trees
42.14.
Coproduct polynomial endofunctors
42.15.
Directed trees
42.16.
The elementhood relation on coalgebras of polynomial endofunctors
42.17.
The elementhood relation on W-types
42.18.
Empty multisets
42.19.
Enriched directed trees
42.20.
Equivalences of directed trees
42.21.
Equivalences of enriched directed trees
42.22.
Extensional W-types
42.23.
Fibers of directed trees
42.24.
Fibers of enriched directed trees
42.25.
Full binary trees
42.26.
Function polynomial endofunctors
42.27.
Functoriality of the combinator of directed trees
42.28.
Functoriality of the fiber operation on directed trees
42.29.
Functoriality of W-types
42.30.
Hereditary W-types
42.31.
Indexed W-types
42.32.
Induction principles on W-types
42.33.
Inequality on W-types
42.34.
Lower types of elements in W-types
42.35.
Morphisms of algebras of polynomial endofunctors
42.36.
Morphisms of coalgebras of polynomial endofunctors
42.37.
Morphisms of directed trees
42.38.
Morphisms of enriched directed trees
42.39.
Morphisms of polynomial endofunctors
42.40.
Multiset-indexed dependent products of types
42.41.
Multisets
42.42.
Multivariable polynomial functors
42.43.
Natural transformations between polynomial endofunctors
42.44.
Planar binary trees
42.45.
Plane trees
42.46.
Polynomial endofunctors
42.47.
Raising universe levels of directed trees
42.48.
Ranks of elements in W-types
42.49.
Rooted morphisms of directed trees
42.50.
Rooted morphisms of enriched directed trees
42.51.
Rooted quasitrees
42.52.
Rooted undirected trees
42.53.
Small multisets
42.54.
Submultisets
42.55.
Transitive multisets
42.56.
The underlying trees of elements of coalgebras of polynomial endofunctors
42.57.
The underlying trees of elements of W-types
42.58.
Undirected trees
42.59.
Univalent polynomial endofunctors
42.60.
The universal multiset
42.61.
The universal polynomial endofunctor
42.62.
The universal tree
42.63.
The W-type of natural numbers
42.64.
The W-type of the type of propositions
42.65.
W-types
43.
Type theories
❱
43.1.
Comprehension of fibered type theories
43.2.
Dependent type theories
43.3.
Fibered dependent type theories
43.4.
Π-types in precategories with attributes
43.5.
Π-types in precategories with families
43.6.
Precategories with attributes
43.7.
Precategories with families
43.8.
Sections of dependent type theories
43.9.
Simple type theories
43.10.
Unityped type theories
44.
Univalent combinatorics
❱
44.1.
2-element decidable subtypes
44.2.
2-element subtypes
44.3.
2-element types
44.4.
The binomial types
44.5.
Bracelets
44.6.
Cartesian products of finite types
44.7.
The classical definition of the standard finite types
44.8.
Complements of decidable subtypes of finite types
44.9.
Complements of isolated elements of finite types
44.10.
Coproducts of finite types
44.11.
Coproducts of inhabited finite types
44.12.
Counting in type theory
44.13.
Counting the elements of decidable subtypes
44.14.
Counting the elements of dependent pair types
44.15.
Counting the elements in Maybe
44.16.
Cubes
44.17.
Cycle partitions of finite types
44.18.
Cycle prime decompositions of natural numbers
44.19.
Cyclic finite types
44.20.
De Morgan's law for finite families of propositions
44.21.
Decidable dependent function types
44.22.
Decidability of dependent pair types
44.23.
Decidable equivalence relations on finite types
44.24.
Decidable propositions
44.25.
Decidable subtypes of finite types
44.26.
Dedekind finite sets
44.27.
Dedekind finite types
44.28.
Counting the elements of dependent function types
44.29.
Dependent pair types of finite types
44.30.
Finite discrete Σ-decompositions
44.31.
Disjunctions
44.32.
Distributivity of set truncation over finite products
44.33.
Double counting
44.34.
Dual Dedekind finite types
44.35.
Embeddings
44.36.
Embeddings between standard finite types
44.37.
Equality in finite types
44.38.
Equality in the standard finite types
44.39.
Equivalences between finite types
44.40.
Equivalences of cubes
44.41.
Equivalences between standard finite types
44.42.
Ferrers diagrams (unlabeled partitions)
44.43.
Fibers of maps between finite types
44.44.
Finite choice
44.45.
Finite subtypes
44.46.
Finite types
44.47.
Finitely enumerable subtypes
44.48.
Finitely enumerable types
44.49.
Finiteness of the type of connected components
44.50.
Finitely presented types
44.51.
Finite function types
44.52.
The image of a map
44.53.
Inequality on types equipped with a counting
44.54.
Inhabited finite types
44.55.
Inhabited finitely enumerable subtypes
44.56.
Inhabited finitely enumerable types
44.57.
Injective maps between finite types
44.58.
An involution on the standard finite types
44.59.
Isotopies of Latin squares
44.60.
Kuratowski finite sets
44.61.
Latin squares
44.62.
Locally finite types
44.63.
The groupoid of main classes of Latin hypercubes
44.64.
The groupoid of main classes of Latin squares
44.65.
The maybe monad on finite types
44.66.
Necklaces
44.67.
Orientations of the complete undirected graph
44.68.
Orientations of cubes
44.69.
Partitions of finite types
44.70.
Petri-nets
44.71.
π-finite types
44.72.
The pigeonhole principle
44.73.
Finitely π-presented types
44.74.
Quotients of finite types
44.75.
Ramsey theory
44.76.
Repetitions of values
44.77.
Repetitions of values in sequences
44.78.
Retracts of finite types
44.79.
Riffle shuffles
44.80.
Sequences of elements in finite types
44.81.
Set quotients of index 2
44.82.
Finite Σ-decompositions of finite types
44.83.
Skipping elements in standard finite types
44.84.
Small types
44.85.
Standard finite pruned trees
44.86.
Standard finite trees
44.87.
The standard finite types
44.88.
Steiner systems
44.89.
Steiner triple systems
44.90.
Subcounting
44.91.
Subfinite indexing
44.92.
Subfinite types
44.93.
Subfinitely enumerable types
44.94.
Combinatorial identities of sums of natural numbers
44.95.
Surjective maps between finite types
44.96.
Symmetric difference of finite subtypes
44.97.
Finite trivial Σ-decompositions
44.98.
Truncated π-finite types
44.99.
Type duality of finite types
44.100.
Unbounded π-finite types
44.101.
Unions of finite subtypes
44.102.
The universal property of the standard finite types
44.103.
Unlabeled partitions
44.104.
Unlabeled rooted trees
44.105.
Unlabeled trees
44.106.
Untruncated π-finite types
45.
Universal algebra
❱
45.1.
Abstract equations over signatures
45.2.
Algebraic theories
45.3.
Algebraic theory of groups
45.4.
Algebras of algebraic theories
45.5.
The category of algebras of an algebraic theory
45.6.
Congruences
45.7.
Equivalences of models of signatures
45.8.
Extensions of signatures
45.9.
Homomorphisms of algebras
45.10.
Isomorphisms of algebras of theories
45.11.
Kernels of homomorphisms of algebras
45.12.
Models of signatures
45.13.
Morphisms of models of signatures
45.14.
The precategory of algebras of an algebraic theory
45.15.
Quotient algebras
45.16.
Signatures
45.17.
Terms over signatures
46.
Wild category theory
❱
46.1.
Coinductive isomorphisms in noncoherent large ω-precategories
46.2.
Coinductive isomorphisms in noncoherent ω-precategories
46.3.
Colax functors between large noncoherent ω-precategories
46.4.
Colax functors between noncoherent ω-precategories
46.5.
Maps between noncoherent large ω-precategories
46.6.
Maps between noncoherent ω-precategories
46.7.
Noncoherent large ω-precategories
46.8.
Noncoherent ω-precategories
Light
Rust
Coal
Navy
Ayu
Latte
Frappé
Macchiato
Mocha
agda-unimath
Agda-unimath art
A dependency graph of the library, color coded by namespace. Fredrik Bakke. 2025 — perpetuity
The graph of mathematical concepts. Andrej Bauer and Matej Petković. 2023
The graph of mathematical concepts. Andrej Bauer and Matej Petković. 2023