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.
Formalizing 100 Theorems
7.2.
Idempotents in Intensional Type Theory
7.3.
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 products of categories
8.27.
Dependent products of large categories
8.28.
Dependent products of large precategories
8.29.
Dependent products of precategories
8.30.
Discrete categories
8.31.
Embedding maps between precategories
8.32.
Embeddings between precategories
8.33.
Endomorphisms in categories
8.34.
Endomorphisms in precategories
8.35.
Epimorphism in large precategories
8.36.
Equivalences between categories
8.37.
Equivalences between large precategories
8.38.
Equivalences between precategories
8.39.
Essential fibers of functors between precategories
8.40.
Essentially injective functors between precategories
8.41.
Essentially surjective functors between precategories
8.42.
Exponential objects in precategories
8.43.
Extensions of functors between precategories
8.44.
Faithful functors between precategories
8.45.
Faithful maps between precategories
8.46.
Full functors between precategories
8.47.
Full large subcategories
8.48.
Full large subprecategories
8.49.
Full maps between precategories
8.50.
Full subcategories
8.51.
Full subprecategories
8.52.
Fully faithful functors between precategories
8.53.
Fully faithful maps between precategories
8.54.
Function categories
8.55.
Function precategories
8.56.
Functors between categories
8.57.
Functors from small to large categories
8.58.
Functors from small to large precategories
8.59.
Functors between large categories
8.60.
Functors between large precategories
8.61.
Functors between nonunital precategories
8.62.
Functors between precategories
8.63.
Functors between set-magmoids
8.64.
Gaunt categories
8.65.
Groupoids
8.66.
Homotopies of natural transformations in large precategories
8.67.
Indiscrete precategories
8.68.
The initial category
8.69.
Initial objects of large categories
8.70.
Initial objects of large precategories
8.71.
Initial objects in a precategory
8.72.
Isomorphism induction in categories
8.73.
Isomorphism induction in precategories
8.74.
Isomorphisms in categories
8.75.
Isomorphisms in large categories
8.76.
Isomorphisms in large precategories
8.77.
Isomorphisms in precategories
8.78.
Isomorphisms in subprecategories
8.79.
Large categories
8.80.
Large function categories
8.81.
Large function precategories
8.82.
Large precategories
8.83.
Large subcategories
8.84.
Large subprecategories
8.85.
Limits in precategories
8.86.
Maps between categories
8.87.
Maps from small to large categories
8.88.
Maps from small to large precategories
8.89.
Maps between precategories
8.90.
Maps between set-magmoids
8.91.
Monads on categories
8.92.
Monads on precategories
8.93.
Monomorphisms in large precategories
8.94.
Natural isomorphisms between functors between categories
8.95.
Natural isomorphisms between functors between large precategories
8.96.
Natural isomorphisms between functors between precategories
8.97.
Natural isomorphisms between maps between categories
8.98.
Natural isomorphisms between maps between precategories
8.99.
Natural numbers object in a precategory
8.100.
Natural transformations between functors between categories
8.101.
Natural transformations between functors from small to large categories
8.102.
Natural transformations between functors from small to large precategories
8.103.
Natural transformations between functors between large categories
8.104.
Natural transformations between functors between large precategories
8.105.
Natural transformations between functors between precategories
8.106.
Natural transformations between maps between categories
8.107.
Natural transformations between maps from small to large precategories
8.108.
Natural transformations between maps between precategories
8.109.
Nonunital precategories
8.110.
One object precategories
8.111.
Opposite categories
8.112.
Opposite large precategories
8.113.
Opposite precategories
8.114.
Opposite preunivalent categories
8.115.
Pointed endofunctors on categories
8.116.
Pointed endofunctors
8.117.
Precategories
8.118.
Precategory of elements of a presheaf
8.119.
The precategory of functors and natural transformations between two precategories
8.120.
The precategory of functors and natural transformations from small to large precategories
8.121.
The precategory of maps and natural transformations from a small to a large precategory
8.122.
The precategory of maps and natural transformations between two precategories
8.123.
Pregroupoids
8.124.
Presheaf categories
8.125.
Preunivalent categories
8.126.
Products in precategories
8.127.
Products of precategories
8.128.
Pseudomonic functors between precategories
8.129.
Pullbacks in precategories
8.130.
Replete subprecategories
8.131.
Representable functors between categories
8.132.
Representable functors between large precategories
8.133.
Representable functors between precategories
8.134.
The representing arrow category
8.135.
Restrictions of functors to cores of precategories
8.136.
Right extensions in precategories
8.137.
Right Kan extensions in precategories
8.138.
Rigid objects in a category
8.139.
Rigid objects in a precategory
8.140.
Set-magmoids
8.141.
Sieves in categories
8.142.
The simplex category
8.143.
Slice precategories
8.144.
Split essentially surjective functors between precategories
8.145.
Strict categories
8.146.
Structure equivalences between set-magmoids
8.147.
Subcategories
8.148.
Subprecategories
8.149.
Subterminal precategories
8.150.
The terminal category
8.151.
Terminal objects in a precategory
8.152.
Wide subcategories
8.153.
Wide subprecategories
8.154.
The Yoneda lemma for categories
8.155.
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.
Elementary number theory
❱
10.1.
The absolute value function on the integers
10.2.
The Ackermann function
10.3.
Addition on integer fractions
10.4.
Addition on the integers
10.5.
Addition on the natural numbers
10.6.
Addition of positive, negative, nonnegative and nonpositive integers
10.7.
Addition on the rational numbers
10.8.
The additive group of rational numbers
10.9.
Arithmetic functions
10.10.
The based induction principle of the natural numbers
10.11.
Based strong induction for the natural numbers
10.12.
Bezout's lemma in the integers
10.13.
Bezout's lemma on the natural numbers
10.14.
The binomial coefficients
10.15.
The binomial theorem for the integers
10.16.
The binomial theorem for the natural numbers
10.17.
Bounded sums of arithmetic functions
10.18.
Catalan numbers
10.19.
The cofibonacci sequence
10.20.
The Collatz bijection
10.21.
The Collatz conjecture
10.22.
The commutative semiring of natural numbers
10.23.
The congruence relations on the integers
10.24.
The congruence relations on the natural numbers
10.25.
The cross-multiplication difference of two integer fractions
10.26.
Cubes of natural numbers
10.27.
Decidable dependent function types
10.28.
The decidable total order of integers
10.29.
The decidable total order of natural numbers
10.30.
The decidable total order of rational numbers
10.31.
The decidable total order of a standard finite type
10.32.
Decidable types in elementary number theory
10.33.
The difference between integers
10.34.
The difference between rational numbers
10.35.
Dirichlet convolution
10.36.
The distance between integers
10.37.
The distance between natural numbers
10.38.
Divisibility of integers
10.39.
Divisibility in modular arithmetic
10.40.
Divisibility of natural numbers
10.41.
The divisibility relation on the standard finite types
10.42.
Equality of integers
10.43.
Equality of natural numbers
10.44.
Euclidean division on the natural numbers
10.45.
Euler's totient function
10.46.
Exponentiation of natural numbers
10.47.
Factorials of natural numbers
10.48.
Falling factorials
10.49.
Fermat numbers
10.50.
The Fibonacci sequence
10.51.
The field of rational numbers
10.52.
The natural numbers base k
10.53.
Finitely cyclic maps
10.54.
The fundamental theorem of arithmetic
10.55.
The Goldbach conjecture
10.56.
The greatest common divisor of integers
10.57.
The greatest common divisor of natural numbers
10.58.
The group of integers
10.59.
The half-integers
10.60.
The Hardy-Ramanujan number
10.61.
Inequality on integer fractions
10.62.
Inequality on the integers
10.63.
Inequality of natural numbers
10.64.
Inequality on the rational numbers
10.65.
Inequality on the standard finite types
10.66.
The infinitude of primes
10.67.
Initial segments of the natural numbers
10.68.
Integer fractions
10.69.
Integer partitions
10.70.
The integers
10.71.
The Jacobi symbol
10.72.
The Kolakoski sequence
10.73.
The Legendre symbol
10.74.
Lower bounds of type families over the natural numbers
10.75.
Maximum on the natural numbers
10.76.
Maximum on the standard finite types
10.77.
The mediant fraction of two integer fractions
10.78.
Mersenne primes
10.79.
Minimum on the natural numbers
10.80.
Minimum on the standard finite types
10.81.
Modular arithmetic
10.82.
Modular arithmetic on the standard finite types
10.83.
The monoid of natural numbers with addition
10.84.
The monoid of the natural numbers with maximum
10.85.
Multiplication on integer fractions
10.86.
Multiplication of integers
10.87.
Multiplication of the elements of a list of natural numbers
10.88.
Multiplication of natural numbers
10.89.
Multiplication of positive, negative, nonnegative and nonpositive integers
10.90.
Multiplication on the rational numbers
10.91.
The multiplicative group of positive rational numbers
10.92.
The multiplicative group of rational numbers
10.93.
Multiplicative inverses of positive integer fractions
10.94.
The multiplicative monoid of natural numbers
10.95.
The multiplicative monoid of rational numbers
10.96.
Multiplicative units in the integers
10.97.
Multiplicative units in modular arithmetic
10.98.
Multiset coefficients
10.99.
The type of natural numbers
10.100.
The negative integers
10.101.
The nonnegative integers
10.102.
The nonpositive integers
10.103.
Nonzero integers
10.104.
Nonzero natural numbers
10.105.
Nonzero rational numbers
10.106.
The ordinal induction principle for the natural numbers
10.107.
Parity of the natural numbers
10.108.
Peano arithmetic
10.109.
Pisano periods
10.110.
The poset of natural numbers ordered by divisibility
10.111.
The positive, negative, nonnegative and nonpositive integers
10.112.
Positive integer fractions
10.113.
The positive integers
10.114.
Positive rational numbers
10.115.
Powers of integers
10.116.
Powers of two
10.117.
Prime numbers
10.118.
Products of natural numbers
10.119.
Proper divisors of natural numbers
10.120.
Pythagorean triples
10.121.
The rational numbers
10.122.
Reduced integer fractions
10.123.
Relatively prime integers
10.124.
Relatively prime natural numbers
10.125.
Repeating an element in a standard finite type
10.126.
Retracts of the type of natural numbers
10.127.
The ring of integers
10.128.
The ring of rational numbers
10.129.
The sieve of Eratosthenes
10.130.
Square-free natural numbers
10.131.
Squares in the integers
10.132.
Squares in ℤₚ
10.133.
Squares in the natural numbers
10.134.
The standard cyclic groups
10.135.
The standard cyclic rings
10.136.
Stirling numbers of the second kind
10.137.
Strict inequality on the integer fractions
10.138.
Strict inequality on the integers
10.139.
Strict inequality on the natural numbers
10.140.
Strict inequality on the rational numbers
10.141.
Strictly ordered pairs of natural numbers
10.142.
The strong induction principle for the natural numbers
10.143.
Sums of natural numbers
10.144.
Taxicab numbers
10.145.
Telephone numbers
10.146.
The triangular numbers
10.147.
The Twin Prime conjecture
10.148.
Type arithmetic with natural numbers
10.149.
Unit elements in the standard finite types
10.150.
Unit similarity on the standard finite types
10.151.
The universal property of the integers
10.152.
The universal property of the natural numbers
10.153.
Upper bounds for type families over the natural numbers
10.154.
The Well-Ordering Principle of the natural numbers
10.155.
The well-ordering principle of the standard finite types
11.
Finite algebra
❱
11.1.
Commutative finite rings
11.2.
Dependent products of commutative finit rings
11.3.
Dependent products of finite rings
11.4.
Finite fields
11.5.
Finite rings
11.6.
Homomorphisms of commutative finite rings
11.7.
Homomorphisms of finite rings
11.8.
Products of commutative finite rings
11.9.
Products of finite rings
11.10.
Semisimple commutative finite rings
12.
Finite group theory
❱
12.1.
The abstract quaternion group of order 8
12.2.
Alternating concrete groups
12.3.
Alternating groups
12.4.
Cartier's delooping of the sign homomorphism
12.5.
The concrete quaternion group
12.6.
Deloopings of the sign homomorphism
12.7.
Abelian groups
12.8.
Finite Commutative monoids
12.9.
Finite groups
12.10.
Finite monoids
12.11.
Finite semigroups
12.12.
The group of n-element types
12.13.
Groups of order 2
12.14.
Orbits of permutations
12.15.
Permutations
12.16.
Permutations of standard finite types
12.17.
The sign homomorphism
12.18.
Simpson's delooping of the sign homomorphism
12.19.
Subgroups of finite groups
12.20.
Tetrahedra in 3-dimensional space
12.21.
Transpositions
12.22.
Transpositions of standard finite types
13.
Foundation
❱
13.1.
0-Connected types
13.2.
0-Images of maps
13.3.
0-Maps
13.4.
1-Types
13.5.
2-Types
13.6.
Action on equivalences of functions
13.7.
The action on equivalences of functions out of subuniverses
13.8.
Action on equivalences of type families
13.9.
Action on equivalences in type families over subuniverses
13.10.
The action of functions on higher identifications
13.11.
The action on homotopies of functions
13.12.
The binary action on identifications of binary functions
13.13.
The action on identifications of dependent functions
13.14.
The action on identifications of functions
13.15.
Apartness relations
13.16.
Arithmetic law for coproduct decomposition and Σ-decomposition
13.17.
Arithmetic law for product decomposition and Π-decomposition
13.18.
Automorphisms
13.19.
The axiom of choice
13.20.
Bands
13.21.
Base changes of span diagrams
13.22.
Binary embeddings
13.23.
Binary equivalences
13.24.
Binary equivalences on unordered pairs of types
13.25.
Binary functoriality of set quotients
13.26.
Homotopies of binary operations
13.27.
Binary operations on unordered pairs of types
13.28.
Binary reflecting maps of equivalence relations
13.29.
Binary relations
13.30.
Binary relations with extensions
13.31.
Binary relations with lifts
13.32.
Binary transport
13.33.
Binary type duality
13.34.
The booleans
13.35.
The Cantor–Schröder–Bernstein–Escardó theorem
13.36.
Cantor's theorem
13.37.
Cartesian morphisms of arrows
13.38.
Cartesian morphisms of span diagrams
13.39.
Cartesian product types
13.40.
Cartesian products of set quotients
13.41.
The category of families of sets
13.42.
The category of sets
13.43.
Choice of representatives for an equivalence relation
13.44.
Codiagonal maps of types
13.45.
Coherently idempotent maps
13.46.
Coherently invertible maps
13.47.
Coinhabited pairs of types
13.48.
Commuting cubes of maps
13.49.
Commuting hexagons of identifications
13.50.
Commuting pentagons of identifications
13.51.
Commuting prisms of maps
13.52.
Commuting squares of homotopies
13.53.
Commuting squares of identifications
13.54.
Commuting squares of maps
13.55.
Commuting tetrahedra of homotopies
13.56.
Commuting tetrahedra of maps
13.57.
Commuting triangles of homotopies
13.58.
Commuting triangles of identifications
13.59.
Commuting triangles of maps
13.60.
Commuting triangles of morphisms of arrows
13.61.
Complements of type families
13.62.
Complements of subtypes
13.63.
Composite maps in inverse sequential diagrams
13.64.
Composition algebra
13.65.
Computational identity types
13.66.
Cones over cospan diagrams
13.67.
Cones over inverse sequential diagrams
13.68.
Conjunction
13.69.
Connected components of types
13.70.
Connected components of universes
13.71.
Connected maps
13.72.
Connected types
13.73.
Constant maps
13.74.
Constant span diagrams
13.75.
Constant type families
13.76.
Contractible maps
13.77.
Contractible types
13.78.
Copartial elements
13.79.
Copartial functions
13.80.
Coproduct decompositions
13.81.
Coproduct decompositions in a subuniverse
13.82.
Coproduct types
13.83.
Coproducts of pullbacks
13.84.
Morphisms in the coslice category of types
13.85.
Cospan diagrams
13.86.
Cospans of types
13.87.
Decidability of dependent function types
13.88.
Decidability of dependent pair types
13.89.
Decidable embeddings
13.90.
Decidable equality
13.91.
Decidable equivalence relations
13.92.
Decidable maps
13.93.
Decidable propositions
13.94.
Decidable relations on types
13.95.
Decidable subtypes
13.96.
Decidable types
13.97.
Dependent binary homotopies
13.98.
The dependent binomial theorem for types (distributivity of dependent function types over coproduct types)
13.99.
Dependent epimorphisms
13.100.
Dependent epimorphisms with respect to truncated types
13.101.
Dependent function types
13.102.
Dependent homotopies
13.103.
Dependent identifications
13.104.
Dependent inverse sequential diagrams of types
13.105.
Dependent pair types
13.106.
Dependent products of pullbacks
13.107.
Dependent sequences
13.108.
Dependent sums of pullbacks
13.109.
Dependent telescopes
13.110.
The dependent universal property of equivalences
13.111.
Descent for coproduct types
13.112.
Descent for dependent pair types
13.113.
Descent for the empty type
13.114.
Descent for equivalences
13.115.
Diagonal maps into cartesian products of types
13.116.
Diagonal maps of types
13.117.
Diagonal span diagrams
13.118.
Diagonals of maps
13.119.
Diagonals of morphisms of arrows
13.120.
Discrete relations
13.121.
Discrete relaxed Σ-decompositions
13.122.
Discrete Σ-decompositions
13.123.
Discrete types
13.124.
Disjunction
13.125.
Double arrows
13.126.
Double negation
13.127.
The double negation modality
13.128.
Double negation stable propositions
13.129.
Double powersets
13.130.
Dubuc-Penon compact types
13.131.
Effective maps for equivalence relations
13.132.
Embeddings
13.133.
Empty types
13.134.
Endomorphisms
13.135.
Epimorphisms
13.136.
Epimorphisms with respect to maps into sets
13.137.
Epimorphisms with respect to truncated types
13.138.
Equality of cartesian product types
13.139.
Equality of coproduct types
13.140.
Equality on dependent function types
13.141.
Equality of dependent pair types
13.142.
Equality in the fibers of a map
13.143.
Equivalence classes
13.144.
Equivalence extensionality
13.145.
Equivalence induction
13.146.
Equivalence injective type families
13.147.
Equivalence relations
13.148.
Equivalences
13.149.
Equivalences of arrows
13.150.
Equivalences of cospans
13.151.
Equivalences of double arrows
13.152.
Equivalences of inverse sequential diagrams of types
13.153.
Equivalences on Maybe
13.154.
Equivalences of span diagrams
13.155.
Equivalences of span diagrams on families of types
13.156.
Equivalences of spans
13.157.
Equivalences of spans of families of types
13.158.
Evaluation of functions
13.159.
Exclusive disjunctions
13.160.
Exclusive sums
13.161.
Existential quantification
13.162.
Exponents of set quotients
13.163.
Extensions of types
13.164.
Faithful maps
13.165.
Families of equivalences
13.166.
Families of maps
13.167.
Families of types over telescopes
13.168.
Fiber inclusions
13.169.
Fibered equivalences
13.170.
Fibered involutions
13.171.
Maps fibered over a map
13.172.
Fibers of maps
13.173.
Finitely coherent equivalences
13.174.
Finitely coherently invertible maps
13.175.
Fixed points of endofunctions
13.176.
Full subtypes of types
13.177.
Function extensionality
13.178.
Function types
13.179.
Functional correspondences
13.180.
Functoriality of cartesian product types
13.181.
Functoriality of coproduct types
13.182.
Functoriality of dependent function types
13.183.
Functoriality of dependent pair types
13.184.
Functoriality of fibers of maps
13.185.
Functoriality of function types
13.186.
Functoriality of propositional truncations
13.187.
Functorialty of pullbacks
13.188.
Functoriality of sequential limits
13.189.
Functoriality of set quotients
13.190.
Functoriality of set truncation
13.191.
Functoriality of truncations
13.192.
The fundamental theorem of identity types
13.193.
Global choice
13.194.
Global subuniverses
13.195.
Higher homotopies of morphisms of arrows
13.196.
Hilbert's ε-operators
13.197.
Homotopies
13.198.
Homotopies of morphisms of arrows
13.199.
Homotopy algebra
13.200.
Homotopy induction
13.201.
The homotopy preorder of types
13.202.
Idempotent maps
13.203.
Identity systems
13.204.
Identity types of truncated types
13.205.
Identity types
13.206.
The image of a map
13.207.
Images of subtypes
13.208.
Implicit function types
13.209.
Impredicative encodings of the logical operations
13.210.
Impredicative universes
13.211.
The induction principle for propositional truncation
13.212.
Infinitely coherent equivalences
13.213.
Inhabited subtypes
13.214.
Inhabited types
13.215.
Injective maps
13.216.
The interchange law
13.217.
Intersections of subtypes
13.218.
Inverse sequential diagrams of types
13.219.
Invertible maps
13.220.
Involutions
13.221.
Irrefutable propositions
13.222.
Isolated elements
13.223.
Isomorphisms of sets
13.224.
Iterated cartesian product types
13.225.
Iterated dependent pair types
13.226.
Iterated dependent product types
13.227.
Iterating automorphisms
13.228.
Iterating functions
13.229.
Iterating involutions
13.230.
Kernel span diagrams of maps
13.231.
Large binary relations
13.232.
Large dependent pair types
13.233.
Large homotopies
13.234.
Large identity types
13.235.
The large locale of propositions
13.236.
The large locale of subtypes
13.237.
The law of excluded middle
13.238.
Lawvere's fixed point theorem
13.239.
The lesser limited principle of omniscience
13.240.
Lifts of types
13.241.
The limited principle of omniscience
13.242.
Locally small types
13.243.
Logical equivalences
13.244.
Maps in global subuniverses
13.245.
Maps in subuniverses
13.246.
The maybe monad
13.247.
Mere embeddings
13.248.
Mere equality
13.249.
Mere equivalences
13.250.
Mere functions
13.251.
Mere logical equivalences
13.252.
Mere path-cosplit maps
13.253.
Monomorphisms
13.254.
Morphisms of arrows
13.255.
Morphisms of binary relations
13.256.
Morphisms of cospan diagrams
13.257.
Morphisms of cospans
13.258.
Morphisms of double arrows
13.259.
Morphisms of inverse sequential diagrams of types
13.260.
Morphisms of span diagrams
13.261.
Morphisms of spans
13.262.
Morphisms of spans on families of types
13.263.
Morphisms of twisted arrows
13.264.
Multisubsets
13.265.
Multivariable correspondences
13.266.
Multivariable decidable relations
13.267.
Multivariable functoriality of set quotients
13.268.
Multivariable homotopies
13.269.
Multivariable operations
13.270.
Multivariable relations
13.271.
Multivariable sections
13.272.
Negated equality
13.273.
Negation
13.274.
Noncontractible types
13.275.
Null-homotopic maps
13.276.
Operations on span diagrams
13.277.
Operations on spans
13.278.
Operations on spans of families of types
13.279.
Opposite spans
13.280.
Pairs of distinct elements
13.281.
Partial elements
13.282.
Partial functions
13.283.
Partial sequences
13.284.
Partitions
13.285.
Path algebra
13.286.
Path-cosplit maps
13.287.
Path-split maps
13.288.
Perfect images
13.289.
Permutations of spans of families of types
13.290.
Π-decompositions of types
13.291.
Π-decompositions of types into types in a subuniverse
13.292.
Pointed torsorial type families
13.293.
Postcomposition of dependent functions
13.294.
Postcomposition of functions
13.295.
Postcomposition of pullbacks
13.296.
Powersets
13.297.
Precomposition of dependent functions
13.298.
Precomposition of functions
13.299.
Precomposition of functions into subuniverses
13.300.
Precomposition of type families
13.301.
Preimages of subtypes
13.302.
The preunivalence axiom
13.303.
Preunivalent type families
13.304.
The principle of omniscience
13.305.
Product decompositions
13.306.
Product decompositions of types in a subuniverse
13.307.
Products of binary relations
13.308.
Products of equivalence relataions
13.309.
Products of tuples of types
13.310.
Products of pullbacks
13.311.
Products of unordered pairs of types
13.312.
Products of unordered tuples of types
13.313.
Projective types
13.314.
Proper subsets
13.315.
Propositional extensionality
13.316.
Propositional maps
13.317.
Propositional resizing
13.318.
Propositional truncations
13.319.
Propositions
13.320.
Pullbacks
13.321.
Pullbacks of subtypes
13.322.
Quasicoherently idempotent maps
13.323.
Raising universe levels
13.324.
Reflecting maps for equivalence relations
13.325.
Reflexive relations
13.326.
The Regensburg extension of the fundamental theorem of identity types
13.327.
Relaxed Σ-decompositions of types
13.328.
Repetitions of values of maps
13.329.
Repetitions in sequences
13.330.
The type theoretic replacement axiom
13.331.
Retractions
13.332.
Retracts of maps
13.333.
Retracts of types
13.334.
Sections
13.335.
Separated types
13.336.
Sequences
13.337.
Sequential limits
13.338.
Set presented types
13.339.
Set quotients
13.340.
Set truncations
13.341.
Sets
13.342.
Shifting sequences
13.343.
Σ-closed subuniverses
13.344.
Σ-decompositions of types into types in a subuniverse
13.345.
Σ-decompositions of types
13.346.
Singleton induction
13.347.
Singleton subtypes
13.348.
Morphisms in the slice category of types
13.349.
Small maps
13.350.
Small types
13.351.
Small universes
13.352.
Sorial type families
13.353.
Span diagrams
13.354.
Span diagrams on families of types
13.355.
Spans of types
13.356.
Spans of families of types
13.357.
Split idempotent maps
13.358.
Split surjective maps
13.359.
Standard apartness relations
13.360.
Standard pullbacks
13.361.
Strict symmetrization of binary relations
13.362.
Strictly involutive identity types
13.363.
The strictly right unital concatenation operation on identifications
13.364.
Strongly extensional maps
13.365.
Structure
13.366.
The structure identity principle
13.367.
Structured type duality
13.368.
Subsingleton induction
13.369.
Subterminal types
13.370.
Subtype duality
13.371.
The subtype identity principle
13.372.
Subtypes
13.373.
Subuniverses
13.374.
Surjective maps
13.375.
Symmetric binary relations
13.376.
Symmetric cores of binary relations
13.377.
Symmetric difference of subtypes
13.378.
The symmetric identity types
13.379.
Symmetric operations
13.380.
Telescopes
13.381.
Terminal spans on families of types
13.382.
Tight apartness relations
13.383.
Torsorial type families
13.384.
Total partial elements
13.385.
Total partial functions
13.386.
Transfinite cocomposition of maps
13.387.
Transport along equivalences
13.388.
Transport along higher identifications
13.389.
Transport along homotopies
13.390.
Transport along identifications
13.391.
Transport-split type families
13.392.
Transposing identifications along equivalences
13.393.
Transposing identifications along retractions
13.394.
Transposing identifications along sections
13.395.
Transposition of span diagrams
13.396.
Trivial relaxed Σ-decompositions
13.397.
Trivial Σ-decompositions
13.398.
Truncated equality
13.399.
Truncated maps
13.400.
Truncated types
13.401.
k-Equivalences
13.402.
Truncation images of maps
13.403.
Truncation levels
13.404.
The truncation modalities
13.405.
Truncations
13.406.
Tuples of types
13.407.
Type arithmetic with the booleans
13.408.
Type arithmetic for cartesian product types
13.409.
Type arithmetic for coproduct types
13.410.
Type arithmetic with dependent function types
13.411.
Type arithmetic for dependent pair types
13.412.
Type arithmetic with the empty type
13.413.
Type arithmetic with the unit type
13.414.
Type duality
13.415.
The type theoretic principle of choice
13.416.
Unions of subtypes
13.417.
Uniqueness of the image of a map
13.418.
Uniqueness quantification
13.419.
The uniqueness of set quotients
13.420.
Uniqueness of set truncations
13.421.
Uniqueness of the truncations
13.422.
The unit type
13.423.
Unital binary operations
13.424.
The univalence axiom
13.425.
The univalence axiom implies function extensionality
13.426.
Univalent type families
13.427.
The universal property of booleans
13.428.
The universal properties of cartesian product types
13.429.
Universal property of contractible types
13.430.
The universal property of coproduct types
13.431.
The universal property of dependent function types
13.432.
The universal property of dependent pair types
13.433.
The universal property of the empty type
13.434.
The universal property of equivalences
13.435.
The universal property of the family of fibers of maps
13.436.
The universal property of fiber products
13.437.
The universal property of identity systems
13.438.
The universal property of identity types
13.439.
The universal property of the image of a map
13.440.
The universal property of the maybe monad
13.441.
The universal property of propositional truncations
13.442.
The universal property of propositional truncations with respect to sets
13.443.
The universal property of pullbacks
13.444.
The universal property of sequential limits
13.445.
The universal property of set quotients
13.446.
The universal property of set truncations
13.447.
The universal property of truncations
13.448.
The universal property of the unit type
13.449.
Universal quantification
13.450.
Universe levels
13.451.
Unordered pairs of elements in a type
13.452.
Unordered pairs of types
13.453.
Unordered n-tuples of elements in a type
13.454.
Unordered tuples of types
13.455.
Vectors of set quotients
13.456.
Weak function extensionality
13.457.
The weak limited principle of omniscience
13.458.
Weakly constant maps
13.459.
Whiskering higher homotopies with respect to composition
13.460.
Whiskering homotopies with respect to composition
13.461.
Whiskering homotopies with respect to concatenation
13.462.
Whiskering identifications with respect to concatenation
13.463.
Whiskering operations
13.464.
The wild category of types
13.465.
Yoneda identity types
14.
Foundation core
❱
14.1.
1-Types
14.2.
Cartesian product types
14.3.
Coherently invertible maps
14.4.
Commuting prisms of maps
14.5.
Commuting squares of homotopies
14.6.
Commuting squares of identifications
14.7.
Commuting squares of maps
14.8.
Commuting triangles of maps
14.9.
Constant maps
14.10.
Contractible maps
14.11.
Contractible types
14.12.
Coproduct types
14.13.
Decidable propositions
14.14.
Dependent identifications
14.15.
Diagonal maps into cartesian products of types
14.16.
Discrete types
14.17.
Embeddings
14.18.
Empty types
14.19.
Endomorphisms
14.20.
Equality of dependent pair types
14.21.
Equivalence relations
14.22.
Equivalences
14.23.
Families of equivalences
14.24.
Fibers of maps
14.25.
Function types
14.26.
Functoriality of dependent function types
14.27.
Functoriality of dependent pair types
14.28.
Homotopies
14.29.
Identity types
14.30.
Injective maps
14.31.
Invertible maps
14.32.
Negation
14.33.
Operations on span diagrams
14.34.
Operations on spans
14.35.
Path-split maps
14.36.
Postcomposition of dependent functions
14.37.
Postcomposition of functions
14.38.
Precomposition of dependent functions
14.39.
Precomposition of functions
14.40.
Propositional maps
14.41.
Propositions
14.42.
Pullbacks
14.43.
Retractions
14.44.
Retracts of types
14.45.
Sections
14.46.
Sets
14.47.
Small types
14.48.
Subtypes
14.49.
Torsorial type families
14.50.
Transport along identifications
14.51.
Truncated maps
14.52.
Truncated types
14.53.
Truncation levels
14.54.
The type theoretic principle of choice
14.55.
The univalence axiom
14.56.
The universal property of pullbacks
14.57.
The universal property of truncations
14.58.
Whiskering homotopies with respect to concatenation
14.59.
Whiskering identifications with respect to concatenation
15.
Graph theory
❱
15.1.
Acyclic undirected graphs
15.2.
Circuits in undirected graphs
15.3.
Closed walks in undirected graphs
15.4.
Complete bipartite graphs
15.5.
Complete multipartite graphs
15.6.
Complete undirected graphs
15.7.
Connected graphs
15.8.
Cycles in undirected graphs
15.9.
Directed graph structures on standard finite sets
15.10.
Directed graphs
15.11.
Discrete graphs
15.12.
Displayed large reflexive graphs
15.13.
Edge-coloured undirected graphs
15.14.
Embeddings of directed graphs
15.15.
Embeddings of undirected graphs
15.16.
Enriched undirected graphs
15.17.
Equivalences of directed graphs
15.18.
Equivalences of enriched undirected graphs
15.19.
Equivalences of undirected graphs
15.20.
Eulerian circuits in undirected graphs
15.21.
Faithful morphisms of undirected graphs
15.22.
Fibers of directed graphs
15.23.
Finite graphs
15.24.
Geometric realizations of undirected graphs
15.25.
Higher directed graphs
15.26.
Hypergraphs
15.27.
Large higher directed graphs
15.28.
Large reflexive graphs
15.29.
Matchings
15.30.
Mere equivalences of undirected graphs
15.31.
Morphisms of directed graphs
15.32.
Morphisms of undirected graphs
15.33.
Incidence in undirected graphs
15.34.
Orientations of undirected graphs
15.35.
Paths in undirected graphs
15.36.
Polygons
15.37.
Raising universe levels of directed graphs
15.38.
Reflecting maps of undirected graphs
15.39.
Reflexive graphs
15.40.
Regular undirected graph
15.41.
Simple undirected graphs
15.42.
Stereoisomerism for enriched undirected graphs
15.43.
Totally faithful morphisms of undirected graphs
15.44.
Trails in directed graphs
15.45.
Trails in undirected graphs
15.46.
Undirected graph structures on standard finite sets
15.47.
Undirected graphs
15.48.
Vertex covers
15.49.
Voltage graphs
15.50.
Walks in directed graphs
15.51.
Walks in undirected graphs
15.52.
Wide displayed large reflexive graphs
16.
Group theory
❱
16.1.
Abelian groups
16.2.
Abelianization of groups
16.3.
Pointwise addition of morphisms of abelian groups
16.4.
Automorphism groups
16.5.
Cartesian products of abelian groups
16.6.
Cartesian products of concrete groups
16.7.
Cartesian products of groups
16.8.
Cartesian products of monoids
16.9.
Cartesian products of semigroups
16.10.
The category of abelian groups
16.11.
The category of concrete groups
16.12.
The category of group actions
16.13.
The category of groups
16.14.
The orbit category of a group
16.15.
The category of semigroups
16.16.
Cayley's theorem
16.17.
The center of a group
16.18.
Center of a monoid
16.19.
Center of a semigroup
16.20.
Central elements of groups
16.21.
Central elements of monoids
16.22.
Central elements of semirings
16.23.
Centralizer subgroups
16.24.
Characteristic subgroups
16.25.
Commutative monoids
16.26.
Commutator subgroups
16.27.
Commutators of elements in groups
16.28.
Commuting elements of groups
16.29.
Commuting elements of monoids
16.30.
Commuting elements of semigroups
16.31.
Commuting squares of group homomorphisms
16.32.
Concrete group actions
16.33.
Concrete groups
16.34.
Concrete monoids
16.35.
Congruence relations on abelian groups
16.36.
Congruence relations on commutative monoids
16.37.
Congruence relations on groups
16.38.
Congruence relations on monoids
16.39.
Congruence relations on semigroups
16.40.
Conjugation in groups
16.41.
Conjugation on concrete groups
16.42.
Contravariant pushforwards of concrete group actions
16.43.
Cores of monoids
16.44.
Cyclic groups
16.45.
Decidable subgroups of groups
16.46.
Dependent products of abelian groups
16.47.
Dependent products of commutative monoids
16.48.
Dependent products of groups
16.49.
Dependent products of monoids
16.50.
Dependent products of semigroups
16.51.
The dihedral group construction
16.52.
The dihedral groups
16.53.
The E₈-lattice
16.54.
Elements of finite order
16.55.
Embeddings of abelian groups
16.56.
Embeddings of groups
16.57.
The endomorphism rings of abelian groups
16.58.
Epimorphisms in groups
16.59.
Equivalences of concrete group actions
16.60.
Equivalences of concrete groups
16.61.
Equivalences of group actions
16.62.
Equivalences between semigroups
16.63.
Exponents of abelian groups
16.64.
Exponents of groups
16.65.
Free concrete group actions
16.66.
Free groups with one generator
16.67.
The full subgroup of a group
16.68.
The full subsemigroup of a semigroup
16.69.
Function groups of abelian groups
16.70.
Function commutative monoids
16.71.
Function groups
16.72.
Function monoids
16.73.
Function semigroups
16.74.
Functoriality of quotient groups
16.75.
Furstenberg groups
16.76.
Generating elements of groups
16.77.
Generating sets of groups
16.78.
Group actions
16.79.
Abstract groups
16.80.
Homomorphisms of abelian groups
16.81.
Homomorphisms of commutative monoids
16.82.
Morphisms of concrete group actions
16.83.
Homomorphisms of concrete groups
16.84.
Homomorphisms of generated subgroups
16.85.
Homomorphisms of group actions
16.86.
Homomorphisms of groups
16.87.
Homomorphisms of groups equipped with normal subgroups
16.88.
Homomorphisms of monoids
16.89.
Homomorphisms of semigroups
16.90.
Images of group homomorphisms
16.91.
Images of semigroup homomorphisms
16.92.
Integer multiples of elements in abelian groups
16.93.
Integer powers of elements of groups
16.94.
Intersections of subgroups of abelian groups
16.95.
Intersections of subgroups of groups
16.96.
Inverse semigroups
16.97.
Invertible elements in monoids
16.98.
Isomorphisms of abelian groups
16.99.
Isomorphisms of concrete groups
16.100.
Isomorphisms of group actions
16.101.
Isomorphisms of groups
16.102.
Isomorphisms of monoids
16.103.
Isomorphisms of semigroups
16.104.
Iterated cartesian products of concrete groups
16.105.
Kernels of homomorphisms between abelian groups
16.106.
Kernels of homomorphisms of concrete groups
16.107.
Kernels of homomorphisms of groups
16.108.
Large semigroups
16.109.
Concrete automorphism groups on sets
16.110.
Mere equivalences of concrete group actions
16.111.
Mere equivalences of group actions
16.112.
Monoid actions
16.113.
Monoids
16.114.
Monomorphisms of concrete groups
16.115.
Monomorphisms in the category of groups
16.116.
Multiples of elements in abelian groups
16.117.
Nontrivial groups
16.118.
Normal closures of subgroups
16.119.
Normal cores of subgroups
16.120.
Normal subgroups
16.121.
Normal subgroups of concrete groups
16.122.
Normal submonoids
16.123.
Normal submonoids of commutative monoids
16.124.
Normalizer subgroups
16.125.
Nullifying group homomorphisms
16.126.
The opposite of a group
16.127.
The opposite of a semigroup
16.128.
The orbit-stabilizer theorem for concrete groups
16.129.
Orbits of concrete group actions
16.130.
Orbits of group actions
16.131.
The order of an element in a group
16.132.
Perfect cores
16.133.
Perfect groups
16.134.
Perfect subgroups
16.135.
Powers of elements in commutative monoids
16.136.
Powers of elements in groups
16.137.
Powers of elements in monoids
16.138.
The precategory of commutative monoids
16.139.
The precategory of concrete groups
16.140.
The precategory of group actions
16.141.
The precategory of groups
16.142.
The precategory of monoids
16.143.
The precategory of orbits of a monoid action
16.144.
The precategory of semigroups
16.145.
Principal group actions
16.146.
Principal torsors of concrete groups
16.147.
Products of elements in a monoid
16.148.
Products of tuples of elements in commutative monoids
16.149.
Pullbacks of subgroups
16.150.
Pullbacks of subsemigroups
16.151.
Quotient groups
16.152.
Quotient groups of concrete groups
16.153.
Quotients of abelian groups
16.154.
Rational commutative monoids
16.155.
Representations of monoids in precategories
16.156.
Saturated congruence relations on commutative monoids
16.157.
Saturated congruence relations on monoids
16.158.
Semigroups
16.159.
Sheargroups
16.160.
Shriek of concrete group homomorphisms
16.161.
Stabilizer groups
16.162.
Stabilizers of concrete group actions
16.163.
Subgroups
16.164.
Subgroups of abelian groups
16.165.
Subgroups of concrete groups
16.166.
Subgroups generated by elements of a group
16.167.
Subgroups generated by families of elements
16.168.
Subgroups generated by subsets of groups
16.169.
Submonoids
16.170.
Submonoids of commutative monoids
16.171.
Subsemigroups
16.172.
Subsets of abelian groups
16.173.
Subsets of commutative monoids
16.174.
Subsets of groups
16.175.
Subsets of monoids
16.176.
Subsets of semigroups
16.177.
The substitution functor of concrete group actions
16.178.
The substitution functor of group actions
16.179.
Surjective group homomorphisms
16.180.
Surjective semigroup homomorphisms
16.181.
Symmetric concrete groups
16.182.
Symmetric groups
16.183.
Torsion elements of groups
16.184.
Torsion-free groups
16.185.
Torsors of abstract groups
16.186.
Transitive concrete group actions
16.187.
Transitive group actions
16.188.
Trivial concrete groups
16.189.
Trivial group homomorphisms
16.190.
Trivial groups
16.191.
Trivial subgroups
16.192.
Unordered tuples of elements in commutative monoids
16.193.
Wild representations of monoids
17.
Higher group theory
❱
17.1.
Abelian higher groups
17.2.
Cartesian products of higher groups
17.3.
Conjugation in higher groups
17.4.
Cyclic higher groups
17.5.
Deloopable groups
17.6.
Deloopable H-spaces
17.7.
Deloopable types
17.8.
Eilenberg-Mac Lane spaces
17.9.
Equivalences of higher groups
17.10.
Fixed points of higher group actions
17.11.
Free higher group actions
17.12.
Higher group actions
17.13.
Higher groups
17.14.
Homomorphisms of higher group actions
17.15.
Homomorphisms of higher groups
17.16.
The higher group of integers
17.17.
Iterated cartesian products of higher groups
17.18.
Iterated deloopings of pointed types
17.19.
Orbits of higher group actions
17.20.
Small ∞-groups
17.21.
Subgroups of higher groups
17.22.
Symmetric higher groups
17.23.
Transitive higher group actions
17.24.
Trivial higher groups
18.
Linear algebra
❱
18.1.
Constant matrices
18.2.
Diagonal vectors
18.3.
Diagonal matrices on rings
18.4.
Functoriality of the type of matrices
18.5.
Functoriality of the type of vectors
18.6.
Matrices
18.7.
Matrices on rings
18.8.
Multiplication of matrices
18.9.
Scalar multiplication on matrices
18.10.
Scalar multiplication of vectors
18.11.
Scalar multiplication of vectors on rings
18.12.
Transposition of matrices
18.13.
Vectors
18.14.
Vectors on commutative rings
18.15.
Vectors on commutative semirings
18.16.
Vectors on euclidean domains
18.17.
Vectors on rings
18.18.
Vectors on semirings
19.
Lists
❱
19.1.
Arrays
19.2.
Concatenation of lists
19.3.
Flattening of lists
19.4.
Functoriality of the list operation
19.5.
Lists
19.6.
Lists of elements in discrete types
19.7.
Permutations of lists
19.8.
Permutations of vectors
19.9.
Predicates on lists
19.10.
Quicksort for lists
19.11.
Reversing lists
19.12.
Sort by insertion for lists
19.13.
Sort by insertion for vectors
19.14.
Sorted lists
19.15.
Sorted vectors
19.16.
Sorting algorithms for lists
19.17.
Sorting algorithms for vectors
19.18.
The universal property of lists with respect to wild monoids
20.
Metric spaces
❱
20.1.
The category of metric spaces and isometries
20.2.
The category of metric spaces and short maps
20.3.
Cauchy approximations in metric spaces
20.4.
Cauchy approximations in premetric spaces
20.5.
Closed premetric structures
20.6.
Complete metric spaces
20.7.
Convergent Cauchy approximations in metric spaces
20.8.
Dependent products of metric spaces
20.9.
Discrete premetric structures
20.10.
Equality of metric spaces
20.11.
Equality of premetric spaces
20.12.
Extensional premetric structures on types
20.13.
Functions between metric spaces
20.14.
The functor from the precategory of metric spaces and isometries to the precategory of sets
20.15.
The inclusion of isometries into the category of metric spaces and short maps
20.16.
Induced premetric structures on preimages
20.17.
Isometric equivalences between premetric spaces
20.18.
Isometries between metric spaces
20.19.
Isometries between premetric spaces
20.20.
Limits of Cauchy approximations in premetric spaces
20.21.
The metric space of cauchy approximations in a metric space
20.22.
The metric space of convergent cauchy approximations in a metric space
20.23.
The standard metric structure on the rational numbers
20.24.
The metric structure on the rational numbers with open neighborhoods
20.25.
Metric spaces
20.26.
Metric structures
20.27.
Monotonic premetric structures on types
20.28.
The poset of premetric structures on a type
20.29.
The precategory of metric spaces and functions
20.30.
The precategory of metric spaces and isometries
20.31.
The precategory of metric spaces and short functions
20.32.
Premetric spaces
20.33.
Premetric structures on types
20.34.
Pseudometric spaces
20.35.
Pseudometric structures on a type
20.36.
Reflexive premetric structures on types
20.37.
Saturated metric spaces
20.38.
Short functions between metric spaces
20.39.
Short functions between premetric spaces
20.40.
Subspaces of metric spaces
20.41.
Symmetric premetric structures on types
20.42.
Triangular premetric structures on types
21.
Modal type theory
❱
21.1.
The action on homotopies of the flat modality
21.2.
The action on identifications of crisp functions
21.3.
The action on identifications of the flat modality
21.4.
Crisp cartesian product types
21.5.
Crisp coproduct types
21.6.
Crisp dependent function types
21.7.
Crisp dependent pair types
21.8.
Crisp function types
21.9.
Crisp identity types
21.10.
The crisp law of excluded middle
21.11.
Crisp pullbacks
21.12.
Crisp types
21.13.
Dependent universal property of flat discrete crisp types
21.14.
Flat discrete crisp types
21.15.
The flat modality
21.16.
The flat-sharp adjunction
21.17.
Functoriality of the flat modality
21.18.
Functoriality of the sharp modality
21.19.
Sharp codiscrete maps
21.20.
Sharp codiscrete types
21.21.
The sharp modality
21.22.
Transport along crisp identifications
21.23.
The universal property of flat discrete crisp types
22.
Online encyclopedia of integer sequences
❱
22.1.
Sequences of the online encyclopedia of integer sequences
23.
Order theory
❱
23.1.
Accessible elements with respect to relations
23.2.
Bottom elements in posets
23.3.
Bottom elements in preorders
23.4.
Chains in posets
23.5.
Chains in preorders
23.6.
Closure operators on large locales
23.7.
Closure operators on large posets
23.8.
Commuting squares of Galois connections between large posets
23.9.
Commuting squares of order preserving maps of large posets
23.10.
Coverings in locales
23.11.
Decidable posets
23.12.
Decidable preorders
23.13.
Decidable subposets
23.14.
Decidable subpreorders
23.15.
Decidable total orders
23.16.
Decidable total preorders
23.17.
Dependent products of large frames
23.18.
Dependent products of large locales
23.19.
Dependent products of large meet-semilattices
23.20.
Dependent products of large posets
23.21.
Dependent products large preorders
23.22.
Dependent products of large suplattices
23.23.
Directed complete posets
23.24.
Directed families in posets
23.25.
Distributive lattices
23.26.
Finite coverings in locales
23.27.
Finite posets
23.28.
Finite preorders
23.29.
Finite total orders
23.30.
Finitely graded posets
23.31.
Frames
23.32.
Galois connections
23.33.
Galois connections between large posets
23.34.
Greatest lower bounds in large posets
23.35.
Greatest lower bounds in posets
23.36.
Homomorphisms of frames
23.37.
Homomorphisms of large frames
23.38.
Homomorphisms of large locales
23.39.
Homomorphisms of large meet-semilattices
23.40.
Homomorphisms of large suplattices
23.41.
Homomorphisms of meet-semilattices
23.42.
Homomorphisms of meet sup lattices
23.43.
Homomorphisms of suplattices
23.44.
Ideals in preorders
23.45.
Inhabited finite total orders
23.46.
Interval subposets
23.47.
Join-semilattices
23.48.
Large frames
23.49.
Large locales
23.50.
Large meet-semilattices
23.51.
Large meet-subsemilattices
23.52.
Large posets
23.53.
Large preorders
23.54.
Large quotient locales
23.55.
Large subframes
23.56.
Large subposets
23.57.
Large subpreorders
23.58.
Large subsuplattices
23.59.
Large suplattices
23.60.
Lattices
23.61.
Least upper bounds in large posets
23.62.
Least upper bounds in posets
23.63.
Locales
23.64.
Locally finite posets
23.65.
Lower bounds in large posets
23.66.
Lower bounds in posets
23.67.
Lower sets in large posets
23.68.
Lower types in preorders
23.69.
Maximal chains in posets
23.70.
Maximal chains in preorders
23.71.
Meet-semilattices
23.72.
Meet-suplattices
23.73.
Nuclei on large locales
23.74.
Order preserving maps between large posets
23.75.
Order preserving maps between large preorders
23.76.
Order preserving maps on posets
23.77.
Order preserving maps on preorders
23.78.
Ordinals
23.79.
Posets
23.80.
Powers of large locales
23.81.
The precategory of decidable total orders
23.82.
The precategory of finite posets
23.83.
The precategory of finite total orders
23.84.
The precategory of inhabited finite total orders
23.85.
The precategory of posets
23.86.
The precategory of total orders
23.87.
Preorders
23.88.
Principal lower sets of large posets
23.89.
Principal upper sets of large posets
23.90.
Reflective Galois connections between large posets
23.91.
Similarity of elements in large posets
23.92.
Similarity of elements in large preorders
23.93.
Similarity of order preserving maps between large posets
23.94.
Similarity of order preserving maps between large preorders
23.95.
Subposets
23.96.
Subpreorders
23.97.
Suplattices
23.98.
Top elements in large posets
23.99.
Top elements in posets
23.100.
Top elements in preorders
23.101.
Total orders
23.102.
Total preorders
23.103.
Upper bounds of chains in posets
23.104.
Upper bounds in large posets
23.105.
Upper bounds in posets
23.106.
Upper sets of large posets
23.107.
Well-founded orders
23.108.
Well-founded relations
23.109.
Zorn's lemma
24.
Organic chemistry
❱
24.1.
Alcohols
24.2.
Alkanes
24.3.
Alkenes
24.4.
Alkynes
24.5.
Ethane
24.6.
Hydrocarbons
24.7.
Methane
24.8.
Saturated carbons
25.
Orthogonal factorization systems
❱
25.1.
Cd-structures
25.2.
Cellular maps
25.3.
The closed modalities
25.4.
Double lifts of families of elements
25.5.
Double negation sheaves
25.6.
Extensions of double lifts of families of elements
25.7.
Extensions of families of elements
25.8.
Extensions of maps
25.9.
Factorization operations
25.10.
Factorization operations into function classes
25.11.
Factorization operations into global function classes
25.12.
Factorizations of maps
25.13.
Factorizations of maps into function classes
25.14.
Factorizations of maps into global function classes
25.15.
Fiberwise orthogonal maps
25.16.
Function classes
25.17.
Functoriality of higher modalities
25.18.
Functoriality of the pullback-hom
25.19.
Global function classes
25.20.
Higher modalities
25.21.
The identity modality
25.22.
Lifting operations
25.23.
Lifting structures on commuting squares of maps
25.24.
Lifts of families of elements
25.25.
Lifts of maps
25.26.
Local families of types
25.27.
Local maps
25.28.
Local types
25.29.
Localizations at maps
25.30.
Localizations at subuniverses
25.31.
Locally small modal-operators
25.32.
Mere lifting properties
25.33.
Modal induction
25.34.
Modal operators
25.35.
Modal subuniverse induction
25.36.
Null families of types
25.37.
Null maps
25.38.
Null types
25.39.
The open modalities
25.40.
Orthogonal factorization systems
25.41.
Orthogonal maps
25.42.
Precomposition of lifts of families of elements by maps
25.43.
The pullback-hom
25.44.
The raise modalities
25.45.
Reflective modalities
25.46.
Reflective subuniverses
25.47.
Regular cd-structures
25.48.
Separated types
25.49.
Σ-closed modalities
25.50.
Σ-closed reflective modalities
25.51.
Σ-closed reflective subuniverses
25.52.
Stable orthogonal factorization systems
25.53.
Types colocal at maps
25.54.
Uniquely eliminating modalities
25.55.
Wide function classes
25.56.
Wide global function classes
25.57.
The zero modality
26.
Polytopes
❱
26.1.
Abstract polytopes
27.
Primitives
❱
27.1.
Characters
27.2.
Floats
27.3.
Machine integers
27.4.
Strings
28.
Real numbers
❱
28.1.
Dedekind real numbers
28.2.
The metric space of real numbers
28.3.
Rational real numbers
29.
Reflection
❱
29.1.
Abstractions
29.2.
Arguments
29.3.
Boolean reflection
29.4.
Definitions
29.5.
Erasing equality
29.6.
Fixity
29.7.
Group solver
29.8.
Literals
29.9.
Metavariables
29.10.
Names
29.11.
Precategory solver
29.12.
Rewriting
29.13.
Terms
29.14.
The type checking monad
30.
Ring theory
❱
30.1.
Additive orders of elements of rings
30.2.
Algebras over rings
30.3.
The binomial theorem for rings
30.4.
The binomial theorem for semirings
30.5.
The category of cyclic rings
30.6.
The category of rings
30.7.
Central elements of rings
30.8.
Central elements of semirings
30.9.
Characteristics of rings
30.10.
Commuting elements of rings
30.11.
Congruence relations on rings
30.12.
Congruence relations on semirings
30.13.
Cyclic rings
30.14.
Dependent products of rings
30.15.
Dependent products of semirings
30.16.
Division rings
30.17.
The free ring with one generator
30.18.
Full ideals of rings
30.19.
Function rings
30.20.
Function semirings
30.21.
Generating elements of rings
30.22.
The group of multiplicative units of a ring
30.23.
Homomorphisms of cyclic rings
30.24.
Homomorphisms of rings
30.25.
Homomorphisms of semirings
30.26.
Ideals generated by subsets of rings
30.27.
Ideals of rings
30.28.
Ideals of semirings
30.29.
Idempotent elements in rings
30.30.
Initial rings
30.31.
Integer multiples of elements of rings
30.32.
Intersections of ideals of rings
30.33.
Intersections of ideals of semirings
30.34.
The invariant basis property of rings
30.35.
Invertible elements in rings
30.36.
Isomorphisms of rings
30.37.
Joins of ideals of rings
30.38.
Joins of left ideals of rings
30.39.
Joins of right ideals of rings
30.40.
Kernels of ring homomorphisms
30.41.
Left ideals generated by subsets of rings
30.42.
Left ideals of rings
30.43.
Local rings
30.44.
Localizations of rings
30.45.
Maximal ideals of rings
30.46.
Modules over rings
30.47.
Multiples of elements in rings
30.48.
Multiplicative orders of elements of rings
30.49.
Nil ideals of rings
30.50.
Nilpotent elements in rings
30.51.
Nilpotent elements in semirings
30.52.
Opposite rings
30.53.
The poset of cyclic rings
30.54.
The poset of ideals of a ring
30.55.
The poset of left ideals of a ring
30.56.
The poset of right ideals of a ring
30.57.
Powers of elements in rings
30.58.
Powers of elements in semirings
30.59.
The precategory of rings
30.60.
The precategory of semirings
30.61.
Products of ideals of rings
30.62.
Products of left ideals of rings
30.63.
Products of right ideals of rings
30.64.
Products of rings
30.65.
Products of subsets of rings
30.66.
Quotient rings
30.67.
Radical ideals of rings
30.68.
Right ideals generated by subsets of rings
30.69.
Right ideals of rings
30.70.
Rings
30.71.
Semirings
30.72.
Subsets of rings
30.73.
Subsets of semirings
30.74.
Sums of elements in rings
30.75.
Sums of elements in semirings
30.76.
Transporting ring structures along isomorphisms of abelian groups
30.77.
Trivial rings
31.
Set theory
❱
31.1.
Baire space
31.2.
Cantor space
31.3.
Cantor's diagonal argument
31.4.
Cardinalities of sets
31.5.
Countable sets
31.6.
Cumulative hierarchy
31.7.
Infinite sets
31.8.
Russell's paradox
31.9.
Uncountable sets
32.
Species
❱
32.1.
Cartesian exponents of species
32.2.
Cartesian products of species of types
32.3.
Cauchy composition of species of types
32.4.
Cauchy composition of species of types in a subuniverse
32.5.
Cauchy exponentials of species of types
32.6.
Cauchy exponentials of species of types in a subuniverse
32.7.
Cauchy products of species of types
32.8.
Cauchy products of species of types in a subuniverse
32.9.
Cauchy series of species of types
32.10.
Cauchy series of species of types in a subuniverse
32.11.
Composition of Cauchy series of species of types
32.12.
Composition of Cauchy series of species of types in subuniverses
32.13.
Coproducts of species of types
32.14.
Coproducts of species of types in subuniverses
32.15.
Cycle index series of species
32.16.
Derivatives of species
32.17.
Dirichlet exponentials of a species of types
32.18.
Dirichlet exponentials of species of types in a subuniverse
32.19.
Dirichlet products of species of types
32.20.
Dirichlet products of species of types in subuniverses
32.21.
Dirichlet series of species of finite inhabited types
32.22.
Dirichlet series of species of types
32.23.
Dirichlet series of species of types in subuniverses
32.24.
Equivalences of species of types
32.25.
Equivalences of species of types in subuniverses
32.26.
Exponential of Cauchy series of species of types
32.27.
Exponential of Cauchy series of species of types in subuniverses
32.28.
Hasse-Weil species
32.29.
Morphisms of finite species
32.30.
Morphisms of species of types
32.31.
Pointing of species of types
32.32.
The precategory of finite species
32.33.
Products of Cauchy series of species of types
32.34.
Products of Cauchy series of species of types in subuniverses
32.35.
Products of Dirichlet series of species of finite inhabited types
32.36.
Products of Dirichlet series of species of types
32.37.
Products of Dirichlet series of species of types in subuniverses
32.38.
Small Composition of species of finite inhabited types
32.39.
Small Cauchy composition of species types in subuniverses
32.40.
Species of finite inhabited types
32.41.
Species of finite types
32.42.
Species of inhabited types
32.43.
Species of types
32.44.
Species of types in subuniverses
32.45.
The unit of Cauchy composition of types
32.46.
The unit of Cauchy composition of species of types in subuniverses
32.47.
Unlabeled structures of finite species
33.
Structured types
❱
33.1.
Cartesian products of types equipped with endomorphisms
33.2.
Central H-spaces
33.3.
Commuting squares of pointed homotopies
33.4.
Commuting squares of pointed maps
33.5.
Commuting triangles of pointed maps
33.6.
Conjugation of pointed types
33.7.
Constant pointed maps
33.8.
Contractible pointed types
33.9.
Cyclic types
33.10.
Dependent globular types
33.11.
Dependent products of H-spaces
33.12.
Dependent products of pointed types
33.13.
Dependent products of wild monoids
33.14.
Dependent reflexive globular types
33.15.
Dependent types equipped with automorphisms
33.16.
Equality of globular types
33.17.
Equivalences between globular types
33.18.
Equivalences of H-spaces
33.19.
Equivalences of pointed arrows
33.20.
Equivalences of types equipped with automorphisms
33.21.
Equivalences of types equipped with endomorphisms
33.22.
Faithful pointed maps
33.23.
Fibers of pointed maps
33.24.
Finite multiplication in magmas
33.25.
Function H-spaces
33.26.
Function magmas
33.27.
Function wild monoids
33.28.
Globular types
33.29.
H-spaces
33.30.
The initial pointed type equipped with an automorphism
33.31.
The involutive type of H-space structures on a pointed type
33.32.
Involutive types
33.33.
Iterated cartesian products of types equipped with endomorphisms
33.34.
Iterated cartesian products of pointed types
33.35.
Large globular types
33.36.
Large reflexive globular types
33.37.
Large symmetric globular types
33.38.
Large transitive globular types
33.39.
Magmas
33.40.
Maps between globular types
33.41.
Maps between large globular types
33.42.
Mere equivalences of types equipped with endomorphisms
33.43.
Morphisms of H-spaces
33.44.
Morphisms of magmas
33.45.
Morphisms of pointed arrows
33.46.
Morphisms of twisted pointed arrows
33.47.
Morphisms of types equipped with automorphisms
33.48.
Morphisms of types equipped with endomorphisms
33.49.
Morphisms of wild monoids
33.50.
Noncoherent H-spaces
33.51.
Opposite pointed spans
33.52.
Pointed 2-homotopies
33.53.
Pointed cartesian product types
33.54.
Pointed dependent functions
33.55.
Pointed dependent pair types
33.56.
Pointed equivalences
33.57.
Pointed families of types
33.58.
Pointed homotopies
33.59.
Pointed isomorphisms
33.60.
Pointed maps
33.61.
Pointed retractions of pointed maps
33.62.
Pointed sections of pointed maps
33.63.
Pointed span diagrams
33.64.
Pointed spans
33.65.
Pointed types
33.66.
Pointed types equipped with automorphisms
33.67.
The pointed unit type
33.68.
Universal property of contractible types with respect to pointed types and maps
33.69.
Postcomposition of pointed maps
33.70.
Precomposition of pointed maps
33.71.
Reflexive globular types
33.72.
Sets equipped with automorphisms
33.73.
Small pointed types
33.74.
Symmetric elements of involutive types
33.75.
Symmetric globular types
33.76.
Symmetric H-spaces
33.77.
Transitive globular types
33.78.
Transposition of pointed span diagrams
33.79.
Types equipped with automorphisms
33.80.
Types equipped with endomorphisms
33.81.
Uniform pointed homotopies
33.82.
The universal property of pointed equivalences
33.83.
Unpointed maps between pointed types
33.84.
Whiskering pointed homotopies with respect to concatenation
33.85.
Whiskering of pointed homotopies with respect to composition of pointed maps
33.86.
The wild category of pointed types
33.87.
Wild groups
33.88.
Wild loops
33.89.
Wild monoids
33.90.
Wild quasigroups
33.91.
Wild semigroups
34.
Synthetic category theory
❱
34.1.
Cone diagrams of synthetic categories
34.2.
Cospans of synthetic categories
34.3.
Equivalences between synthetic categories
34.4.
Invertible functors between synthetic categories
34.5.
Pullbacks of synthetic categories
34.6.
Retractions of functors between synthetic categories
34.7.
Sections of functor between synthetic categories
34.8.
Synthetic categories
35.
Synthetic homotopy theory
❱
35.1.
0-acyclic maps
35.2.
0-acyclic types
35.3.
1-acyclic types
35.4.
Acyclic maps
35.5.
Acyclic types
35.6.
The category of connected set bundles over the circle
35.7.
Cavallo's trick
35.8.
The circle
35.9.
Cocartesian morphisms of arrows
35.10.
Cocones under pointed span diagrams
35.11.
Cocones under sequential diagrams
35.12.
Cocones under spans
35.13.
Codiagonals of maps
35.14.
Coequalizers
35.15.
Cofibers
35.16.
Coforks
35.17.
Correspondence between cocones under sequential diagrams and certain coforks
35.18.
Conjugation of loops
35.19.
Connected set bundles over the circle
35.20.
Connective prespectra
35.21.
Connective spectra
35.22.
Dependent cocones under sequential diagrams
35.23.
Dependent cocones under spans
35.24.
Dependent coforks
35.25.
Dependent descent for the circle
35.26.
The dependent pullback property of pushouts
35.27.
Dependent pushout-products
35.28.
Dependent sequential diagrams
35.29.
Dependent suspension structures
35.30.
The dependent universal property of coequalizers
35.31.
The dependent universal property of pushouts
35.32.
The dependent universal property of sequential colimits
35.33.
Dependent universal property of suspensions
35.34.
The descent property of the circle
35.35.
Descent data for constant type families over the circle
35.36.
Descent data for families of dependent pair types over the circle
35.37.
Descent data for families of equivalence types over the circle
35.38.
Descent data for families of function types over the circle
35.39.
Subtypes of descent data for the circle
35.40.
Descent data for type families of equivalence types over pushouts
35.41.
Descent data for type families of function types over pushouts
35.42.
Descent data for type families of identity types over pushouts
35.43.
Descent data for pushouts
35.44.
Descent data for sequential colimits
35.45.
Descent property of pushouts
35.46.
Descent property of sequential colimits
35.47.
Double loop spaces
35.48.
The Eckmann-Hilton argument
35.49.
Equifibered sequential diagrams
35.50.
Equivalences of cocones under sequential diagrams
35.51.
Equivalences of coforks
35.52.
Equivalances of dependent sequential diagrams
35.53.
Equivalences of descent data for pushouts
35.54.
Equivalences of sequential diagrams
35.55.
Families with descent data for pushouts
35.56.
Families with descent data for sequential colimits
35.57.
The flattening lemma for coequalizers
35.58.
The flattening lemma for pushouts
35.59.
The flattening lemma for sequential colimits
35.60.
Free loops
35.61.
Functoriality of the loop space operation
35.62.
Functoriality of sequential colimits
35.63.
Functoriality of suspensions
35.64.
Groups of loops in 1-types
35.65.
Hatcher's acyclic type
35.66.
Identity systems of descent data for pushouts
35.67.
The induction principle of pushouts
35.68.
The infinite complex projective space
35.69.
Infinite cyclic types
35.70.
The interval
35.71.
Iterated loop spaces
35.72.
Iterated suspensions of pointed types
35.73.
Join powers of types
35.74.
Joins of maps
35.75.
Joins of types
35.76.
The loop homotopy on the circle
35.77.
Loop spaces
35.78.
Maps of prespectra
35.79.
Mere spheres
35.80.
Morphisms of cocones under morphisms of sequential diagrams
35.81.
Morphisms of coforks
35.82.
Morphisms of dependent sequential diagrams
35.83.
Morphisms of descent data of the circle
35.84.
Morphisms of descent data for pushouts
35.85.
Morphisms of sequential diagrams
35.86.
The multiplication operation on the circle
35.87.
Null cocones under pointed span diagrams
35.88.
The plus-principle
35.89.
Powers of loops
35.90.
Premanifolds
35.91.
Prespectra
35.92.
The pullback property of pushouts
35.93.
Pushout-products
35.94.
Pushouts
35.95.
Pushouts of pointed types
35.96.
The recursion principle of pushouts
35.97.
Retracts of sequential diagrams
35.98.
Rewriting rules for pushouts
35.99.
Sections of families over the circle
35.100.
Sections of descent data for pushouts
35.101.
Sequential colimits
35.102.
Sequential diagrams
35.103.
Sequentially compact types
35.104.
Shifts of sequential diagrams
35.105.
Smash products of pointed types
35.106.
Spectra
35.107.
The sphere prespectrum
35.108.
Spheres
35.109.
Suspension prespectra
35.110.
Suspension Structures
35.111.
Suspensions of pointed types
35.112.
Suspensions of types
35.113.
Tangent spheres
35.114.
Total cocones of type families over cocones under sequential diagrams
35.115.
Total sequential diagrams of dependent sequential diagrams
35.116.
Triple loop spaces
35.117.
k-acyclic maps
35.118.
k-acyclic types
35.119.
The universal cover of the circle
35.120.
The universal property of the circle
35.121.
The universal property of coequalizers
35.122.
The universal property of pushouts
35.123.
The universal property of sequential colimits
35.124.
Universal property of suspensions
35.125.
Universal Property of suspensions of pointed types
35.126.
Wedges of pointed types
35.127.
Zigzags between sequential diagrams
36.
Trees
❱
36.1.
Algebras for polynomial endofunctors
36.2.
Bases of directed trees
36.3.
Bases of enriched directed trees
36.4.
Binary W-types
36.5.
Bounded multisets
36.6.
The coalgebra of directed trees
36.7.
The coalgebra of enriched directed trees
36.8.
Coalgebras of polynomial endofunctors
36.9.
The combinator of directed trees
36.10.
Combinators of enriched directed trees
36.11.
Directed trees
36.12.
The elementhood relation on coalgebras of polynomial endofunctors
36.13.
The elementhood relation on W-types
36.14.
Empty multisets
36.15.
Enriched directed trees
36.16.
Equivalences of directed trees
36.17.
Equivalences of enriched directed trees
36.18.
Extensional W-types
36.19.
Fibers of directed trees
36.20.
Fibers of enriched directed trees
36.21.
Full binary trees
36.22.
Functoriality of the combinator of directed trees
36.23.
Functoriality of the fiber operation on directed trees
36.24.
Functoriality of W-types
36.25.
Hereditary W-types
36.26.
Indexed W-types
36.27.
Induction principles on W-types
36.28.
Inequality on W-types
36.29.
Lower types of elements in W-types
36.30.
Morphisms of algebras of polynomial endofunctors
36.31.
Morphisms of coalgebras of polynomial endofunctors
36.32.
Morphisms of directed trees
36.33.
Morphisms of enriched directed trees
36.34.
Multiset-indexed dependent products of types
36.35.
Multisets
36.36.
Planar binary trees
36.37.
Plane trees
36.38.
Polynomial endofunctors
36.39.
Raising universe levels of directed trees
36.40.
Ranks of elements in W-types
36.41.
Rooted morphisms of directed trees
36.42.
Rooted morphisms of enriched directed trees
36.43.
Rooted quasitrees
36.44.
Rooted undirected trees
36.45.
Small multisets
36.46.
Submultisets
36.47.
Transitive multisets
36.48.
The underlying trees of elements of coalgebras of polynomial endofunctors
36.49.
The underlying trees of elements of W-types
36.50.
Undirected trees
36.51.
The universal multiset
36.52.
The universal tree
36.53.
The W-type of natural numbers
36.54.
The W-type of the type of propositions
36.55.
W-types
37.
Type theories
❱
37.1.
Comprehension of fibered type theories
37.2.
Dependent type theories
37.3.
Fibered dependent type theories
37.4.
Π-types in precategories with attributes
37.5.
Π-types in precategories with families
37.6.
Precategories with attributes
37.7.
Precategories with families
37.8.
Sections of dependent type theories
37.9.
Simple type theories
37.10.
Unityped type theories
38.
Univalent combinatorics
❱
38.1.
2-element decidable subtypes
38.2.
2-element subtypes
38.3.
2-element types
38.4.
The binomial types
38.5.
Bracelets
38.6.
Cartesian products of finite types
38.7.
The classical definition of the standard finite types
38.8.
Complements of isolated elements of finite types
38.9.
Coproducts of finite types
38.10.
Counting in type theory
38.11.
Counting the elements of decidable subtypes
38.12.
Counting the elements of dependent pair types
38.13.
Counting the elements of the fiber of a map
38.14.
Counting the elements in Maybe
38.15.
Cubes
38.16.
Cycle partitions of finite types
38.17.
Cycle prime decompositions of natural numbers
38.18.
Cyclic finite types
38.19.
Decidable dependent function types
38.20.
Decidability of dependent pair types
38.21.
Decidable equivalence relations on finite types
38.22.
Decidable propositions
38.23.
Decidable subtypes of finite types
38.24.
Dedekind finite sets
38.25.
Counting the elements of dependent function types
38.26.
Dependent pair types of finite types
38.27.
Finite discrete Σ-decompositions
38.28.
Distributivity of set truncation over finite products
38.29.
Double counting
38.30.
Embeddings
38.31.
Embeddings between standard finite types
38.32.
Equality in finite types
38.33.
Equality in the standard finite types
38.34.
Equivalences between finite types
38.35.
Equivalences of cubes
38.36.
Equivalences between standard finite types
38.37.
Ferrers diagrams (unlabeled partitions)
38.38.
Fibers of maps between finite types
38.39.
Finite choice
38.40.
Finite presentations of types
38.41.
Finite types
38.42.
Finiteness of the type of connected components
38.43.
Finitely presented types
38.44.
Finite function types
38.45.
The image of a map
38.46.
Inequality on types equipped with a counting
38.47.
Inhabited finite types
38.48.
Injective maps between finite types
38.49.
An involution on the standard finite types
38.50.
Isotopies of Latin squares
38.51.
Kuratowski finite sets
38.52.
Latin squares
38.53.
Locally finite types
38.54.
The groupoid of main classes of Latin hypercubes
38.55.
The groupoid of main classes of Latin squares
38.56.
The maybe monad on finite types
38.57.
Necklaces
38.58.
Orientations of the complete undirected graph
38.59.
Orientations of cubes
38.60.
Partitions of finite types
38.61.
Petri-nets
38.62.
π-finite types
38.63.
The pigeonhole principle
38.64.
Finitely π-presented types
38.65.
Quotients of finite types
38.66.
Ramsey theory
38.67.
Repetitions of values
38.68.
Repetitions of values in sequences
38.69.
Retracts of finite types
38.70.
Sequences of elements in finite types
38.71.
Set quotients of index 2
38.72.
Finite Σ-decompositions of finite types
38.73.
Skipping elements in standard finite types
38.74.
Small types
38.75.
Standard finite pruned trees
38.76.
Standard finite trees
38.77.
The standard finite types
38.78.
Steiner systems
38.79.
Steiner triple systems
38.80.
Combinatorial identities of sums of natural numbers
38.81.
Surjective maps between finite types
38.82.
Symmetric difference of finite subtypes
38.83.
Finite trivial Σ-decompositions
38.84.
Type duality of finite types
38.85.
Unions of finite subtypes
38.86.
The universal property of the standard finite types
38.87.
Unlabeled partitions
38.88.
Unlabeled rooted trees
38.89.
Unlabeled trees
39.
Universal algebra
❱
39.1.
Abstract equations over signatures
39.2.
Algebraic theories
39.3.
Algebraic theory of groups
39.4.
Algebras
39.5.
Congruences
39.6.
Homomorphisms of algebras
39.7.
Kernels of homomorphisms of algebras
39.8.
Models of signatures
39.9.
Quotient algebras
39.10.
Signatures
39.11.
Terms over signatures
40.
Wild category theory
❱
40.1.
Colax functors between large noncoherent wild higher precategories
40.2.
Colax functors between noncoherent wild higher precategories
40.3.
Isomorphisms in noncoherent large wild higher precategories
40.4.
Isomorphisms in noncoherent wild higher precategories
40.5.
Maps between noncoherent large wild higher precategories
40.6.
Maps between noncoherent wild higher precategories
40.7.
Noncoherent large wild higher precategories
40.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