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.
Idempotents in Intensional Type Theory
7.3.
Sequences of the online encyclopedia of integer sequences
7.4.
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.
Pointed endofunctors on categories
8.118.
Pointed endofunctors
8.119.
Precategories
8.120.
Precategory of elements of a presheaf
8.121.
The precategory of functors and natural transformations between two precategories
8.122.
The precategory of functors and natural transformations from small to large precategories
8.123.
The precategory of maps and natural transformations from a small to a large precategory
8.124.
The precategory of maps and natural transformations between two precategories
8.125.
Pregroupoids
8.126.
Presheaf categories
8.127.
Preunivalent categories
8.128.
Products in precategories
8.129.
Products of precategories
8.130.
Pseudomonic functors between precategories
8.131.
Pullbacks in precategories
8.132.
Replete subprecategories
8.133.
Representable functors between categories
8.134.
Representable functors between large precategories
8.135.
Representable functors between precategories
8.136.
The representing arrow category
8.137.
Restrictions of functors to cores of precategories
8.138.
Right extensions in precategories
8.139.
Right Kan extensions in precategories
8.140.
Rigid objects in a category
8.141.
Rigid objects in a precategory
8.142.
Set-magmoids
8.143.
Sieves in categories
8.144.
The simplex category
8.145.
Slice precategories
8.146.
Split essentially surjective functors between precategories
8.147.
Strict categories
8.148.
Structure equivalences between set-magmoids
8.149.
Subcategories
8.150.
Subprecategories
8.151.
Subterminal precategories
8.152.
The terminal category
8.153.
Terminal objects in a precategory
8.154.
Wide subcategories
8.155.
Wide subprecategories
8.156.
The Yoneda lemma for categories
8.157.
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 Ackermann function
11.3.
Addition on integer fractions
11.4.
Addition on the integers
11.5.
Addition on the natural numbers
11.6.
Addition of positive, negative, nonnegative and nonpositive integers
11.7.
Addition on the rational numbers
11.8.
The additive group of rational numbers
11.9.
Arithmetic functions
11.10.
The based induction principle of the natural numbers
11.11.
Based strong induction for the natural numbers
11.12.
Bezout's lemma in the integers
11.13.
Bezout's lemma on the natural numbers
11.14.
The binomial coefficients
11.15.
The binomial theorem for the integers
11.16.
The binomial theorem for the natural numbers
11.17.
Bounded sums of arithmetic functions
11.18.
Catalan numbers
11.19.
The cofibonacci sequence
11.20.
The Collatz bijection
11.21.
The Collatz conjecture
11.22.
The commutative semiring of natural numbers
11.23.
The congruence relations on the integers
11.24.
The congruence relations on the natural numbers
11.25.
The cross-multiplication difference of two integer fractions
11.26.
Cubes of natural numbers
11.27.
Decidable dependent function types
11.28.
The decidable total order of integers
11.29.
The decidable total order of natural numbers
11.30.
The decidable total order of rational numbers
11.31.
The decidable total order of a standard finite type
11.32.
Decidable types in elementary number theory
11.33.
The difference between integers
11.34.
The difference between rational numbers
11.35.
Dirichlet convolution
11.36.
The distance between integers
11.37.
The distance between natural numbers
11.38.
Divisibility of integers
11.39.
Divisibility in modular arithmetic
11.40.
Divisibility of natural numbers
11.41.
The divisibility relation on the standard finite types
11.42.
Equality of integers
11.43.
Equality of natural numbers
11.44.
The Euclid–Mullin sequence
11.45.
Euclidean division on the natural numbers
11.46.
Euler's totient function
11.47.
Exponentiation of natural numbers
11.48.
Factorials of natural numbers
11.49.
Falling factorials
11.50.
Fermat numbers
11.51.
The Fibonacci sequence
11.52.
The field of rational numbers
11.53.
The natural numbers base k
11.54.
Finitely cyclic maps
11.55.
The fundamental theorem of arithmetic
11.56.
The Goldbach conjecture
11.57.
The greatest common divisor of integers
11.58.
The greatest common divisor of natural numbers
11.59.
The group of integers
11.60.
The half-integers
11.61.
The Hardy-Ramanujan number
11.62.
Inequality on integer fractions
11.63.
Inequality on the integers
11.64.
Inequality of natural numbers
11.65.
Inequality on the rational numbers
11.66.
Inequality on the standard finite types
11.67.
The infinitude of primes
11.68.
Initial segments of the natural numbers
11.69.
Integer fractions
11.70.
Integer partitions
11.71.
The integers
11.72.
The Jacobi symbol
11.73.
The Kolakoski sequence
11.74.
The Legendre symbol
11.75.
Lower bounds of type families over the natural numbers
11.76.
Maximum on the natural numbers
11.77.
Maximum on the standard finite types
11.78.
The mediant fraction of two integer fractions
11.79.
Mersenne primes
11.80.
Minimum on the natural numbers
11.81.
Minimum on the standard finite types
11.82.
Modular arithmetic
11.83.
Modular arithmetic on the standard finite types
11.84.
The monoid of natural numbers with addition
11.85.
The monoid of the natural numbers with maximum
11.86.
Multiplication on integer fractions
11.87.
Multiplication of integers
11.88.
Multiplication of the elements of a list of natural numbers
11.89.
Multiplication of natural numbers
11.90.
Multiplication of positive, negative, nonnegative and nonpositive integers
11.91.
Multiplication on the rational numbers
11.92.
The multiplicative group of positive rational numbers
11.93.
The multiplicative group of rational numbers
11.94.
Multiplicative inverses of positive integer fractions
11.95.
The multiplicative monoid of natural numbers
11.96.
The multiplicative monoid of rational numbers
11.97.
Multiplicative units in the integers
11.98.
Multiplicative units in modular arithmetic
11.99.
Multiset coefficients
11.100.
The type of natural numbers
11.101.
The negative integers
11.102.
The nonnegative integers
11.103.
The nonpositive integers
11.104.
Nonzero integers
11.105.
Nonzero natural numbers
11.106.
Nonzero rational numbers
11.107.
The ordinal induction principle for the natural numbers
11.108.
Parity of the natural numbers
11.109.
Peano arithmetic
11.110.
Pisano periods
11.111.
The poset of natural numbers ordered by divisibility
11.112.
The positive, negative, nonnegative and nonpositive integers
11.113.
Positive integer fractions
11.114.
The positive integers
11.115.
Positive rational numbers
11.116.
Powers of integers
11.117.
Powers of two
11.118.
Prime numbers
11.119.
Products of natural numbers
11.120.
Proper divisors of natural numbers
11.121.
Pythagorean triples
11.122.
The rational numbers
11.123.
Reduced integer fractions
11.124.
Relatively prime integers
11.125.
Relatively prime natural numbers
11.126.
Repeating an element in a standard finite type
11.127.
Retracts of the type of natural numbers
11.128.
The ring of integers
11.129.
The ring of rational numbers
11.130.
The sieve of Eratosthenes
11.131.
Square-free natural numbers
11.132.
Squares in the integers
11.133.
Squares in ℤₚ
11.134.
Squares in the natural numbers
11.135.
The standard cyclic groups
11.136.
The standard cyclic rings
11.137.
Stirling numbers of the second kind
11.138.
Strict inequality on the integer fractions
11.139.
Strict inequality on the integers
11.140.
Strict inequality on the natural numbers
11.141.
Strict inequality on the rational numbers
11.142.
Strict inequality on the standard finite types
11.143.
Strictly ordered pairs of natural numbers
11.144.
The strong induction principle for the natural numbers
11.145.
Sums of natural numbers
11.146.
Sylvester's sequence
11.147.
Taxicab numbers
11.148.
Telephone numbers
11.149.
The triangular numbers
11.150.
The Twin Prime conjecture
11.151.
Type arithmetic with natural numbers
11.152.
Unit elements in the standard finite types
11.153.
Unit similarity on the standard finite types
11.154.
The universal property of the integers
11.155.
The universal property of the natural numbers
11.156.
Upper bounds for type families over the natural numbers
11.157.
The well-ordering principle of the natural numbers
11.158.
The well-ordering principle of the standard finite types
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 functions
14.13.
The action on identifications of dependent functions
14.14.
The action on identifications of functions
14.15.
Apartness relations
14.16.
Arithmetic law for coproduct decomposition and Σ-decomposition
14.17.
Arithmetic law for product decomposition and Π-decomposition
14.18.
Automorphisms
14.19.
The axiom of choice
14.20.
Bands
14.21.
Base changes of span diagrams
14.22.
Bicomposition of functions
14.23.
Binary embeddings
14.24.
Binary equivalences
14.25.
Binary equivalences on unordered pairs of types
14.26.
Binary functoriality of set quotients
14.27.
Homotopies of binary operations
14.28.
Binary operations on unordered pairs of types
14.29.
Binary reflecting maps of equivalence relations
14.30.
Binary relations
14.31.
Binary relations with extensions
14.32.
Binary relations with lifts
14.33.
Binary transport
14.34.
Binary type duality
14.35.
The booleans
14.36.
The Cantor–Schröder–Bernstein–Escardó theorem
14.37.
Cantor's theorem
14.38.
Cartesian morphisms of arrows
14.39.
Cartesian morphisms of span diagrams
14.40.
Cartesian product types
14.41.
Cartesian products of set quotients
14.42.
The category of families of sets
14.43.
The category of sets
14.44.
Choice of representatives for an equivalence relation
14.45.
Codiagonal maps of types
14.46.
Coherently idempotent maps
14.47.
Coherently invertible maps
14.48.
Coinhabited pairs of types
14.49.
Commuting cubes of maps
14.50.
Commuting hexagons of identifications
14.51.
Commuting pentagons of identifications
14.52.
Commuting prisms of maps
14.53.
Commuting squares of homotopies
14.54.
Commuting squares of identifications
14.55.
Commuting squares of maps
14.56.
Commuting tetrahedra of homotopies
14.57.
Commuting tetrahedra of maps
14.58.
Commuting triangles of homotopies
14.59.
Commuting triangles of identifications
14.60.
Commuting triangles of maps
14.61.
Commuting triangles of morphisms of arrows
14.62.
Complements of type families
14.63.
Complements of subtypes
14.64.
Composite maps in inverse sequential diagrams
14.65.
Composition algebra
14.66.
Computational identity types
14.67.
Cones over cospan diagrams
14.68.
Cones over inverse sequential diagrams
14.69.
Conjunction
14.70.
Connected components of types
14.71.
Connected components of universes
14.72.
Connected maps
14.73.
Connected types
14.74.
Constant maps
14.75.
Constant span diagrams
14.76.
Constant type families
14.77.
The continuation monad
14.78.
Contractible maps
14.79.
Contractible types
14.80.
Copartial elements
14.81.
Copartial functions
14.82.
Coproduct decompositions
14.83.
Coproduct decompositions in a subuniverse
14.84.
Coproduct types
14.85.
Coproducts of pullbacks
14.86.
Morphisms in the coslice category of types
14.87.
Cospan diagrams
14.88.
Cospans of types
14.89.
Decidability of dependent function types
14.90.
Decidability of dependent pair types
14.91.
Decidable embeddings
14.92.
Decidable equality
14.93.
Decidable equivalence relations
14.94.
Decidable maps
14.95.
Decidable propositions
14.96.
Decidable relations on types
14.97.
Decidable subtypes
14.98.
Decidable types
14.99.
Dependent binary homotopies
14.100.
The dependent binomial theorem for types (distributivity of dependent function types over coproduct types)
14.101.
Dependent epimorphisms
14.102.
Dependent epimorphisms with respect to truncated types
14.103.
Dependent function types
14.104.
Dependent homotopies
14.105.
Dependent identifications
14.106.
Dependent inverse sequential diagrams of types
14.107.
Dependent pair types
14.108.
Dependent products of pullbacks
14.109.
Dependent sequences
14.110.
Dependent sums of pullbacks
14.111.
Dependent telescopes
14.112.
The dependent universal property of equivalences
14.113.
Descent for coproduct types
14.114.
Descent for dependent pair types
14.115.
Descent for the empty type
14.116.
Descent for equivalences
14.117.
Diagonal maps into cartesian products of types
14.118.
Diagonal maps of types
14.119.
Diagonal span diagrams
14.120.
Diagonals of maps
14.121.
Diagonals of morphisms of arrows
14.122.
Discrete binary relations
14.123.
Discrete reflexive relations
14.124.
Discrete relaxed Σ-decompositions
14.125.
Discrete Σ-decompositions
14.126.
Discrete types
14.127.
Disjunction
14.128.
Double arrows
14.129.
Double negation
14.130.
The double negation modality
14.131.
Double negation stable propositions
14.132.
Double powersets
14.133.
Dubuc-Penon compact types
14.134.
Effective maps for equivalence relations
14.135.
Embeddings
14.136.
Empty types
14.137.
Endomorphisms
14.138.
Epimorphisms
14.139.
Epimorphisms with respect to maps into sets
14.140.
Epimorphisms with respect to truncated types
14.141.
Equality of cartesian product types
14.142.
Equality of coproduct types
14.143.
Equality on dependent function types
14.144.
Equality of dependent pair types
14.145.
Equality in the fibers of a map
14.146.
Equivalence classes
14.147.
Equivalence extensionality
14.148.
Equivalence induction
14.149.
Equivalence injective type families
14.150.
Equivalence relations
14.151.
Equivalences
14.152.
Equivalences of arrows
14.153.
Equivalences of cospans
14.154.
Equivalences of double arrows
14.155.
Equivalences of inverse sequential diagrams of types
14.156.
Equivalences on Maybe
14.157.
Equivalences of span diagrams
14.158.
Equivalences of span diagrams on families of types
14.159.
Equivalences of spans
14.160.
Equivalences of spans of families of types
14.161.
Evaluation of functions
14.162.
Exclusive disjunctions
14.163.
Exclusive sums
14.164.
Existential quantification
14.165.
Exponents of set quotients
14.166.
Extensions of types
14.167.
Faithful maps
14.168.
Families of equivalences
14.169.
Families of maps
14.170.
Families of types over telescopes
14.171.
Fiber inclusions
14.172.
Fibered equivalences
14.173.
Fibered involutions
14.174.
Maps fibered over a map
14.175.
Fibers of maps
14.176.
Finitely coherent equivalences
14.177.
Finitely coherently invertible maps
14.178.
Fixed points of endofunctions
14.179.
Full subtypes of types
14.180.
Function extensionality
14.181.
Function types
14.182.
Functional correspondences
14.183.
Functoriality of the action on identifications of functions
14.184.
Functoriality of cartesian product types
14.185.
Functoriality of coproduct types
14.186.
Functoriality of dependent function types
14.187.
Functoriality of dependent pair types
14.188.
Functoriality of fibers of maps
14.189.
Functoriality of function types
14.190.
Functoriality of morphisms of arrows
14.191.
Functoriality of propositional truncations
14.192.
Functorialty of pullbacks
14.193.
Functoriality of sequential limits
14.194.
Functoriality of set quotients
14.195.
Functoriality of set truncation
14.196.
Functoriality of truncations
14.197.
The fundamental theorem of identity types
14.198.
Global choice
14.199.
Global subuniverses
14.200.
Higher homotopies of morphisms of arrows
14.201.
Hilbert's ε-operators
14.202.
Homotopies
14.203.
Homotopies of morphisms of arrows
14.204.
Homotopies of morphisms of cospan diagrams
14.205.
Homotopy algebra
14.206.
Homotopy induction
14.207.
The homotopy preorder of types
14.208.
Idempotent maps
14.209.
Identity systems
14.210.
Identity types of truncated types
14.211.
Identity types
14.212.
The image of a map
14.213.
Images of subtypes
14.214.
Implicit function types
14.215.
Impredicative encodings of the logical operations
14.216.
Impredicative universes
14.217.
The induction principle for propositional truncation
14.218.
Infinitely coherent equivalences
14.219.
Inhabited subtypes
14.220.
Inhabited types
14.221.
Injective maps
14.222.
The interchange law
14.223.
Intersections of subtypes
14.224.
Inverse sequential diagrams of types
14.225.
Invertible maps
14.226.
Involutions
14.227.
Irrefutable propositions
14.228.
Isolated elements
14.229.
Isomorphisms of sets
14.230.
Iterated cartesian product types
14.231.
Iterated dependent pair types
14.232.
Iterated dependent product types
14.233.
Iterating automorphisms
14.234.
Iterating functions
14.235.
Iterating involutions
14.236.
Kernel span diagrams of maps
14.237.
Large binary relations
14.238.
Large dependent pair types
14.239.
Large homotopies
14.240.
Large identity types
14.241.
The large locale of propositions
14.242.
The large locale of subtypes
14.243.
The law of excluded middle
14.244.
Lawvere's fixed point theorem
14.245.
The lesser limited principle of omniscience
14.246.
Lifts of types
14.247.
The limited principle of omniscience
14.248.
Locally small types
14.249.
Logical equivalences
14.250.
Maps in global subuniverses
14.251.
Maps in subuniverses
14.252.
The maybe monad
14.253.
Mere embeddings
14.254.
Mere equality
14.255.
Mere equivalences
14.256.
Mere functions
14.257.
Mere logical equivalences
14.258.
Mere path-cosplit maps
14.259.
Monomorphisms
14.260.
Morphisms of arrows
14.261.
Morphisms of binary relations
14.262.
Morphisms of cospan diagrams
14.263.
Morphisms of cospans
14.264.
Morphisms of double arrows
14.265.
Morphisms of inverse sequential diagrams of types
14.266.
Morphisms of span diagrams
14.267.
Morphisms of spans
14.268.
Morphisms of spans on families of types
14.269.
Morphisms of twisted arrows
14.270.
Multisubsets
14.271.
Multivariable correspondences
14.272.
Multivariable decidable relations
14.273.
Multivariable functoriality of set quotients
14.274.
Multivariable homotopies
14.275.
Multivariable operations
14.276.
Multivariable relations
14.277.
Multivariable sections
14.278.
Negated equality
14.279.
Negation
14.280.
Noncontractible types
14.281.
Null-homotopic maps
14.282.
Operations on span diagrams
14.283.
Operations on spans
14.284.
Operations on spans of families of types
14.285.
Opposite spans
14.286.
Pairs of distinct elements
14.287.
Partial elements
14.288.
Partial functions
14.289.
Partial sequences
14.290.
Partitions
14.291.
Path algebra
14.292.
Path-cosplit maps
14.293.
Path-split maps
14.294.
Perfect images
14.295.
Permutations of spans of families of types
14.296.
Π-decompositions of types
14.297.
Π-decompositions of types into types in a subuniverse
14.298.
Pointed torsorial type families
14.299.
Postcomposition of dependent functions
14.300.
Postcomposition of functions
14.301.
Postcomposition of pullbacks
14.302.
Powersets
14.303.
Precomposition of dependent functions
14.304.
Precomposition of functions
14.305.
Precomposition of functions into subuniverses
14.306.
Precomposition of type families
14.307.
Preimages of subtypes
14.308.
The preunivalence axiom
14.309.
Preunivalent type families
14.310.
The principle of omniscience
14.311.
Product decompositions
14.312.
Product decompositions of types in a subuniverse
14.313.
Products of binary relations
14.314.
Products of equivalence relataions
14.315.
Products of tuples of types
14.316.
Products of pullbacks
14.317.
Products of unordered pairs of types
14.318.
Products of unordered tuples of types
14.319.
Projective types
14.320.
Proper subsets
14.321.
Propositional extensionality
14.322.
Propositional maps
14.323.
Propositional resizing
14.324.
Propositional truncations
14.325.
Propositions
14.326.
Pullback cones
14.327.
Pullbacks
14.328.
Pullbacks of subtypes
14.329.
Quasicoherently idempotent maps
14.330.
Raising universe levels
14.331.
Reflecting maps for equivalence relations
14.332.
Reflexive relations
14.333.
The Regensburg extension of the fundamental theorem of identity types
14.334.
Relaxed Σ-decompositions of types
14.335.
Repetitions of values of maps
14.336.
Repetitions in sequences
14.337.
The type theoretic replacement axiom
14.338.
Retractions
14.339.
Retracts of maps
14.340.
Retracts of types
14.341.
Sections
14.342.
Types separated at subuniverses
14.343.
Sequences
14.344.
Sequential limits
14.345.
Set presented types
14.346.
Set quotients
14.347.
Set truncations
14.348.
Sets
14.349.
Shifting sequences
14.350.
Σ-closed subuniverses
14.351.
Σ-decompositions of types into types in a subuniverse
14.352.
Σ-decompositions of types
14.353.
Singleton induction
14.354.
Singleton subtypes
14.355.
Morphisms in the slice category of types
14.356.
Small maps
14.357.
Small types
14.358.
Small universes
14.359.
Sorial type families
14.360.
Span diagrams
14.361.
Span diagrams on families of types
14.362.
Spans of types
14.363.
Spans of families of types
14.364.
Split idempotent maps
14.365.
Split surjective maps
14.366.
Standard apartness relations
14.367.
Standard pullbacks
14.368.
Strict symmetrization of binary relations
14.369.
Strictly involutive identity types
14.370.
The strictly right unital concatenation operation on identifications
14.371.
Strongly extensional maps
14.372.
Structure
14.373.
The structure identity principle
14.374.
Structured type duality
14.375.
Subsingleton induction
14.376.
Subterminal types
14.377.
Subtype duality
14.378.
The subtype identity principle
14.379.
Subtypes
14.380.
Subuniverses
14.381.
Surjective maps
14.382.
Symmetric binary relations
14.383.
Symmetric cores of binary relations
14.384.
Symmetric difference of subtypes
14.385.
The symmetric identity types
14.386.
Symmetric operations
14.387.
Telescopes
14.388.
Terminal spans on families of types
14.389.
Tight apartness relations
14.390.
Torsorial type families
14.391.
Total partial elements
14.392.
Total partial functions
14.393.
Transfinite cocomposition of maps
14.394.
Transport along equivalences
14.395.
Transport along higher identifications
14.396.
Transport along homotopies
14.397.
Transport along identifications
14.398.
Transport-split type families
14.399.
Transposing identifications along equivalences
14.400.
Transposing identifications along retractions
14.401.
Transposing identifications along sections
14.402.
Transposition of span diagrams
14.403.
Trivial relaxed Σ-decompositions
14.404.
Trivial Σ-decompositions
14.405.
Truncated equality
14.406.
Truncated maps
14.407.
Truncated types
14.408.
k-Equivalences
14.409.
Truncation images of maps
14.410.
Truncation levels
14.411.
The truncation modalities
14.412.
Truncations
14.413.
Tuples of types
14.414.
Type arithmetic with the booleans
14.415.
Type arithmetic for cartesian product types
14.416.
Type arithmetic for coproduct types
14.417.
Type arithmetic with dependent function types
14.418.
Type arithmetic for dependent pair types
14.419.
Type arithmetic with the empty type
14.420.
Type arithmetic with the unit type
14.421.
Type duality
14.422.
The type theoretic principle of choice
14.423.
Unions of subtypes
14.424.
Uniqueness of the image of a map
14.425.
Uniqueness quantification
14.426.
The uniqueness of set quotients
14.427.
Uniqueness of set truncations
14.428.
Uniqueness of the truncations
14.429.
The unit type
14.430.
Unital binary operations
14.431.
The univalence axiom
14.432.
The univalence axiom implies function extensionality
14.433.
Univalent type families
14.434.
The universal property of booleans
14.435.
The universal properties of cartesian product types
14.436.
Universal property of contractible types
14.437.
The universal property of coproduct types
14.438.
The universal property of dependent function types
14.439.
The universal property of dependent pair types
14.440.
The universal property of the empty type
14.441.
The universal property of equivalences
14.442.
The universal property of the family of fibers of maps
14.443.
The universal property of fiber products
14.444.
The universal property of identity systems
14.445.
The universal property of identity types
14.446.
The universal property of the image of a map
14.447.
The universal property of the maybe monad
14.448.
The universal property of propositional truncations
14.449.
The universal property of propositional truncations with respect to sets
14.450.
The universal property of pullbacks
14.451.
The universal property of sequential limits
14.452.
The universal property of set quotients
14.453.
The universal property of set truncations
14.454.
The universal property of truncations
14.455.
The universal property of the unit type
14.456.
Universal quantification
14.457.
Universe levels
14.458.
Unordered pairs of elements in a type
14.459.
Unordered pairs of types
14.460.
Unordered n-tuples of elements in a type
14.461.
Unordered tuples of types
14.462.
Vectors of set quotients
14.463.
Weak function extensionality
14.464.
The weak limited principle of omniscience
14.465.
Weakly constant maps
14.466.
Whiskering higher homotopies with respect to composition
14.467.
Whiskering homotopies with respect to composition
14.468.
Whiskering homotopies with respect to concatenation
14.469.
Whiskering identifications with respect to concatenation
14.470.
Whiskering operations
14.471.
The wild category of types
14.472.
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.
Dependent globular types
16.2.
Dependent reflexive globular types
16.3.
Equality of globular types
16.4.
Equivalences between globular types
16.5.
Maps between globular types
16.6.
Globular types
16.7.
Maps between large globular types
16.8.
Large globular types
16.9.
Large reflexive globular types
16.10.
Large symmetric globular types
16.11.
Large transitive globular types
16.12.
Reflexive globular types
16.13.
Symmetric globular types
16.14.
Transitive globular types
17.
Graph theory
❱
17.1.
Acyclic undirected graphs
17.2.
Circuits in undirected graphs
17.3.
Closed walks in undirected graphs
17.4.
Complete bipartite graphs
17.5.
Complete multipartite graphs
17.6.
Complete undirected graphs
17.7.
Connected graphs
17.8.
Cycles in undirected graphs
17.9.
Directed graph structures on standard finite sets
17.10.
Directed graphs
17.11.
Discrete directed graphs
17.12.
Discrete reflexive graphs
17.13.
Displayed large reflexive graphs
17.14.
Edge-coloured undirected graphs
17.15.
Embeddings of directed graphs
17.16.
Embeddings of undirected graphs
17.17.
Enriched undirected graphs
17.18.
Equivalences of directed graphs
17.19.
Equivalences of enriched undirected graphs
17.20.
Equivalences of undirected graphs
17.21.
Eulerian circuits in undirected graphs
17.22.
Faithful morphisms of undirected graphs
17.23.
Fibers of directed graphs
17.24.
Finite graphs
17.25.
Geometric realizations of undirected graphs
17.26.
Higher directed graphs
17.27.
Hypergraphs
17.28.
Large higher directed graphs
17.29.
Large reflexive graphs
17.30.
Matchings
17.31.
Mere equivalences of undirected graphs
17.32.
Morphisms of directed graphs
17.33.
Morphisms of undirected graphs
17.34.
Incidence in undirected graphs
17.35.
Orientations of undirected graphs
17.36.
Paths in undirected graphs
17.37.
Polygons
17.38.
Raising universe levels of directed graphs
17.39.
Reflecting maps of undirected graphs
17.40.
Reflexive graphs
17.41.
Regular undirected graph
17.42.
Simple undirected graphs
17.43.
Stereoisomerism for enriched undirected graphs
17.44.
Totally faithful morphisms of undirected graphs
17.45.
Trails in directed graphs
17.46.
Trails in undirected graphs
17.47.
Undirected graph structures on standard finite sets
17.48.
Undirected graphs
17.49.
Vertex covers
17.50.
Voltage graphs
17.51.
Walks in directed graphs
17.52.
Walks in undirected graphs
17.53.
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.
Automorphism groups
18.5.
Cartesian products of abelian groups
18.6.
Cartesian products of concrete groups
18.7.
Cartesian products of groups
18.8.
Cartesian products of monoids
18.9.
Cartesian products of semigroups
18.10.
The category of abelian groups
18.11.
The category of concrete groups
18.12.
The category of group actions
18.13.
The category of groups
18.14.
The orbit category of a group
18.15.
The category of semigroups
18.16.
Cayley's theorem
18.17.
The center of a group
18.18.
Center of a monoid
18.19.
Center of a semigroup
18.20.
Central elements of groups
18.21.
Central elements of monoids
18.22.
Central elements of semirings
18.23.
Centralizer subgroups
18.24.
Characteristic subgroups
18.25.
Commutative monoids
18.26.
Commutator subgroups
18.27.
Commutators of elements in groups
18.28.
Commuting elements of groups
18.29.
Commuting elements of monoids
18.30.
Commuting elements of semigroups
18.31.
Commuting squares of group homomorphisms
18.32.
Concrete group actions
18.33.
Concrete groups
18.34.
Concrete monoids
18.35.
Congruence relations on abelian groups
18.36.
Congruence relations on commutative monoids
18.37.
Congruence relations on groups
18.38.
Congruence relations on monoids
18.39.
Congruence relations on semigroups
18.40.
Conjugation in groups
18.41.
Conjugation on concrete groups
18.42.
Contravariant pushforwards of concrete group actions
18.43.
Cores of monoids
18.44.
Cyclic groups
18.45.
Decidable subgroups of groups
18.46.
Dependent products of abelian groups
18.47.
Dependent products of commutative monoids
18.48.
Dependent products of groups
18.49.
Dependent products of monoids
18.50.
Dependent products of semigroups
18.51.
The dihedral group construction
18.52.
The dihedral groups
18.53.
The E₈-lattice
18.54.
Elements of finite order
18.55.
Embeddings of abelian groups
18.56.
Embeddings of groups
18.57.
The endomorphism rings of abelian groups
18.58.
Epimorphisms in groups
18.59.
Equivalences of concrete group actions
18.60.
Equivalences of concrete groups
18.61.
Equivalences of group actions
18.62.
Equivalences between semigroups
18.63.
Exponents of abelian groups
18.64.
Exponents of groups
18.65.
Free concrete group actions
18.66.
Free groups with one generator
18.67.
The full subgroup of a group
18.68.
The full subsemigroup of a semigroup
18.69.
Function groups of abelian groups
18.70.
Function commutative monoids
18.71.
Function groups
18.72.
Function monoids
18.73.
Function semigroups
18.74.
Functoriality of quotient groups
18.75.
Furstenberg groups
18.76.
Generating elements of groups
18.77.
Generating sets of groups
18.78.
Group actions
18.79.
Abstract groups
18.80.
Homomorphisms of abelian groups
18.81.
Homomorphisms of commutative monoids
18.82.
Morphisms of concrete group actions
18.83.
Homomorphisms of concrete groups
18.84.
Homomorphisms of generated subgroups
18.85.
Homomorphisms of group actions
18.86.
Homomorphisms of groups
18.87.
Homomorphisms of groups equipped with normal subgroups
18.88.
Homomorphisms of monoids
18.89.
Homomorphisms of semigroups
18.90.
Images of group homomorphisms
18.91.
Images of semigroup homomorphisms
18.92.
Integer multiples of elements in abelian groups
18.93.
Integer powers of elements of groups
18.94.
Intersections of subgroups of abelian groups
18.95.
Intersections of subgroups of groups
18.96.
Inverse semigroups
18.97.
Invertible elements in monoids
18.98.
Isomorphisms of abelian groups
18.99.
Isomorphisms of concrete groups
18.100.
Isomorphisms of group actions
18.101.
Isomorphisms of groups
18.102.
Isomorphisms of monoids
18.103.
Isomorphisms of semigroups
18.104.
Iterated cartesian products of concrete groups
18.105.
Kernels of homomorphisms between abelian groups
18.106.
Kernels of homomorphisms of concrete groups
18.107.
Kernels of homomorphisms of groups
18.108.
Large semigroups
18.109.
Concrete automorphism groups on sets
18.110.
Mere equivalences of concrete group actions
18.111.
Mere equivalences of group actions
18.112.
Monoid actions
18.113.
Monoids
18.114.
Monomorphisms of concrete groups
18.115.
Monomorphisms in the category of groups
18.116.
Multiples of elements in abelian groups
18.117.
Nontrivial groups
18.118.
Normal closures of subgroups
18.119.
Normal cores of subgroups
18.120.
Normal subgroups
18.121.
Normal subgroups of concrete groups
18.122.
Normal submonoids
18.123.
Normal submonoids of commutative monoids
18.124.
Normalizer subgroups
18.125.
Nullifying group homomorphisms
18.126.
The opposite of a group
18.127.
The opposite of a semigroup
18.128.
The orbit-stabilizer theorem for concrete groups
18.129.
Orbits of concrete group actions
18.130.
Orbits of group actions
18.131.
The order of an element in a group
18.132.
Perfect cores
18.133.
Perfect groups
18.134.
Perfect subgroups
18.135.
Powers of elements in commutative monoids
18.136.
Powers of elements in groups
18.137.
Powers of elements in monoids
18.138.
The precategory of commutative monoids
18.139.
The precategory of concrete groups
18.140.
The precategory of group actions
18.141.
The precategory of groups
18.142.
The precategory of monoids
18.143.
The precategory of orbits of a monoid action
18.144.
The precategory of semigroups
18.145.
Principal group actions
18.146.
Principal torsors of concrete groups
18.147.
Products of elements in a monoid
18.148.
Products of tuples of elements in commutative monoids
18.149.
Pullbacks of subgroups
18.150.
Pullbacks of subsemigroups
18.151.
Quotient groups
18.152.
Quotient groups of concrete groups
18.153.
Quotients of abelian groups
18.154.
Rational commutative monoids
18.155.
Representations of monoids in precategories
18.156.
Saturated congruence relations on commutative monoids
18.157.
Saturated congruence relations on monoids
18.158.
Semigroups
18.159.
Sheargroups
18.160.
Shriek of concrete group homomorphisms
18.161.
Stabilizer groups
18.162.
Stabilizers of concrete group actions
18.163.
Subgroups
18.164.
Subgroups of abelian groups
18.165.
Subgroups of concrete groups
18.166.
Subgroups generated by elements of a group
18.167.
Subgroups generated by families of elements
18.168.
Subgroups generated by subsets of groups
18.169.
Submonoids
18.170.
Submonoids of commutative monoids
18.171.
Subsemigroups
18.172.
Subsets of abelian groups
18.173.
Subsets of commutative monoids
18.174.
Subsets of groups
18.175.
Subsets of monoids
18.176.
Subsets of semigroups
18.177.
The substitution functor of concrete group actions
18.178.
The substitution functor of group actions
18.179.
Surjective group homomorphisms
18.180.
Surjective semigroup homomorphisms
18.181.
Symmetric concrete groups
18.182.
Symmetric groups
18.183.
Torsion elements of groups
18.184.
Torsion-free groups
18.185.
Torsors of abstract groups
18.186.
Transitive concrete group actions
18.187.
Transitive group actions
18.188.
Trivial concrete groups
18.189.
Trivial group homomorphisms
18.190.
Trivial groups
18.191.
Trivial subgroups
18.192.
Unordered tuples of elements in commutative monoids
18.193.
Wild representations of monoids
19.
Higher group theory
❱
19.1.
Abelian higher groups
19.2.
Cartesian products of higher groups
19.3.
Conjugation in higher groups
19.4.
Cyclic higher groups
19.5.
Deloopable groups
19.6.
Deloopable H-spaces
19.7.
Deloopable types
19.8.
Eilenberg-Mac Lane spaces
19.9.
Equivalences of higher groups
19.10.
Fixed points of higher group actions
19.11.
Free higher group actions
19.12.
Higher group actions
19.13.
Higher groups
19.14.
Homomorphisms of higher group actions
19.15.
Homomorphisms of higher groups
19.16.
The higher group of integers
19.17.
Iterated cartesian products of higher groups
19.18.
Iterated deloopings of pointed types
19.19.
Orbits of higher group actions
19.20.
Small ∞-groups
19.21.
Subgroups of higher groups
19.22.
Symmetric higher groups
19.23.
Transitive higher group actions
19.24.
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.
Metric spaces
❱
22.1.
The category of metric spaces and isometries
22.2.
The category of metric spaces and short maps
22.3.
Cauchy approximations in metric spaces
22.4.
Cauchy approximations in premetric spaces
22.5.
Closed premetric structures
22.6.
Complete metric spaces
22.7.
Convergent Cauchy approximations in metric spaces
22.8.
Dependent products of metric spaces
22.9.
Discrete premetric structures
22.10.
Equality of metric spaces
22.11.
Equality of premetric spaces
22.12.
Extensional premetric structures on types
22.13.
Functions between metric spaces
22.14.
The functor from the precategory of metric spaces and isometries to the precategory of sets
22.15.
The inclusion of isometries into the category of metric spaces and short maps
22.16.
Induced premetric structures on preimages
22.17.
Isometric equivalences between premetric spaces
22.18.
Isometries between metric spaces
22.19.
Isometries between premetric spaces
22.20.
Limits of Cauchy approximations in premetric spaces
22.21.
The metric space of cauchy approximations in a metric space
22.22.
The metric space of convergent cauchy approximations in a metric space
22.23.
The standard metric structure on the rational numbers
22.24.
The metric structure on the rational numbers with open neighborhoods
22.25.
Metric spaces
22.26.
Metric structures
22.27.
Monotonic premetric structures on types
22.28.
The poset of premetric structures on a type
22.29.
The precategory of metric spaces and functions
22.30.
The precategory of metric spaces and isometries
22.31.
The precategory of metric spaces and short functions
22.32.
Premetric spaces
22.33.
Premetric structures on types
22.34.
Pseudometric spaces
22.35.
Pseudometric structures on a type
22.36.
Reflexive premetric structures on types
22.37.
Saturated metric spaces
22.38.
Short functions between metric spaces
22.39.
Short functions between premetric spaces
22.40.
Subspaces of metric spaces
22.41.
Symmetric premetric structures on types
22.42.
Triangular premetric structures on types
23.
Modal type theory
❱
23.1.
The action on homotopies of the flat modality
23.2.
The action on identifications of crisp functions
23.3.
The action on identifications of the flat modality
23.4.
Crisp cartesian product types
23.5.
Crisp coproduct types
23.6.
Crisp dependent function types
23.7.
Crisp dependent pair types
23.8.
Crisp function types
23.9.
Crisp identity types
23.10.
The crisp law of excluded middle
23.11.
Crisp pullbacks
23.12.
Crisp types
23.13.
Dependent universal property of flat discrete crisp types
23.14.
Flat discrete crisp types
23.15.
The flat modality
23.16.
The flat-sharp adjunction
23.17.
Functoriality of the flat modality
23.18.
Functoriality of the sharp modality
23.19.
Sharp codiscrete maps
23.20.
Sharp codiscrete types
23.21.
The sharp modality
23.22.
Transport along crisp identifications
23.23.
The universal property of flat discrete crisp types
24.
Order theory
❱
24.1.
Accessible elements with respect to relations
24.2.
Bottom elements in large posets
24.3.
Bottom elements in posets
24.4.
Bottom elements in preorders
24.5.
Chains in posets
24.6.
Chains in preorders
24.7.
Closure operators on large locales
24.8.
Closure operators on large posets
24.9.
Commuting squares of Galois connections between large posets
24.10.
Commuting squares of order preserving maps of large posets
24.11.
Coverings in locales
24.12.
Decidable posets
24.13.
Decidable preorders
24.14.
Decidable subposets
24.15.
Decidable subpreorders
24.16.
Decidable total orders
24.17.
Decidable total preorders
24.18.
Dependent products of large frames
24.19.
Dependent products of large locales
24.20.
Dependent products of large meet-semilattices
24.21.
Dependent products of large posets
24.22.
Dependent products large preorders
24.23.
Dependent products of large suplattices
24.24.
Distributive lattices
24.25.
Finite coverings in locales
24.26.
Finite posets
24.27.
Finite preorders
24.28.
Finite total orders
24.29.
Finitely graded posets
24.30.
Frames
24.31.
Galois connections
24.32.
Galois connections between large posets
24.33.
Greatest lower bounds in large posets
24.34.
Greatest lower bounds in posets
24.35.
Homomorphisms of frames
24.36.
Homomorphisms of large frames
24.37.
Homomorphisms of large locales
24.38.
Homomorphisms of large meet-semilattices
24.39.
Homomorphisms of large suplattices
24.40.
Homomorphisms of meet-semilattices
24.41.
Homomorphisms of meet-suplattices
24.42.
Homomorphisms of suplattices
24.43.
Ideals in preorders
24.44.
Incidence algebras
24.45.
Inflattices
24.46.
Inhabited chains in posets
24.47.
Inhabited chains in preorders
24.48.
Inhabited finite total orders
24.49.
Interval subposets
24.50.
Join preserving maps between posets
24.51.
Join-semilattices
24.52.
The Knaster–Tarski fixed point theorem
24.53.
Large frames
24.54.
Large locales
24.55.
Large meet-semilattices
24.56.
Large meet-subsemilattices
24.57.
Large posets
24.58.
Large preorders
24.59.
Large quotient locales
24.60.
Large subframes
24.61.
Large subposets
24.62.
Large subpreorders
24.63.
Large subsuplattices
24.64.
Large suplattices
24.65.
Lattices
24.66.
Least upper bounds in large posets
24.67.
Least upper bounds in posets
24.68.
Locales
24.69.
Locally finite posets
24.70.
Lower bounds in large posets
24.71.
Lower bounds in posets
24.72.
Lower sets in large posets
24.73.
Lower types in preorders
24.74.
Maximal chains in posets
24.75.
Maximal chains in preorders
24.76.
Meet-semilattices
24.77.
Meet-suplattices
24.78.
Nuclei on large locales
24.79.
Opposite large posets
24.80.
Opposite large preorders
24.81.
Opposite posets
24.82.
Opposite preorders
24.83.
Order preserving maps between large posets
24.84.
Order preserving maps between large preorders
24.85.
Order preserving maps between posets
24.86.
Order preserving maps between preorders
24.87.
Ordinals
24.88.
Posets
24.89.
Powers of large locales
24.90.
The precategory of decidable total orders
24.91.
The precategory of finite posets
24.92.
The precategory of finite total orders
24.93.
The precategory of inhabited finite total orders
24.94.
The precategory of posets
24.95.
The precategory of total orders
24.96.
Preorders
24.97.
Principal lower sets of large posets
24.98.
Principal upper sets of large posets
24.99.
Reflective Galois connections between large posets
24.100.
Resizing posets
24.101.
Resizing preorders
24.102.
Resizing suplattices
24.103.
Similarity of elements in large posets
24.104.
Similarity of elements in large preorders
24.105.
Similarity of order preserving maps between large posets
24.106.
Similarity of order preserving maps between large preorders
24.107.
Subposets
24.108.
Subpreorders
24.109.
Suplattices
24.110.
Supremum preserving maps between posets
24.111.
Top elements in large posets
24.112.
Top elements in posets
24.113.
Top elements in preorders
24.114.
Total orders
24.115.
Total preorders
24.116.
Upper bounds of chains in posets
24.117.
Upper bounds in large posets
24.118.
Upper bounds in posets
24.119.
Upper sets of large posets
24.120.
Well-founded orders
24.121.
Well-founded relations
24.122.
Zorn's lemma
25.
Organic chemistry
❱
25.1.
Alcohols
25.2.
Alkanes
25.3.
Alkenes
25.4.
Alkynes
25.5.
Ethane
25.6.
Hydrocarbons
25.7.
Methane
25.8.
Saturated carbons
26.
Orthogonal factorization systems
❱
26.1.
Cd-structures
26.2.
Cellular maps
26.3.
The closed modalities
26.4.
Continuation modalities
26.5.
Double lifts of families of elements
26.6.
Double negation sheaves
26.7.
Extensions of double lifts of families of elements
26.8.
Extensions of families of elements
26.9.
Extensions of maps
26.10.
Factorization operations
26.11.
Factorization operations into function classes
26.12.
Factorization operations into global function classes
26.13.
Factorizations of maps
26.14.
Factorizations of maps into function classes
26.15.
Factorizations of maps into global function classes
26.16.
Families of types local at a map
26.17.
Fiberwise orthogonal maps
26.18.
Function classes
26.19.
Functoriality of higher modalities
26.20.
Functoriality of the pullback-hom
26.21.
Global function classes
26.22.
Higher modalities
26.23.
The identity modality
26.24.
Large Lawvere–Tierney topologies
26.25.
Lawvere–Tierney topologies
26.26.
Lifting operations
26.27.
Lifting structures on commuting squares of maps
26.28.
Lifts of families of elements
26.29.
Lifts of maps
26.30.
Localizations at maps
26.31.
Localizations at subuniverses
26.32.
Locally small modal-operators
26.33.
Maps local at maps
26.34.
Mere lifting properties
26.35.
Modal induction
26.36.
Modal operators
26.37.
Modal subuniverse induction
26.38.
Null families of types
26.39.
Null maps
26.40.
Null types
26.41.
The open modalities
26.42.
Orthogonal factorization systems
26.43.
Orthogonal maps
26.44.
Precomposition of lifts of families of elements by maps
26.45.
The pullback-hom
26.46.
The raise modalities
26.47.
Reflective modalities
26.48.
Reflective subuniverses
26.49.
Regular cd-structures
26.50.
Σ-closed modalities
26.51.
Σ-closed reflective modalities
26.52.
Σ-closed reflective subuniverses
26.53.
Stable orthogonal factorization systems
26.54.
Types colocal at maps
26.55.
Types local at maps
26.56.
Types separated at maps
26.57.
Uniquely eliminating modalities
26.58.
Wide function classes
26.59.
Wide global function classes
26.60.
The zero modality
27.
Polytopes
❱
27.1.
Abstract polytopes
28.
Primitives
❱
28.1.
Characters
28.2.
Floats
28.3.
Machine integers
28.4.
Strings
29.
Real numbers
❱
29.1.
Dedekind real numbers
29.2.
The metric space of real numbers
29.3.
Rational real numbers
30.
Reflection
❱
30.1.
Abstractions
30.2.
Arguments
30.3.
Boolean reflection
30.4.
Definitions
30.5.
Erasing equality
30.6.
Fixity
30.7.
Group solver
30.8.
Literals
30.9.
Metavariables
30.10.
Names
30.11.
Precategory solver
30.12.
Rewriting
30.13.
Terms
30.14.
The type checking monad
31.
Ring theory
❱
31.1.
Additive orders of elements of rings
31.2.
Algebras over rings
31.3.
The binomial theorem for rings
31.4.
The binomial theorem for semirings
31.5.
The category of cyclic rings
31.6.
The category of rings
31.7.
Central elements of rings
31.8.
Central elements of semirings
31.9.
Characteristics of rings
31.10.
Commuting elements of rings
31.11.
Congruence relations on rings
31.12.
Congruence relations on semirings
31.13.
Cyclic rings
31.14.
Dependent products of rings
31.15.
Dependent products of semirings
31.16.
Division rings
31.17.
The free ring with one generator
31.18.
Full ideals of rings
31.19.
Function rings
31.20.
Function semirings
31.21.
Generating elements of rings
31.22.
The group of multiplicative units of a ring
31.23.
Homomorphisms of cyclic rings
31.24.
Homomorphisms of rings
31.25.
Homomorphisms of semirings
31.26.
Ideals generated by subsets of rings
31.27.
Ideals of rings
31.28.
Ideals of semirings
31.29.
Idempotent elements in rings
31.30.
Initial rings
31.31.
Integer multiples of elements of rings
31.32.
Intersections of ideals of rings
31.33.
Intersections of ideals of semirings
31.34.
The invariant basis property of rings
31.35.
Invertible elements in rings
31.36.
Isomorphisms of rings
31.37.
Joins of ideals of rings
31.38.
Joins of left ideals of rings
31.39.
Joins of right ideals of rings
31.40.
Kernels of ring homomorphisms
31.41.
Left ideals generated by subsets of rings
31.42.
Left ideals of rings
31.43.
Local rings
31.44.
Localizations of rings
31.45.
Maximal ideals of rings
31.46.
Modules over rings
31.47.
Multiples of elements in rings
31.48.
Multiplicative orders of elements of rings
31.49.
Nil ideals of rings
31.50.
Nilpotent elements in rings
31.51.
Nilpotent elements in semirings
31.52.
Opposite rings
31.53.
The poset of cyclic rings
31.54.
The poset of ideals of a ring
31.55.
The poset of left ideals of a ring
31.56.
The poset of right ideals of a ring
31.57.
Powers of elements in rings
31.58.
Powers of elements in semirings
31.59.
The precategory of rings
31.60.
The precategory of semirings
31.61.
Products of ideals of rings
31.62.
Products of left ideals of rings
31.63.
Products of right ideals of rings
31.64.
Products of rings
31.65.
Products of subsets of rings
31.66.
Quotient rings
31.67.
Radical ideals of rings
31.68.
Right ideals generated by subsets of rings
31.69.
Right ideals of rings
31.70.
Rings
31.71.
Semirings
31.72.
Subsets of rings
31.73.
Subsets of semirings
31.74.
Sums of elements in rings
31.75.
Sums of elements in semirings
31.76.
Transporting ring structures along isomorphisms of abelian groups
31.77.
Trivial rings
32.
Set theory
❱
32.1.
Baire space
32.2.
Cantor space
32.3.
Cantor's diagonal argument
32.4.
Cardinalities of sets
32.5.
Countable sets
32.6.
Cumulative hierarchy
32.7.
Infinite sets
32.8.
Russell's paradox
32.9.
Uncountable sets
33.
Species
❱
33.1.
Cartesian exponents of species
33.2.
Cartesian products of species of types
33.3.
Cauchy composition of species of types
33.4.
Cauchy composition of species of types in a subuniverse
33.5.
Cauchy exponentials of species of types
33.6.
Cauchy exponentials of species of types in a subuniverse
33.7.
Cauchy products of species of types
33.8.
Cauchy products of species of types in a subuniverse
33.9.
Cauchy series of species of types
33.10.
Cauchy series of species of types in a subuniverse
33.11.
Composition of Cauchy series of species of types
33.12.
Composition of Cauchy series of species of types in subuniverses
33.13.
Coproducts of species of types
33.14.
Coproducts of species of types in subuniverses
33.15.
Cycle index series of species
33.16.
Derivatives of species
33.17.
Dirichlet exponentials of a species of types
33.18.
Dirichlet exponentials of species of types in a subuniverse
33.19.
Dirichlet products of species of types
33.20.
Dirichlet products of species of types in subuniverses
33.21.
Dirichlet series of species of finite inhabited types
33.22.
Dirichlet series of species of types
33.23.
Dirichlet series of species of types in subuniverses
33.24.
Equivalences of species of types
33.25.
Equivalences of species of types in subuniverses
33.26.
Exponential of Cauchy series of species of types
33.27.
Exponential of Cauchy series of species of types in subuniverses
33.28.
Hasse-Weil species
33.29.
Morphisms of finite species
33.30.
Morphisms of species of types
33.31.
Pointing of species of types
33.32.
The precategory of finite species
33.33.
Products of Cauchy series of species of types
33.34.
Products of Cauchy series of species of types in subuniverses
33.35.
Products of Dirichlet series of species of finite inhabited types
33.36.
Products of Dirichlet series of species of types
33.37.
Products of Dirichlet series of species of types in subuniverses
33.38.
Small Composition of species of finite inhabited types
33.39.
Small Cauchy composition of species types in subuniverses
33.40.
Species of finite inhabited types
33.41.
Species of finite types
33.42.
Species of inhabited types
33.43.
Species of types
33.44.
Species of types in subuniverses
33.45.
The unit of Cauchy composition of types
33.46.
The unit of Cauchy composition of species of types in subuniverses
33.47.
Unlabeled structures of finite species
34.
Structured types
❱
34.1.
Cartesian products of types equipped with endomorphisms
34.2.
Central H-spaces
34.3.
Commuting squares of pointed homotopies
34.4.
Commuting squares of pointed maps
34.5.
Commuting triangles of pointed maps
34.6.
Conjugation of pointed types
34.7.
Constant pointed maps
34.8.
Contractible pointed types
34.9.
Cyclic types
34.10.
Dependent products of H-spaces
34.11.
Dependent products of pointed types
34.12.
Dependent products of wild monoids
34.13.
Dependent types equipped with automorphisms
34.14.
Equivalences of H-spaces
34.15.
Equivalences of pointed arrows
34.16.
Equivalences of types equipped with automorphisms
34.17.
Equivalences of types equipped with endomorphisms
34.18.
Faithful pointed maps
34.19.
Fibers of pointed maps
34.20.
Finite multiplication in magmas
34.21.
Function H-spaces
34.22.
Function magmas
34.23.
Function wild monoids
34.24.
H-spaces
34.25.
The initial pointed type equipped with an automorphism
34.26.
The involutive type of H-space structures on a pointed type
34.27.
Involutive types
34.28.
Iterated cartesian products of types equipped with endomorphisms
34.29.
Iterated cartesian products of pointed types
34.30.
Magmas
34.31.
Mere equivalences of types equipped with endomorphisms
34.32.
Morphisms of H-spaces
34.33.
Morphisms of magmas
34.34.
Morphisms of pointed arrows
34.35.
Morphisms of twisted pointed arrows
34.36.
Morphisms of types equipped with automorphisms
34.37.
Morphisms of types equipped with endomorphisms
34.38.
Morphisms of wild monoids
34.39.
Noncoherent H-spaces
34.40.
Opposite pointed spans
34.41.
Pointed 2-homotopies
34.42.
Pointed cartesian product types
34.43.
Pointed dependent functions
34.44.
Pointed dependent pair types
34.45.
Pointed equivalences
34.46.
Pointed families of types
34.47.
Pointed homotopies
34.48.
Pointed isomorphisms
34.49.
Pointed maps
34.50.
Pointed retractions of pointed maps
34.51.
Pointed sections of pointed maps
34.52.
Pointed span diagrams
34.53.
Pointed spans
34.54.
Pointed types
34.55.
Pointed types equipped with automorphisms
34.56.
The pointed unit type
34.57.
Universal property of contractible types with respect to pointed types and maps
34.58.
Postcomposition of pointed maps
34.59.
Precomposition of pointed maps
34.60.
Sets equipped with automorphisms
34.61.
Small pointed types
34.62.
Symmetric elements of involutive types
34.63.
Symmetric H-spaces
34.64.
Transposition of pointed span diagrams
34.65.
Types equipped with automorphisms
34.66.
Types equipped with endomorphisms
34.67.
Uniform pointed homotopies
34.68.
The universal property of pointed equivalences
34.69.
Unpointed maps between pointed types
34.70.
Whiskering pointed homotopies with respect to concatenation
34.71.
Whiskering of pointed homotopies with respect to composition of pointed maps
34.72.
The wild category of pointed types
34.73.
Wild groups
34.74.
Wild loops
34.75.
Wild monoids
34.76.
Wild quasigroups
34.77.
Wild semigroups
35.
Synthetic category theory
❱
35.1.
Cone diagrams of synthetic categories
35.2.
Cospans of synthetic categories
35.3.
Equivalences between synthetic categories
35.4.
Invertible functors between synthetic categories
35.5.
Pullbacks of synthetic categories
35.6.
Retractions of functors between synthetic categories
35.7.
Sections of functor between synthetic categories
35.8.
Synthetic categories
36.
Synthetic homotopy theory
❱
36.1.
0-acyclic maps
36.2.
0-acyclic types
36.3.
1-acyclic types
36.4.
Acyclic maps
36.5.
Acyclic types
36.6.
The category of connected set bundles over the circle
36.7.
Cavallo's trick
36.8.
The circle
36.9.
Cocartesian morphisms of arrows
36.10.
Cocones under pointed span diagrams
36.11.
Cocones under sequential diagrams
36.12.
Cocones under spans
36.13.
Codiagonals of maps
36.14.
Coequalizers
36.15.
Cofibers
36.16.
Coforks
36.17.
Correspondence between cocones under sequential diagrams and certain coforks
36.18.
Conjugation of loops
36.19.
Connected set bundles over the circle
36.20.
Connective prespectra
36.21.
Connective spectra
36.22.
Dependent cocones under sequential diagrams
36.23.
Dependent cocones under spans
36.24.
Dependent coforks
36.25.
Dependent descent for the circle
36.26.
The dependent pullback property of pushouts
36.27.
Dependent pushout-products
36.28.
Dependent sequential diagrams
36.29.
Dependent suspension structures
36.30.
The dependent universal property of coequalizers
36.31.
The dependent universal property of pushouts
36.32.
The dependent universal property of sequential colimits
36.33.
Dependent universal property of suspensions
36.34.
The descent property of the circle
36.35.
Descent data for constant type families over the circle
36.36.
Descent data for families of dependent pair types over the circle
36.37.
Descent data for families of equivalence types over the circle
36.38.
Descent data for families of function types over the circle
36.39.
Subtypes of descent data for the circle
36.40.
Descent data for type families of equivalence types over pushouts
36.41.
Descent data for type families of function types over pushouts
36.42.
Descent data for type families of identity types over pushouts
36.43.
Descent data for pushouts
36.44.
Descent data for sequential colimits
36.45.
Descent property of pushouts
36.46.
Descent property of sequential colimits
36.47.
Double loop spaces
36.48.
The Eckmann-Hilton argument
36.49.
Equifibered sequential diagrams
36.50.
Equivalences of cocones under sequential diagrams
36.51.
Equivalences of coforks
36.52.
Equivalances of dependent sequential diagrams
36.53.
Equivalences of descent data for pushouts
36.54.
Equivalences of sequential diagrams
36.55.
Families with descent data for pushouts
36.56.
Families with descent data for sequential colimits
36.57.
The flattening lemma for coequalizers
36.58.
The flattening lemma for pushouts
36.59.
The flattening lemma for sequential colimits
36.60.
Free loops
36.61.
Functoriality of the loop space operation
36.62.
Functoriality of sequential colimits
36.63.
Functoriality of suspensions
36.64.
Groups of loops in 1-types
36.65.
Hatcher's acyclic type
36.66.
Identity systems of descent data for pushouts
36.67.
The induction principle of pushouts
36.68.
The infinite complex projective space
36.69.
Infinite cyclic types
36.70.
The interval
36.71.
Iterated loop spaces
36.72.
Iterated suspensions of pointed types
36.73.
Join powers of types
36.74.
Joins of maps
36.75.
Joins of types
36.76.
The loop homotopy on the circle
36.77.
Loop spaces
36.78.
Maps of prespectra
36.79.
Mere spheres
36.80.
Morphisms of cocones under morphisms of sequential diagrams
36.81.
Morphisms of coforks
36.82.
Morphisms of dependent sequential diagrams
36.83.
Morphisms of descent data of the circle
36.84.
Morphisms of descent data for pushouts
36.85.
Morphisms of sequential diagrams
36.86.
The multiplication operation on the circle
36.87.
Null cocones under pointed span diagrams
36.88.
The plus-principle
36.89.
Powers of loops
36.90.
Premanifolds
36.91.
Prespectra
36.92.
The pullback property of pushouts
36.93.
Pushout-products
36.94.
Pushouts
36.95.
Pushouts of pointed types
36.96.
The recursion principle of pushouts
36.97.
Retracts of sequential diagrams
36.98.
Rewriting rules for pushouts
36.99.
Sections of families over the circle
36.100.
Sections of descent data for pushouts
36.101.
Sequential colimits
36.102.
Sequential diagrams
36.103.
Sequentially compact types
36.104.
Shifts of sequential diagrams
36.105.
Smash products of pointed types
36.106.
Spectra
36.107.
The sphere prespectrum
36.108.
Spheres
36.109.
Suspension prespectra
36.110.
Suspension Structures
36.111.
Suspensions of pointed types
36.112.
Suspensions of types
36.113.
Tangent spheres
36.114.
Total cocones of type families over cocones under sequential diagrams
36.115.
Total sequential diagrams of dependent sequential diagrams
36.116.
Triple loop spaces
36.117.
k-acyclic maps
36.118.
k-acyclic types
36.119.
The universal cover of the circle
36.120.
The universal property of the circle
36.121.
The universal property of coequalizers
36.122.
The universal property of pushouts
36.123.
The universal property of sequential colimits
36.124.
Universal property of suspensions
36.125.
Universal Property of suspensions of pointed types
36.126.
Wedges of pointed types
36.127.
Zigzags between sequential diagrams
37.
Trees
❱
37.1.
Algebras for polynomial endofunctors
37.2.
Bases of directed trees
37.3.
Bases of enriched directed trees
37.4.
Binary W-types
37.5.
Bounded multisets
37.6.
The coalgebra of directed trees
37.7.
The coalgebra of enriched directed trees
37.8.
Coalgebras of polynomial endofunctors
37.9.
The combinator of directed trees
37.10.
Combinators of enriched directed trees
37.11.
Directed trees
37.12.
The elementhood relation on coalgebras of polynomial endofunctors
37.13.
The elementhood relation on W-types
37.14.
Empty multisets
37.15.
Enriched directed trees
37.16.
Equivalences of directed trees
37.17.
Equivalences of enriched directed trees
37.18.
Extensional W-types
37.19.
Fibers of directed trees
37.20.
Fibers of enriched directed trees
37.21.
Full binary trees
37.22.
Functoriality of the combinator of directed trees
37.23.
Functoriality of the fiber operation on directed trees
37.24.
Functoriality of W-types
37.25.
Hereditary W-types
37.26.
Indexed W-types
37.27.
Induction principles on W-types
37.28.
Inequality on W-types
37.29.
Lower types of elements in W-types
37.30.
Morphisms of algebras of polynomial endofunctors
37.31.
Morphisms of coalgebras of polynomial endofunctors
37.32.
Morphisms of directed trees
37.33.
Morphisms of enriched directed trees
37.34.
Multiset-indexed dependent products of types
37.35.
Multisets
37.36.
Planar binary trees
37.37.
Plane trees
37.38.
Polynomial endofunctors
37.39.
Raising universe levels of directed trees
37.40.
Ranks of elements in W-types
37.41.
Rooted morphisms of directed trees
37.42.
Rooted morphisms of enriched directed trees
37.43.
Rooted quasitrees
37.44.
Rooted undirected trees
37.45.
Small multisets
37.46.
Submultisets
37.47.
Transitive multisets
37.48.
The underlying trees of elements of coalgebras of polynomial endofunctors
37.49.
The underlying trees of elements of W-types
37.50.
Undirected trees
37.51.
The universal multiset
37.52.
The universal tree
37.53.
The W-type of natural numbers
37.54.
The W-type of the type of propositions
37.55.
W-types
38.
Type theories
❱
38.1.
Comprehension of fibered type theories
38.2.
Dependent type theories
38.3.
Fibered dependent type theories
38.4.
Π-types in precategories with attributes
38.5.
Π-types in precategories with families
38.6.
Precategories with attributes
38.7.
Precategories with families
38.8.
Sections of dependent type theories
38.9.
Simple type theories
38.10.
Unityped type theories
39.
Univalent combinatorics
❱
39.1.
2-element decidable subtypes
39.2.
2-element subtypes
39.3.
2-element types
39.4.
The binomial types
39.5.
Bracelets
39.6.
Cartesian products of finite types
39.7.
The classical definition of the standard finite types
39.8.
Complements of isolated elements of finite types
39.9.
Coproducts of finite types
39.10.
Counting in type theory
39.11.
Counting the elements of decidable subtypes
39.12.
Counting the elements of dependent pair types
39.13.
Counting the elements of the fiber of a map
39.14.
Counting the elements in Maybe
39.15.
Cubes
39.16.
Cycle partitions of finite types
39.17.
Cycle prime decompositions of natural numbers
39.18.
Cyclic finite types
39.19.
Decidable dependent function types
39.20.
Decidability of dependent pair types
39.21.
Decidable equivalence relations on finite types
39.22.
Decidable propositions
39.23.
Decidable subtypes of finite types
39.24.
Dedekind finite sets
39.25.
Counting the elements of dependent function types
39.26.
Dependent pair types of finite types
39.27.
Finite discrete Σ-decompositions
39.28.
Distributivity of set truncation over finite products
39.29.
Double counting
39.30.
Embeddings
39.31.
Embeddings between standard finite types
39.32.
Equality in finite types
39.33.
Equality in the standard finite types
39.34.
Equivalences between finite types
39.35.
Equivalences of cubes
39.36.
Equivalences between standard finite types
39.37.
Ferrers diagrams (unlabeled partitions)
39.38.
Fibers of maps between finite types
39.39.
Finite choice
39.40.
Finite presentations of types
39.41.
Finite types
39.42.
Finiteness of the type of connected components
39.43.
Finitely presented types
39.44.
Finite function types
39.45.
The image of a map
39.46.
Inequality on types equipped with a counting
39.47.
Inhabited finite types
39.48.
Injective maps between finite types
39.49.
An involution on the standard finite types
39.50.
Isotopies of Latin squares
39.51.
Kuratowski finite sets
39.52.
Latin squares
39.53.
Locally finite types
39.54.
The groupoid of main classes of Latin hypercubes
39.55.
The groupoid of main classes of Latin squares
39.56.
The maybe monad on finite types
39.57.
Necklaces
39.58.
Orientations of the complete undirected graph
39.59.
Orientations of cubes
39.60.
Partitions of finite types
39.61.
Petri-nets
39.62.
π-finite types
39.63.
The pigeonhole principle
39.64.
Finitely π-presented types
39.65.
Quotients of finite types
39.66.
Ramsey theory
39.67.
Repetitions of values
39.68.
Repetitions of values in sequences
39.69.
Retracts of finite types
39.70.
Sequences of elements in finite types
39.71.
Set quotients of index 2
39.72.
Finite Σ-decompositions of finite types
39.73.
Skipping elements in standard finite types
39.74.
Small types
39.75.
Standard finite pruned trees
39.76.
Standard finite trees
39.77.
The standard finite types
39.78.
Steiner systems
39.79.
Steiner triple systems
39.80.
Combinatorial identities of sums of natural numbers
39.81.
Surjective maps between finite types
39.82.
Symmetric difference of finite subtypes
39.83.
Finite trivial Σ-decompositions
39.84.
Type duality of finite types
39.85.
Unions of finite subtypes
39.86.
The universal property of the standard finite types
39.87.
Unlabeled partitions
39.88.
Unlabeled rooted trees
39.89.
Unlabeled trees
40.
Universal algebra
❱
40.1.
Abstract equations over signatures
40.2.
Algebraic theories
40.3.
Algebraic theory of groups
40.4.
Algebras
40.5.
Congruences
40.6.
Homomorphisms of algebras
40.7.
Kernels of homomorphisms of algebras
40.8.
Models of signatures
40.9.
Quotient algebras
40.10.
Signatures
40.11.
Terms over signatures
41.
Wild category theory
❱
41.1.
Colax functors between large noncoherent wild higher precategories
41.2.
Colax functors between noncoherent wild higher precategories
41.3.
Isomorphisms in noncoherent large wild higher precategories
41.4.
Isomorphisms in noncoherent wild higher precategories
41.5.
Maps between noncoherent large wild higher precategories
41.6.
Maps between noncoherent wild higher precategories
41.7.
Noncoherent large wild higher precategories
41.8.
Noncoherent wild higher precategories
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