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 acknowledgements
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 library contents
7.
Formalization of results from the literature
❱
7.1.
Freek Wiedijk's 100 Theorems
7.2.
1000+ theorems
7.3.
Idempotents in Intensional Type Theory
7.4.
Introduction to homotopy type theory
7.5.
Sequences of the online encyclopedia of integer sequences
7.6.
Sequential Colimits in Homotopy Type Theory
The agda-unimath library
8.
Category theory
❱
8.1.
Adjunctions between large categories
8.2.
Adjunctions between large precategories
8.3.
Anafunctors between categories
8.4.
Anafunctors between precategories
8.5.
The augmented simplex category
8.6.
Categories
8.7.
The category of functors and natural transformations between two categories
8.8.
The category of functors and natural transformations from small to large categories
8.9.
The category of maps and natural transformations between two categories
8.10.
The category of maps and natural transformations from small to large categories
8.11.
Commuting squares of morphisms in large precategories
8.12.
Commuting squares of morphisms in precategories
8.13.
Commuting squares of morphisms in set-magmoids
8.14.
Commuting triangles of morphisms in precategories
8.15.
Commuting triangles of morphisms in set-magmoids
8.16.
Complete precategories
8.17.
Composition operations on binary families of sets
8.18.
Cones in precategories
8.19.
Conservative functors between precategories
8.20.
Constant functors
8.21.
Copresheaf categories
8.22.
Coproducts in precategories
8.23.
Cores of categories
8.24.
Cores of precategories
8.25.
Coslice precategories
8.26.
Dependent composition operations over precategories
8.27.
Dependent products of categories
8.28.
Dependent products of large categories
8.29.
Dependent products of large precategories
8.30.
Dependent products of precategories
8.31.
Discrete categories
8.32.
Displayed precategories
8.33.
Embedding maps between precategories
8.34.
Embeddings between precategories
8.35.
Endomorphisms in categories
8.36.
Endomorphisms in precategories
8.37.
Epimorphism in large precategories
8.38.
Equivalences between categories
8.39.
Equivalences between large precategories
8.40.
Equivalences between precategories
8.41.
Essential fibers of functors between precategories
8.42.
Essentially injective functors between precategories
8.43.
Essentially surjective functors between precategories
8.44.
Exponential objects in precategories
8.45.
Extensions of functors between precategories
8.46.
Faithful functors between precategories
8.47.
Faithful maps between precategories
8.48.
Full functors between precategories
8.49.
Full large subcategories
8.50.
Full large subprecategories
8.51.
Full maps between precategories
8.52.
Full subcategories
8.53.
Full subprecategories
8.54.
Fully faithful functors between precategories
8.55.
Fully faithful maps between precategories
8.56.
Function categories
8.57.
Function precategories
8.58.
Functors between categories
8.59.
Functors from small to large categories
8.60.
Functors from small to large precategories
8.61.
Functors between large categories
8.62.
Functors between large precategories
8.63.
Functors between nonunital precategories
8.64.
Functors between precategories
8.65.
Functors between set-magmoids
8.66.
Gaunt categories
8.67.
Groupoids
8.68.
Homotopies of natural transformations in large precategories
8.69.
Indiscrete precategories
8.70.
The initial category
8.71.
Initial objects of large categories
8.72.
Initial objects of large precategories
8.73.
Initial objects in a precategory
8.74.
Isomorphism induction in categories
8.75.
Isomorphism induction in precategories
8.76.
Isomorphisms in categories
8.77.
Isomorphisms in large categories
8.78.
Isomorphisms in large precategories
8.79.
Isomorphisms in precategories
8.80.
Isomorphisms in subprecategories
8.81.
Large categories
8.82.
Large function categories
8.83.
Large function precategories
8.84.
Large precategories
8.85.
Large subcategories
8.86.
Large subprecategories
8.87.
Limits in precategories
8.88.
Maps between categories
8.89.
Maps from small to large categories
8.90.
Maps from small to large precategories
8.91.
Maps between precategories
8.92.
Maps between set-magmoids
8.93.
Monads on categories
8.94.
Monads on precategories
8.95.
Monomorphisms in large precategories
8.96.
Natural isomorphisms between functors between categories
8.97.
Natural isomorphisms between functors between large precategories
8.98.
Natural isomorphisms between functors between precategories
8.99.
Natural isomorphisms between maps between categories
8.100.
Natural isomorphisms between maps between precategories
8.101.
Natural numbers object in a precategory
8.102.
Natural transformations between functors between categories
8.103.
Natural transformations between functors from small to large categories
8.104.
Natural transformations between functors from small to large precategories
8.105.
Natural transformations between functors between large categories
8.106.
Natural transformations between functors between large precategories
8.107.
Natural transformations between functors between precategories
8.108.
Natural transformations between maps between categories
8.109.
Natural transformations between maps from small to large precategories
8.110.
Natural transformations between maps between precategories
8.111.
Nonunital precategories
8.112.
One object precategories
8.113.
Opposite categories
8.114.
Opposite large precategories
8.115.
Opposite precategories
8.116.
Opposite preunivalent categories
8.117.
Opposite strongly preunivalent categories
8.118.
Pointed endofunctors on categories
8.119.
Pointed endofunctors
8.120.
Precategories
8.121.
Precategory of elements of a presheaf
8.122.
The precategory of functors and natural transformations between two precategories
8.123.
The precategory of functors and natural transformations from small to large precategories
8.124.
The precategory of maps and natural transformations from a small to a large precategory
8.125.
The precategory of maps and natural transformations between two precategories
8.126.
Pregroupoids
8.127.
Presheaf categories
8.128.
Preunivalent categories
8.129.
Products in precategories
8.130.
Products of precategories
8.131.
Pseudomonic functors between precategories
8.132.
Pullbacks in precategories
8.133.
Replete subprecategories
8.134.
Representable functors between categories
8.135.
Representable functors between large precategories
8.136.
Representable functors between precategories
8.137.
The representing arrow category
8.138.
Restrictions of functors to cores of precategories
8.139.
Right extensions in precategories
8.140.
Right Kan extensions in precategories
8.141.
Rigid objects in a category
8.142.
Rigid objects in a precategory
8.143.
Set-magmoids
8.144.
Sieves in categories
8.145.
The simplex category
8.146.
Slice precategories
8.147.
Split essentially surjective functors between precategories
8.148.
Strict categories
8.149.
Strongly preunivalent categories
8.150.
Structure equivalences between set-magmoids
8.151.
Subcategories
8.152.
Subprecategories
8.153.
Subterminal precategories
8.154.
The terminal category
8.155.
Terminal objects in a precategory
8.156.
Wide subcategories
8.157.
Wide subprecategories
8.158.
The Yoneda lemma for categories
8.159.
The Yoneda lemma for precategories
9.
Commutative algebra
❱
9.1.
The binomial theorem in commutative rings
9.2.
The binomial theorem in commutative semirings
9.3.
Boolean rings
9.4.
The category of commutative rings
9.5.
Commutative rings
9.6.
Commutative semirings
9.7.
Dependent products of commutative rings
9.8.
Dependent products of commutative semirings
9.9.
Discrete fields
9.10.
The Eisenstein integers
9.11.
Euclidean domains
9.12.
Full ideals of commutative rings
9.13.
Function commutative rings
9.14.
Function commutative semirings
9.15.
The Gaussian integers
9.16.
The group of multiplicative units of a commutative ring
9.17.
Homomorphisms of commutative rings
9.18.
Homomorphisms of commutative semirings
9.19.
Ideals of commutative rings
9.20.
Ideals of commutative semirings
9.21.
Ideals generated by subsets of commutative rings
9.22.
Integer multiples of elements of commutative rings
9.23.
Integral domains
9.24.
Intersections of ideals of commutative rings
9.25.
Intersections of radical ideals of commutative rings
9.26.
Invertible elements in commutative rings
9.27.
Isomorphisms of commutative rings
9.28.
Joins of ideals of commutative rings
9.29.
Joins of radical ideals of commutative rings
9.30.
Local commutative rings
9.31.
Maximal ideals of commutative rings
9.32.
Multiples of elements in commutative rings
9.33.
Nilradical of a commutative ring
9.34.
The nilradical of a commutative semiring
9.35.
The poset of ideals of a commutative ring
9.36.
The poset of radical ideals of a commutative ring
9.37.
Powers of elements in commutative rings
9.38.
Powers of elements in commutative semirings
9.39.
The precategory of commutative rings
9.40.
The precategory of commutative semirings
9.41.
Prime ideals of commutative rings
9.42.
Products of commutative rings
9.43.
Products of ideals of commutative rings
9.44.
Products of radical ideals of a commutative ring
9.45.
Products of subsets of commutative rings
9.46.
Radical ideals of commutative rings
9.47.
Radical ideals generated by subsets of commutative rings
9.48.
Radicals of ideals of commutative rings
9.49.
Subsets of commutative rings
9.50.
Subsets of commutative semirings
9.51.
Sums in commutative rings
9.52.
Sums in commutative semirings
9.53.
Transporting commutative ring structures along isomorphisms of abelian groups
9.54.
Trivial commutative rings
9.55.
The Zariski locale
9.56.
The Zariski topology on the set of prime ideals of a commutative ring
10.
Domain theory
❱
10.1.
Directed complete posets
10.2.
Directed families in posets
10.3.
Kleene's fixed point theorem for ω-complete posets
10.4.
Kleene's fixed point theorem for posets
10.5.
ω-Complete posets
10.6.
ω-Continuous maps between ω-complete posets
10.7.
ω-Continuous maps between posets
10.8.
Reindexing directed families in posets
10.9.
Scott-continuous maps between posets
11.
Elementary number theory
❱
11.1.
The absolute value function on the integers
11.2.
The absolute value function on the rational numbers
11.3.
The Ackermann function
11.4.
Addition on integer fractions
11.5.
Addition on the integers
11.6.
Addition on the natural numbers
11.7.
Addition of positive, negative, nonnegative and nonpositive integers
11.8.
Addition on the rational numbers
11.9.
The additive group of rational numbers
11.10.
The Archimedean property of integer fractions
11.11.
The Archimedean property of the integers
11.12.
The Archimedean property of the natural numbers
11.13.
The Archimedean property of the positive rational numbers
11.14.
The Archimedean property of ℚ
11.15.
Arithmetic functions
11.16.
Arithmetic sequences of positive rational numbers
11.17.
The based induction principle of the natural numbers
11.18.
Based strong induction for the natural numbers
11.19.
The Bell numbers
11.20.
Bernoulli's inequality on the positive rational numbers
11.21.
Bezout's lemma in the integers
11.22.
Bezout's lemma on the natural numbers
11.23.
The binomial coefficients
11.24.
The binomial theorem for the integers
11.25.
The binomial theorem for the natural numbers
11.26.
Bounded sums of arithmetic functions
11.27.
Catalan numbers
11.28.
Closed intervals of rational numbers
11.29.
The cofibonacci sequence
11.30.
The Collatz bijection
11.31.
The Collatz conjecture
11.32.
The commutative semiring of natural numbers
11.33.
Conatural numbers
11.34.
The congruence relations on the integers
11.35.
The congruence relations on the natural numbers
11.36.
The cross-multiplication difference of two integer fractions
11.37.
Cubes of natural numbers
11.38.
Decidable dependent function types
11.39.
The decidable total order of integers
11.40.
The decidable total order of natural numbers
11.41.
The decidable total order of rational numbers
11.42.
The decidable total order of a standard finite type
11.43.
Decidable types in elementary number theory
11.44.
The difference between integers
11.45.
The difference between rational numbers
11.46.
Dirichlet convolution
11.47.
The distance between integers
11.48.
The distance between natural numbers
11.49.
The distance between rational numbers
11.50.
Divisibility of integers
11.51.
Divisibility in modular arithmetic
11.52.
Divisibility of natural numbers
11.53.
The divisibility relation on the standard finite types
11.54.
Equality of conatural numbers
11.55.
Equality of integers
11.56.
Equality of natural numbers
11.57.
Equality of rational numbers
11.58.
The Euclid–Mullin sequence
11.59.
Euclidean division on the natural numbers
11.60.
Euler's totient function
11.61.
Exponentiation of natural numbers
11.62.
Factorials of natural numbers
11.63.
Falling factorials
11.64.
Fermat numbers
11.65.
The Fibonacci sequence
11.66.
The field of rational numbers
11.67.
The natural numbers base k
11.68.
Finitely cyclic maps
11.69.
The fundamental theorem of arithmetic
11.70.
Geometric sequences of positive rational numbers
11.71.
The Goldbach conjecture
11.72.
The greatest common divisor of integers
11.73.
The greatest common divisor of natural numbers
11.74.
The group of integers
11.75.
The half-integers
11.76.
The Hardy-Ramanujan number
11.77.
The inclusion of the natural numbers into the conatural numbers
11.78.
Inequality of arithmetic and geometric means on the integers
11.79.
Inequality of arithmetic and geometric means on the rational numbers
11.80.
Inequality of conatural numbers
11.81.
Inequality on integer fractions
11.82.
Inequality on the integers
11.83.
Inequality of natural numbers
11.84.
Inequality on the rational numbers
11.85.
Inequality on the standard finite types
11.86.
Infinite conatural numbers
11.87.
The infinitude of primes
11.88.
Initial segments of the natural numbers
11.89.
Integer fractions
11.90.
Integer partitions
11.91.
The integers
11.92.
The Jacobi symbol
11.93.
The Kolakoski sequence
11.94.
The Legendre symbol
11.95.
Lower bounds of type families over the natural numbers
11.96.
Maximum on the natural numbers
11.97.
Maximum on the rational numbers
11.98.
Maximum on the standard finite types
11.99.
The mediant fraction of two integer fractions
11.100.
Mersenne primes
11.101.
Minimum on the natural numbers
11.102.
Minimum on the rational numbers
11.103.
Minimum on the standard finite types
11.104.
Modular arithmetic
11.105.
Modular arithmetic on the standard finite types
11.106.
The monoid of natural numbers with addition
11.107.
The monoid of the natural numbers with maximum
11.108.
Multiplication on integer fractions
11.109.
Multiplication of integers
11.110.
Multiplication of the elements of a list of natural numbers
11.111.
Multiplication of natural numbers
11.112.
Multiplication of positive, negative, nonnegative and nonpositive integers
11.113.
Multiplication on the rational numbers
11.114.
The multiplicative group of positive rational numbers
11.115.
The multiplicative group of rational numbers
11.116.
Multiplicative inverses of positive integer fractions
11.117.
The multiplicative monoid of natural numbers
11.118.
The multiplicative monoid of rational numbers
11.119.
Multiplicative units in the integers
11.120.
Multiplicative units in modular arithmetic
11.121.
Multiset coefficients
11.122.
The type of natural numbers
11.123.
Negative integer fractions
11.124.
The negative integers
11.125.
Negative rational numbers
11.126.
Nonnegative integer fractions
11.127.
The nonnegative integers
11.128.
Nonnegative rational numbers
11.129.
The nonpositive integers
11.130.
Nonzero integers
11.131.
Nonzero natural numbers
11.132.
Nonzero rational numbers
11.133.
The ordinal induction principle for the natural numbers
11.134.
Parity of the natural numbers
11.135.
Peano arithmetic
11.136.
Pisano periods
11.137.
The poset of natural numbers ordered by divisibility
11.138.
The positive, negative, nonnegative and nonpositive integers
11.139.
The positive, negative, and nonnegative rational numbers
11.140.
Positive conatural numbers
11.141.
Positive integer fractions
11.142.
The positive integers
11.143.
Positive rational numbers
11.144.
Powers of integers
11.145.
Powers of two
11.146.
Prime numbers
11.147.
Products of natural numbers
11.148.
Proper divisors of natural numbers
11.149.
Pythagorean triples
11.150.
The rational numbers
11.151.
Reduced integer fractions
11.152.
Relatively prime integers
11.153.
Relatively prime natural numbers
11.154.
Repeating an element in a standard finite type
11.155.
Retracts of the type of natural numbers
11.156.
The ring of integers
11.157.
The ring of rational numbers
11.158.
The sieve of Eratosthenes
11.159.
Square-free natural numbers
11.160.
Squares in the integers
11.161.
Squares in ℤₚ
11.162.
Squares in the natural numbers
11.163.
Squares in the rational numbers
11.164.
The standard cyclic groups
11.165.
The standard cyclic rings
11.166.
Stirling numbers of the second kind
11.167.
Strict inequality on the integer fractions
11.168.
Strict inequality on the integers
11.169.
Strict inequality on the natural numbers
11.170.
Strict inequality on the rational numbers
11.171.
Strict inequality on the standard finite types
11.172.
Strictly ordered pairs of natural numbers
11.173.
The strong induction principle for the natural numbers
11.174.
Sums of natural numbers
11.175.
Sylvester's sequence
11.176.
Taxicab numbers
11.177.
Telephone numbers
11.178.
The triangular numbers
11.179.
The Twin Prime conjecture
11.180.
Type arithmetic with natural numbers
11.181.
Unit elements in the standard finite types
11.182.
Unit fractions in the rational numbers types
11.183.
Unit similarity on the standard finite types
11.184.
The universal property of the conatural numbers
11.185.
The universal property of the integers
11.186.
The universal property of the natural numbers
11.187.
Upper bounds for type families over the natural numbers
11.188.
The well-ordering principle of the natural numbers
11.189.
The well-ordering principle of the standard finite types
11.190.
The zero conatural number
12.
Finite algebra
❱
12.1.
Commutative finite rings
12.2.
Dependent products of commutative finit rings
12.3.
Dependent products of finite rings
12.4.
Finite fields
12.5.
Finite rings
12.6.
Homomorphisms of commutative finite rings
12.7.
Homomorphisms of finite rings
12.8.
Products of commutative finite rings
12.9.
Products of finite rings
12.10.
Semisimple commutative finite rings
13.
Finite group theory
❱
13.1.
The abstract quaternion group of order 8
13.2.
Alternating concrete groups
13.3.
Alternating groups
13.4.
Cartier's delooping of the sign homomorphism
13.5.
The concrete quaternion group
13.6.
Deloopings of the sign homomorphism
13.7.
Abelian groups
13.8.
Finite Commutative monoids
13.9.
Finite groups
13.10.
Finite monoids
13.11.
Finite semigroups
13.12.
The group of n-element types
13.13.
Groups of order 2
13.14.
Orbits of permutations
13.15.
Permutations
13.16.
Permutations of standard finite types
13.17.
The sign homomorphism
13.18.
Simpson's delooping of the sign homomorphism
13.19.
Subgroups of finite groups
13.20.
Tetrahedra in 3-dimensional space
13.21.
Transpositions
13.22.
Transpositions of standard finite types
14.
Foundation
❱
14.1.
0-Connected types
14.2.
0-Images of maps
14.3.
0-Maps
14.4.
1-Types
14.5.
2-Types
14.6.
Action on equivalences of functions
14.7.
The action on equivalences of functions out of subuniverses
14.8.
Action on equivalences of type families
14.9.
Action on equivalences in type families over subuniverses
14.10.
The action of functions on higher identifications
14.11.
The action on homotopies of functions
14.12.
The binary action on identifications of binary dependent functions
14.13.
The binary action on identifications of binary functions
14.14.
The action on identifications of dependent functions
14.15.
The action on identifications of functions
14.16.
Apartness relations
14.17.
Arithmetic law for coproduct decomposition and Σ-decomposition
14.18.
Arithmetic law for product decomposition and Π-decomposition
14.19.
Automorphisms
14.20.
The axiom of choice
14.21.
Bands
14.22.
Base changes of span diagrams
14.23.
Bicomposition of functions
14.24.
Binary dependent identifications
14.25.
Binary embeddings
14.26.
Binary equivalences
14.27.
Binary equivalences on unordered pairs of types
14.28.
Binary functoriality of set quotients
14.29.
Homotopies of binary operations
14.30.
Binary operations on unordered pairs of types
14.31.
Binary reflecting maps of equivalence relations
14.32.
Binary relations
14.33.
Binary relations with extensions
14.34.
Binary relations with lifts
14.35.
Binary transport
14.36.
Binary type duality
14.37.
The booleans
14.38.
The Cantor–Schröder–Bernstein–Escardó theorem
14.39.
Cantor's theorem
14.40.
Cartesian morphisms of arrows
14.41.
Cartesian morphisms of span diagrams
14.42.
Cartesian product types
14.43.
Cartesian products of set quotients
14.44.
The category of families of sets
14.45.
The category of sets
14.46.
Choice of representatives for an equivalence relation
14.47.
Coalgebras of the maybe monad
14.48.
Codiagonal maps of types
14.49.
Coherently idempotent maps
14.50.
Coherently invertible maps
14.51.
Coinhabited pairs of types
14.52.
Commuting cubes of maps
14.53.
Commuting hexagons of identifications
14.54.
Commuting pentagons of identifications
14.55.
Commuting prisms of maps
14.56.
Commuting squares of homotopies
14.57.
Commuting squares of identifications
14.58.
Commuting squares of maps
14.59.
Commuting tetrahedra of homotopies
14.60.
Commuting tetrahedra of maps
14.61.
Commuting triangles of homotopies
14.62.
Commuting triangles of identifications
14.63.
Commuting triangles of maps
14.64.
Commuting triangles of morphisms of arrows
14.65.
Complements of type families
14.66.
Complements of subtypes
14.67.
Composite maps in inverse sequential diagrams
14.68.
Composition algebra
14.69.
Composition of spans
14.70.
Computational identity types
14.71.
Cones over cospan diagrams
14.72.
Cones over inverse sequential diagrams
14.73.
Conjunction
14.74.
Connected components of types
14.75.
Connected components of universes
14.76.
Connected maps
14.77.
Connected types
14.78.
Constant maps
14.79.
Constant span diagrams
14.80.
Constant type families
14.81.
The continuation monad
14.82.
Contractible maps
14.83.
Contractible types
14.84.
Copartial elements
14.85.
Copartial functions
14.86.
Coproduct decompositions
14.87.
Coproduct decompositions in a subuniverse
14.88.
Coproduct types
14.89.
Coproducts of pullbacks
14.90.
Morphisms in the coslice category of types
14.91.
Cospan diagrams
14.92.
Cospans of types
14.93.
Decidability of dependent function types
14.94.
Decidability of dependent pair types
14.95.
Decidable embeddings
14.96.
Decidable equality
14.97.
Decidable equivalence relations
14.98.
Decidable maps
14.99.
Decidable propositions
14.100.
Decidable relations on types
14.101.
Decidable subtypes
14.102.
Decidable types
14.103.
Dependent binary homotopies
14.104.
The dependent binomial theorem for types (distributivity of dependent function types over coproduct types)
14.105.
Dependent epimorphisms
14.106.
Dependent epimorphisms with respect to truncated types
14.107.
Dependent function types
14.108.
Dependent homotopies
14.109.
Dependent identifications
14.110.
Dependent inverse sequential diagrams of types
14.111.
Dependent pair types
14.112.
Dependent products of pullbacks
14.113.
Dependent sequences
14.114.
Dependent sums of pullbacks
14.115.
Dependent telescopes
14.116.
The dependent universal property of equivalences
14.117.
Descent for coproduct types
14.118.
Descent for dependent pair types
14.119.
Descent for the empty type
14.120.
Descent for equivalences
14.121.
Diaconescu's theorem
14.122.
Diagonal maps into cartesian products of types
14.123.
Diagonal maps of types
14.124.
Diagonal span diagrams
14.125.
Diagonals of maps
14.126.
Diagonals of morphisms of arrows
14.127.
Discrete binary relations
14.128.
Discrete reflexive relations
14.129.
Discrete relaxed Σ-decompositions
14.130.
Discrete Σ-decompositions
14.131.
Discrete types
14.132.
Disjoint subtypes
14.133.
Disjunction
14.134.
Double arrows
14.135.
Double negation
14.136.
The double negation modality
14.137.
Double negation stable equality
14.138.
Double negation stable propositions
14.139.
Double powersets
14.140.
Dubuc-Penon compact types
14.141.
Effective maps for equivalence relations
14.142.
Embeddings
14.143.
Empty types
14.144.
Endomorphisms
14.145.
Epimorphisms
14.146.
Epimorphisms with respect to maps into sets
14.147.
Epimorphisms with respect to truncated types
14.148.
Equality of cartesian product types
14.149.
Equality of coproduct types
14.150.
Equality on dependent function types
14.151.
Equality of dependent pair types
14.152.
Equality in the fibers of a map
14.153.
Equivalence classes
14.154.
Equivalence extensionality
14.155.
Equivalence induction
14.156.
Equivalence injective type families
14.157.
Equivalence relations
14.158.
Equivalences
14.159.
Equivalences of arrows
14.160.
Equivalences of cospans
14.161.
Equivalences of double arrows
14.162.
Equivalences of inverse sequential diagrams of types
14.163.
Equivalences on Maybe
14.164.
Equivalences of span diagrams
14.165.
Equivalences of span diagrams on families of types
14.166.
Equivalences of spans
14.167.
Equivalences of spans of families of types
14.168.
Evaluation of functions
14.169.
Exclusive disjunctions
14.170.
Exclusive sums
14.171.
Existential quantification
14.172.
Exponents of set quotients
14.173.
Extensions of types
14.174.
Extensions of types in a global subuniverse
14.175.
Extensions of types in a subuniverse
14.176.
Faithful maps
14.177.
Families of equivalences
14.178.
Families of maps
14.179.
Families of types over telescopes
14.180.
Fiber inclusions
14.181.
Fibered equivalences
14.182.
Fibered involutions
14.183.
Maps fibered over a map
14.184.
Fibers of maps
14.185.
Finitely coherent equivalences
14.186.
Finitely coherently invertible maps
14.187.
Fixed points of endofunctions
14.188.
Full subtypes of types
14.189.
Function extensionality
14.190.
Function types
14.191.
Functional correspondences
14.192.
Functoriality of the action on identifications of functions
14.193.
Functoriality of cartesian product types
14.194.
Functoriality of coproduct types
14.195.
Functoriality of dependent function types
14.196.
Functoriality of dependent pair types
14.197.
Functoriality of disjunction
14.198.
Functoriality of fibers of maps
14.199.
Functoriality of function types
14.200.
Functoriality of morphisms of arrows
14.201.
Functoriality of propositional truncations
14.202.
Functorialty of pullbacks
14.203.
Functoriality of sequential limits
14.204.
Functoriality of set quotients
14.205.
Functoriality of set truncation
14.206.
Functoriality of truncations
14.207.
Fundamental theorem of equivalence relations
14.208.
The fundamental theorem of identity types
14.209.
Global choice
14.210.
Global subuniverses
14.211.
The globular type of dependent functions
14.212.
The globular type of functions
14.213.
Higher homotopies of morphisms of arrows
14.214.
Hilbert's ε-operators
14.215.
Homotopies
14.216.
Homotopies of morphisms of arrows
14.217.
Homotopies of morphisms of cospan diagrams
14.218.
Homotopy algebra
14.219.
Homotopy induction
14.220.
The homotopy preorder of types
14.221.
Horizontal composition of spans of spans
14.222.
Idempotent maps
14.223.
Identity systems
14.224.
Identity types of truncated types
14.225.
Identity types
14.226.
The image of a map
14.227.
Images of subtypes
14.228.
Implicit function types
14.229.
Impredicative encodings of the logical operations
14.230.
Impredicative universes
14.231.
The induction principle for propositional truncation
14.232.
Infinitely coherent equivalences
14.233.
Inhabited subtypes
14.234.
Inhabited types
14.235.
Injective maps
14.236.
The interchange law
14.237.
Intersections of subtypes
14.238.
Inverse sequential diagrams of types
14.239.
Invertible maps
14.240.
Involutions
14.241.
Irrefutable propositions
14.242.
Isolated elements
14.243.
Isomorphisms of sets
14.244.
Iterated cartesian product types
14.245.
Iterated dependent pair types
14.246.
Iterated dependent product types
14.247.
Iterating automorphisms
14.248.
Iterating families of maps over a map
14.249.
Iterating functions
14.250.
Iterating involutions
14.251.
Kernel span diagrams of maps
14.252.
Large apartness relations
14.253.
Large binary relations
14.254.
Large dependent pair types
14.255.
Large homotopies
14.256.
Large identity types
14.257.
The large locale of propositions
14.258.
The large locale of subtypes
14.259.
The law of excluded middle
14.260.
Lawvere's fixed point theorem
14.261.
The lesser limited principle of omniscience
14.262.
Lifts of types
14.263.
The limited principle of omniscience
14.264.
The locale of propositions
14.265.
Locally small types
14.266.
Logical equivalences
14.267.
Maps in global subuniverses
14.268.
Maps in subuniverses
14.269.
The maybe monad
14.270.
Mere embeddings
14.271.
Mere equality
14.272.
Mere equivalences
14.273.
Mere functions
14.274.
Mere logical equivalences
14.275.
Mere path-cosplit maps
14.276.
Monomorphisms
14.277.
Morphisms of arrows
14.278.
Morphisms of binary relations
14.279.
Morphisms of coalgebras of the maybe monad
14.280.
Morphisms of cospan diagrams
14.281.
Morphisms of cospans
14.282.
Morphisms of double arrows
14.283.
Morphisms of inverse sequential diagrams of types
14.284.
Morphisms of span diagrams
14.285.
Morphisms of spans
14.286.
Morphisms of spans on families of types
14.287.
Morphisms of twisted arrows
14.288.
Multisubsets
14.289.
Multivariable correspondences
14.290.
Multivariable decidable relations
14.291.
Multivariable functoriality of set quotients
14.292.
Multivariable homotopies
14.293.
Multivariable operations
14.294.
Multivariable relations
14.295.
Multivariable sections
14.296.
Negated equality
14.297.
Negation
14.298.
Noncontractible types
14.299.
Null-homotopic maps
14.300.
Operations on span diagrams
14.301.
Operations on spans
14.302.
Operations on spans of families of types
14.303.
Opposite spans
14.304.
Pairs of distinct elements
14.305.
Partial elements
14.306.
Partial functions
14.307.
Partial sequences
14.308.
Partitions
14.309.
Path algebra
14.310.
Path-cosplit maps
14.311.
Path-split maps
14.312.
Path-split type families
14.313.
Perfect images
14.314.
Permutations of spans of families of types
14.315.
Π-decompositions of types
14.316.
Π-decompositions of types into types in a subuniverse
14.317.
Pointed torsorial type families
14.318.
Postcomposition of dependent functions
14.319.
Postcomposition of functions
14.320.
Postcomposition of pullbacks
14.321.
Powersets
14.322.
Precomposition of dependent functions
14.323.
Precomposition of functions
14.324.
Precomposition of functions into subuniverses
14.325.
Precomposition of type families
14.326.
The preunivalence axiom
14.327.
Preunivalent type families
14.328.
The principle of omniscience
14.329.
Product decompositions
14.330.
Product decompositions of types in a subuniverse
14.331.
Products of binary relations
14.332.
Products of equivalence relataions
14.333.
Products of tuples of types
14.334.
Products of pullbacks
14.335.
Products of unordered pairs of types
14.336.
Products of unordered tuples of types
14.337.
Projective types
14.338.
Proper subsets
14.339.
Propositional extensionality
14.340.
Propositional maps
14.341.
Propositional resizing
14.342.
Propositional truncations
14.343.
Propositions
14.344.
Pullback cones
14.345.
Pullbacks
14.346.
Pullbacks of subtypes
14.347.
Quasicoherently idempotent maps
14.348.
Raising universe levels
14.349.
Reflecting maps for equivalence relations
14.350.
Reflexive relations
14.351.
The Regensburg extension of the fundamental theorem of identity types
14.352.
Relaxed Σ-decompositions of types
14.353.
Repetitions of values of maps
14.354.
Repetitions in sequences
14.355.
The type theoretic replacement axiom
14.356.
Retractions
14.357.
Retracts of maps
14.358.
Retracts of types
14.359.
Sections
14.360.
Types separated at subuniverses
14.361.
Sequences
14.362.
Sequential limits
14.363.
Set presented types
14.364.
Set quotients
14.365.
Set truncations
14.366.
Sets
14.367.
Shifting sequences
14.368.
Σ-closed subuniverses
14.369.
Σ-decompositions of types into types in a subuniverse
14.370.
Σ-decompositions of types
14.371.
Singleton induction
14.372.
Singleton subtypes
14.373.
Morphisms in the slice category of types
14.374.
Small maps
14.375.
Small types
14.376.
Small universes
14.377.
Sorial type families
14.378.
Span diagrams
14.379.
Span diagrams on families of types
14.380.
Spans of types
14.381.
Spans of families of types
14.382.
Spans of spans
14.383.
Split idempotent maps
14.384.
Split surjective maps
14.385.
Standard apartness relations
14.386.
Standard pullbacks
14.387.
Standard ternary pullbacks
14.388.
Strict symmetrization of binary relations
14.389.
Strictly involutive identity types
14.390.
The strictly right unital concatenation operation on identifications
14.391.
The strong preunivalence axiom
14.392.
Strongly extensional maps
14.393.
Structure
14.394.
The structure identity principle
14.395.
Structured equality duality
14.396.
Structured type duality
14.397.
Subsequences
14.398.
Subsingleton induction
14.399.
Subterminal types
14.400.
Subtype duality
14.401.
The subtype identity principle
14.402.
Subtypes
14.403.
Subuniverses
14.404.
Surjective maps
14.405.
Symmetric binary relations
14.406.
Symmetric cores of binary relations
14.407.
Symmetric difference of subtypes
14.408.
The symmetric identity types
14.409.
Symmetric operations
14.410.
Telescopes
14.411.
Terminal spans on families of types
14.412.
Tight apartness relations
14.413.
Torsorial type families
14.414.
Total partial elements
14.415.
Total partial functions
14.416.
Transfinite cocomposition of maps
14.417.
Transport along equivalences
14.418.
Transport along higher identifications
14.419.
Transport along homotopies
14.420.
Transport along identifications
14.421.
Transport-split type families
14.422.
Transposing identifications along equivalences
14.423.
Transposing identifications along retractions
14.424.
Transposing identifications along sections
14.425.
Transposition of span diagrams
14.426.
Trivial relaxed Σ-decompositions
14.427.
Trivial Σ-decompositions
14.428.
Truncated equality
14.429.
Truncated maps
14.430.
Truncated types
14.431.
k-Equivalences
14.432.
Truncation images of maps
14.433.
Truncation levels
14.434.
The truncation modalities
14.435.
Truncations
14.436.
Tuples of types
14.437.
Type arithmetic with the booleans
14.438.
Type arithmetic for cartesian product types
14.439.
Type arithmetic for coproduct types
14.440.
Type arithmetic with dependent function types
14.441.
Type arithmetic for dependent pair types
14.442.
Type arithmetic with the empty type
14.443.
Type arithmetic with standard pullbacks
14.444.
Type arithmetic with the unit type
14.445.
Type duality
14.446.
The type theoretic principle of choice
14.447.
Uniformly decidable type families
14.448.
Unions of subtypes
14.449.
Uniqueness of the image of a map
14.450.
Uniqueness quantification
14.451.
The uniqueness of set quotients
14.452.
Uniqueness of set truncations
14.453.
Uniqueness of the truncations
14.454.
The unit type
14.455.
Unital binary operations
14.456.
The univalence axiom
14.457.
The univalence axiom implies function extensionality
14.458.
Univalent type families
14.459.
The universal property of booleans
14.460.
The universal properties of cartesian product types
14.461.
Universal property of contractible types
14.462.
The universal property of coproduct types
14.463.
The universal property of dependent function types
14.464.
The universal property of dependent pair types
14.465.
The universal property of the empty type
14.466.
The universal property of equivalences
14.467.
The universal property of the family of fibers of maps
14.468.
The universal property of fiber products
14.469.
The universal property of identity systems
14.470.
The universal property of identity types
14.471.
The universal property of the image of a map
14.472.
The universal property of the maybe monad
14.473.
The universal property of propositional truncations
14.474.
The universal property of propositional truncations with respect to sets
14.475.
The universal property of pullbacks
14.476.
The universal property of sequential limits
14.477.
The universal property of set quotients
14.478.
The universal property of set truncations
14.479.
The universal property of truncations
14.480.
The universal property of the unit type
14.481.
Universal quantification
14.482.
Universe levels
14.483.
Unordered pairs of elements in a type
14.484.
Unordered pairs of types
14.485.
Unordered n-tuples of elements in a type
14.486.
Unordered tuples of types
14.487.
Vectors of set quotients
14.488.
Vertical composition of spans of spans
14.489.
Weak function extensionality
14.490.
The weak limited principle of omniscience
14.491.
Weakly constant maps
14.492.
Whiskering higher homotopies with respect to composition
14.493.
Whiskering homotopies with respect to composition
14.494.
Whiskering homotopies with respect to concatenation
14.495.
Whiskering identifications with respect to concatenation
14.496.
Whiskering operations
14.497.
The wild category of types
14.498.
Yoneda identity types
15.
Foundation core
❱
15.1.
1-Types
15.2.
Cartesian product types
15.3.
Coherently invertible maps
15.4.
Commuting prisms of maps
15.5.
Commuting squares of homotopies
15.6.
Commuting squares of identifications
15.7.
Commuting squares of maps
15.8.
Commuting triangles of maps
15.9.
Constant maps
15.10.
Contractible maps
15.11.
Contractible types
15.12.
Coproduct types
15.13.
Decidable propositions
15.14.
Dependent identifications
15.15.
Diagonal maps into cartesian products of types
15.16.
Discrete types
15.17.
Embeddings
15.18.
Empty types
15.19.
Endomorphisms
15.20.
Equality of dependent pair types
15.21.
Equivalence relations
15.22.
Equivalences
15.23.
Families of equivalences
15.24.
Fibers of maps
15.25.
Function types
15.26.
Functoriality of dependent function types
15.27.
Functoriality of dependent pair types
15.28.
Homotopies
15.29.
Identity types
15.30.
Injective maps
15.31.
Invertible maps
15.32.
Negation
15.33.
Operations on span diagrams
15.34.
Operations on spans
15.35.
Path-split maps
15.36.
Postcomposition of dependent functions
15.37.
Postcomposition of functions
15.38.
Precomposition of dependent functions
15.39.
Precomposition of functions
15.40.
Propositional maps
15.41.
Propositions
15.42.
Pullbacks
15.43.
Retractions
15.44.
Retracts of types
15.45.
Sections
15.46.
Sets
15.47.
Small types
15.48.
Subtypes
15.49.
Torsorial type families
15.50.
Transport along identifications
15.51.
Truncated maps
15.52.
Truncated types
15.53.
Truncation levels
15.54.
The type theoretic principle of choice
15.55.
The univalence axiom
15.56.
The universal property of pullbacks
15.57.
The universal property of truncations
15.58.
Whiskering homotopies with respect to concatenation
15.59.
Whiskering identifications with respect to concatenation
16.
Globular types
❱
16.1.
Base change of dependent globular types
16.2.
Base change of dependent reflexive globular types
16.3.
Binary dependent globular types
16.4.
Binary dependent reflexive globular types
16.5.
Binary globular maps
16.6.
Colax reflexive globular maps
16.7.
Colax transitive globular maps
16.8.
Composition structure on globular types
16.9.
Constant globular types
16.10.
Dependent globular types
16.11.
Dependent reflexive globular types
16.12.
Dependent sums of globular types
16.13.
Discrete dependent reflexive globular types
16.14.
Discrete globular types
16.15.
Discrete reflexive globular types
16.16.
Empty globular types
16.17.
Equality of globular types
16.18.
Exponentials of globular types
16.19.
Fibers of globular maps
16.20.
Equivalences between globular types
16.21.
Maps between globular types
16.22.
Globular types
16.23.
Large colax reflexive globular maps
16.24.
Large colax transitive globular maps
16.25.
Maps between large globular types
16.26.
Large globular types
16.27.
Large lax reflexive globular maps
16.28.
Large lax transitive globular maps
16.29.
Large reflexive globular maps
16.30.
Large reflexive globular types
16.31.
Large symmetric globular types
16.32.
Large transitive globular maps
16.33.
Large transitive globular types
16.34.
Lax reflexive globular maps
16.35.
Lax transitive globular maps
16.36.
Points of globular types
16.37.
Points of reflexive globular types
16.38.
Pointwise extensions of binary families of globular types
16.39.
Pointwise extensions of binary families of reflexive globular types
16.40.
Pointwise extensions of families of globular types
16.41.
Pointwise extensions of families of reflexive globular types
16.42.
Products of families of globular types
16.43.
Reflexive globular equivalences
16.44.
Reflexive globular maps
16.45.
Reflexive globular types
16.46.
Sections of dependent globular types
16.47.
Superglobular types
16.48.
Symmetric globular types
16.49.
Terminal globular types
16.50.
Transitive globular maps
16.51.
Transitive globular types
16.52.
The unit globular type
16.53.
The unit reflexive globular type
16.54.
The universal globular type
16.55.
The universal reflexive globular type
17.
Graph theory
❱
17.1.
Acyclic undirected graphs
17.2.
Base change of dependent directed graphs
17.3.
Base change of dependent reflexive graphs
17.4.
Cartesian products of directed graphs
17.5.
Cartesian products of reflexive graphs
17.6.
Circuits in undirected graphs
17.7.
Closed walks in undirected graphs
17.8.
Complete bipartite graphs
17.9.
Complete multipartite graphs
17.10.
Complete undirected graphs
17.11.
Connected graphs
17.12.
Cycles in undirected graphs
17.13.
Dependent directed graphs
17.14.
Dependent products of directed graphs
17.15.
Dependent products of reflexive graphs
17.16.
Dependent reflexive graphs
17.17.
Dependent sums directed graphs
17.18.
Dependent sums reflexive graphs
17.19.
Directed graph duality
17.20.
Directed graph structures on standard finite sets
17.21.
Directed graphs
17.22.
Discrete dependent reflexive graphs
17.23.
Discrete directed graphs
17.24.
Discrete reflexive graphs
17.25.
Displayed large reflexive graphs
17.26.
Edge-colored undirected graphs
17.27.
Embeddings of directed graphs
17.28.
Embeddings of undirected graphs
17.29.
Enriched undirected graphs
17.30.
Equivalences of dependent directed graphs
17.31.
Equivalences of dependent reflexive graphs
17.32.
Equivalences of directed graphs
17.33.
Equivalences of enriched undirected graphs
17.34.
Equivalences of reflexive graphs
17.35.
Equivalences of undirected graphs
17.36.
Eulerian circuits in undirected graphs
17.37.
Faithful morphisms of undirected graphs
17.38.
Fibers of directed graphs
17.39.
Fibers of morphisms into directed graphs
17.40.
Fibers of morphisms into reflexive graphs
17.41.
Finite graphs
17.42.
Geometric realizations of undirected graphs
17.43.
Higher directed graphs
17.44.
Hypergraphs
17.45.
Internal homs of directed graphs
17.46.
Large higher directed graphs
17.47.
Large reflexive graphs
17.48.
Matchings
17.49.
Mere equivalences of undirected graphs
17.50.
Morphisms of dependent directed graphs
17.51.
Morphisms of directed graphs
17.52.
Morphisms of reflexive graphs
17.53.
Morphisms of undirected graphs
17.54.
Incidence in undirected graphs
17.55.
Orientations of undirected graphs
17.56.
Paths in undirected graphs
17.57.
Polygons
17.58.
Raising universe levels of directed graphs
17.59.
Reflecting maps of undirected graphs
17.60.
Reflexive graphs
17.61.
Regular undirected graph
17.62.
Sections of dependent directed graphs
17.63.
Sections of dependent reflexive graphs
17.64.
Simple undirected graphs
17.65.
Stereoisomerism for enriched undirected graphs
17.66.
Terminal directed graphs
17.67.
Terminal reflexive graphs
17.68.
Totally faithful morphisms of undirected graphs
17.69.
Trails in directed graphs
17.70.
Trails in undirected graphs
17.71.
Undirected graph structures on standard finite sets
17.72.
Undirected graphs
17.73.
The universal directed graph
17.74.
The universal reflexive graph
17.75.
Vertex covers
17.76.
Voltage graphs
17.77.
Walks in directed graphs
17.78.
Walks in undirected graphs
17.79.
Wide displayed large reflexive graphs
18.
Group theory
❱
18.1.
Abelian groups
18.2.
Abelianization of groups
18.3.
Pointwise addition of morphisms of abelian groups
18.4.
Arithmetic sequences in semigroups
18.5.
Automorphism groups
18.6.
Cartesian products of abelian groups
18.7.
Cartesian products of concrete groups
18.8.
Cartesian products of groups
18.9.
Cartesian products of monoids
18.10.
Cartesian products of semigroups
18.11.
The category of abelian groups
18.12.
The category of concrete groups
18.13.
The category of group actions
18.14.
The category of groups
18.15.
The orbit category of a group
18.16.
The category of semigroups
18.17.
Cayley's theorem
18.18.
The center of a group
18.19.
Center of a monoid
18.20.
Center of a semigroup
18.21.
Central elements of groups
18.22.
Central elements of monoids
18.23.
Central elements of semirings
18.24.
Centralizer subgroups
18.25.
Characteristic subgroups
18.26.
Commutative monoids
18.27.
Commutator subgroups
18.28.
Commutators of elements in groups
18.29.
Commuting elements of groups
18.30.
Commuting elements of monoids
18.31.
Commuting elements of semigroups
18.32.
Commuting squares of group homomorphisms
18.33.
Concrete group actions
18.34.
Concrete groups
18.35.
Concrete monoids
18.36.
Congruence relations on abelian groups
18.37.
Congruence relations on commutative monoids
18.38.
Congruence relations on groups
18.39.
Congruence relations on monoids
18.40.
Congruence relations on semigroups
18.41.
Conjugation in groups
18.42.
Conjugation on concrete groups
18.43.
Contravariant pushforwards of concrete group actions
18.44.
Cores of monoids
18.45.
Cyclic groups
18.46.
Decidable subgroups of groups
18.47.
Dependent products of abelian groups
18.48.
Dependent products of commutative monoids
18.49.
Dependent products of groups
18.50.
Dependent products of monoids
18.51.
Dependent products of semigroups
18.52.
The dihedral group construction
18.53.
The dihedral groups
18.54.
The E₈-lattice
18.55.
Elements of finite order
18.56.
Embeddings of abelian groups
18.57.
Embeddings of groups
18.58.
The endomorphism rings of abelian groups
18.59.
Epimorphisms in groups
18.60.
Equivalences of concrete group actions
18.61.
Equivalences of concrete groups
18.62.
Equivalences of group actions
18.63.
Equivalences between semigroups
18.64.
Exponents of abelian groups
18.65.
Exponents of groups
18.66.
Free concrete group actions
18.67.
Free groups with one generator
18.68.
The full subgroup of a group
18.69.
The full subsemigroup of a semigroup
18.70.
Function groups of abelian groups
18.71.
Function commutative monoids
18.72.
Function groups
18.73.
Function monoids
18.74.
Function semigroups
18.75.
Functoriality of quotient groups
18.76.
Furstenberg groups
18.77.
Generating elements of groups
18.78.
Generating sets of groups
18.79.
Group actions
18.80.
Abstract groups
18.81.
Homomorphisms of abelian groups
18.82.
Homomorphisms of commutative monoids
18.83.
Morphisms of concrete group actions
18.84.
Homomorphisms of concrete groups
18.85.
Homomorphisms of generated subgroups
18.86.
Homomorphisms of group actions
18.87.
Homomorphisms of groups
18.88.
Homomorphisms of groups equipped with normal subgroups
18.89.
Homomorphisms of monoids
18.90.
Homomorphisms of semigroups
18.91.
Homotopy automorphism groups
18.92.
Images of group homomorphisms
18.93.
Images of semigroup homomorphisms
18.94.
Integer multiples of elements in abelian groups
18.95.
Integer powers of elements of groups
18.96.
Intersections of subgroups of abelian groups
18.97.
Intersections of subgroups of groups
18.98.
Inverse semigroups
18.99.
Invertible elements in monoids
18.100.
Isomorphisms of abelian groups
18.101.
Isomorphisms of concrete groups
18.102.
Isomorphisms of group actions
18.103.
Isomorphisms of groups
18.104.
Isomorphisms of monoids
18.105.
Isomorphisms of semigroups
18.106.
Iterated cartesian products of concrete groups
18.107.
Kernels of homomorphisms between abelian groups
18.108.
Kernels of homomorphisms of concrete groups
18.109.
Kernels of homomorphisms of groups
18.110.
Large semigroups
18.111.
Concrete automorphism groups on sets
18.112.
Mere equivalences of concrete group actions
18.113.
Mere equivalences of group actions
18.114.
Minkowski multiplication of subsets of a commutative monoid
18.115.
Minkowski multiplication on subsets of a monoid
18.116.
Minkowski multiplication on subsets of a semigroup
18.117.
Monoid actions
18.118.
Monoids
18.119.
Monomorphisms of concrete groups
18.120.
Monomorphisms in the category of groups
18.121.
Multiples of elements in abelian groups
18.122.
Nontrivial groups
18.123.
Normal closures of subgroups
18.124.
Normal cores of subgroups
18.125.
Normal subgroups
18.126.
Normal subgroups of concrete groups
18.127.
Normal submonoids
18.128.
Normal submonoids of commutative monoids
18.129.
Normalizer subgroups
18.130.
Nullifying group homomorphisms
18.131.
The opposite of a group
18.132.
The opposite of a semigroup
18.133.
The orbit-stabilizer theorem for concrete groups
18.134.
Orbits of concrete group actions
18.135.
Orbits of group actions
18.136.
The order of an element in a group
18.137.
Perfect cores
18.138.
Perfect groups
18.139.
Perfect subgroups
18.140.
Powers of elements in commutative monoids
18.141.
Powers of elements in groups
18.142.
Powers of elements in monoids
18.143.
The precategory of commutative monoids
18.144.
The precategory of concrete groups
18.145.
The precategory of group actions
18.146.
The precategory of groups
18.147.
The precategory of monoids
18.148.
The precategory of orbits of a monoid action
18.149.
The precategory of semigroups
18.150.
Principal group actions
18.151.
Principal torsors of concrete groups
18.152.
Products of elements in a monoid
18.153.
Products of tuples of elements in commutative monoids
18.154.
Pullbacks of subgroups
18.155.
Pullbacks of subsemigroups
18.156.
Quotient groups
18.157.
Quotient groups of concrete groups
18.158.
Quotients of abelian groups
18.159.
Rational commutative monoids
18.160.
Representations of monoids in precategories
18.161.
Saturated congruence relations on commutative monoids
18.162.
Saturated congruence relations on monoids
18.163.
Semigroups
18.164.
Sheargroups
18.165.
Shriek of concrete group homomorphisms
18.166.
Stabilizer groups
18.167.
Stabilizers of concrete group actions
18.168.
Subgroups
18.169.
Subgroups of abelian groups
18.170.
Subgroups of concrete groups
18.171.
Subgroups generated by elements of a group
18.172.
Subgroups generated by families of elements
18.173.
Subgroups generated by subsets of groups
18.174.
Submonoids
18.175.
Submonoids of commutative monoids
18.176.
Subsemigroups
18.177.
Subsets of abelian groups
18.178.
Subsets of commutative monoids
18.179.
Subsets of groups
18.180.
Subsets of monoids
18.181.
Subsets of semigroups
18.182.
The substitution functor of concrete group actions
18.183.
The substitution functor of group actions
18.184.
Surjective group homomorphisms
18.185.
Surjective semigroup homomorphisms
18.186.
Symmetric concrete groups
18.187.
Symmetric groups
18.188.
Torsion elements of groups
18.189.
Torsion-free groups
18.190.
Torsors of abstract groups
18.191.
Transitive concrete group actions
18.192.
Transitive group actions
18.193.
Trivial concrete groups
18.194.
Trivial group homomorphisms
18.195.
Trivial groups
18.196.
Trivial subgroups
18.197.
Unordered tuples of elements in commutative monoids
18.198.
Wild representations of monoids
19.
Higher group theory
❱
19.1.
Abelian higher groups
19.2.
Automorphism groups
19.3.
Cartesian products of higher groups
19.4.
Conjugation in higher groups
19.5.
Cyclic higher groups
19.6.
Deloopable groups
19.7.
Deloopable H-spaces
19.8.
Deloopable types
19.9.
Eilenberg-Mac Lane spaces
19.10.
Equivalences of higher groups
19.11.
Fixed points of higher group actions
19.12.
Free higher group actions
19.13.
Higher group actions
19.14.
Higher groups
19.15.
Homomorphisms of higher group actions
19.16.
Homomorphisms of higher groups
19.17.
The higher group of integers
19.18.
Iterated cartesian products of higher groups
19.19.
Iterated deloopings of pointed types
19.20.
Orbits of higher group actions
19.21.
Small ∞-groups
19.22.
Subgroups of higher groups
19.23.
Symmetric higher groups
19.24.
Transitive higher group actions
19.25.
Trivial higher groups
20.
Linear algebra
❱
20.1.
Constant matrices
20.2.
Diagonal vectors
20.3.
Diagonal matrices on rings
20.4.
Functoriality of the type of matrices
20.5.
Functoriality of the type of vectors
20.6.
Matrices
20.7.
Matrices on rings
20.8.
Multiplication of matrices
20.9.
Scalar multiplication on matrices
20.10.
Scalar multiplication of vectors
20.11.
Scalar multiplication of vectors on rings
20.12.
Transposition of matrices
20.13.
Vectors
20.14.
Vectors on commutative rings
20.15.
Vectors on commutative semirings
20.16.
Vectors on euclidean domains
20.17.
Vectors on rings
20.18.
Vectors on semirings
21.
Lists
❱
21.1.
Arrays
21.2.
Concatenation of lists
21.3.
Flattening of lists
21.4.
Functoriality of the list operation
21.5.
Lists
21.6.
Lists of elements in discrete types
21.7.
Permutations of lists
21.8.
Permutations of vectors
21.9.
Predicates on lists
21.10.
Quicksort for lists
21.11.
Reversing lists
21.12.
Sort by insertion for lists
21.13.
Sort by insertion for vectors
21.14.
Sorted lists
21.15.
Sorted vectors
21.16.
Sorting algorithms for lists
21.17.
Sorting algorithms for vectors
21.18.
The universal property of lists with respect to wild monoids
22.
Logic
❱
22.1.
Complements of De Morgan subtypes
22.2.
Complements of decidable subtypes
22.3.
Complements of double negation stable subtypes
22.4.
De Morgan embeddings
22.5.
De Morgan maps
22.6.
De Morgan propositions
22.7.
De Morgan subtypes
22.8.
De Morgan types
22.9.
De Morgan's law
22.10.
Double negation eliminating maps
22.11.
Double negation elimination
22.12.
Double negation stable embeddings
22.13.
Double negation stable subtypes
22.14.
Functoriality of existential quantification
22.15.
Markovian types
22.16.
Markov's principle
23.
Metric spaces
❱
23.1.
The category of metric spaces and isometries
23.2.
The category of metric spaces and short maps
23.3.
Cauchy approximations in metric spaces
23.4.
Cauchy approximations in premetric spaces
23.5.
Cauchy sequences in complete metric spaces
23.6.
Cauchy sequences in metric spaces
23.7.
Closed premetric structures
23.8.
Complete metric spaces
23.9.
Continuous functions between metric spaces
23.10.
Continuous functions between premetric spaces
23.11.
Convergent Cauchy approximations in metric spaces
23.12.
Convergent sequences in metric spaces
23.13.
Dependent products of metric spaces
23.14.
Discrete premetric structures
23.15.
Equality of metric spaces
23.16.
Equality of premetric spaces
23.17.
Extensional premetric structures on types
23.18.
Functions between metric spaces
23.19.
The functor from the precategory of metric spaces and isometries to the precategory of sets
23.20.
The inclusion of isometries into the category of metric spaces and short maps
23.21.
Induced premetric structures on preimages
23.22.
Isometric equivalences between premetric spaces
23.23.
Isometries between metric spaces
23.24.
Isometries between premetric spaces
23.25.
Limits of Cauchy approximations in premetric spaces
23.26.
Limits of sequences in metric spaces
23.27.
Limits of sequences in premetric spaces
23.28.
Limits of sequences in pseudometric spaces
23.29.
The metric space of Cauchy approximations in a complete metric space
23.30.
The metric space of Cauchy approximations in a metric space
23.31.
The metric space of Cauchy approximations in a saturated complete metric space
23.32.
The metric space of convergent Cauchy approximations in a metric space
23.33.
The metric space of convergent sequences in metric spaces
23.34.
The metric space of functions between metric spaces
23.35.
The metric space of isometries between metric spaces
23.36.
The standard metric structure on the rational numbers
23.37.
The metric structure on the rational numbers with open neighborhoods
23.38.
The metric space of short functions between metric spaces
23.39.
Metric spaces
23.40.
Metric structures
23.41.
Monotonic premetric structures on types
23.42.
The poset of premetric structures on a type
23.43.
The precategory of metric spaces and functions
23.44.
The precategory of metric spaces and isometries
23.45.
The precategory of metric spaces and short functions
23.46.
Premetric spaces
23.47.
Premetric structures on types
23.48.
Pseudometric spaces
23.49.
Pseudometric structures on a type
23.50.
Reflexive premetric structures on types
23.51.
Saturated complete metric spaces
23.52.
Saturated metric spaces
23.53.
Sequences in metric spaces
23.54.
Sequences in premetric spaces
23.55.
Sequences in pseudometric spaces
23.56.
Short functions between metric spaces
23.57.
Short functions between premetric spaces
23.58.
Subspaces of metric spaces
23.59.
Symmetric premetric structures on types
23.60.
Triangular premetric structures on types
23.61.
Uniformly continuous functions between metric spaces
23.62.
Uniformly continuous functions between premetric spaces
24.
Modal type theory
❱
24.1.
The action on homotopies of the flat modality
24.2.
The action on identifications of crisp functions
24.3.
The action on identifications of the flat modality
24.4.
Crisp cartesian product types
24.5.
Crisp coproduct types
24.6.
Crisp dependent function types
24.7.
Crisp dependent pair types
24.8.
Crisp function types
24.9.
Crisp identity types
24.10.
The crisp law of excluded middle
24.11.
Crisp pullbacks
24.12.
Crisp types
24.13.
Dependent universal property of flat discrete crisp types
24.14.
Flat discrete crisp types
24.15.
The flat modality
24.16.
The flat-sharp adjunction
24.17.
Functoriality of the flat modality
24.18.
Functoriality of the sharp modality
24.19.
Sharp codiscrete maps
24.20.
Sharp codiscrete types
24.21.
The sharp modality
24.22.
Transport along crisp identifications
24.23.
The universal property of flat discrete crisp types
25.
Order theory
❱
25.1.
Accessible elements with respect to relations
25.2.
Bottom elements in large posets
25.3.
Bottom elements in posets
25.4.
Bottom elements in preorders
25.5.
Chains in posets
25.6.
Chains in preorders
25.7.
Closure operators on large locales
25.8.
Closure operators on large posets
25.9.
Commuting squares of Galois connections between large posets
25.10.
Commuting squares of order preserving maps of large posets
25.11.
Coverings in locales
25.12.
Decidable posets
25.13.
Decidable preorders
25.14.
Decidable subposets
25.15.
Decidable subpreorders
25.16.
Decidable total orders
25.17.
Decidable total preorders
25.18.
Deflationary maps on a poset
25.19.
Deflationary maps on a preorder
25.20.
Dependent products of large frames
25.21.
Dependent products of large inflattices
25.22.
Dependent products of large locales
25.23.
Dependent products of large meet-semilattices
25.24.
Dependent products of large posets
25.25.
Dependent products of large preorders
25.26.
Dependent products of large suplattices
25.27.
Distributive lattices
25.28.
Finite coverings in locales
25.29.
Finite posets
25.30.
Finite preorders
25.31.
Finite total orders
25.32.
Finitely graded posets
25.33.
Frames
25.34.
Galois connections
25.35.
Galois connections between large posets
25.36.
Greatest lower bounds in large posets
25.37.
Greatest lower bounds in posets
25.38.
Homomorphisms of frames
25.39.
Homomorphisms of large frames
25.40.
Homomorphisms of large locales
25.41.
Homomorphisms of large meet-semilattices
25.42.
Homomorphisms of large suplattices
25.43.
Homomorphisms of meet-semilattices
25.44.
Homomorphisms of meet-suplattices
25.45.
Homomorphisms of suplattices
25.46.
Ideals in preorders
25.47.
Incidence algebras
25.48.
Increasing sequences in partially ordered sets
25.49.
Inflationary maps on a poset
25.50.
Inflationary maps on a preorder
25.51.
Inflattices
25.52.
Inhabited chains in posets
25.53.
Inhabited chains in preorders
25.54.
Inhabited finite total orders
25.55.
Interval subposets
25.56.
Join preserving maps between posets
25.57.
Join-semilattices
25.58.
The Knaster–Tarski fixed point theorem
25.59.
Large frames
25.60.
Large inflattices
25.61.
Large join-semilattices
25.62.
Large locales
25.63.
Large meet-semilattices
25.64.
Large meet-subsemilattices
25.65.
Large posets
25.66.
Large preorders
25.67.
Large quotient locales
25.68.
Large strict orders
25.69.
Large strict preorders
25.70.
Large subframes
25.71.
Large subposets
25.72.
Large subpreorders
25.73.
Large subsuplattices
25.74.
Large suplattices
25.75.
Lattices
25.76.
Least upper bounds in large posets
25.77.
Least upper bounds in posets
25.78.
Locales
25.79.
Locally finite posets
25.80.
Lower bounds in large posets
25.81.
Lower bounds in posets
25.82.
Lower sets in large posets
25.83.
Lower types in preorders
25.84.
Maximal chains in posets
25.85.
Maximal chains in preorders
25.86.
Meet-semilattices
25.87.
Meet-suplattices
25.88.
Nuclei on large locales
25.89.
Opposite large posets
25.90.
Opposite large preorders
25.91.
Opposite posets
25.92.
Opposite preorders
25.93.
Order preserving maps between large posets
25.94.
Order preserving maps between large preorders
25.95.
Order preserving maps between posets
25.96.
Order preserving maps between preorders
25.97.
Ordinals
25.98.
Posets
25.99.
Powers of large locales
25.100.
The precategory of decidable total orders
25.101.
The precategory of finite posets
25.102.
The precategory of finite total orders
25.103.
The precategory of inhabited finite total orders
25.104.
The precategory of posets
25.105.
The precategory of total orders
25.106.
Preorders
25.107.
Principal lower sets of large posets
25.108.
Principal upper sets of large posets
25.109.
Reflective Galois connections between large posets
25.110.
Resizing posets
25.111.
Resizing preorders
25.112.
Resizing suplattices
25.113.
Sequences in partially ordered sets
25.114.
Sequences in preorders
25.115.
Sequences in strictly preordered sets
25.116.
Similarity of elements in large posets
25.117.
Similarity of elements in large preorders
25.118.
Similarity of elements in large strict orders
25.119.
Similarity of elements in large strict preorders
25.120.
Similarity of elements in strict orders
25.121.
Similarity of elements in strict preorders
25.122.
Similarity of order preserving maps between large posets
25.123.
Similarity of order preserving maps between large preorders
25.124.
Strict order preserving maps
25.125.
Strict orders
25.126.
Strict preorders
25.127.
Strictly increasing sequences in strictly preordered sets
25.128.
Strictly inflationary maps on a strictly preordered type
25.129.
Strictly preordered sets
25.130.
Subposets
25.131.
Subpreorders
25.132.
Suplattices
25.133.
Supremum preserving maps between posets
25.134.
Top elements in large posets
25.135.
Top elements in posets
25.136.
Top elements in preorders
25.137.
Total orders
25.138.
Total preorders
25.139.
Transitive well-founded relations
25.140.
Transposing inequalities in posets along order-preserving retractions
25.141.
Transposing inequalities in posets along sections of order-preserving maps
25.142.
Upper bounds of chains in posets
25.143.
Upper bounds in large posets
25.144.
Upper bounds in posets
25.145.
Upper sets of large posets
25.146.
Well-founded relations
25.147.
Zorn's lemma
26.
Organic chemistry
❱
26.1.
Alcohols
26.2.
Alkanes
26.3.
Alkenes
26.4.
Alkynes
26.5.
Ethane
26.6.
Hydrocarbons
26.7.
Methane
26.8.
Saturated carbons
27.
Orthogonal factorization systems
❱
27.1.
Cd-structures
27.2.
Cellular maps
27.3.
The closed modalities
27.4.
Continuation modalities
27.5.
Double lifts of families of elements
27.6.
Double negation sheaves
27.7.
Extensions of double lifts of families of elements
27.8.
Extensions of families of elements
27.9.
Extensions of maps
27.10.
Factorization operations
27.11.
Factorization operations into function classes
27.12.
Factorization operations into global function classes
27.13.
Factorizations of maps
27.14.
Factorizations of maps into function classes
27.15.
Factorizations of maps into global function classes
27.16.
Families of types local at a map
27.17.
Fiberwise orthogonal maps
27.18.
Function classes
27.19.
Functoriality of higher modalities
27.20.
Functoriality of localizations at global subuniverses
27.21.
Functoriality of the pullback-hom
27.22.
Functoriality of reflective global subuniverses
27.23.
Global function classes
27.24.
Higher modalities
27.25.
The identity modality
27.26.
Large Lawvere–Tierney topologies
27.27.
Lawvere–Tierney topologies
27.28.
Lifting operations
27.29.
Lifting structures on commuting squares of maps
27.30.
Lifts of families of elements
27.31.
Lifts of maps
27.32.
Localizations at global subuniverses
27.33.
Localizations at maps
27.34.
Localizations at subuniverses
27.35.
Locally small modal-operators
27.36.
Maps local at maps
27.37.
Mere lifting properties
27.38.
Modal induction
27.39.
Modal operators
27.40.
Modal subuniverse induction
27.41.
Null families of types
27.42.
Null maps
27.43.
Null types
27.44.
The open modalities
27.45.
Orthogonal factorization systems
27.46.
Orthogonal maps
27.47.
Precomposition of lifts of families of elements by maps
27.48.
The pullback-hom
27.49.
The raise modalities
27.50.
Reflective global subuniverses
27.51.
Reflective modalities
27.52.
Reflective subuniverses
27.53.
Regular cd-structures
27.54.
Σ-closed modalities
27.55.
Σ-closed reflective modalities
27.56.
Σ-closed reflective subuniverses
27.57.
Stable orthogonal factorization systems
27.58.
Types colocal at maps
27.59.
Types local at maps
27.60.
Types separated at maps
27.61.
Uniquely eliminating modalities
27.62.
The universal property of localizations at global subuniverses
27.63.
Wide function classes
27.64.
Wide global function classes
27.65.
The zero modality
28.
Polytopes
❱
28.1.
Abstract polytopes
29.
Primitives
❱
29.1.
Characters
29.2.
Floats
29.3.
Machine integers
29.4.
Strings
30.
Real numbers
❱
30.1.
The absolute value of real numbers
30.2.
Addition of lower Dedekind real numbers
30.3.
Addition of Dedekind real numbers
30.4.
Addition of upper Dedekind real numbers
30.5.
Apartness of real numbers
30.6.
Arithmetically located Dedekind cuts
30.7.
Cauchy completeness of the Dedekind real numbers
30.8.
Dedekind real numbers
30.9.
The difference between real numbers
30.10.
The distance between real numbers
30.11.
Inequality on the lower Dedekind real numbers
30.12.
Inequality on the real numbers
30.13.
Inequality on the upper Dedekind real numbers
30.14.
The addition isometry on real numbers
30.15.
The negation isometry on real numbers
30.16.
Lower Dedekind real numbers
30.17.
The maximum of lower Dedekind real numbers
30.18.
The maximum of real numbers
30.19.
The maximum of upper Dedekind real numbers
30.20.
The metric space of real numbers
30.21.
The minimum of lower Dedekind real numbers
30.22.
The minimum of real numbers
30.23.
The minimum of upper Dedekind real numbers
30.24.
Negation of lower and upper Dedekind real numbers
30.25.
Negation of real numbers
30.26.
Nonnegative real numbers
30.27.
Positive real numbers
30.28.
Raising the universe levels of real numbers
30.29.
Rational lower Dedekind real numbers
30.30.
Rational real numbers
30.31.
Rational upper Dedekind real numbers
30.32.
Similarity of real numbers
30.33.
Strict inequality of real numbers
30.34.
Transposition of addition and subtraction through cuts of Dedekind real numbers
30.35.
Upper Dedekind real numbers
31.
Reflection
❱
31.1.
Abstractions
31.2.
Arguments
31.3.
Boolean reflection
31.4.
Definitions
31.5.
Erasing equality
31.6.
Fixity
31.7.
Group solver
31.8.
Literals
31.9.
Metavariables
31.10.
Names
31.11.
Precategory solver
31.12.
Rewriting
31.13.
Terms
31.14.
The type checking monad
32.
Ring theory
❱
32.1.
Additive orders of elements of rings
32.2.
Algebras over rings
32.3.
The binomial theorem for rings
32.4.
The binomial theorem for semirings
32.5.
The category of cyclic rings
32.6.
The category of rings
32.7.
Central elements of rings
32.8.
Central elements of semirings
32.9.
Characteristics of rings
32.10.
Commuting elements of rings
32.11.
Congruence relations on rings
32.12.
Congruence relations on semirings
32.13.
Cyclic rings
32.14.
Dependent products of rings
32.15.
Dependent products of semirings
32.16.
Division rings
32.17.
The free ring with one generator
32.18.
Full ideals of rings
32.19.
Function rings
32.20.
Function semirings
32.21.
Generating elements of rings
32.22.
The group of multiplicative units of a ring
32.23.
Homomorphisms of cyclic rings
32.24.
Homomorphisms of rings
32.25.
Homomorphisms of semirings
32.26.
Ideals generated by subsets of rings
32.27.
Ideals of rings
32.28.
Ideals of semirings
32.29.
Idempotent elements in rings
32.30.
Initial rings
32.31.
Integer multiples of elements of rings
32.32.
Intersections of ideals of rings
32.33.
Intersections of ideals of semirings
32.34.
The invariant basis property of rings
32.35.
Invertible elements in rings
32.36.
Isomorphisms of rings
32.37.
Joins of ideals of rings
32.38.
Joins of left ideals of rings
32.39.
Joins of right ideals of rings
32.40.
Kernels of ring homomorphisms
32.41.
Left ideals generated by subsets of rings
32.42.
Left ideals of rings
32.43.
Local rings
32.44.
Localizations of rings
32.45.
Maximal ideals of rings
32.46.
Modules over rings
32.47.
Multiples of elements in rings
32.48.
Multiplicative orders of elements of rings
32.49.
Nil ideals of rings
32.50.
Nilpotent elements in rings
32.51.
Nilpotent elements in semirings
32.52.
Opposite rings
32.53.
The poset of cyclic rings
32.54.
The poset of ideals of a ring
32.55.
The poset of left ideals of a ring
32.56.
The poset of right ideals of a ring
32.57.
Powers of elements in rings
32.58.
Powers of elements in semirings
32.59.
The precategory of rings
32.60.
The precategory of semirings
32.61.
Products of ideals of rings
32.62.
Products of left ideals of rings
32.63.
Products of right ideals of rings
32.64.
Products of rings
32.65.
Products of subsets of rings
32.66.
Quotient rings
32.67.
Radical ideals of rings
32.68.
Right ideals generated by subsets of rings
32.69.
Right ideals of rings
32.70.
Rings
32.71.
Semirings
32.72.
Subsets of rings
32.73.
Subsets of semirings
32.74.
Sums of elements in rings
32.75.
Sums of elements in semirings
32.76.
Transporting ring structures along isomorphisms of abelian groups
32.77.
Trivial rings
33.
Set theory
❱
33.1.
Baire space
33.2.
Cantor space
33.3.
Cantor's diagonal argument
33.4.
Cardinalities of sets
33.5.
Countable sets
33.6.
Cumulative hierarchy
33.7.
Infinite sets
33.8.
Russell's paradox
33.9.
Uncountable sets
34.
Species
❱
34.1.
Cartesian exponents of species
34.2.
Cartesian products of species of types
34.3.
Cauchy composition of species of types
34.4.
Cauchy composition of species of types in a subuniverse
34.5.
Cauchy exponentials of species of types
34.6.
Cauchy exponentials of species of types in a subuniverse
34.7.
Cauchy products of species of types
34.8.
Cauchy products of species of types in a subuniverse
34.9.
Cauchy series of species of types
34.10.
Cauchy series of species of types in a subuniverse
34.11.
Composition of Cauchy series of species of types
34.12.
Composition of Cauchy series of species of types in subuniverses
34.13.
Coproducts of species of types
34.14.
Coproducts of species of types in subuniverses
34.15.
Cycle index series of species
34.16.
Derivatives of species
34.17.
Dirichlet exponentials of a species of types
34.18.
Dirichlet exponentials of species of types in a subuniverse
34.19.
Dirichlet products of species of types
34.20.
Dirichlet products of species of types in subuniverses
34.21.
Dirichlet series of species of finite inhabited types
34.22.
Dirichlet series of species of types
34.23.
Dirichlet series of species of types in subuniverses
34.24.
Equivalences of species of types
34.25.
Equivalences of species of types in subuniverses
34.26.
Exponential of Cauchy series of species of types
34.27.
Exponential of Cauchy series of species of types in subuniverses
34.28.
Hasse-Weil species
34.29.
Morphisms of finite species
34.30.
Morphisms of species of types
34.31.
Pointing of species of types
34.32.
The precategory of finite species
34.33.
Products of Cauchy series of species of types
34.34.
Products of Cauchy series of species of types in subuniverses
34.35.
Products of Dirichlet series of species of finite inhabited types
34.36.
Products of Dirichlet series of species of types
34.37.
Products of Dirichlet series of species of types in subuniverses
34.38.
Small Composition of species of finite inhabited types
34.39.
Small Cauchy composition of species types in subuniverses
34.40.
Species of finite inhabited types
34.41.
Species of finite types
34.42.
Species of inhabited types
34.43.
Species of types
34.44.
Species of types in subuniverses
34.45.
The unit of Cauchy composition of types
34.46.
The unit of Cauchy composition of species of types in subuniverses
34.47.
Unlabeled structures of finite species
35.
Structured types
❱
35.1.
Cartesian products of types equipped with endomorphisms
35.2.
Central H-spaces
35.3.
Commuting squares of pointed homotopies
35.4.
Commuting squares of pointed maps
35.5.
Commuting triangles of pointed maps
35.6.
Conjugation of pointed types
35.7.
Constant pointed maps
35.8.
Contractible pointed types
35.9.
Cyclic types
35.10.
Dependent products of H-spaces
35.11.
Dependent products of pointed types
35.12.
Dependent products of wild monoids
35.13.
Dependent types equipped with automorphisms
35.14.
Equivalences of H-spaces
35.15.
Equivalences of pointed arrows
35.16.
Equivalences of types equipped with automorphisms
35.17.
Equivalences of types equipped with endomorphisms
35.18.
Faithful pointed maps
35.19.
Fibers of pointed maps
35.20.
Finite multiplication in magmas
35.21.
Function H-spaces
35.22.
Function magmas
35.23.
Function wild monoids
35.24.
H-spaces
35.25.
The initial pointed type equipped with an automorphism
35.26.
The involutive type of H-space structures on a pointed type
35.27.
Involutive types
35.28.
Iterated cartesian products of types equipped with endomorphisms
35.29.
Iterated cartesian products of pointed types
35.30.
Magmas
35.31.
Mere equivalences of types equipped with endomorphisms
35.32.
Morphisms of H-spaces
35.33.
Morphisms of magmas
35.34.
Morphisms of pointed arrows
35.35.
Morphisms of twisted pointed arrows
35.36.
Morphisms of types equipped with automorphisms
35.37.
Morphisms of types equipped with endomorphisms
35.38.
Morphisms of wild monoids
35.39.
Noncoherent H-spaces
35.40.
Opposite pointed spans
35.41.
Pointed 2-homotopies
35.42.
Pointed cartesian product types
35.43.
Pointed dependent functions
35.44.
Pointed dependent pair types
35.45.
Pointed equivalences
35.46.
Pointed families of types
35.47.
Pointed homotopies
35.48.
Pointed isomorphisms
35.49.
Pointed maps
35.50.
Pointed retractions of pointed maps
35.51.
Pointed sections of pointed maps
35.52.
Pointed span diagrams
35.53.
Pointed spans
35.54.
Pointed types
35.55.
Pointed types equipped with automorphisms
35.56.
The pointed unit type
35.57.
Universal property of contractible types with respect to pointed types and maps
35.58.
Postcomposition of pointed maps
35.59.
Precomposition of pointed maps
35.60.
Sets equipped with automorphisms
35.61.
Small pointed types
35.62.
Symmetric elements of involutive types
35.63.
Symmetric H-spaces
35.64.
Transposition of pointed span diagrams
35.65.
Types equipped with automorphisms
35.66.
Types equipped with endomorphisms
35.67.
Uniform pointed homotopies
35.68.
The universal property of pointed equivalences
35.69.
Unpointed maps between pointed types
35.70.
Whiskering pointed homotopies with respect to concatenation
35.71.
Whiskering of pointed homotopies with respect to composition of pointed maps
35.72.
The wild category of pointed types
35.73.
Wild groups
35.74.
Wild loops
35.75.
Wild monoids
35.76.
Wild quasigroups
35.77.
Wild semigroups
36.
Synthetic category theory
❱
36.1.
Cone diagrams of synthetic categories
36.2.
Cospans of synthetic categories
36.3.
Equivalences between synthetic categories
36.4.
Invertible functors between synthetic categories
36.5.
Pullbacks of synthetic categories
36.6.
Retractions of functors between synthetic categories
36.7.
Sections of functor between synthetic categories
36.8.
Synthetic categories
37.
Synthetic homotopy theory
❱
37.1.
0-acyclic maps
37.2.
0-acyclic types
37.3.
1-acyclic types
37.4.
Acyclic maps
37.5.
Acyclic types
37.6.
The category of connected set bundles over the circle
37.7.
Cavallo's trick
37.8.
The circle
37.9.
Cocartesian morphisms of arrows
37.10.
Cocones under pointed span diagrams
37.11.
Cocones under sequential diagrams
37.12.
Cocones under spans
37.13.
Codiagonals of maps
37.14.
Coequalizers
37.15.
Cofibers of maps
37.16.
Cofibers of pointed maps
37.17.
Coforks
37.18.
Correspondence between cocones under sequential diagrams and certain coforks
37.19.
Conjugation of loops
37.20.
Connected set bundles over the circle
37.21.
Connective prespectra
37.22.
Connective spectra
37.23.
Dependent cocones under sequential diagrams
37.24.
Dependent cocones under spans
37.25.
Dependent coforks
37.26.
Dependent descent for the circle
37.27.
The dependent pullback property of pushouts
37.28.
Dependent pushout-products
37.29.
Dependent sequential diagrams
37.30.
Dependent suspension structures
37.31.
The dependent universal property of coequalizers
37.32.
The dependent universal property of pushouts
37.33.
The dependent universal property of sequential colimits
37.34.
Dependent universal property of suspensions
37.35.
The descent property of the circle
37.36.
Descent data for constant type families over the circle
37.37.
Descent data for families of dependent pair types over the circle
37.38.
Descent data for families of equivalence types over the circle
37.39.
Descent data for families of function types over the circle
37.40.
Subtypes of descent data for the circle
37.41.
Descent data for type families of equivalence types over pushouts
37.42.
Descent data for type families of function types over pushouts
37.43.
Descent data for type families of identity types over pushouts
37.44.
Descent data for pushouts
37.45.
Descent data for sequential colimits
37.46.
Descent property of pushouts
37.47.
Descent property of sequential colimits
37.48.
Double loop spaces
37.49.
The Eckmann-Hilton argument
37.50.
Equifibered sequential diagrams
37.51.
Equivalences of cocones under sequential diagrams
37.52.
Equivalences of coforks
37.53.
Equivalances of dependent sequential diagrams
37.54.
Equivalences of descent data for pushouts
37.55.
Equivalences of sequential diagrams
37.56.
Families with descent data for pushouts
37.57.
Families with descent data for sequential colimits
37.58.
The flattening lemma for coequalizers
37.59.
The flattening lemma for pushouts
37.60.
The flattening lemma for sequential colimits
37.61.
Free loops
37.62.
Functoriality of the loop space operation
37.63.
Functoriality of sequential colimits
37.64.
Functoriality of suspensions
37.65.
Groups of loops in 1-types
37.66.
Hatcher's acyclic type
37.67.
Homotopy groups
37.68.
Identity systems of descent data for pushouts
37.69.
The induction principle of pushouts
37.70.
The infinite complex projective space
37.71.
Infinite cyclic types
37.72.
The interval
37.73.
Iterated loop spaces
37.74.
Iterated suspensions of pointed types
37.75.
Join powers of types
37.76.
Joins of maps
37.77.
Joins of types
37.78.
Left half-smash products
37.79.
The loop homotopy on the circle
37.80.
Loop spaces
37.81.
Maps of prespectra
37.82.
Mere spheres
37.83.
Morphisms of cocones under morphisms of sequential diagrams
37.84.
Morphisms of coforks
37.85.
Morphisms of dependent sequential diagrams
37.86.
Morphisms of descent data of the circle
37.87.
Morphisms of descent data for pushouts
37.88.
Morphisms of sequential diagrams
37.89.
The multiplication operation on the circle
37.90.
Null cocones under pointed span diagrams
37.91.
The plus-principle
37.92.
Powers of loops
37.93.
Premanifolds
37.94.
Prespectra
37.95.
The pullback property of pushouts
37.96.
Pushout-products
37.97.
Pushouts
37.98.
Pushouts of pointed types
37.99.
The recursion principle of pushouts
37.100.
Retracts of sequential diagrams
37.101.
Rewriting rules for pushouts
37.102.
Sections of families over the circle
37.103.
Sections of descent data for pushouts
37.104.
Sequential colimits
37.105.
Sequential diagrams
37.106.
Sequentially compact types
37.107.
Shifts of sequential diagrams
37.108.
Smash products of pointed types
37.109.
Spectra
37.110.
The sphere prespectrum
37.111.
Spheres
37.112.
Suspension prespectra
37.113.
Suspension Structures
37.114.
Suspensions of pointed types
37.115.
Suspensions of propositions
37.116.
Suspensions of types
37.117.
Tangent spheres
37.118.
Total cocones of type families over cocones under sequential diagrams
37.119.
Total sequential diagrams of dependent sequential diagrams
37.120.
Triple loop spaces
37.121.
k-acyclic maps
37.122.
k-acyclic types
37.123.
The universal cover of the circle
37.124.
The universal property of the circle
37.125.
The universal property of coequalizers
37.126.
The universal property of pushouts
37.127.
The universal property of sequential colimits
37.128.
Universal property of suspensions
37.129.
Universal Property of suspensions of pointed types
37.130.
Wedges of pointed types
37.131.
Zigzags between sequential diagrams
38.
Trees
❱
38.1.
Algebras for polynomial endofunctors
38.2.
Bases of directed trees
38.3.
Bases of enriched directed trees
38.4.
Binary W-types
38.5.
Bounded multisets
38.6.
The coalgebra of directed trees
38.7.
The coalgebra of enriched directed trees
38.8.
Coalgebras of polynomial endofunctors
38.9.
The combinator of directed trees
38.10.
Combinators of enriched directed trees
38.11.
Directed trees
38.12.
The elementhood relation on coalgebras of polynomial endofunctors
38.13.
The elementhood relation on W-types
38.14.
Empty multisets
38.15.
Enriched directed trees
38.16.
Equivalences of directed trees
38.17.
Equivalences of enriched directed trees
38.18.
Extensional W-types
38.19.
Fibers of directed trees
38.20.
Fibers of enriched directed trees
38.21.
Full binary trees
38.22.
Functoriality of the combinator of directed trees
38.23.
Functoriality of the fiber operation on directed trees
38.24.
Functoriality of W-types
38.25.
Hereditary W-types
38.26.
Indexed W-types
38.27.
Induction principles on W-types
38.28.
Inequality on W-types
38.29.
Lower types of elements in W-types
38.30.
Morphisms of algebras of polynomial endofunctors
38.31.
Morphisms of coalgebras of polynomial endofunctors
38.32.
Morphisms of directed trees
38.33.
Morphisms of enriched directed trees
38.34.
Multiset-indexed dependent products of types
38.35.
Multisets
38.36.
Planar binary trees
38.37.
Plane trees
38.38.
Polynomial endofunctors
38.39.
Raising universe levels of directed trees
38.40.
Ranks of elements in W-types
38.41.
Rooted morphisms of directed trees
38.42.
Rooted morphisms of enriched directed trees
38.43.
Rooted quasitrees
38.44.
Rooted undirected trees
38.45.
Small multisets
38.46.
Submultisets
38.47.
Transitive multisets
38.48.
The underlying trees of elements of coalgebras of polynomial endofunctors
38.49.
The underlying trees of elements of W-types
38.50.
Undirected trees
38.51.
The universal multiset
38.52.
The universal tree
38.53.
The W-type of natural numbers
38.54.
The W-type of the type of propositions
38.55.
W-types
39.
Type theories
❱
39.1.
Comprehension of fibered type theories
39.2.
Dependent type theories
39.3.
Fibered dependent type theories
39.4.
Π-types in precategories with attributes
39.5.
Π-types in precategories with families
39.6.
Precategories with attributes
39.7.
Precategories with families
39.8.
Sections of dependent type theories
39.9.
Simple type theories
39.10.
Unityped type theories
40.
Univalent combinatorics
❱
40.1.
2-element decidable subtypes
40.2.
2-element subtypes
40.3.
2-element types
40.4.
The binomial types
40.5.
Bracelets
40.6.
Cartesian products of finite types
40.7.
The classical definition of the standard finite types
40.8.
Complements of isolated elements of finite types
40.9.
Coproducts of finite types
40.10.
Counting in type theory
40.11.
Counting the elements of decidable subtypes
40.12.
Counting the elements of dependent pair types
40.13.
Counting the elements of the fiber of a map
40.14.
Counting the elements in Maybe
40.15.
Cubes
40.16.
Cycle partitions of finite types
40.17.
Cycle prime decompositions of natural numbers
40.18.
Cyclic finite types
40.19.
De Morgan's law for finite families of propositions
40.20.
Decidable dependent function types
40.21.
Decidability of dependent pair types
40.22.
Decidable equivalence relations on finite types
40.23.
Decidable propositions
40.24.
Decidable subtypes of finite types
40.25.
Dedekind finite sets
40.26.
Counting the elements of dependent function types
40.27.
Dependent pair types of finite types
40.28.
Finite discrete Σ-decompositions
40.29.
Distributivity of set truncation over finite products
40.30.
Double counting
40.31.
Embeddings
40.32.
Embeddings between standard finite types
40.33.
Equality in finite types
40.34.
Equality in the standard finite types
40.35.
Equivalences between finite types
40.36.
Equivalences of cubes
40.37.
Equivalences between standard finite types
40.38.
Ferrers diagrams (unlabeled partitions)
40.39.
Fibers of maps between finite types
40.40.
Finite choice
40.41.
Finite presentations of types
40.42.
Finite types
40.43.
Finiteness of the type of connected components
40.44.
Finitely presented types
40.45.
Finite function types
40.46.
The image of a map
40.47.
Inequality on types equipped with a counting
40.48.
Inhabited finite types
40.49.
Injective maps between finite types
40.50.
An involution on the standard finite types
40.51.
Isotopies of Latin squares
40.52.
Kuratowski finite sets
40.53.
Latin squares
40.54.
Locally finite types
40.55.
The groupoid of main classes of Latin hypercubes
40.56.
The groupoid of main classes of Latin squares
40.57.
The maybe monad on finite types
40.58.
Necklaces
40.59.
Orientations of the complete undirected graph
40.60.
Orientations of cubes
40.61.
Partitions of finite types
40.62.
Petri-nets
40.63.
π-finite types
40.64.
The pigeonhole principle
40.65.
Finitely π-presented types
40.66.
Quotients of finite types
40.67.
Ramsey theory
40.68.
Repetitions of values
40.69.
Repetitions of values in sequences
40.70.
Retracts of finite types
40.71.
Riffle shuffles
40.72.
Sequences of elements in finite types
40.73.
Set quotients of index 2
40.74.
Finite Σ-decompositions of finite types
40.75.
Skipping elements in standard finite types
40.76.
Small types
40.77.
Standard finite pruned trees
40.78.
Standard finite trees
40.79.
The standard finite types
40.80.
Steiner systems
40.81.
Steiner triple systems
40.82.
Combinatorial identities of sums of natural numbers
40.83.
Surjective maps between finite types
40.84.
Symmetric difference of finite subtypes
40.85.
Finite trivial Σ-decompositions
40.86.
Type duality of finite types
40.87.
Unbounded π-finite types
40.88.
Unions of finite subtypes
40.89.
The universal property of the standard finite types
40.90.
Unlabeled partitions
40.91.
Unlabeled rooted trees
40.92.
Unlabeled trees
40.93.
Untruncated π-finite types
41.
Universal algebra
❱
41.1.
Abstract equations over signatures
41.2.
Algebraic theories
41.3.
Algebraic theory of groups
41.4.
Algebras
41.5.
Congruences
41.6.
Homomorphisms of algebras
41.7.
Kernels of homomorphisms of algebras
41.8.
Models of signatures
41.9.
Quotient algebras
41.10.
Signatures
41.11.
Terms over signatures
42.
Wild category theory
❱
42.1.
Coinductive isomorphisms in noncoherent large ω-precategories
42.2.
Coinductive isomorphisms in noncoherent ω-precategories
42.3.
Colax functors between large noncoherent ω-precategories
42.4.
Colax functors between noncoherent ω-precategories
42.5.
Maps between noncoherent large ω-precategories
42.6.
Maps between noncoherent ω-precategories
42.7.
Noncoherent large ω-precategories
42.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 field. Fredrik Bakke. 2025 - perpetuity
The graph of mathematical concepts. Andrej Bauer and Matej Petković. 2023
A dependency graph of the library, color coded by field. Fredrik Bakke. 2025 - perpetuity
The graph of mathematical concepts. Andrej Bauer and Matej Petković. 2023