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 contents
5.
Art
6.
Formalization of results from the literature
❱
6.1.
Sequential Colimits in Homotopy Type Theory
The agda-unimath library
7.
Category theory
❱
7.1.
Adjunctions between large categories
7.2.
Adjunctions between large precategories
7.3.
Anafunctors between categories
7.4.
Anafunctors between precategories
7.5.
The augmented simplex category
7.6.
Categories
7.7.
The category of functors and natural transformations between two categories
7.8.
The category of functors and natural transformations from small to large categories
7.9.
The category of maps and natural transformations between two categories
7.10.
The category of maps and natural transformations from small to large categories
7.11.
Commuting squares of morphisms in large precategories
7.12.
Commuting squares of morphisms in precategories
7.13.
Commuting squares of morphisms in set-magmoids
7.14.
Composition operations on binary families of sets
7.15.
Conservative functors between precategories
7.16.
Constant functors
7.17.
Copresheaf categories
7.18.
Coproducts in precategories
7.19.
Cores of categories
7.20.
Cores of precategories
7.21.
Dependent products of categories
7.22.
Dependent products of large categories
7.23.
Dependent products of large precategories
7.24.
Dependent products of precategories
7.25.
Discrete categories
7.26.
Embedding maps between precategories
7.27.
Embeddings between precategories
7.28.
Endomorphisms in categories
7.29.
Endomorphisms in precategories
7.30.
Epimorphism in large precategories
7.31.
Equivalences between categories
7.32.
Equivalences between large precategories
7.33.
Equivalences between precategories
7.34.
Essential fibers of functors between precategories
7.35.
Essentially injective functors between precategories
7.36.
Essentially surjective functors between precategories
7.37.
Exponential objects in precategories
7.38.
Faithful functors between precategories
7.39.
Faithful maps between precategories
7.40.
Full functors between precategories
7.41.
Full large subcategories
7.42.
Full large subprecategories
7.43.
Full maps between precategories
7.44.
Full subcategories
7.45.
Full subprecategories
7.46.
Fully faithful functors between precategories
7.47.
Fully faithful maps between precategories
7.48.
Function categories
7.49.
Function precategories
7.50.
Functors between categories
7.51.
Functors from small to large categories
7.52.
Functors from small to large precategories
7.53.
Functors between large categories
7.54.
Functors between large precategories
7.55.
Functors between nonunital precategories
7.56.
Functors between precategories
7.57.
Functors between set-magmoids
7.58.
Gaunt categories
7.59.
Groupoids
7.60.
Homotopies of natural transformations in large precategories
7.61.
Indiscrete precategories
7.62.
The initial category
7.63.
Initial objects of large categories
7.64.
Initial objects of large precategories
7.65.
Initial objects in a precategory
7.66.
Isomorphism induction in categories
7.67.
Isomorphism induction in precategories
7.68.
Isomorphisms in categories
7.69.
Isomorphisms in large categories
7.70.
Isomorphisms in large precategories
7.71.
Isomorphisms in precategories
7.72.
Isomorphisms in subprecategories
7.73.
Large categories
7.74.
Large function categories
7.75.
Large function precategories
7.76.
Large precategories
7.77.
Large subcategories
7.78.
Large subprecategories
7.79.
Maps between categories
7.80.
Maps from small to large categories
7.81.
Maps from small to large precategories
7.82.
Maps between precategories
7.83.
Maps between set-magmoids
7.84.
Monads on categories
7.85.
Monads on precategories
7.86.
Monomorphisms in large precategories
7.87.
Natural isomorphisms between functors between categories
7.88.
Natural isomorphisms between functors between large precategories
7.89.
Natural isomorphisms between functors between precategories
7.90.
Natural isomorphisms between maps between categories
7.91.
Natural isomorphisms between maps between precategories
7.92.
Natural numbers object in a precategory
7.93.
Natural transformations between functors between categories
7.94.
Natural transformations between functors from small to large categories
7.95.
Natural transformations between functors from small to large precategories
7.96.
Natural transformations between functors between large categories
7.97.
Natural transformations between functors between large precategories
7.98.
Natural transformations between functors between precategories
7.99.
Natural transformations between maps between categories
7.100.
Natural transformations between maps from small to large precategories
7.101.
Natural transformations between maps between precategories
7.102.
Nonunital precategories
7.103.
One object precategories
7.104.
Opposite categories
7.105.
Opposite large precategories
7.106.
Opposite precategories
7.107.
Opposite preunivalent categories
7.108.
Pointed endofunctors on categories
7.109.
Pointed endofunctors
7.110.
Precategories
7.111.
Precategory of elements of a presheaf
7.112.
The precategory of functors and natural transformations between two precategories
7.113.
The precategory of functors and natural transformations from small to large precategories
7.114.
The precategory of maps and natural transformations from a small to a large precategory
7.115.
The precategory of maps and natural transformations between two precategories
7.116.
Pregroupoids
7.117.
Presheaf categories
7.118.
Preunivalent categories
7.119.
Products in precategories
7.120.
Products of precategories
7.121.
Pseudomonic functors between precategories
7.122.
Pullbacks in precategories
7.123.
Replete subprecategories
7.124.
Representable functors between categories
7.125.
Representable functors between large precategories
7.126.
Representable functors between precategories
7.127.
The representing arrow category
7.128.
Restrictions of functors to cores of precategories
7.129.
Rigid objects in a category
7.130.
Rigid objects in a precategory
7.131.
Set-magmoids
7.132.
Sieves in categories
7.133.
The simplex category
7.134.
Slice precategories
7.135.
Split essentially surjective functors between precategories
7.136.
Strict categories
7.137.
Structure equivalences between set-magmoids
7.138.
Subcategories
7.139.
Subprecategories
7.140.
Subterminal precategories
7.141.
The terminal category
7.142.
Terminal objects in a precategory
7.143.
Wide subcategories
7.144.
Wide subprecategories
7.145.
The Yoneda lemma for categories
7.146.
The Yoneda lemma for precategories
8.
Commutative algebra
❱
8.1.
The binomial theorem in commutative rings
8.2.
The binomial theorem in commutative semirings
8.3.
Boolean rings
8.4.
The category of commutative rings
8.5.
Commutative rings
8.6.
Commutative semirings
8.7.
Dependent products of commutative rings
8.8.
Dependent products of commutative semirings
8.9.
Discrete fields
8.10.
The Eisenstein integers
8.11.
Euclidean domains
8.12.
Full ideals of commutative rings
8.13.
Function commutative rings
8.14.
Function commutative semirings
8.15.
The Gaussian integers
8.16.
The group of multiplicative units of a commutative ring
8.17.
Homomorphisms of commutative rings
8.18.
Homomorphisms of commutative semirings
8.19.
Ideals of commutative rings
8.20.
Ideals of commutative semirings
8.21.
Ideals generated by subsets of commutative rings
8.22.
Integer multiples of elements of commutative rings
8.23.
Integral domains
8.24.
Intersections of ideals of commutative rings
8.25.
Intersections of radical ideals of commutative rings
8.26.
Invertible elements in commutative rings
8.27.
Isomorphisms of commutative rings
8.28.
Joins of ideals of commutative rings
8.29.
Joins of radical ideals of commutative rings
8.30.
Local commutative rings
8.31.
Maximal ideals of commutative rings
8.32.
Multiples of elements in commutative rings
8.33.
Nilradical of a commutative ring
8.34.
The nilradical of a commutative semiring
8.35.
The poset of ideals of a commutative ring
8.36.
The poset of radical ideals of a commutative ring
8.37.
Powers of elements in commutative rings
8.38.
Powers of elements in commutative semirings
8.39.
The precategory of commutative rings
8.40.
The precategory of commutative semirings
8.41.
Prime ideals of commutative rings
8.42.
Products of commutative rings
8.43.
Products of ideals of commutative rings
8.44.
Products of radical ideals of a commutative ring
8.45.
Products of subsets of commutative rings
8.46.
Radical ideals of commutative rings
8.47.
Radical ideals generated by subsets of commutative rings
8.48.
Radicals of ideals of commutative rings
8.49.
Subsets of commutative rings
8.50.
Subsets of commutative semirings
8.51.
Sums in commutative rings
8.52.
Sums in commutative semirings
8.53.
Transporting commutative ring structures along isomorphisms of abelian groups
8.54.
Trivial commutative rings
8.55.
The Zariski locale
8.56.
The Zariski topology on the set of prime ideals of a commutative ring
9.
Elementary number theory
❱
9.1.
The absolute value function on the integers
9.2.
The Ackermann function
9.3.
Addition on integer fractions
9.4.
Addition on the integers
9.5.
Addition on the natural numbers
9.6.
Addition of positive, negative, nonnegative and nonpositive integers
9.7.
Addition on the rational numbers
9.8.
The additive group of rational numbers
9.9.
Arithmetic functions
9.10.
The based induction principle of the natural numbers
9.11.
Based strong induction for the natural numbers
9.12.
Bezout's lemma in the integers
9.13.
Bezout's lemma on the natural numbers
9.14.
The binomial coefficients
9.15.
The binomial theorem for the integers
9.16.
The binomial theorem for the natural numbers
9.17.
Bounded sums of arithmetic functions
9.18.
Catalan numbers
9.19.
The cofibonacci sequence
9.20.
The Collatz bijection
9.21.
The Collatz conjecture
9.22.
The commutative semiring of natural numbers
9.23.
The congruence relations on the integers
9.24.
The congruence relations on the natural numbers
9.25.
The cross-multiplication difference of two integer fractions
9.26.
Cubes of natural numbers
9.27.
Decidable dependent function types
9.28.
The decidable total order of integers
9.29.
The decidable total order of natural numbers
9.30.
The decidable total order of rational numbers
9.31.
The decidable total order of a standard finite type
9.32.
Decidable types in elementary number theory
9.33.
The difference between integers
9.34.
The difference between rational numbers
9.35.
Dirichlet convolution
9.36.
The distance between integers
9.37.
The distance between natural numbers
9.38.
Divisibility of integers
9.39.
Divisibility in modular arithmetic
9.40.
Divisibility of natural numbers
9.41.
The divisibility relation on the standard finite types
9.42.
Equality of integers
9.43.
Equality of natural numbers
9.44.
Euclidean division on the natural numbers
9.45.
Euler's totient function
9.46.
Exponentiation of natural numbers
9.47.
Factorials of natural numbers
9.48.
Falling factorials
9.49.
The Fibonacci sequence
9.50.
The field of rational numbers
9.51.
The natural numbers base k
9.52.
Finitely cyclic maps
9.53.
The fundamental theorem of arithmetic
9.54.
The Goldbach conjecture
9.55.
The greatest common divisor of integers
9.56.
The greatest common divisor of natural numbers
9.57.
The group of integers
9.58.
The half-integers
9.59.
The Hardy-Ramanujan number
9.60.
Inequality on integer fractions
9.61.
Inequality on the integers
9.62.
Inequality of natural numbers
9.63.
Inequality on the rational numbers
9.64.
Inequality on the standard finite types
9.65.
The infinitude of primes
9.66.
Initial segments of the natural numbers
9.67.
Integer fractions
9.68.
Integer partitions
9.69.
The integers
9.70.
The Jacobi symbol
9.71.
The Kolakoski sequence
9.72.
The Legendre symbol
9.73.
Lower bounds of type families over the natural numbers
9.74.
Maximum on the natural numbers
9.75.
Maximum on the standard finite types
9.76.
The mediant fraction of two integer fractions
9.77.
Mersenne primes
9.78.
Minimum on the natural numbers
9.79.
Minimum on the standard finite types
9.80.
Modular arithmetic
9.81.
Modular arithmetic on the standard finite types
9.82.
The monoid of natural numbers with addition
9.83.
The monoid of the natural numbers with maximum
9.84.
Multiplication on integer fractions
9.85.
Multiplication of integers
9.86.
Multiplication of the elements of a list of natural numbers
9.87.
Multiplication of natural numbers
9.88.
Multiplication of positive, negative, nonnegative and nonpositive integers
9.89.
Multiplication on the rational numbers
9.90.
The multiplicative group of positive rational numbers
9.91.
The multiplicative group of rational numbers
9.92.
Multiplicative inverses of positive integer fractions
9.93.
The multiplicative monoid of natural numbers
9.94.
The multiplicative monoid of rational numbers
9.95.
Multiplicative units in the integers
9.96.
Multiplicative units in modular arithmetic
9.97.
Multiset coefficients
9.98.
The type of natural numbers
9.99.
The negative integers
9.100.
The nonnegative integers
9.101.
The nonpositive integers
9.102.
Nonzero integers
9.103.
Nonzero natural numbers
9.104.
Nonzero rational numbers
9.105.
The ordinal induction principle for the natural numbers
9.106.
Parity of the natural numbers
9.107.
Peano arithmetic
9.108.
Pisano periods
9.109.
The poset of natural numbers ordered by divisibility
9.110.
The positive, negative, nonnegative and nonpositive integers
9.111.
Positive integer fractions
9.112.
The positive integers
9.113.
Positive rational numbers
9.114.
Powers of integers
9.115.
Powers of two
9.116.
Prime numbers
9.117.
Products of natural numbers
9.118.
Proper divisors of natural numbers
9.119.
Pythagorean triples
9.120.
The rational numbers
9.121.
Reduced integer fractions
9.122.
Relatively prime integers
9.123.
Relatively prime natural numbers
9.124.
Repeating an element in a standard finite type
9.125.
Retracts of the type of natural numbers
9.126.
The ring of integers
9.127.
The ring of rational numbers
9.128.
The sieve of Eratosthenes
9.129.
Square-free natural numbers
9.130.
Squares in the integers
9.131.
Squares in ℤₚ
9.132.
Squares in the natural numbers
9.133.
The standard cyclic groups
9.134.
The standard cyclic rings
9.135.
Stirling numbers of the second kind
9.136.
Strict inequality on the integer fractions
9.137.
Strict inequality on the integers
9.138.
Strict inequality on the natural numbers
9.139.
Strict inequality on the rational numbers
9.140.
Strictly ordered pairs of natural numbers
9.141.
The strong induction principle for the natural numbers
9.142.
Sums of natural numbers
9.143.
Taxicab numbers
9.144.
Telephone numbers
9.145.
The triangular numbers
9.146.
The Twin Prime conjecture
9.147.
Type arithmetic with natural numbers
9.148.
Unit elements in the standard finite types
9.149.
Unit similarity on the standard finite types
9.150.
The universal property of the integers
9.151.
The universal property of the natural numbers
9.152.
Upper bounds for type families over the natural numbers
9.153.
The Well-Ordering Principle of the natural numbers
9.154.
The well-ordering principle of the standard finite types
10.
Finite algebra
❱
10.1.
Commutative finite rings
10.2.
Dependent products of commutative finit rings
10.3.
Dependent products of finite rings
10.4.
Finite fields
10.5.
Finite rings
10.6.
Homomorphisms of commutative finite rings
10.7.
Homomorphisms of finite rings
10.8.
Products of commutative finite rings
10.9.
Products of finite rings
10.10.
Semisimple commutative finite rings
11.
Finite group theory
❱
11.1.
The abstract quaternion group of order 8
11.2.
Alternating concrete groups
11.3.
Alternating groups
11.4.
Cartier's delooping of the sign homomorphism
11.5.
The concrete quaternion group
11.6.
Deloopings of the sign homomorphism
11.7.
Abelian groups
11.8.
Finite Commutative monoids
11.9.
Finite groups
11.10.
Finite monoids
11.11.
Finite semigroups
11.12.
The group of n-element types
11.13.
Groups of order 2
11.14.
Orbits of permutations
11.15.
Permutations
11.16.
Permutations of standard finite types
11.17.
The sign homomorphism
11.18.
Simpson's delooping of the sign homomorphism
11.19.
Subgroups of finite groups
11.20.
Tetrahedra in 3-dimensional space
11.21.
Transpositions
11.22.
Transpositions of standard finite types
12.
Foundation
❱
12.1.
0-Connected types
12.2.
0-Images of maps
12.3.
0-Maps
12.4.
1-Types
12.5.
2-Types
12.6.
Action on equivalences of functions
12.7.
The action on equivalences of functions out of subuniverses
12.8.
Action on equivalences of type families
12.9.
Action on equivalences in type families over subuniverses
12.10.
The action of functions on higher identifications
12.11.
The action on homotopies of functions
12.12.
The binary action on identifications of binary functions
12.13.
The action on identifications of dependent functions
12.14.
The action on identifications of functions
12.15.
Apartness relations
12.16.
Arithmetic law for coproduct decomposition and Σ-decomposition
12.17.
Arithmetic law for product decomposition and Π-decomposition
12.18.
Automorphisms
12.19.
The axiom of choice
12.20.
Bands
12.21.
Base changes of span diagrams
12.22.
Binary embeddings
12.23.
Binary equivalences
12.24.
Binary equivalences on unordered pairs of types
12.25.
Binary functoriality of set quotients
12.26.
Homotopies of binary operations
12.27.
Binary operations on unordered pairs of types
12.28.
Binary reflecting maps of equivalence relations
12.29.
Binary relations
12.30.
Binary relations with extensions
12.31.
Binary relations with lifts
12.32.
Binary transport
12.33.
Binary type duality
12.34.
The booleans
12.35.
The Cantor–Schröder–Bernstein–Escardó theorem
12.36.
Cantor's diagonal argument
12.37.
Cartesian morphisms of arrows
12.38.
Cartesian morphisms of span diagrams
12.39.
Cartesian product types
12.40.
Cartesian products of set quotients
12.41.
The category of families of sets
12.42.
The category of sets
12.43.
Choice of representatives for an equivalence relation
12.44.
Codiagonal maps of types
12.45.
Coherently invertible maps
12.46.
Coinhabited pairs of types
12.47.
Commuting cubes of maps
12.48.
Commuting hexagons of identifications
12.49.
Commuting pentagons of identifications
12.50.
Commuting prisms of maps
12.51.
Commuting squares of homotopies
12.52.
Commuting squares of identifications
12.53.
Commuting squares of maps
12.54.
Commuting tetrahedra of homotopies
12.55.
Commuting tetrahedra of maps
12.56.
Commuting triangles of homotopies
12.57.
Commuting triangles of identifications
12.58.
Commuting triangles of maps
12.59.
Commuting triangles of morphisms of arrows
12.60.
Complements of type families
12.61.
Complements of subtypes
12.62.
Composite maps in inverse sequential diagrams
12.63.
Composition algebra
12.64.
Computational identity types
12.65.
Cones over cospan diagrams
12.66.
Cones over inverse sequential diagrams
12.67.
Conjunction
12.68.
Connected components of types
12.69.
Connected components of universes
12.70.
Connected maps
12.71.
Connected types
12.72.
Constant maps
12.73.
Constant span diagrams
12.74.
Constant type families
12.75.
Contractible maps
12.76.
Contractible types
12.77.
Copartial elements
12.78.
Copartial functions
12.79.
Coproduct decompositions
12.80.
Coproduct decompositions in a subuniverse
12.81.
Coproduct types
12.82.
Coproducts of pullbacks
12.83.
Morphisms in the coslice category of types
12.84.
Cospan diagrams
12.85.
Cospans of types
12.86.
Decidability of dependent function types
12.87.
Decidability of dependent pair types
12.88.
Decidable embeddings
12.89.
Decidable equality
12.90.
Decidable equivalence relations
12.91.
Decidable maps
12.92.
Decidable propositions
12.93.
Decidable relations on types
12.94.
Decidable subtypes
12.95.
Decidable types
12.96.
Dependent binary homotopies
12.97.
The dependent binomial theorem for types (distributivity of dependent function types over coproduct types)
12.98.
Dependent epimorphisms
12.99.
Dependent epimorphisms with respect to truncated types
12.100.
Dependent function types
12.101.
Dependent homotopies
12.102.
Dependent identifications
12.103.
Dependent inverse sequential diagrams of types
12.104.
Dependent pair types
12.105.
Dependent products of pullbacks
12.106.
Dependent sequences
12.107.
Dependent sums of pullbacks
12.108.
Dependent telescopes
12.109.
The dependent universal property of equivalences
12.110.
Descent for coproduct types
12.111.
Descent for dependent pair types
12.112.
Descent for the empty type
12.113.
Descent for equivalences
12.114.
Diagonal maps into cartesian products of types
12.115.
Diagonal maps of types
12.116.
Diagonal span diagrams
12.117.
Diagonals of maps
12.118.
Diagonals of morphisms of arrows
12.119.
Discrete relations
12.120.
Discrete relaxed Σ-decompositions
12.121.
Discrete Σ-decompositions
12.122.
Discrete types
12.123.
Disjunction
12.124.
Double arrows
12.125.
Double negation
12.126.
The double negation modality
12.127.
Double powersets
12.128.
Dubuc-Penon compact types
12.129.
Effective maps for equivalence relations
12.130.
Embeddings
12.131.
Empty types
12.132.
Endomorphisms
12.133.
Epimorphisms
12.134.
Epimorphisms with respect to maps into sets
12.135.
Epimorphisms with respect to truncated types
12.136.
Equality of cartesian product types
12.137.
Equality of coproduct types
12.138.
Equality on dependent function types
12.139.
Equality of dependent pair types
12.140.
Equality in the fibers of a map
12.141.
Equivalence classes
12.142.
Equivalence extensionality
12.143.
Equivalence induction
12.144.
Equivalence injective type families
12.145.
Equivalence relations
12.146.
Equivalences
12.147.
Equivalences of arrows
12.148.
Equivalences of cospans
12.149.
Equivalences of double arrows
12.150.
Equivalences of inverse sequential diagrams of types
12.151.
Equivalences on Maybe
12.152.
Equivalences of span diagrams
12.153.
Equivalences of span diagrams on families of types
12.154.
Equivalences of spans
12.155.
Equivalences of spans of families of types
12.156.
Evaluation of functions
12.157.
Exclusive disjunctions
12.158.
Exclusive sums
12.159.
Existential quantification
12.160.
Exponents of set quotients
12.161.
Extensions of types
12.162.
Faithful maps
12.163.
Families of equivalences
12.164.
Families of maps
12.165.
Families of types over telescopes
12.166.
Fiber inclusions
12.167.
Fibered equivalences
12.168.
Fibered involutions
12.169.
Maps fibered over a map
12.170.
Fibers of maps
12.171.
Finitely coherent equivalences
12.172.
Finitely coherently invertible maps
12.173.
Fixed points of endofunctions
12.174.
Full subtypes of types
12.175.
Function extensionality
12.176.
Function types
12.177.
Functional correspondences
12.178.
Functoriality of cartesian product types
12.179.
Functoriality of coproduct types
12.180.
Functoriality of dependent function types
12.181.
Functoriality of dependent pair types
12.182.
Functoriality of fibers of maps
12.183.
Functoriality of function types
12.184.
Functoriality of propositional truncations
12.185.
Functorialty of pullbacks
12.186.
Functoriality of sequential limits
12.187.
Functoriality of set quotients
12.188.
Functoriality of set truncation
12.189.
Functoriality of truncations
12.190.
The fundamental theorem of identity types
12.191.
Global choice
12.192.
Global subuniverses
12.193.
Higher homotopies of morphisms of arrows
12.194.
Hilbert's ε-operators
12.195.
Homotopies
12.196.
Homotopies of morphisms of arrows
12.197.
Homotopy algebra
12.198.
Homotopy induction
12.199.
The homotopy preorder of types
12.200.
Idempotent maps
12.201.
Identity systems
12.202.
Identity types of truncated types
12.203.
Identity types
12.204.
The image of a map
12.205.
Images of subtypes
12.206.
Implicit function types
12.207.
Impredicative encodings of the logical operations
12.208.
Impredicative universes
12.209.
The induction principle for propositional truncation
12.210.
Infinitely coherent equivalences
12.211.
Inhabited subtypes
12.212.
Inhabited types
12.213.
Injective maps
12.214.
The interchange law
12.215.
Intersections of subtypes
12.216.
Inverse sequential diagrams of types
12.217.
Invertible maps
12.218.
Involutions
12.219.
Isolated elements
12.220.
Isomorphisms of sets
12.221.
Iterated cartesian product types
12.222.
Iterated dependent pair types
12.223.
Iterated dependent product types
12.224.
Iterating automorphisms
12.225.
Iterating functions
12.226.
Iterating involutions
12.227.
Kernel span diagrams of maps
12.228.
Large binary relations
12.229.
Large dependent pair types
12.230.
Large homotopies
12.231.
Large identity types
12.232.
The large locale of propositions
12.233.
The large locale of subtypes
12.234.
The law of excluded middle
12.235.
Lawvere's fixed point theorem
12.236.
The lesser limited principle of omniscience
12.237.
Lifts of types
12.238.
The limited principle of omniscience
12.239.
Locally small types
12.240.
Logical equivalences
12.241.
The maybe modality
12.242.
Mere embeddings
12.243.
Mere equality
12.244.
Mere equivalences
12.245.
Mere functions
12.246.
Mere logical equivalences
12.247.
Mere path-cosplit maps
12.248.
Monomorphisms
12.249.
Morphisms of arrows
12.250.
Morphisms of binary relations
12.251.
Morphisms of cospan diagrams
12.252.
Morphisms of cospans
12.253.
Morphisms of double arrows
12.254.
Morphisms of inverse sequential diagrams of types
12.255.
Morphisms of span diagrams
12.256.
Morphisms of spans
12.257.
Morphisms of spans on families of types
12.258.
Morphisms of twisted arrows
12.259.
Multisubsets
12.260.
Multivariable correspondences
12.261.
Multivariable decidable relations
12.262.
Multivariable functoriality of set quotients
12.263.
Multivariable homotopies
12.264.
Multivariable operations
12.265.
Multivariable relations
12.266.
Multivariable sections
12.267.
Negated equality
12.268.
Negation
12.269.
Noncontractible types
12.270.
Operations on span diagrams
12.271.
Operations on spans
12.272.
Operations on spans of families of types
12.273.
Opposite spans
12.274.
Pairs of distinct elements
12.275.
Partial elements
12.276.
Partial functions
12.277.
Partial sequences
12.278.
Partitions
12.279.
Path algebra
12.280.
Path-cosplit maps
12.281.
Path-split maps
12.282.
Perfect images
12.283.
Permutations of spans of families of types
12.284.
Π-decompositions of types
12.285.
Π-decompositions of types into types in a subuniverse
12.286.
Pointed torsorial type families
12.287.
Postcomposition of dependent functions
12.288.
Postcomposition of functions
12.289.
Postcomposition of pullbacks
12.290.
Powersets
12.291.
Precomposition of dependent functions
12.292.
Precomposition of functions
12.293.
Precomposition of functions into subuniverses
12.294.
Precomposition of type families
12.295.
Preimages of subtypes
12.296.
The preunivalence axiom
12.297.
Preunivalent type families
12.298.
The principle of omniscience
12.299.
Product decompositions
12.300.
Product decompositions of types in a subuniverse
12.301.
Products of binary relations
12.302.
Products of equivalence relataions
12.303.
Products of tuples of types
12.304.
Products of pullbacks
12.305.
Products of unordered pairs of types
12.306.
Products of unordered tuples of types
12.307.
Projective types
12.308.
Proper subsets
12.309.
Propositional extensionality
12.310.
Propositional maps
12.311.
Propositional resizing
12.312.
Propositional truncations
12.313.
Propositions
12.314.
Pullbacks
12.315.
Pullbacks of subtypes
12.316.
Quasicoherently idempotent maps
12.317.
Raising universe levels
12.318.
Reflecting maps for equivalence relations
12.319.
Reflexive relations
12.320.
The Regensburg extension of the fundamental theorem of identity types
12.321.
Relaxed Σ-decompositions of types
12.322.
Repetitions of values of maps
12.323.
Repetitions in sequences
12.324.
The type theoretic replacement axiom
12.325.
Retractions
12.326.
Retracts of maps
12.327.
Retracts of types
12.328.
Russell's paradox
12.329.
Sections
12.330.
Separated types
12.331.
Sequences
12.332.
Sequential limits
12.333.
Set presented types
12.334.
Set quotients
12.335.
Set truncations
12.336.
Sets
12.337.
Shifting sequences
12.338.
Σ-closed subuniverses
12.339.
Σ-decompositions of types into types in a subuniverse
12.340.
Σ-decompositions of types
12.341.
Singleton induction
12.342.
Singleton subtypes
12.343.
Morphisms in the slice category of types
12.344.
Small maps
12.345.
Small types
12.346.
Small universes
12.347.
Sorial type families
12.348.
Span diagrams
12.349.
Span diagrams on families of types
12.350.
Spans of types
12.351.
Spans of families of types
12.352.
Split idempotent maps
12.353.
Split surjective maps
12.354.
Standard apartness relations
12.355.
Standard pullbacks
12.356.
Strict symmetrization of binary relations
12.357.
Strictly involutive identity types
12.358.
The strictly right unital concatenation operation on identifications
12.359.
Strongly extensional maps
12.360.
Structure
12.361.
The structure identity principle
12.362.
Structured type duality
12.363.
Subsingleton induction
12.364.
Subterminal types
12.365.
Subtype duality
12.366.
The subtype identity principle
12.367.
Subtypes
12.368.
Subuniverses
12.369.
Surjective maps
12.370.
Symmetric binary relations
12.371.
Symmetric cores of binary relations
12.372.
Symmetric difference of subtypes
12.373.
The symmetric identity types
12.374.
Symmetric operations
12.375.
Telescopes
12.376.
Terminal spans on families of types
12.377.
Tight apartness relations
12.378.
Torsorial type families
12.379.
Total partial elements
12.380.
Total partial functions
12.381.
Transfinite cocomposition of maps
12.382.
Transport along equivalences
12.383.
Transport along higher identifications
12.384.
Transport along homotopies
12.385.
Transport along identifications
12.386.
Transport-split type families
12.387.
Transposing identifications along equivalences
12.388.
Transposing identifications along retractions
12.389.
Transposing identifications along sections
12.390.
Transposition of span diagrams
12.391.
Trivial relaxed Σ-decompositions
12.392.
Trivial Σ-decompositions
12.393.
Truncated equality
12.394.
Truncated maps
12.395.
Truncated types
12.396.
k-Equivalences
12.397.
Truncation images of maps
12.398.
Truncation levels
12.399.
The truncation modalities
12.400.
Truncations
12.401.
Tuples of types
12.402.
Type arithmetic with the booleans
12.403.
Type arithmetic for cartesian product types
12.404.
Type arithmetic for coproduct types
12.405.
Type arithmetic with dependent function types
12.406.
Type arithmetic for dependent pair types
12.407.
Type arithmetic with the empty type
12.408.
Type arithmetic with the unit type
12.409.
Type duality
12.410.
The type theoretic principle of choice
12.411.
Unions of subtypes
12.412.
Uniqueness of the image of a map
12.413.
Uniqueness quantification
12.414.
The uniqueness of set quotients
12.415.
Uniqueness of set truncations
12.416.
Uniqueness of the truncations
12.417.
The unit type
12.418.
Unital binary operations
12.419.
The univalence axiom
12.420.
The univalence axiom implies function extensionality
12.421.
Univalent type families
12.422.
The universal property of booleans
12.423.
The universal properties of cartesian product types
12.424.
Universal property of contractible types
12.425.
The universal property of coproduct types
12.426.
The universal property of dependent function types
12.427.
The universal property of dependent pair types
12.428.
The universal property of the empty type
12.429.
The universal property of equivalences
12.430.
The universal property of the family of fibers of maps
12.431.
The universal property of fiber products
12.432.
The universal property of identity systems
12.433.
The universal property of identity types
12.434.
The universal property of the image of a map
12.435.
The universal property of maybe
12.436.
The universal property of propositional truncations
12.437.
The universal property of propositional truncations with respect to sets
12.438.
The universal property of pullbacks
12.439.
The universal property of sequential limits
12.440.
The universal property of set quotients
12.441.
The universal property of set truncations
12.442.
The universal property of truncations
12.443.
The universal property of the unit type
12.444.
Universal quantification
12.445.
Universe levels
12.446.
Unordered pairs of elements in a type
12.447.
Unordered pairs of types
12.448.
Unordered n-tuples of elements in a type
12.449.
Unordered tuples of types
12.450.
Vectors of set quotients
12.451.
Weak function extensionality
12.452.
The weak limited principle of omniscience
12.453.
Weakly constant maps
12.454.
Whiskering higher homotopies with respect to composition
12.455.
Whiskering homotopies with respect to composition
12.456.
Whiskering homotopies with respect to concatenation
12.457.
Whiskering identifications with respect to concatenation
12.458.
Whiskering operations
12.459.
The wild category of types
12.460.
Yoneda identity types
13.
Foundation core
❱
13.1.
1-Types
13.2.
Cartesian product types
13.3.
Coherently invertible maps
13.4.
Commuting prisms of maps
13.5.
Commuting squares of homotopies
13.6.
Commuting squares of identifications
13.7.
Commuting squares of maps
13.8.
Commuting triangles of maps
13.9.
Constant maps
13.10.
Contractible maps
13.11.
Contractible types
13.12.
Coproduct types
13.13.
Decidable propositions
13.14.
Dependent identifications
13.15.
Diagonal maps into cartesian products of types
13.16.
Discrete types
13.17.
Embeddings
13.18.
Empty types
13.19.
Endomorphisms
13.20.
Equality of dependent pair types
13.21.
Equivalence relations
13.22.
Equivalences
13.23.
Families of equivalences
13.24.
Fibers of maps
13.25.
Function types
13.26.
Functoriality of dependent function types
13.27.
Functoriality of dependent pair types
13.28.
Homotopies
13.29.
Identity types
13.30.
Injective maps
13.31.
Invertible maps
13.32.
Negation
13.33.
Operations on span diagrams
13.34.
Operations on spans
13.35.
Path-split maps
13.36.
Postcomposition of dependent functions
13.37.
Postcomposition of functions
13.38.
Precomposition of dependent functions
13.39.
Precomposition of functions
13.40.
Propositional maps
13.41.
Propositions
13.42.
Pullbacks
13.43.
Retractions
13.44.
Retracts of types
13.45.
Sections
13.46.
Sets
13.47.
Small types
13.48.
Subtypes
13.49.
Torsorial type families
13.50.
Transport along identifications
13.51.
Truncated maps
13.52.
Truncated types
13.53.
Truncation levels
13.54.
The type theoretic principle of choice
13.55.
The univalence axiom
13.56.
The universal property of pullbacks
13.57.
The universal property of truncations
13.58.
Whiskering homotopies with respect to concatenation
13.59.
Whiskering identifications with respect to concatenation
14.
Graph theory
❱
14.1.
Acyclic undirected graphs
14.2.
Circuits in undirected graphs
14.3.
Closed walks in undirected graphs
14.4.
Complete bipartite graphs
14.5.
Complete multipartite graphs
14.6.
Complete undirected graphs
14.7.
Connected graphs
14.8.
Cycles in undirected graphs
14.9.
Directed graph structures on standard finite sets
14.10.
Directed graphs
14.11.
Discrete graphs
14.12.
Displayed large reflexive graphs
14.13.
Edge-coloured undirected graphs
14.14.
Embeddings of directed graphs
14.15.
Embeddings of undirected graphs
14.16.
Enriched undirected graphs
14.17.
Equivalences of directed graphs
14.18.
Equivalences of enriched undirected graphs
14.19.
Equivalences of undirected graphs
14.20.
Eulerian circuits in undirected graphs
14.21.
Faithful morphisms of undirected graphs
14.22.
Fibers of directed graphs
14.23.
Finite graphs
14.24.
Geometric realizations of undirected graphs
14.25.
Higher directed graphs
14.26.
Hypergraphs
14.27.
Large higher directed graphs
14.28.
Large reflexive graphs
14.29.
Matchings
14.30.
Mere equivalences of undirected graphs
14.31.
Morphisms of directed graphs
14.32.
Morphisms of undirected graphs
14.33.
Incidence in undirected graphs
14.34.
Orientations of undirected graphs
14.35.
Paths in undirected graphs
14.36.
Polygons
14.37.
Raising universe levels of directed graphs
14.38.
Reflecting maps of undirected graphs
14.39.
Reflexive graphs
14.40.
Regular undirected graph
14.41.
Simple undirected graphs
14.42.
Stereoisomerism for enriched undirected graphs
14.43.
Totally faithful morphisms of undirected graphs
14.44.
Trails in directed graphs
14.45.
Trails in undirected graphs
14.46.
Undirected graph structures on standard finite sets
14.47.
Undirected graphs
14.48.
Vertex covers
14.49.
Voltage graphs
14.50.
Walks in directed graphs
14.51.
Walks in undirected graphs
14.52.
Wide displayed large reflexive graphs
15.
Group theory
❱
15.1.
Abelian groups
15.2.
Abelianization of groups
15.3.
Pointwise addition of morphisms of abelian groups
15.4.
Automorphism groups
15.5.
Cartesian products of abelian groups
15.6.
Cartesian products of concrete groups
15.7.
Cartesian products of groups
15.8.
Cartesian products of monoids
15.9.
Cartesian products of semigroups
15.10.
The category of abelian groups
15.11.
The category of concrete groups
15.12.
The category of group actions
15.13.
The category of groups
15.14.
The orbit category of a group
15.15.
The category of semigroups
15.16.
Cayley's theorem
15.17.
The center of a group
15.18.
Center of a monoid
15.19.
Center of a semigroup
15.20.
Central elements of groups
15.21.
Central elements of monoids
15.22.
Central elements of semirings
15.23.
Centralizer subgroups
15.24.
Characteristic subgroups
15.25.
Commutative monoids
15.26.
Commutator subgroups
15.27.
Commutators of elements in groups
15.28.
Commuting elements of groups
15.29.
Commuting elements of monoids
15.30.
Commuting elements of semigroups
15.31.
Commuting squares of group homomorphisms
15.32.
Concrete group actions
15.33.
Concrete groups
15.34.
Concrete monoids
15.35.
Congruence relations on abelian groups
15.36.
Congruence relations on commutative monoids
15.37.
Congruence relations on groups
15.38.
Congruence relations on monoids
15.39.
Congruence relations on semigroups
15.40.
Conjugation in groups
15.41.
Conjugation on concrete groups
15.42.
Contravariant pushforwards of concrete group actions
15.43.
Cores of monoids
15.44.
Cyclic groups
15.45.
Decidable subgroups of groups
15.46.
Dependent products of abelian groups
15.47.
Dependent products of commutative monoids
15.48.
Dependent products of groups
15.49.
Dependent products of monoids
15.50.
Dependent products of semigroups
15.51.
The dihedral group construction
15.52.
The dihedral groups
15.53.
The E₈-lattice
15.54.
Elements of finite order
15.55.
Embeddings of abelian groups
15.56.
Embeddings of groups
15.57.
The endomorphism rings of abelian groups
15.58.
Epimorphisms in groups
15.59.
Equivalences of concrete group actions
15.60.
Equivalences of concrete groups
15.61.
Equivalences of group actions
15.62.
Equivalences between semigroups
15.63.
Exponents of abelian groups
15.64.
Exponents of groups
15.65.
Free concrete group actions
15.66.
Free groups with one generator
15.67.
The full subgroup of a group
15.68.
The full subsemigroup of a semigroup
15.69.
Function groups of abelian groups
15.70.
Function commutative monoids
15.71.
Function groups
15.72.
Function monoids
15.73.
Function semigroups
15.74.
Functoriality of quotient groups
15.75.
Furstenberg groups
15.76.
Generating elements of groups
15.77.
Generating sets of groups
15.78.
Group actions
15.79.
Abstract groups
15.80.
Homomorphisms of abelian groups
15.81.
Homomorphisms of commutative monoids
15.82.
Morphisms of concrete group actions
15.83.
Homomorphisms of concrete groups
15.84.
Homomorphisms of generated subgroups
15.85.
Homomorphisms of group actions
15.86.
Homomorphisms of groups
15.87.
Homomorphisms of groups equipped with normal subgroups
15.88.
Homomorphisms of monoids
15.89.
Homomorphisms of semigroups
15.90.
Images of group homomorphisms
15.91.
Images of semigroup homomorphisms
15.92.
Integer multiples of elements in abelian groups
15.93.
Integer powers of elements of groups
15.94.
Intersections of subgroups of abelian groups
15.95.
Intersections of subgroups of groups
15.96.
Inverse semigroups
15.97.
Invertible elements in monoids
15.98.
Isomorphisms of abelian groups
15.99.
Isomorphisms of concrete groups
15.100.
Isomorphisms of group actions
15.101.
Isomorphisms of groups
15.102.
Isomorphisms of monoids
15.103.
Isomorphisms of semigroups
15.104.
Iterated cartesian products of concrete groups
15.105.
Kernels of homomorphisms between abelian groups
15.106.
Kernels of homomorphisms of concrete groups
15.107.
Kernels of homomorphisms of groups
15.108.
Large semigroups
15.109.
Concrete automorphism groups on sets
15.110.
Mere equivalences of concrete group actions
15.111.
Mere equivalences of group actions
15.112.
Monoid actions
15.113.
Monoids
15.114.
Monomorphisms of concrete groups
15.115.
Monomorphisms in the category of groups
15.116.
Multiples of elements in abelian groups
15.117.
Nontrivial groups
15.118.
Normal closures of subgroups
15.119.
Normal cores of subgroups
15.120.
Normal subgroups
15.121.
Normal subgroups of concrete groups
15.122.
Normal submonoids
15.123.
Normal submonoids of commutative monoids
15.124.
Normalizer subgroups
15.125.
Nullifying group homomorphisms
15.126.
The opposite of a group
15.127.
The opposite of a semigroup
15.128.
The orbit-stabilizer theorem for concrete groups
15.129.
Orbits of concrete group actions
15.130.
Orbits of group actions
15.131.
The order of an element in a group
15.132.
Perfect cores
15.133.
Perfect groups
15.134.
Perfect subgroups
15.135.
Powers of elements in commutative monoids
15.136.
Powers of elements in groups
15.137.
Powers of elements in monoids
15.138.
The precategory of commutative monoids
15.139.
The precategory of concrete groups
15.140.
The precategory of group actions
15.141.
The precategory of groups
15.142.
The precategory of monoids
15.143.
The precategory of orbits of a monoid action
15.144.
The precategory of semigroups
15.145.
Principal group actions
15.146.
Principal torsors of concrete groups
15.147.
Products of elements in a monoid
15.148.
Products of tuples of elements in commutative monoids
15.149.
Pullbacks of subgroups
15.150.
Pullbacks of subsemigroups
15.151.
Quotient groups
15.152.
Quotient groups of concrete groups
15.153.
Quotients of abelian groups
15.154.
Rational commutative monoids
15.155.
Representations of monoids in precategories
15.156.
Saturated congruence relations on commutative monoids
15.157.
Saturated congruence relations on monoids
15.158.
Semigroups
15.159.
Sheargroups
15.160.
Shriek of concrete group homomorphisms
15.161.
Stabilizer groups
15.162.
Stabilizers of concrete group actions
15.163.
Subgroups
15.164.
Subgroups of abelian groups
15.165.
Subgroups of concrete groups
15.166.
Subgroups generated by elements of a group
15.167.
Subgroups generated by families of elements
15.168.
Subgroups generated by subsets of groups
15.169.
Submonoids
15.170.
Submonoids of commutative monoids
15.171.
Subsemigroups
15.172.
Subsets of abelian groups
15.173.
Subsets of commutative monoids
15.174.
Subsets of groups
15.175.
Subsets of monoids
15.176.
Subsets of semigroups
15.177.
The substitution functor of concrete group actions
15.178.
The substitution functor of group actions
15.179.
Surjective group homomorphisms
15.180.
Surjective semigroup homomorphisms
15.181.
Symmetric concrete groups
15.182.
Symmetric groups
15.183.
Torsion elements of groups
15.184.
Torsion-free groups
15.185.
Torsors of abstract groups
15.186.
Transitive concrete group actions
15.187.
Transitive group actions
15.188.
Trivial concrete groups
15.189.
Trivial group homomorphisms
15.190.
Trivial groups
15.191.
Trivial subgroups
15.192.
Unordered tuples of elements in commutative monoids
15.193.
Wild representations of monoids
16.
Higher group theory
❱
16.1.
Cartesian products of higher groups
16.2.
Conjugation in higher groups
16.3.
Cyclic higher groups
16.4.
Deloopable groups
16.5.
Deloopable H-spaces
16.6.
Deloopable types
16.7.
Eilenberg-Mac Lane spaces
16.8.
Equivalences of higher groups
16.9.
Fixed points of higher group actions
16.10.
Free higher group actions
16.11.
Higher group actions
16.12.
Higher groups
16.13.
Homomorphisms of higher group actions
16.14.
Homomorphisms of higher groups
16.15.
The higher group of integers
16.16.
Iterated cartesian products of higher groups
16.17.
Iterated deloopings of pointed types
16.18.
Orbits of higher group actions
16.19.
Small ∞-groups
16.20.
Subgroups of higher groups
16.21.
Symmetric higher groups
16.22.
Transitive higher group actions
16.23.
Trivial higher groups
17.
Linear algebra
❱
17.1.
Constant matrices
17.2.
Diagonal vectors
17.3.
Diagonal matrices on rings
17.4.
Functoriality of the type of matrices
17.5.
Functoriality of the type of vectors
17.6.
Matrices
17.7.
Matrices on rings
17.8.
Multiplication of matrices
17.9.
Scalar multiplication on matrices
17.10.
Scalar multiplication of vectors
17.11.
Scalar multiplication of vectors on rings
17.12.
Transposition of matrices
17.13.
Vectors
17.14.
Vectors on commutative rings
17.15.
Vectors on commutative semirings
17.16.
Vectors on euclidean domains
17.17.
Vectors on rings
17.18.
Vectors on semirings
18.
Lists
❱
18.1.
Arrays
18.2.
Concatenation of lists
18.3.
Flattening of lists
18.4.
Functoriality of the list operation
18.5.
Lists
18.6.
Lists of elements in discrete types
18.7.
Permutations of lists
18.8.
Permutations of vectors
18.9.
Predicates on lists
18.10.
Quicksort for lists
18.11.
Reversing lists
18.12.
Sort by insertion for lists
18.13.
Sort by insertion for vectors
18.14.
Sorted lists
18.15.
Sorted vectors
18.16.
Sorting algorithms for lists
18.17.
Sorting algorithms for vectors
18.18.
The universal property of lists with respect to wild monoids
19.
Modal type theory
❱
19.1.
Crisp identity types
19.2.
The crisp law of excluded middle
19.3.
Flat dependent function types
19.4.
Flat dependent pair types
19.5.
Flat discrete types
19.6.
The flat modality
19.7.
The flat-sharp adjunction
19.8.
Sharp codiscrete maps
19.9.
Sharp codiscrete types
19.10.
The sharp modality
20.
Online encyclopedia of integer sequences
❱
20.1.
Sequences of the online encyclopedia of integer sequences
21.
Order theory
❱
21.1.
Accessible elements with respect to relations
21.2.
Bottom elements in posets
21.3.
Bottom elements in preorders
21.4.
Chains in posets
21.5.
Chains in preorders
21.6.
Closure operators on large locales
21.7.
Closure operators on large posets
21.8.
Commuting squares of Galois connections between large posets
21.9.
Commuting squares of order preserving maps of large posets
21.10.
Coverings in locales
21.11.
Decidable posets
21.12.
Decidable preorders
21.13.
Decidable subposets
21.14.
Decidable subpreorders
21.15.
Decidable total orders
21.16.
Decidable total preorders
21.17.
Dependent products of large frames
21.18.
Dependent products of large locales
21.19.
Dependent products of large meet-semilattices
21.20.
Dependent products of large posets
21.21.
Dependent products large preorders
21.22.
Dependent products of large suplattices
21.23.
Directed complete posets
21.24.
Directed families in posets
21.25.
Distributive lattices
21.26.
Finite coverings in locales
21.27.
Finite posets
21.28.
Finite preorders
21.29.
Finite total orders
21.30.
Finitely graded posets
21.31.
Frames
21.32.
Galois connections
21.33.
Galois connections between large posets
21.34.
Greatest lower bounds in large posets
21.35.
Greatest lower bounds in posets
21.36.
Homomorphisms of frames
21.37.
Homomorphisms of large frames
21.38.
Homomorphisms of large locales
21.39.
Homomorphisms of large meet-semilattices
21.40.
Homomorphisms of large suplattices
21.41.
Homomorphisms of meet-semilattices
21.42.
Homomorphisms of meet sup lattices
21.43.
Homomorphisms of suplattices
21.44.
Ideals in preorders
21.45.
Inhabited finite total orders
21.46.
Interval subposets
21.47.
Join-semilattices
21.48.
Large frames
21.49.
Large locales
21.50.
Large meet-semilattices
21.51.
Large meet-subsemilattices
21.52.
Large posets
21.53.
Large preorders
21.54.
Large quotient locales
21.55.
Large subframes
21.56.
Large subposets
21.57.
Large subpreorders
21.58.
Large subsuplattices
21.59.
Large suplattices
21.60.
Lattices
21.61.
Least upper bounds in large posets
21.62.
Least upper bounds in posets
21.63.
Locales
21.64.
Locally finite posets
21.65.
Lower bounds in large posets
21.66.
Lower bounds in posets
21.67.
Lower sets in large posets
21.68.
Lower types in preorders
21.69.
Maximal chains in posets
21.70.
Maximal chains in preorders
21.71.
Meet-semilattices
21.72.
Meet-suplattices
21.73.
Nuclei on large locales
21.74.
Order preserving maps between large posets
21.75.
Order preserving maps between large preorders
21.76.
Order preserving maps on posets
21.77.
Order preserving maps on preorders
21.78.
Posets
21.79.
Powers of large locales
21.80.
The precategory of decidable total orders
21.81.
The precategory of finite posets
21.82.
The precategory of finite total orders
21.83.
The precategory of inhabited finite total orders
21.84.
The precategory of posets
21.85.
The precategory of total orders
21.86.
Preorders
21.87.
Principal lower sets of large posets
21.88.
Principal upper sets of large posets
21.89.
Reflective Galois connections between large posets
21.90.
Similarity of elements in large posets
21.91.
Similarity of elements in large preorders
21.92.
Similarity of order preserving maps between large posets
21.93.
Similarity of order preserving maps between large preorders
21.94.
Subposets
21.95.
Subpreorders
21.96.
Suplattices
21.97.
Top elements in large posets
21.98.
Top elements in posets
21.99.
Top elements in preorders
21.100.
Total orders
21.101.
Total preorders
21.102.
Upper bounds in large posets
21.103.
Upper bounds in posets
21.104.
Upper sets of large posets
21.105.
Well-founded orders
21.106.
Well-founded relations
22.
Organic Chemistry
❱
22.1.
Alcohols
22.2.
Alkanes
22.3.
Alkenes
22.4.
Alkynes
22.5.
Ethane
22.6.
Hydrocarbons
22.7.
Methane
22.8.
Saturated carbons
23.
Orthogonal factorization systems
❱
23.1.
Cd-structures
23.2.
Cellular maps
23.3.
The closed modalities
23.4.
Double lifts of families of elements
23.5.
Extensions of double lifts of families of elements
23.6.
Extensions of families of elements
23.7.
Extensions of maps
23.8.
Factorization operations
23.9.
Factorization operations into function classes
23.10.
Factorization operations into global function classes
23.11.
Factorizations of maps
23.12.
Factorizations of maps into function classes
23.13.
Factorizations of maps into global function classes
23.14.
Fiberwise orthogonal maps
23.15.
Function classes
23.16.
Functoriality of higher modalities
23.17.
Functoriality of the pullback-hom
23.18.
Global function classes
23.19.
Higher modalities
23.20.
The identity modality
23.21.
Lifting operations
23.22.
Lifting structures on commuting squares of maps
23.23.
Lifts of families of elements
23.24.
Lifts of maps
23.25.
Local families of types
23.26.
Local maps
23.27.
Local types
23.28.
Localizations at maps
23.29.
Localizations at subuniverses
23.30.
Locally small modal-operators
23.31.
Mere lifting properties
23.32.
Modal induction
23.33.
Modal operators
23.34.
Modal subuniverse induction
23.35.
Null families of types
23.36.
Null maps
23.37.
Null types
23.38.
The open modalities
23.39.
Orthogonal factorization systems
23.40.
Orthogonal maps
23.41.
Precomposition of lifts of families of elements by maps
23.42.
The pullback-hom
23.43.
The raise modalities
23.44.
Reflective modalities
23.45.
Reflective subuniverses
23.46.
Regular cd-structures
23.47.
Separated types
23.48.
Σ-closed modalities
23.49.
Σ-closed reflective modalities
23.50.
Σ-closed reflective subuniverses
23.51.
Stable orthogonal factorization systems
23.52.
Uniquely eliminating modalities
23.53.
Wide function classes
23.54.
Wide global function classes
23.55.
The zero modality
24.
Polytopes
❱
24.1.
Abstract polytopes
25.
Primitives
❱
25.1.
Characters
25.2.
Floats
25.3.
Machine integers
25.4.
Strings
26.
Real numbers
❱
26.1.
Dedekind real numbers
26.2.
Rational real numbers
27.
Reflection
❱
27.1.
Abstractions
27.2.
Arguments
27.3.
Boolean reflection
27.4.
Definitions
27.5.
Erasing equality
27.6.
Fixity
27.7.
Group solver
27.8.
Literals
27.9.
Metavariables
27.10.
Names
27.11.
Precategory solver
27.12.
Rewriting
27.13.
Terms
27.14.
The type checking monad
28.
Ring theory
❱
28.1.
Additive orders of elements of rings
28.2.
Algebras over rings
28.3.
The binomial theorem for rings
28.4.
The binomial theorem for semirings
28.5.
The category of cyclic rings
28.6.
The category of rings
28.7.
Central elements of rings
28.8.
Central elements of semirings
28.9.
Characteristics of rings
28.10.
Commuting elements of rings
28.11.
Congruence relations on rings
28.12.
Congruence relations on semirings
28.13.
Cyclic rings
28.14.
Dependent products of rings
28.15.
Dependent products of semirings
28.16.
Division rings
28.17.
The free ring with one generator
28.18.
Full ideals of rings
28.19.
Function rings
28.20.
Function semirings
28.21.
Generating elements of rings
28.22.
The group of multiplicative units of a ring
28.23.
Homomorphisms of cyclic rings
28.24.
Homomorphisms of rings
28.25.
Homomorphisms of semirings
28.26.
Ideals generated by subsets of rings
28.27.
Ideals of rings
28.28.
Ideals of semirings
28.29.
Idempotent elements in rings
28.30.
Initial rings
28.31.
Integer multiples of elements of rings
28.32.
Intersections of ideals of rings
28.33.
Intersections of ideals of semirings
28.34.
The invariant basis property of rings
28.35.
Invertible elements in rings
28.36.
Isomorphisms of rings
28.37.
Joins of ideals of rings
28.38.
Joins of left ideals of rings
28.39.
Joins of right ideals of rings
28.40.
Kernels of ring homomorphisms
28.41.
Left ideals generated by subsets of rings
28.42.
Left ideals of rings
28.43.
Local rings
28.44.
Localizations of rings
28.45.
Maximal ideals of rings
28.46.
Modules over rings
28.47.
Multiples of elements in rings
28.48.
Multiplicative orders of elements of rings
28.49.
Nil ideals of rings
28.50.
Nilpotent elements in rings
28.51.
Nilpotent elements in semirings
28.52.
Opposite rings
28.53.
The poset of cyclic rings
28.54.
The poset of ideals of a ring
28.55.
The poset of left ideals of a ring
28.56.
The poset of right ideals of a ring
28.57.
Powers of elements in rings
28.58.
Powers of elements in semirings
28.59.
The precategory of rings
28.60.
The precategory of semirings
28.61.
Products of ideals of rings
28.62.
Products of left ideals of rings
28.63.
Products of right ideals of rings
28.64.
Products of rings
28.65.
Products of subsets of rings
28.66.
Quotient rings
28.67.
Radical ideals of rings
28.68.
Right ideals generated by subsets of rings
28.69.
Right ideals of rings
28.70.
Rings
28.71.
Semirings
28.72.
Subsets of rings
28.73.
Subsets of semirings
28.74.
Sums of elements in rings
28.75.
Sums of elements in semirings
28.76.
Transporting ring structures along isomorphisms of abelian groups
28.77.
Trivial rings
29.
Set theory
❱
29.1.
Baire space
29.2.
Cantor space
29.3.
Cardinalities of sets
29.4.
Countable sets
29.5.
Cumulative hierarchy
29.6.
Infinite sets
29.7.
Uncountable sets
30.
Species
❱
30.1.
Cartesian exponents of species
30.2.
Cartesian products of species of types
30.3.
Cauchy composition of species of types
30.4.
Cauchy composition of species of types in a subuniverse
30.5.
Cauchy exponentials of species of types
30.6.
Cauchy exponentials of species of types in a subuniverse
30.7.
Cauchy products of species of types
30.8.
Cauchy products of species of types in a subuniverse
30.9.
Cauchy series of species of types
30.10.
Cauchy series of species of types in a subuniverse
30.11.
Composition of Cauchy series of species of types
30.12.
Composition of Cauchy series of species of types in subuniverses
30.13.
Coproducts of species of types
30.14.
Coproducts of species of types in subuniverses
30.15.
Cycle index series of species
30.16.
Derivatives of species
30.17.
Dirichlet exponentials of a species of types
30.18.
Dirichlet exponentials of species of types in a subuniverse
30.19.
Dirichlet products of species of types
30.20.
Dirichlet products of species of types in subuniverses
30.21.
Dirichlet series of species of finite inhabited types
30.22.
Dirichlet series of species of types
30.23.
Dirichlet series of species of types in subuniverses
30.24.
Equivalences of species of types
30.25.
Equivalences of species of types in subuniverses
30.26.
Exponential of Cauchy series of species of types
30.27.
Exponential of Cauchy series of species of types in subuniverses
30.28.
Hasse-Weil species
30.29.
Morphisms of finite species
30.30.
Morphisms of species of types
30.31.
Pointing of species of types
30.32.
The precategory of finite species
30.33.
Products of Cauchy series of species of types
30.34.
Products of Cauchy series of species of types in subuniverses
30.35.
Products of Dirichlet series of species of finite inhabited types
30.36.
Products of Dirichlet series of species of types
30.37.
Products of Dirichlet series of species of types in subuniverses
30.38.
Small Composition of species of finite inhabited types
30.39.
Small Cauchy composition of species types in subuniverses
30.40.
Species of finite inhabited types
30.41.
Species of finite types
30.42.
Species of inhabited types
30.43.
Species of types
30.44.
Species of types in subuniverses
30.45.
The unit of Cauchy composition of types
30.46.
The unit of Cauchy composition of species of types in subuniverses
30.47.
Unlabeled structures of finite species
31.
Structured types
❱
31.1.
Cartesian products of types equipped with endomorphisms
31.2.
Central H-spaces
31.3.
Commuting squares of pointed homotopies
31.4.
Commuting squares of pointed maps
31.5.
Commuting triangles of pointed maps
31.6.
Conjugation of pointed types
31.7.
Constant pointed maps
31.8.
Contractible pointed types
31.9.
Cyclic types
31.10.
Dependent products of H-spaces
31.11.
Dependent products of pointed types
31.12.
Dependent products of wild monoids
31.13.
Dependent types equipped with automorphisms
31.14.
Equivalences of H-spaces
31.15.
Equivalences of pointed arrows
31.16.
Equivalences of types equipped with automorphisms
31.17.
Equivalences of types equipped with endomorphisms
31.18.
Faithful pointed maps
31.19.
Fibers of pointed maps
31.20.
Finite multiplication in magmas
31.21.
Function H-spaces
31.22.
Function magmas
31.23.
Function wild monoids
31.24.
Globular types
31.25.
H-spaces
31.26.
The initial pointed type equipped with an automorphism
31.27.
The involutive type of H-space structures on a pointed type
31.28.
Involutive types
31.29.
Iterated cartesian products of types equipped with endomorphisms
31.30.
Iterated cartesian products of pointed types
31.31.
Large globular types
31.32.
Large reflexive globular types
31.33.
Large symmetric globular types
31.34.
Large transitive globular types
31.35.
Magmas
31.36.
Maps between globular types
31.37.
Maps between large globular types
31.38.
Mere equivalences of types equipped with endomorphisms
31.39.
Morphisms of H-spaces
31.40.
Morphisms of magmas
31.41.
Morphisms of pointed arrows
31.42.
Morphisms of twisted pointed arrows
31.43.
Morphisms of types equipped with automorphisms
31.44.
Morphisms of types equipped with endomorphisms
31.45.
Morphisms of wild monoids
31.46.
Noncoherent H-spaces
31.47.
Opposite pointed spans
31.48.
Pointed 2-homotopies
31.49.
Pointed cartesian product types
31.50.
Pointed dependent functions
31.51.
Pointed dependent pair types
31.52.
Pointed equivalences
31.53.
Pointed families of types
31.54.
Pointed homotopies
31.55.
Pointed isomorphisms
31.56.
Pointed maps
31.57.
Pointed retractions of pointed maps
31.58.
Pointed sections of pointed maps
31.59.
Pointed span diagrams
31.60.
Pointed spans
31.61.
Pointed types
31.62.
Pointed types equipped with automorphisms
31.63.
The pointed unit type
31.64.
Universal property of contractible types with respect to pointed types and maps
31.65.
Postcomposition of pointed maps
31.66.
Precomposition of pointed maps
31.67.
Reflexive globular types
31.68.
Sets equipped with automorphisms
31.69.
Small pointed types
31.70.
Symmetric elements of involutive types
31.71.
Symmetric globular types
31.72.
Symmetric H-spaces
31.73.
Transitive globular types
31.74.
Transposition of pointed span diagrams
31.75.
Types equipped with automorphisms
31.76.
Types equipped with endomorphisms
31.77.
Uniform pointed homotopies
31.78.
The universal property of pointed equivalences
31.79.
Unpointed maps between pointed types
31.80.
Whiskering pointed homotopies with respect to concatenation
31.81.
Whiskering of pointed homotopies with respect to composition of pointed maps
31.82.
Wild groups
31.83.
Wild loops
31.84.
Wild monoids
31.85.
Wild quasigroups
31.86.
Wild semigroups
32.
Synthetic homotopy theory
❱
32.1.
0-acyclic maps
32.2.
0-acyclic types
32.3.
1-acyclic types
32.4.
Acyclic maps
32.5.
Acyclic types
32.6.
The category of connected set bundles over the circle
32.7.
Cavallo's trick
32.8.
The circle
32.9.
Cocartesian morphisms of arrows
32.10.
Cocones under pointed span diagrams
32.11.
Cocones under sequential diagrams
32.12.
Cocones under spans
32.13.
Codiagonals of maps
32.14.
Coequalizers
32.15.
Cofibers
32.16.
Coforks
32.17.
Correspondence between cocones under sequential diagrams and certain coforks
32.18.
Conjugation of loops
32.19.
Connected set bundles over the circle
32.20.
Dependent cocones under sequential diagrams
32.21.
Dependent cocones under spans
32.22.
Dependent coforks
32.23.
Dependent descent for the circle
32.24.
The dependent pullback property of pushouts
32.25.
Dependent pushout-products
32.26.
Dependent sequential diagrams
32.27.
Dependent suspension structures
32.28.
The dependent universal property of coequalizers
32.29.
The dependent universal property of pushouts
32.30.
The dependent universal property of sequential colimits
32.31.
Dependent universal property of suspensions
32.32.
The descent property of the circle
32.33.
Descent data for constant type families over the circle
32.34.
Descent data for families of dependent pair types over the circle
32.35.
Descent data for families of equivalence types over the circle
32.36.
Descent data for families of function types over the circle
32.37.
Subtypes of descent data for the circle
32.38.
Descent data for type families of equivalence types over pushouts
32.39.
Descent data for type families of function types over pushouts
32.40.
Descent data for type families of identity types over pushouts
32.41.
Descent data for pushouts
32.42.
Descent data for sequential colimits
32.43.
Descent property of pushouts
32.44.
Descent property of sequential colimits
32.45.
Double loop spaces
32.46.
The Eckmann-Hilton argument
32.47.
Equifibered sequential diagrams
32.48.
Equivalences of cocones under sequential diagrams
32.49.
Equivalences of coforks
32.50.
Equivalances of dependent sequential diagrams
32.51.
Equivalences of descent data for pushouts
32.52.
Equivalences of sequential diagrams
32.53.
Families with descent data for pushouts
32.54.
Families with descent data for sequential colimits
32.55.
The flattening lemma for coequalizers
32.56.
The flattening lemma for pushouts
32.57.
The flattening lemma for sequential colimits
32.58.
Free loops
32.59.
Functoriality of the loop space operation
32.60.
Functoriality of sequential colimits
32.61.
Functoriality of suspensions
32.62.
Groups of loops in 1-types
32.63.
Hatcher's acyclic type
32.64.
Identity systems of descent data for pushouts
32.65.
The induction principle of pushouts
32.66.
The infinite complex projective space
32.67.
Infinite cyclic types
32.68.
The interval
32.69.
Iterated loop spaces
32.70.
Iterated suspensions of pointed types
32.71.
Join powers of types
32.72.
Joins of maps
32.73.
Joins of types
32.74.
The loop homotopy on the circle
32.75.
Loop spaces
32.76.
Maps of prespectra
32.77.
Mere spheres
32.78.
Morphisms of cocones under morphisms of sequential diagrams
32.79.
Morphisms of coforks
32.80.
Morphisms of dependent sequential diagrams
32.81.
Morphisms of descent data of the circle
32.82.
Morphisms of descent data for pushouts
32.83.
Morphisms of sequential diagrams
32.84.
The multiplication operation on the circle
32.85.
Null cocones under pointed span diagrams
32.86.
The plus-principle
32.87.
Powers of loops
32.88.
Premanifolds
32.89.
Prespectra
32.90.
The pullback property of pushouts
32.91.
Pushout-products
32.92.
Pushouts
32.93.
Pushouts of pointed types
32.94.
The recursion principle of pushouts
32.95.
Retracts of sequential diagrams
32.96.
Rewriting rules for pushouts
32.97.
Sections of families over the circle
32.98.
Sections of descent data for pushouts
32.99.
Sequential colimits
32.100.
Sequential diagrams
32.101.
Sequentially compact types
32.102.
Shifts of sequential diagrams
32.103.
Smash products of pointed types
32.104.
Spectra
32.105.
The sphere prespectrum
32.106.
Spheres
32.107.
Suspension prespectra
32.108.
Suspension Structures
32.109.
Suspensions of pointed types
32.110.
Suspensions of types
32.111.
Tangent spheres
32.112.
Total cocones of type families over cocones under sequential diagrams
32.113.
Total sequential diagrams of dependent sequential diagrams
32.114.
Triple loop spaces
32.115.
k-acyclic maps
32.116.
k-acyclic types
32.117.
The universal cover of the circle
32.118.
The universal property of the circle
32.119.
The universal property of coequalizers
32.120.
The universal property of pushouts
32.121.
The universal property of sequential colimits
32.122.
Universal property of suspensions
32.123.
Universal Property of suspensions of pointed types
32.124.
Wedges of pointed types
32.125.
Zigzags between sequential diagrams
33.
Trees
❱
33.1.
Algebras for polynomial endofunctors
33.2.
Bases of directed trees
33.3.
Bases of enriched directed trees
33.4.
Binary W-types
33.5.
Bounded multisets
33.6.
The coalgebra of directed trees
33.7.
The coalgebra of enriched directed trees
33.8.
Coalgebras of polynomial endofunctors
33.9.
The combinator of directed trees
33.10.
Combinators of enriched directed trees
33.11.
Directed trees
33.12.
The elementhood relation on coalgebras of polynomial endofunctors
33.13.
The elementhood relation on W-types
33.14.
Empty multisets
33.15.
Enriched directed trees
33.16.
Equivalences of directed trees
33.17.
Equivalences of enriched directed trees
33.18.
Extensional W-types
33.19.
Fibers of directed trees
33.20.
Fibers of enriched directed trees
33.21.
Full binary trees
33.22.
Functoriality of the combinator of directed trees
33.23.
Functoriality of the fiber operation on directed trees
33.24.
Functoriality of W-types
33.25.
Hereditary W-types
33.26.
Indexed W-types
33.27.
Induction principles on W-types
33.28.
Inequality on W-types
33.29.
Lower types of elements in W-types
33.30.
Morphisms of algebras of polynomial endofunctors
33.31.
Morphisms of coalgebras of polynomial endofunctors
33.32.
Morphisms of directed trees
33.33.
Morphisms of enriched directed trees
33.34.
Multiset-indexed dependent products of types
33.35.
Multisets
33.36.
Planar binary trees
33.37.
Plane trees
33.38.
Polynomial endofunctors
33.39.
Raising universe levels of directed trees
33.40.
Ranks of elements in W-types
33.41.
Rooted morphisms of directed trees
33.42.
Rooted morphisms of enriched directed trees
33.43.
Rooted quasitrees
33.44.
Rooted undirected trees
33.45.
Small multisets
33.46.
Submultisets
33.47.
Transitive multisets
33.48.
The underlying trees of elements of coalgebras of polynomial endofunctors
33.49.
The underlying trees of elements of W-types
33.50.
Undirected trees
33.51.
The universal multiset
33.52.
The universal tree
33.53.
The W-type of natural numbers
33.54.
The W-type of the type of propositions
33.55.
W-types
34.
Type theories
❱
34.1.
Comprehension of fibered type theories
34.2.
Dependent type theories
34.3.
Fibered dependent type theories
34.4.
Π-types in precategories with attributes
34.5.
Π-types in precategories with families
34.6.
Precategories with attributes
34.7.
Precategories with families
34.8.
Sections of dependent type theories
34.9.
Simple type theories
34.10.
Unityped type theories
35.
Univalent combinatorics
❱
35.1.
2-element decidable subtypes
35.2.
2-element subtypes
35.3.
2-element types
35.4.
The binomial types
35.5.
Bracelets
35.6.
Cartesian products of finite types
35.7.
The classical definition of the standard finite types
35.8.
Complements of isolated elements of finite types
35.9.
Coproducts of finite types
35.10.
Counting in type theory
35.11.
Counting the elements of decidable subtypes
35.12.
Counting the elements of dependent pair types
35.13.
Counting the elements of the fiber of a map
35.14.
Counting the elements in Maybe
35.15.
Cubes
35.16.
Cycle partitions of finite types
35.17.
Cycle prime decompositions of natural numbers
35.18.
Cyclic finite types
35.19.
Decidable dependent function types
35.20.
Decidability of dependent pair types
35.21.
Decidable equivalence relations on finite types
35.22.
Decidable propositions
35.23.
Decidable subtypes of finite types
35.24.
Dedekind finite sets
35.25.
Counting the elements of dependent function types
35.26.
Dependent pair types of finite types
35.27.
Finite discrete Σ-decompositions
35.28.
Distributivity of set truncation over finite products
35.29.
Double counting
35.30.
Injective maps
35.31.
Embeddings between standard finite types
35.32.
Equality in finite types
35.33.
Equality in the standard finite types
35.34.
Equivalences between finite types
35.35.
Equivalences of cubes
35.36.
Equivalences between standard finite types
35.37.
Ferrers diagrams (unlabeled partitions)
35.38.
Fibers of maps between finite types
35.39.
Finite choice
35.40.
Finiteness of the type of connected components
35.41.
Finite presentations of types
35.42.
Finite types
35.43.
Finitely presented types
35.44.
Finite function types
35.45.
The image of a map
35.46.
Inequality on types equipped with a counting
35.47.
Inhabited finite types
35.48.
Injective maps between finite types
35.49.
An involution on the standard finite types
35.50.
Isotopies of Latin squares
35.51.
Kuratowsky finite sets
35.52.
Latin squares
35.53.
The groupoid of main classes of Latin hypercubes
35.54.
The groupoid of main classes of Latin squares
35.55.
The maybe modality on finite types
35.56.
Necklaces
35.57.
Orientations of the complete undirected graph
35.58.
Orientations of cubes
35.59.
Partitions of finite types
35.60.
Petri-nets
35.61.
π-finite types
35.62.
The pigeonhole principle
35.63.
Finitely π-presented types
35.64.
Quotients of finite types
35.65.
Ramsey theory
35.66.
Repetitions of values
35.67.
Repetitions of values in sequences
35.68.
Retracts of finite types
35.69.
Sequences of elements in finite types
35.70.
Set quotients of index 2
35.71.
Finite Σ-decompositions of finite types
35.72.
Skipping elements in standard finite types
35.73.
Small types
35.74.
Standard finite pruned trees
35.75.
Standard finite trees
35.76.
The standard finite types
35.77.
Steiner systems
35.78.
Steiner triple systems
35.79.
Combinatorial identities of sums of natural numbers
35.80.
Surjective maps between finite types
35.81.
Symmetric difference of finite subtypes
35.82.
Finite trivial Σ-decompositions
35.83.
Type duality of finite types
35.84.
Unions of finite subtypes
35.85.
The universal property of the standard finite types
35.86.
Unlabeled partitions
35.87.
Unlabeled rooted trees
35.88.
Unlabeled trees
36.
Universal algebra
❱
36.1.
Abstract equations over signatures
36.2.
Algebraic theories
36.3.
Algebraic theory of groups
36.4.
Algebras
36.5.
Congruences
36.6.
Homomorphisms of algebras
36.7.
Kernels of homomorphisms of algebras
36.8.
Models of signatures
36.9.
Quotient algebras
36.10.
Signatures
36.11.
Terms over signatures
37.
Wild category theory
❱
37.1.
Colax functors between large noncoherent wild higher precategories
37.2.
Colax functors between noncoherent wild higher precategories
37.3.
Isomorphisms in noncoherent large wild higher precategories
37.4.
Isomorphisms in noncoherent wild higher precategories
37.5.
Maps between noncoherent large wild higher precategories
37.6.
Maps between noncoherent wild higher precategories
37.7.
Noncoherent large wild higher precategories
37.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