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