Overview
1.
Overview
❱
1.1.
Home
1.2.
Community
❱
1.2.1.
Maintainers
1.2.2.
Contributors
1.2.3.
Statement of inclusivity
1.2.4.
Projects using Agda-Unimath
1.2.5.
Grant acknowledgements
1.3.
Guides
❱
1.3.1.
Installing the library
1.3.2.
Design principles
1.3.3.
Contributing to the library
1.3.4.
Structuring your file
❱
1.3.4.1.
File template
1.3.5.
The library coding style
1.3.6.
Guidelines for mixfix operators
1.3.7.
Citing the library
1.4.
Library contents
1.5.
Art
The agda-unimath library
2.
Category theory
❱
2.1.
Adjunctions between large precategories
2.2.
Anafunctors between categories
2.3.
Anafunctors between precategories
2.4.
Categories
2.5.
Coproducts in precategories
2.6.
Dependent products of categories
2.7.
Dependent products of precategories
2.8.
Discrete categories
2.9.
Endomorphisms in categories
2.10.
Endomorphisms in precategories
2.11.
Epimorphism in large precategories
2.12.
Equivalences between categories
2.13.
Equivalences between large precategories
2.14.
Equivalences between precategories
2.15.
Exponential objects in precategories
2.16.
Function categories
2.17.
Function precategories
2.18.
Functors between categories
2.19.
Functors between large precategories
2.20.
Functors between precategories
2.21.
Groupoids
2.22.
Homotopies of natural transformations in large precategories
2.23.
Initial objects of a precategory
2.24.
Isomorphisms in categories
2.25.
Isomorphisms in large precategories
2.26.
Isomorphisms in precategories
2.27.
Large categories
2.28.
Large precategories
2.29.
Monomorphisms in large precategories
2.30.
Natural isomorphisms between functors between categories
2.31.
Natural isomorphisms between functors on large precategories
2.32.
Natural isomorphisms between functors between precategories
2.33.
Natural numbers object in a precategory
2.34.
Natural transformations between functors between categories
2.35.
Natural transformations between functors between large precategories
2.36.
Natural transformations between functors on precategories
2.37.
One object precategories
2.38.
Opposite precategories
2.39.
Precategories
2.40.
The precategory of functors and natural transformations between two fixed precategories
2.41.
Pregroupoids
2.42.
Products in precategories
2.43.
Products of precategories
2.44.
Pullbacks in precategories
2.45.
Representable functors between categories
2.46.
Representable functors between precategories
2.47.
Sieves in categories
2.48.
Slice precategories
2.49.
Terminal object of a precategory
2.50.
The Yoneda lemma for categories
2.51.
The Yoneda lemma for precategories
3.
Commutative algebra
❱
3.1.
The binomial theorem in commutative rings
3.2.
The binomial theorem in commutative semirings
3.3.
Boolean rings
3.4.
The category of commutative rings
3.5.
Commutative rings
3.6.
Commutative semirings
3.7.
Dependent products of commutative rings
3.8.
Dependent products of commutative semirings
3.9.
Discrete fields
3.10.
The Eisenstein integers
3.11.
Euclidean domains
3.12.
Full ideals of commutative rings
3.13.
Function commutative rings
3.14.
Function commutative semirings
3.15.
The Gaussian integers
3.16.
Homomorphisms of commutative rings
3.17.
Homomorphisms of commutative semirings
3.18.
Ideals of commutative rings
3.19.
Ideals of commutative semirings
3.20.
Ideals generated by subsets of commutative rings
3.21.
Integer multiples of elements of commutative rings
3.22.
Integral domains
3.23.
Intersections of ideals of commutative rings
3.24.
Intersections of radical ideals of commutative rings
3.25.
Invertible elements in commutative rings
3.26.
Isomorphisms of commutative rings
3.27.
Joins of ideals of commutative rings
3.28.
Joins of radical ideals of commutative rings
3.29.
Local commutative rings
3.30.
Maximal ideals of commutative rings
3.31.
Multiples of elements in commutative rings
3.32.
Nilradical of a commutative ring
3.33.
The nilradical of a commutative semiring
3.34.
The poset of ideals of a commutative ring
3.35.
The poset of radical ideals of a commutative ring
3.36.
Powers of elements in commutative rings
3.37.
Powers of elements in commutative semirings
3.38.
The precategory of commutative rings
3.39.
The precategory of commutative semirings
3.40.
Prime ideals of commutative rings
3.41.
Products of commutative rings
3.42.
Products of ideals of commutative rings
3.43.
Products of radical ideals of a commutative ring
3.44.
Products of subsets of commutative rings
3.45.
Radical ideals of commutative rings
3.46.
Radical ideals generated by subsets of commutative rings
3.47.
Radicals of ideals of commutative rings
3.48.
Subsets of commutative rings
3.49.
Subsets of commutative semirings
3.50.
Sums in commutative rings
3.51.
Sums in commutative semirings
3.52.
Transporting commutative ring structures along isomorphisms of abelian groups
3.53.
Trivial commutative rings
3.54.
The Zariski locale
3.55.
The Zariski topology on the set of prime ideals of a commutative ring
4.
Elementary number theory
❱
4.1.
The absolute value function on the integers
4.2.
The Ackermann function
4.3.
Addition on integer fractions
4.4.
Addition on the integers
4.5.
Addition on the natural numbers
4.6.
Addition on the rational numbers
4.7.
Arithmetic functions
4.8.
The based induction principle of the natural numbers
4.9.
Based strong induction for the natural numbers
4.10.
Bezout's lemma in the integers
4.11.
Bezout's lemma on the natural numbers
4.12.
The binomial coefficients
4.13.
The binomial theorem for the integers
4.14.
The binomial theorem for the natural numbers
4.15.
Bounded sums of arithmetic functions
4.16.
Catalan numbers
4.17.
The cofibonacci sequence
4.18.
The Collatz bijection
4.19.
The Collatz conjecture
4.20.
The commutative ring of integers
4.21.
The commutative semiring of natural numbers
4.22.
The congruence relations on the integers
4.23.
The congruence relations on the natural numbers
4.24.
Decidable dependent function types
4.25.
Natural numbers are a total decidable poset
4.26.
Decidable types in elementary number theory
4.27.
The difference between integers
4.28.
Dirichlet convolution
4.29.
The distance between integers
4.30.
The distance between natural numbers
4.31.
Divisibility of integers
4.32.
Divisibility in modular arithmetic
4.33.
Divisibility of natural numbers
4.34.
The divisibility relation on the standard finite types
4.35.
Equality of integers
4.36.
Equality of natural numbers
4.37.
Euclidean division on the natural numbers
4.38.
Euler's totient function
4.39.
Exponentiation of natural numbers
4.40.
Factorials of natural numbers
4.41.
Falling factorials
4.42.
The Fibonacci sequence
4.43.
The natural numbers base k
4.44.
Finitely cyclic maps
4.45.
The fundamental theorem of arithmetic
4.46.
The Goldbach conjecture
4.47.
The greatest common divisor of integers
4.48.
The greatest common divisor of natural numbers
4.49.
The group of integers
4.50.
The groups ℤ/kℤ
4.51.
The half-integers
4.52.
Inequality on integer fractions
4.53.
Inequality on the integers
4.54.
Inequality of natural numbers
4.55.
Inequality on the rational numbers
4.56.
Inequality on the standard finite types
4.57.
The infinitude of primes
4.58.
Initial segments of the natural numbers
4.59.
Integer fractions
4.60.
Integer partitions
4.61.
The integers
4.62.
The Kolakoski sequence
4.63.
Lower bounds of type families over the natural numbers
4.64.
Maximum on the natural numbers
4.65.
Maximum on the standard finite types
4.66.
Mersenne primes
4.67.
Minimum on the natural numbers
4.68.
Minimum on the standard finite types
4.69.
Modular arithmetic
4.70.
Modular arithmetic on the standard finite types
4.71.
The monoid of natural numbers with addition
4.72.
The monoid of the natural numbers with maximum
4.73.
Multiplication on integer fractions
4.74.
Multiplication of integers
4.75.
Multiplication of the elements of a list of natural numbers
4.76.
Multiplication of natural numbers
4.77.
Multiplication on the rational numbers
4.78.
Multiset coefficients
4.79.
The type of natural numbers
4.80.
Nonzero natural numbers
4.81.
The ordinal induction principle for the natural numbers
4.82.
Parity of the natural numbers
4.83.
Pisano periods
4.84.
Powers of integers
4.85.
Powers of two
4.86.
Prime numbers
4.87.
Products of natural numbers
4.88.
Proper divisors of natural numbers
4.89.
Pythagorean triples
4.90.
The rational numbers
4.91.
Reduced integer fractions
4.92.
Relatively prime integers
4.93.
Relatively prime natural numbers
4.94.
Repeating an element in a standard finite type
4.95.
Retracts of the type of natural numbers
4.96.
The sieve of Eratosthenes
4.97.
Square-free natural numbers
4.98.
Stirling numbers of the second kind
4.99.
Strict inequality natural numbers
4.100.
Strictly ordered pairs of natural numbers
4.101.
The strong induction principle for the natural numbers
4.102.
Sums of natural numbers
4.103.
Telephone numbers
4.104.
The triangular numbers
4.105.
The Twin Prime conjecture
4.106.
Type arithmetic with natural numbers
4.107.
Unit elements in the standard finite types
4.108.
Unit similarity on the standard finite types
4.109.
The universal property of the integers
4.110.
The universal property of the natural numbers
4.111.
Upper bounds for type families over the natural numbers
4.112.
The Well-Ordering Principle of the natural numbers
4.113.
The well-ordering principle of the standard finite types
5.
Finite algebra
❱
5.1.
Commutative finite rings
5.2.
Dependent products of commutative finit rings
5.3.
Dependent products of finite rings
5.4.
Abelian groups
5.5.
Finite Commutative monoids
5.6.
Finite fields
5.7.
Abstract finite groups
5.8.
Finite monoids
5.9.
Finite rings
5.10.
Finite semigroups
5.11.
Homomorphisms of commutative finite rings
5.12.
Homomorphisms of finite rings
5.13.
Products of commutative finite rings
5.14.
Products of finite rings
5.15.
Semisimple commutative finite rings
6.
Finite group theory
❱
6.1.
The abstract quaternion group of order 8
6.2.
Alternating concrete groups
6.3.
Alternating groups
6.4.
Cartier's delooping of the sign homomorphism
6.5.
The concrete quaternion group
6.6.
Deloopings of the sign homomorphism
6.7.
Finite groups
6.8.
Finite monoids
6.9.
Finite semigroups
6.10.
The group of n-element types
6.11.
Groups of order 2
6.12.
Orbits of permutations
6.13.
Permutations
6.14.
Permutations of standard finite types
6.15.
The sign homomorphism
6.16.
Simpson's delooping of the sign homomorphism
6.17.
Subgroups of finite groups
6.18.
Tetrahedra in 3-dimensional space
6.19.
Transpositions
6.20.
Transpositions of standard finite types
7.
Foundation
❱
7.1.
0-Connected types
7.2.
0-Images of maps
7.3.
0-Maps
7.4.
1-Types
7.5.
2-Types
7.6.
Action on equivalences of functions
7.7.
The action on equivalences of functions out of subuniverses
7.8.
Action on equivalences of type families
7.9.
Action on equivalences in type families over subuniverses
7.10.
The binary action on identifications of binary functions
7.11.
The action on identifications of dependent functions
7.12.
The action on identifications of functions
7.13.
Apartness relations
7.14.
Arithmetic law for coproduct decomposition and Σ-decomposition
7.15.
Arithmetic law for product decomposition and Π-decomposition
7.16.
Automorphisms
7.17.
Axiom L
7.18.
The axiom of choice
7.19.
Bands
7.20.
Binary embeddings
7.21.
Binary equivalences
7.22.
Binary equivalences on unordered pairs of types
7.23.
Binary functoriality of set quotients
7.24.
Homotopies of binary operations
7.25.
Binary operations on unordered pairs of types
7.26.
Binary reflecting maps of equivalence relations
7.27.
Binary relations
7.28.
Binary transport
7.29.
The booleans
7.30.
The Cantor–Schröder–Bernstein–Escardó theorem
7.31.
Cantor's diagonal argument
7.32.
Cartesian product types
7.33.
Cartesian products of set quotients
7.34.
The category of sets
7.35.
Choice of representatives for an equivalence relation
7.36.
Coherently invertible maps
7.37.
Commuting 3-simplices of homotopies
7.38.
Commuting 3-simplices of maps
7.39.
Commuting cubes of maps
7.40.
Commuting hexagons of identifications
7.41.
Commuting squares of identifications
7.42.
Commuting squares of maps
7.43.
Commuting triangles of homotopies
7.44.
Commuting triangles of maps
7.45.
Complements of type families
7.46.
Complements of subtypes
7.47.
Cones over cospans
7.48.
Conjunction of propositions
7.49.
Connected components of types
7.50.
Connected components of universes
7.51.
Connected maps
7.52.
Connected types
7.53.
Constant maps
7.54.
Constant type families
7.55.
Contractible maps
7.56.
Contractible types
7.57.
Coproduct decompositions
7.58.
Coproduct decompositions in a subuniverse
7.59.
Coproduct types
7.60.
Morphisms in the coslice category of types
7.61.
Cospans of types
7.62.
Decidability of dependent function types
7.63.
Decidability of dependent pair types
7.64.
Decidable embeddings
7.65.
Decidable equality
7.66.
Decidable equivalence relations
7.67.
Decidable maps
7.68.
Decidable propositions
7.69.
Decidable relations on types
7.70.
Decidable subtypes
7.71.
Decidable types
7.72.
The dependent binomial theorem for types (distributivity of dependent function types over coproduct types)
7.73.
Dependent identifications
7.74.
Dependent pair types
7.75.
Descent for coproduct types
7.76.
Descent for dependent pair types
7.77.
Descent for the empty type
7.78.
Descent for equivalences
7.79.
Diagonal maps of types
7.80.
Diagonals of maps
7.81.
Discrete reflexive relations
7.82.
Discrete relaxed Σ-decompositions
7.83.
Discrete Σ-decompositions
7.84.
Discrete types
7.85.
Disjunction of propositions
7.86.
Double negation
7.87.
The double negation modality
7.88.
Double powersets
7.89.
Dubuc-Penon compact types
7.90.
Effective maps for equivalence relations
7.91.
Embeddings
7.92.
Empty types
7.93.
Endomorphisms
7.94.
Epimorphisms
7.95.
Epimorphisms with respect to maps into sets
7.96.
Epimorphisms with respect to truncated types
7.97.
Equality of cartesian product types
7.98.
Equality of coproduct types
7.99.
Equality on dependent function types
7.100.
Equality of dependent pair types
7.101.
Equality in the fibers of a map
7.102.
Equivalence classes
7.103.
Equivalence extensionality
7.104.
Equivalence induction
7.105.
Equivalence relations
7.106.
Equivalences
7.107.
Equivalences on Maybe
7.108.
Exclusive disjunction of propositions
7.109.
Existential quantification
7.110.
Exponents of set quotients
7.111.
Faithful maps
7.112.
Fiber inclusions
7.113.
Fibered equivalences
7.114.
Fibered involutions
7.115.
Maps fibered over a map
7.116.
Fibers of maps
7.117.
Full subtypes of types
7.118.
Function extensionality
7.119.
Function types
7.120.
Functional correspondences
7.121.
Functoriality of cartesian product types
7.122.
Functoriality of coproduct types
7.123.
Functoriality of dependent function types
7.124.
Functoriality of dependent pair types
7.125.
The functoriality of fiber
7.126.
Functoriality of function types
7.127.
Functoriality of propositional truncations
7.128.
Functoriality of set quotients
7.129.
Functoriality of set truncation
7.130.
Functoriality of truncations
7.131.
The fundamental theorem of identity types
7.132.
Global choice
7.133.
Hilbert's ε-operators
7.134.
Homotopies
7.135.
Homotopy induction
7.136.
Identity systems
7.137.
Identity types of truncated types
7.138.
Identity types
7.139.
The image of a map
7.140.
Images of subtypes
7.141.
Impredicative encodings of the logical operations
7.142.
Impredicative universes
7.143.
The induction principle for propositional truncation
7.144.
Inhabited subtypes
7.145.
Inhabited types
7.146.
Injective maps
7.147.
The interchange law
7.148.
Intersections of subtypes
7.149.
Invertible maps
7.150.
Involutions
7.151.
Isolated points
7.152.
Isomorphisms of sets
7.153.
Iterated cartesian product types
7.154.
Iterating automorphisms
7.155.
Iterating functions
7.156.
Iterating involutions
7.157.
Large binary relations
7.158.
Large dependent pair types
7.159.
Large homotopies
7.160.
Large identity types
7.161.
The large locale of propositions
7.162.
The large locale of subtypes
7.163.
The law of excluded middle
7.164.
Lawvere's fixed point theorem
7.165.
The lesser limited principle of omniscience
7.166.
The limited principle of omniscience
7.167.
Locally small types
7.168.
Logical equivalences
7.169.
The maybe modality
7.170.
Mere embeddings
7.171.
Mere equality
7.172.
Mere equivalences
7.173.
Monomorphisms
7.174.
Morphisms of cospans
7.175.
Multisubsets
7.176.
Multivariable correspondences
7.177.
Multivariable decidable relations
7.178.
Multivariable functoriality of set quotients
7.179.
Multivariable operations
7.180.
Multivariable relations
7.181.
Negation
7.182.
Non-contractible types
7.183.
Pairs of distinct elements
7.184.
Partial elements
7.185.
Partitions
7.186.
Path algebra
7.187.
Path-split maps
7.188.
Perfect images
7.189.
Π-decompositions of types
7.190.
Π-decompositions of types into types in a subuniverse
7.191.
Pointed torsorial type families
7.192.
Powersets
7.193.
Preidempotent maps
7.194.
Preimages of subtypes
7.195.
The principle of omniscience
7.196.
Product decompositions
7.197.
Product decompositions of types in a subuniverse
7.198.
Products of binary relations
7.199.
Products of equivalence relataions
7.200.
Products of tuples of types
7.201.
Products of unordered pairs of types
7.202.
Products of unordered tuples of types
7.203.
Projective types
7.204.
Proper subsets
7.205.
Propositional extensionality
7.206.
Propositional maps
7.207.
Propositional resizing
7.208.
Propositional truncations
7.209.
Propositions
7.210.
Pullback squares
7.211.
Pullbacks
7.212.
Raising universe levels
7.213.
Reflecting maps for equivalence relations
7.214.
Reflexive relations
7.215.
Relaxed Σ-decompositions of types
7.216.
Repetitions of values of maps
7.217.
Repetitions in sequences
7.218.
The replacement axiom for type theory
7.219.
Retractions
7.220.
Russell's paradox
7.221.
Sections
7.222.
Sequences
7.223.
Set presented types
7.224.
Set quotients
7.225.
Set truncations
7.226.
Sets
7.227.
Shifting sequences
7.228.
Σ-closed subuniverses
7.229.
Σ-decompositions of types into types in a subuniverse
7.230.
Σ-decompositions of types
7.231.
Singleton induction
7.232.
Singleton subtypes
7.233.
Morphisms in the slice category of types
7.234.
Small maps
7.235.
Small types
7.236.
Small universes
7.237.
Sorial type families
7.238.
Spans of types
7.239.
Split surjective maps
7.240.
Standard apartness relations
7.241.
Strongly extensional maps
7.242.
Structure
7.243.
The structure identity principle
7.244.
Structured type duality
7.245.
Subterminal types
7.246.
Subtype duality
7.247.
The subtype identity principle
7.248.
Subtypes
7.249.
Subuniverses
7.250.
Surjective maps
7.251.
Symmetric binary relations
7.252.
Symmetric cores of binary relations
7.253.
Symmetric difference of subtypes
7.254.
The symmetric identity types
7.255.
Symmetric operations
7.256.
Tight apartness relations
7.257.
Torsorial type families
7.258.
Transport along equivalences
7.259.
Transport along identifications
7.260.
Trivial relaxed Σ-decompositions
7.261.
Trivial Σ-decompositions
7.262.
Truncated equality
7.263.
Truncated maps
7.264.
Truncated types
7.265.
k-Equivalences
7.266.
Truncation images of maps
7.267.
Truncation levels
7.268.
The truncation modalities
7.269.
Truncations
7.270.
Tuples of types
7.271.
Type arithmetic with the booleans
7.272.
Type arithmetic for cartesian product types
7.273.
Type arithmetic for coproduct types
7.274.
Type arithmetic with dependent function types
7.275.
Type arithmetic for dependent pair types
7.276.
Type arithmetic with the empty type
7.277.
Type arithmetic with the unit type
7.278.
Type duality
7.279.
The type theoretic principle of choice
7.280.
Unions of subtypes
7.281.
Unique existence
7.282.
Uniqueness of the image of a map
7.283.
The uniqueness of set quotients
7.284.
Uniqueness of set truncations
7.285.
Uniqueness of the truncations
7.286.
The unit type
7.287.
Unital binary operations
7.288.
The univalence axiom
7.289.
The univalence axiom implies function extensionality
7.290.
Univalent type families
7.291.
The universal property of booleans
7.292.
The universal propert of cartesian product types
7.293.
The universal property of coproduct types
7.294.
The universal property of dependent pair types
7.295.
The universal property of the empty type
7.296.
The universal property of fiber products
7.297.
The universal property of identity systems
7.298.
The universal property of identity types
7.299.
The universal property of the image of a map
7.300.
The universal property of maybe
7.301.
The universal property of propositional truncations
7.302.
The universal property of propositional truncations with respect to sets
7.303.
The universal property of pullbacks
7.304.
The universal property of set quotients
7.305.
The universal property of set truncations
7.306.
The universal property of truncations
7.307.
The universal property of the unit type
7.308.
Universe levels
7.309.
Unordered pairs of elements in a type
7.310.
Unordered pairs of types
7.311.
Unordered n-tuples of elements in a type
7.312.
Unordered tuples of types
7.313.
Vectors of set quotients
7.314.
Weak function extensionality
7.315.
The weak limited principle of omniscience
7.316.
Weakly constant maps
7.317.
Whiskering homotopies
8.
Foundation core
❱
8.1.
1-Types
8.2.
Cartesian product types
8.3.
Coherently invertible maps
8.4.
Commuting squares of maps
8.5.
Commuting triangles of maps
8.6.
Constant maps
8.7.
Contractible maps
8.8.
Contractible types
8.9.
Coproduct types
8.10.
Decidable propositions
8.11.
Dependent identifications
8.12.
Diagonal maps of types
8.13.
Discrete types
8.14.
Embeddings
8.15.
Empty types
8.16.
Endomorphisms
8.17.
Equality of dependent pair types
8.18.
Equivalence induction
8.19.
Equivalence relations
8.20.
Equivalences
8.21.
Fibers of maps
8.22.
Function extensionality
8.23.
Function types
8.24.
Functoriality of dependent function types
8.25.
Functoriality of dependent pair types
8.26.
Functoriality of function types
8.27.
Homotopies
8.28.
Identity types
8.29.
Injective maps
8.30.
Invertible maps
8.31.
Negation
8.32.
Path-split maps
8.33.
Propositional maps
8.34.
Propositions
8.35.
Pullbacks
8.36.
Retractions
8.37.
Sections
8.38.
Sets
8.39.
Singleton induction
8.40.
Small types
8.41.
Subtypes
8.42.
Transport along identifications
8.43.
Truncated maps
8.44.
Truncated types
8.45.
Truncation levels
8.46.
The univalence axiom
8.47.
The universal property of pullbacks
8.48.
The universal property of truncations
8.49.
Whiskering homotopies
9.
Graph theory
❱
9.1.
Acyclic undirected graphs
9.2.
Circuits in undirected graphs
9.3.
Closed walks in undirected graphs
9.4.
Complete bipartite graphs
9.5.
Complete multipartite graphs
9.6.
Complete undirected graphs
9.7.
Connected graphs
9.8.
Cycles in undirected graphs
9.9.
Directed graph structures on standard finite sets
9.10.
Directed graphs
9.11.
Edge-coloured undirected graphs
9.12.
Embeddings of directed graphs
9.13.
Embeddings of undirected graphs
9.14.
Enriched undirected graphs
9.15.
Equivalences of directed graphs
9.16.
Equivalences of enriched undirected graphs
9.17.
Equivalences of undirected graphs
9.18.
Eulerian circuits in undirected graphs
9.19.
Faithful morphisms of undirected graphs
9.20.
Fibers of directed graphs
9.21.
Finite graphs
9.22.
Geometric realizations of undirected graphs
9.23.
Hypergraphs
9.24.
Matchings
9.25.
Mere equivalences of undirected graphs
9.26.
Morphisms of directed graphs
9.27.
Morphisms of undirected graphs
9.28.
Incidence in undirected graphs
9.29.
Orientations of undirected graphs
9.30.
Paths in undirected graphs
9.31.
Polygons
9.32.
Raising universe levels of directed graphs
9.33.
Reflecting maps of undirected graphs
9.34.
Reflexive graphs
9.35.
Regular undirected graph
9.36.
Simple undirected graphs
9.37.
Stereoisomerism for enriched undirected graphs
9.38.
Totally faithful morphisms of undirected graphs
9.39.
Trails in directed graphs
9.40.
Trails in undirected graphs
9.41.
Undirected graph structures on standard finite sets
9.42.
Undirected graphs
9.43.
Vertex covers
9.44.
Voltage graphs
9.45.
Walks in directed graphs
9.46.
Walks in undirected graphs
10.
Group theory
❱
10.1.
Abelian groups
10.2.
Pointwise addition of morphisms of abelian groups
10.3.
Automorphism groups
10.4.
Cartesian products of abelian groups
10.5.
Cartesian products of concrete groups
10.6.
Cartesian products of groups
10.7.
Cartesian products of monoids
10.8.
Cartesian products of semigroups
10.9.
The category of concrete groups
10.10.
The category of groups
10.11.
The category of semigroups
10.12.
Cayley's theorem
10.13.
The center of a group
10.14.
Center of a monoid
10.15.
Center of a semigroup
10.16.
Central elements of groups
10.17.
Central elements of monoids
10.18.
Central elements of semirings
10.19.
Centralizer subgroups
10.20.
Commutative monoids
10.21.
Commutators of elements in groups
10.22.
Commuting elements of groups
10.23.
Commuting elements of monoids
10.24.
Commuting elements of semigroups
10.25.
Concrete group actions
10.26.
Concrete groups
10.27.
Concrete monoids
10.28.
Congruence relations on abelian groups
10.29.
Congruence relations on commutative monoids
10.30.
Congruence relations on groups
10.31.
Congruence relations on monoids
10.32.
Congruence relations on semigroups
10.33.
Conjugation in groups
10.34.
Conjugation on concrete groups
10.35.
Contravariant pushforwards of concrete group actions
10.36.
Core of a monoid
10.37.
Cyclic groups
10.38.
Decidable subgroups of groups
10.39.
Dependent products of abelian groups
10.40.
Dependent products of commutative monoids
10.41.
Dependent products of groups
10.42.
Dependent products of monoids
10.43.
Dependent products of semigroups
10.44.
The dihedral group construction
10.45.
The dihedral groups
10.46.
The E₈-lattice
10.47.
Embeddings of abelian groups
10.48.
Embeddings of groups
10.49.
The endomorphism rings of abelian groups
10.50.
Epimorphisms in groups
10.51.
Equivalences of concrete group actions
10.52.
Equivalences of concrete groups
10.53.
Equivalences of group actions
10.54.
Equivalences between semigroups
10.55.
Free concrete group actions
10.56.
Free groups with one generator
10.57.
The full subgroup of a group
10.58.
Function groups of abelian groups
10.59.
Function commutative monoids
10.60.
Function groups
10.61.
Function monoids
10.62.
Function semigroups
10.63.
Furstenberg groups
10.64.
Generating elements of groups
10.65.
Generating sets of groups
10.66.
Group actions
10.67.
Abstract groups
10.68.
Homomorphisms of abelian groups
10.69.
Homomorphisms of commutative monoids
10.70.
Morphisms of concrete group actions
10.71.
Homomorphisms of concrete groups
10.72.
Homomorphisms of generated subgroups
10.73.
Homomorphisms of group actions
10.74.
Homomorphisms of groups
10.75.
Homomorphisms of monoids
10.76.
Homomorphisms of semigroups
10.77.
Images of group homomorphisms
10.78.
Integer multiples of elements in abelian groups
10.79.
Integer powers of elements of groups
10.80.
Intersections of subgroups of abelian groups
10.81.
Intersections of subgroups of groups
10.82.
Inverse semigroups
10.83.
Invertible elements in monoids
10.84.
Isomorphisms of abelian groups
10.85.
Isomorphisms of concrete groups
10.86.
Isomorphisms of group actions
10.87.
Isomorphisms of groups
10.88.
Isomorphisms of semigroups
10.89.
Iterated cartesian products of concrete groups
10.90.
Kernels
10.91.
Kernels of homomorphisms of concrete groups
10.92.
Large semigroups
10.93.
Concrete automorphism groups on sets
10.94.
Mere equivalences of concrete group actions
10.95.
Mere equivalences of group actions
10.96.
Monoid actions
10.97.
Monoids
10.98.
Monomorphisms of concrete groups
10.99.
Monomorphisms in the category of groups
10.100.
Multiples of elements in abelian groups
10.101.
Normal closures of subgroups
10.102.
Normal cores of subgroups
10.103.
Normal subgroups
10.104.
Normal subgroups of concrete groups
10.105.
Normal submonoids
10.106.
Normal submonoids of commutative monoids
10.107.
Normalizer subgroups
10.108.
The opposite of a group
10.109.
The orbit-stabilizer theorem for concrete groups
10.110.
Orbits of concrete group actions
10.111.
Orbits of group actions
10.112.
The precategory of orbits of a monoid action
10.113.
The order of an element in a group
10.114.
Powers of elements in commutative monoids
10.115.
Powers of elements in groups
10.116.
Powers of elements in monoids
10.117.
The precategory of abelian groups
10.118.
The precategory of commutative monoids
10.119.
The precategory of concrete groups
10.120.
The precategory of group actions
10.121.
The precategory of groups
10.122.
The precategory of monoids
10.123.
The precategory of semigroups
10.124.
Principal group actions
10.125.
Principal torsors of concrete groups
10.126.
Products of elements in a monoid
10.127.
Products of tuples of elements in commutative monoids
10.128.
Quotient groups
10.129.
Quotient groups of concrete groups
10.130.
Quotients of abelian groups
10.131.
Rational commutative monoids
10.132.
Representations of monoids in precategories
10.133.
Saturated congruence relations on commutative monoids
10.134.
Saturated congruence relations on monoids
10.135.
Semigroups
10.136.
Sheargroups
10.137.
Shriek of concrete group homomorphisms
10.138.
Stabilizer groups
10.139.
Stabilizers of concrete group actions
10.140.
Subgroups
10.141.
Subgroups of abelian groups
10.142.
Subgroups of concrete groups
10.143.
Subgroups generated by elements of a group
10.144.
Subgroups generated by subsets of groups
10.145.
Submonoids
10.146.
Submonoids of commutative monoids
10.147.
Subsemigroups
10.148.
Subsets of abelian groups
10.149.
Subsets of commutative monoids
10.150.
Subsets of groups
10.151.
Subsets of monoids
10.152.
The substitution functor of concrete group actions
10.153.
The substitution functor of group actions
10.154.
Surjective group homomorphisms
10.155.
Symmetric concrete groups
10.156.
Symmetric groups
10.157.
Torsors of abstract groups
10.158.
Transitive concrete group actions
10.159.
Transitive group actions
10.160.
Trivial concrete groups
10.161.
Trivial group homomorphisms
10.162.
Trivial subgroups
10.163.
Unordered tuples of elements in commutative monoids
10.164.
Wild representations of monoids
11.
Higher group theory
❱
11.1.
Cartesian products of higher groups
11.2.
Conjugation in higher groups
11.3.
Cyclic higher groups
11.4.
Equivalences of higher groups
11.5.
Fixed points of higher group actions
11.6.
Free higher group actions
11.7.
Higher group actions
11.8.
Higher groups
11.9.
Homomorphisms of higher group actions
11.10.
Homomorphisms of higher groups
11.11.
The higher group of integers
11.12.
Iterated cartesian products of higher groups
11.13.
Orbits of higher group actions
11.14.
Subgroups of higher groups
11.15.
Symmetric higher groups
11.16.
Trivial higher groups
12.
Linear algebra
❱
12.1.
Constant matrices
12.2.
Diagonal vectors
12.3.
Diagonal matrices on rings
12.4.
Functoriality of matrices
12.5.
Functoriality of the type of vectors
12.6.
Matrices
12.7.
Matrices on rings
12.8.
Multiplication of matrices
12.9.
Scalar multiplication on matrices
12.10.
Scalar multiplication of vectors
12.11.
Scalar multiplication of vectors on rings
12.12.
Transposition of matrices
12.13.
Vectors
12.14.
Vectors on commutative rings
12.15.
Vectors on commutative semirings
12.16.
Vectors on euclidean domains
12.17.
Vectors on rings
12.18.
Vectors on semirings
13.
Lists
❱
13.1.
Arrays
13.2.
Concatenation of lists
13.3.
Flattening of lists
13.4.
Functoriality of the list operation
13.5.
Lists
13.6.
Lists of elements in discrete types
13.7.
Permutations of lists
13.8.
Permutations of vectors
13.9.
Predicates on lists
13.10.
Quicksort for lists
13.11.
Reversing lists
13.12.
Sort by insertion for lists
13.13.
Sort by insertion for vectors
13.14.
Sorted lists
13.15.
Sorted vectors
13.16.
Sorting algorithms for lists
13.17.
Sorting algorithms for vectors
13.18.
The universal property of lists with respect to wild monoids
14.
Online encyclopedia of integer sequences
❱
14.1.
Sequences of the online encyclopedia of integer sequences
15.
Order theory
❱
15.1.
Bottom elements in posets
15.2.
Bottom elements in preorders
15.3.
Chains in posets
15.4.
Chains in preorders
15.5.
Closure operators on large locales
15.6.
Closure operators on large posets
15.7.
Coverings in locales
15.8.
Decidable posets
15.9.
Decidable preorders
15.10.
Decidable subposets
15.11.
Decidable subpreorders
15.12.
Decidable total orders
15.13.
Decidable total preorders
15.14.
Dependent products of large frames
15.15.
Dependent products of large locales
15.16.
Dependent products of large meet-semilattices
15.17.
Dependent products of large posets
15.18.
Dependent products large preorders
15.19.
Dependent products of large suplattices
15.20.
Directed complete posets
15.21.
Directed families in posets
15.22.
Distributive lattices
15.23.
Finite coverings in locales
15.24.
Finite posets
15.25.
Finite preorders
15.26.
Finitely graded posets
15.27.
Frames
15.28.
Galois connections
15.29.
Galois connections between large posets
15.30.
Greatest lower bounds in large posets
15.31.
Greatest lower bounds in posets
15.32.
Homomorphisms of frames
15.33.
Homomorphisms of large frames
15.34.
Homomorphisms of large locales
15.35.
Homomorphisms of large meet-semilattices
15.36.
Homomorphisms of large suplattices
15.37.
Homomorphisms of meet-semilattices
15.38.
Homomorphisms of meet sup lattices
15.39.
Homomorphisms of suplattices
15.40.
Ideals in preorders
15.41.
Interval subposets
15.42.
Join-semilattices
15.43.
Large frames
15.44.
Large locales
15.45.
Large meet-semilattices
15.46.
Large meet-subsemilattices
15.47.
Large posets
15.48.
Large preorders
15.49.
Large quotient locales
15.50.
Large subframes
15.51.
Large subposets
15.52.
Large subpreorders
15.53.
Large subsuplattices
15.54.
Large suplattices
15.55.
Lattices
15.56.
Least upper bounds in large posets
15.57.
Least upper bounds in posets
15.58.
Locales
15.59.
Locally finite posets
15.60.
Lower bounds in large posets
15.61.
Lower bounds in posets
15.62.
Lower types in preorders
15.63.
Maximal chains in posets
15.64.
Maximal chains in preorders
15.65.
Meet-semilattices
15.66.
Meet-suplattices
15.67.
Nuclei on large locales
15.68.
Order preserving maps between large posets
15.69.
Order preserving maps between large preorders
15.70.
Order preserving maps on posets
15.71.
Order preserving maps on preorders
15.72.
Posets
15.73.
Powers of large locales
15.74.
Preorders
15.75.
Reflective Galois connections between large posets
15.76.
Similarity of elements in large posets
15.77.
Similarity of elements in large preorders
15.78.
Subposets
15.79.
Subpreorders
15.80.
Suplattices
15.81.
Top elements in large posets
15.82.
Top elements in posets
15.83.
Top elements in preorders
15.84.
Total orders
15.85.
Total preorders
15.86.
Upper bounds in large posets
15.87.
Upper bounds in posets
16.
Organic Chemistry
❱
16.1.
Alcohols
16.2.
Alkanes
16.3.
Alkenes
16.4.
Alkynes
16.5.
Ethane
16.6.
Hydrocarbons
16.7.
Methane
16.8.
Saturated carbons
17.
Orthogonal factorization systems
❱
17.1.
The closed modalities
17.2.
Extensions of maps
17.3.
Factorization operations
17.4.
Factorization operations into function classes
17.5.
Factorizations of maps
17.6.
Function classes
17.7.
Higher modalities
17.8.
The identity modality
17.9.
Lifting operations
17.10.
Lifting squares
17.11.
Lifts of maps
17.12.
Local families
17.13.
Local maps
17.14.
Local types
17.15.
Localizations at maps
17.16.
Localizations at subuniverses
17.17.
Locally small modal-operators
17.18.
Mere lifting properties
17.19.
Modal operators
17.20.
Null types
17.21.
The open modalities
17.22.
Orthogonal factorization systems
17.23.
Orthogonal maps
17.24.
The pullback-hom
17.25.
The raise modalities
17.26.
Reflective modalities
17.27.
Reflective subuniverses
17.28.
Separated types
17.29.
Σ-closed modalities
17.30.
Σ-closed reflective modalities
17.31.
Σ-closed reflective subuniverses
17.32.
Stable orthogonal factorization systems
17.33.
Uniquely eliminating modalities
17.34.
Wide function classes
17.35.
The zero modality
18.
Polytopes
❱
18.1.
Abstract polytopes
19.
Primitives
❱
19.1.
Characters
19.2.
Floats
19.3.
Machine integers
19.4.
Strings
20.
Real numbers
❱
20.1.
Dedekind real numbers
21.
Reflection
❱
21.1.
Abstractions
21.2.
Arguments
21.3.
Boolean reflection
21.4.
Definitions
21.5.
Fixity
21.6.
Group solver
21.7.
Literals
21.8.
Metavariables
21.9.
Names
21.10.
Precategory solver
21.11.
Terms
21.12.
The type checking monad
22.
Ring theory
❱
22.1.
Algebras over rings
22.2.
The binomial theorem for rings
22.3.
The binomial theorem for semirings
22.4.
The category of rings
22.5.
Central elements of rings
22.6.
Central elements of semirings
22.7.
Commuting elements of rings
22.8.
Congruence relations on rings
22.9.
Congruence relations on semirings
22.10.
Dependent products of rings
22.11.
Dependent products of semirings
22.12.
Division rings
22.13.
Full ideals of rings
22.14.
Function rings
22.15.
Function semirings
22.16.
Homomorphisms of rings
22.17.
Homomorphisms of semirings
22.18.
Ideals generated by subsets of rings
22.19.
Ideals of rings
22.20.
Ideals of semirings
22.21.
Idempotent elements in rings
22.22.
Integer multiples of elements of rings
22.23.
Intersections of ideals of rings
22.24.
Intersections of ideals of semirings
22.25.
The invariant basis property of rings
22.26.
Invertible elements in rings
22.27.
Isomorphisms of rings
22.28.
Joins of ideals of rings
22.29.
Joins of left ideals of rings
22.30.
Joins of right ideals of rings
22.31.
Left ideals generated by subsets of rings
22.32.
Left ideals of rings
22.33.
Local rings
22.34.
Localizations of rings
22.35.
Maximal ideals of rings
22.36.
Modules over rings
22.37.
Multiples of elements in rings
22.38.
Nil ideals of rings
22.39.
Nilpotent elements in rings
22.40.
Nilpotent elements in semirings
22.41.
Opposite rings
22.42.
The poset of ideals of a ring
22.43.
The poset of left ideals of a ring
22.44.
The poset of right ideals of a ring
22.45.
Powers of elements in rings
22.46.
Powers of elements in semirings
22.47.
The precategory of rings
22.48.
The precategory of semirings
22.49.
Products of ideals of rings
22.50.
Products of left ideals of rings
22.51.
Products of right ideals of rings
22.52.
Products of rings
22.53.
Products of subsets of rings
22.54.
Quotient rings
22.55.
Radical ideals of rings
22.56.
Right ideals generated by subsets of rings
22.57.
Right ideals of rings
22.58.
Rings
22.59.
Semirings
22.60.
Subsets of rings
22.61.
Subsets of semirings
22.62.
Sums of elements in rings
22.63.
Sums of elements in semirings
22.64.
Transporting ring structures along isomorphisms of abelian groups
22.65.
Trivial rings
23.
Set theory
❱
23.1.
Baire space
23.2.
Cantor space
23.3.
Cardinalities of sets
23.4.
Countable sets
23.5.
Cumulative hierarchy
23.6.
Infinite sets
23.7.
Uncountable sets
24.
Species
❱
24.1.
Cartesian exponents of species
24.2.
Cartesian products of species of types
24.3.
Cauchy composition of species of types
24.4.
Cauchy composition of species of types in a subuniverse
24.5.
Cauchy exponentials of species of types
24.6.
Cauchy exponentials of species of types in a subuniverse
24.7.
Cauchy products of species of types
24.8.
Cauchy products of species of types in a subuniverse
24.9.
Cauchy series of species of types
24.10.
Cauchy series of species of types in a subuniverse
24.11.
Composition of Cauchy series of species of types
24.12.
Composition of Cauchy series of species of types in subuniverses
24.13.
Coproducts of species of types
24.14.
Coproducts of species of types in subuniverses
24.15.
Cycle index series of species
24.16.
Derivatives of species
24.17.
Dirichlet exponentials of a species of types
24.18.
Dirichlet exponentials of species of types in a subuniverse
24.19.
Dirichlet products of species of types
24.20.
Dirichlet products of species of types in subuniverses
24.21.
Dirichlet series of species of finite inhabited types
24.22.
Dirichlet series of species of types
24.23.
Dirichlet series of species of types in subuniverses
24.24.
Equivalences of species of types
24.25.
Equivalences of species of types in subuniverses
24.26.
Exponential of Cauchy series of species of types
24.27.
Exponential of Cauchy series of species of types in subuniverses
24.28.
Hasse-Weil species
24.29.
Morphisms of finite species
24.30.
Morphisms of species of types
24.31.
Pointing of species of types
24.32.
The precategory of finite species
24.33.
Products of Cauchy series of species of types
24.34.
Products of Cauchy series of species of types in subuniverses
24.35.
Products of Dirichlet series of species of finite inhabited types
24.36.
Products of Dirichlet series of species of types
24.37.
Products of Dirichlet series of species of types in subuniverses
24.38.
Small Composition of species of finite inhabited types
24.39.
Small Cauchy composition of species types in subuniverses
24.40.
Species of finite inhabited types
24.41.
Species of finite types
24.42.
Species of inhabited types
24.43.
Species of types
24.44.
Species of types in subuniverses
24.45.
The unit of Cauchy composition of types
24.46.
The unit of Cauchy composition of species of types in subuniverses
24.47.
Unlabeled structures of finite species
25.
Structured types
❱
25.1.
Cartesian products of types equipped with endomorphisms
25.2.
Central H-spaces
25.3.
Commuting squares of pointed maps
25.4.
Conjugation of pointed types
25.5.
Constant maps of pointed types
25.6.
Contractible pointed types
25.7.
Dependent products of H-spaces
25.8.
Dependent products of pointed types
25.9.
Dependent products of wild monoids
25.10.
Equivalences of types equipped with endomorphisms
25.11.
Faithful pointed maps
25.12.
Fibers of pointed maps
25.13.
Finite multiplication in magmas
25.14.
Function H-spaces
25.15.
Function magmas
25.16.
Function wild monoids
25.17.
H-spaces
25.18.
The initial pointed type equipped with an automorphism
25.19.
The involutive type of H-space structures on a pointed type
25.20.
Involutive types
25.21.
Iterated cartesian products of types equipped with endomorphisms
25.22.
Iterated cartesian products of pointed types
25.23.
Magmas
25.24.
Mere equivalences of types equipped with endomorphisms
25.25.
Morphisms of H-spaces
25.26.
Morphisms of magmas
25.27.
Morphisms of types equipped with endomorphisms
25.28.
Morphisms of wild monoids
25.29.
Non-coherent H-spaces
25.30.
Pointed cartesian product types
25.31.
Pointed dependent functions
25.32.
Pointed dependent pair types
25.33.
Pointed equivalences
25.34.
Pointed families of types
25.35.
Pointed homotopies
25.36.
Pointed maps
25.37.
Pointed sections of pointed maps
25.38.
Pointed types
25.39.
Pointed types equipped with automorphisms
25.40.
The pointed unit type
25.41.
Symmetric elements of involutive types
25.42.
Symmetric H-spaces
25.43.
Types equipped with automorphisms
25.44.
Types equipped with endomorphisms
25.45.
Unpointed maps between pointed types
25.46.
Wild groups
25.47.
Wild loops
25.48.
Wild monoids
25.49.
Wild quasigroups
25.50.
Wild semigroups
26.
Synthetic homotopy theory
❱
26.1.
Formalization of the Symmetry book - 26 descent
26.2.
Formalization of the Symmetry book - 26 id pushout
26.3.
Formalization of the Symmetry book - 27 sequences
26.4.
Acyclic maps
26.5.
Acyclic types
26.6.
Cavallo's trick
26.7.
The circle
26.8.
Cocones under spans
26.9.
Cocones under spans of pointed types
26.10.
Cofibers
26.11.
Conjugation of loops
26.12.
Dependent cocones under spans
26.13.
The dependent pullback property of pushouts
26.14.
Dependent suspension structures
26.15.
The dependent universal property of pushouts
26.16.
Dependent universal property of suspensions
26.17.
The descent property of the circle
26.18.
Descent data for constant type families over the circle
26.19.
Descent data for families of dependent pair types over the circle
26.20.
Descent data for families of equivalence types over the circle
26.21.
Descent data for families of function types over the circle
26.22.
Subtypes of descent data for the circle
26.23.
Double loop spaces
26.24.
The flattening lemma for pushouts
26.25.
Free loops
26.26.
Functoriality of the loop space operation
26.27.
Groups of loops in 1-types
26.28.
Hatcher's acyclic type
26.29.
The induction principle of pushouts
26.30.
The infinite complex projective space
26.31.
Infinite cyclic types
26.32.
The interval
26.33.
Iterated loop spaces
26.34.
Join powers of types
26.35.
Joins of types
26.36.
Loop spaces
26.37.
The multiplication operation on the circle
26.38.
The plus-principle
26.39.
Powers of loops
26.40.
Prespectra
26.41.
The pullback property of pushouts
26.42.
Pushouts
26.43.
Pushouts of pointed types
26.44.
Sections of families over the circle
26.45.
Smash products of pointed types
26.46.
Spectra
26.47.
Spheres
26.48.
Suspension Structures
26.49.
Suspensions of pointed types
26.50.
Suspensions of types
26.51.
Triple loop spaces
26.52.
The universal cover of the circle
26.53.
The universal property of the circle
26.54.
The universal property of pushouts
26.55.
Universal property of suspensions
26.56.
Universal Property of suspensions of pointed types
26.57.
Wedges of pointed types
27.
Trees
❱
27.1.
Algebras for polynomial endofunctors
27.2.
Bases of directed trees
27.3.
Bases of enriched directed trees
27.4.
The coalgebra of directed trees
27.5.
The coalgebra of enriched directed trees
27.6.
Coalgebras of polynomial endofunctors
27.7.
The combinator of directed trees
27.8.
Combinators of enriched directed trees
27.9.
Directed trees
27.10.
The elementhood relation on coalgebras of polynomial endofunctors
27.11.
The elementhood relation on W-types
27.12.
Enriched directed trees
27.13.
Equivalences of directed trees
27.14.
Equivalences of enriched directed trees
27.15.
Extensional W-types
27.16.
Fibers of directed trees
27.17.
Fibers of enriched directed trees
27.18.
Functoriality of the combinator of directed trees
27.19.
Functoriality of the fiber operation on directed trees
27.20.
Functoriality of W-types
27.21.
Indexed W-types
27.22.
Induction principles on W-types
27.23.
Inequality on W-types
27.24.
Lower types of elements in W-types
27.25.
Morphisms of algebras of polynomial endofunctors
27.26.
Morphisms of coalgebras of polynomial endofunctors
27.27.
Morphisms of directed trees
27.28.
Morphisms of enriched directed trees
27.29.
Multisets
27.30.
Planar binary trees
27.31.
Polynomial endofunctors
27.32.
Raising universe levels of directed trees
27.33.
Ranks of elements in W-types
27.34.
Rooted morphisms of directed trees
27.35.
Rooted morphisms of enriched directed trees
27.36.
Rooted quasitrees
27.37.
Rooted undirected trees
27.38.
Small multisets
27.39.
Submultisets
27.40.
Transitive multisets
27.41.
The underlying trees of elements of coalgebras of polynomial endofunctors
27.42.
The underlying trees of elements of W-types
27.43.
Undirected rees
27.44.
The universal multiset
27.45.
The W-type of natural numbers
27.46.
The W-type of the type of propositions
27.47.
W-types
28.
Type theories
❱
28.1.
Comprehension of fibered type theories
28.2.
Dependent type theories
28.3.
Fibered dependent type theories
28.4.
Sections of dependent type theories
28.5.
Simple type theories
28.6.
Unityped type theories
29.
Univalent combinatorics
❱
29.1.
2-element decidable subtypes
29.2.
2-element subtypes
29.3.
2-element types
29.4.
The binomial types
29.5.
Bracelets
29.6.
Cartesian products of finite types
29.7.
The classical definition of the standard finite types
29.8.
Complements of isolated points of finite types
29.9.
Coproducts of finite types
29.10.
Counting in type theory
29.11.
Counting the elements of decidable subtypes
29.12.
Counting the elements of dependent pair types
29.13.
Counting the elements of the fiber of a map
29.14.
Counting the elements in Maybe
29.15.
Cubes
29.16.
Cycle partitions of finite types
29.17.
Cycle prime decompositions of natural numbers
29.18.
Cyclic types
29.19.
Decidable dependent function types
29.20.
Decidability of dependent pair types
29.21.
Decidable equivalence relations on finite types
29.22.
Decidable propositions
29.23.
Decidable subtypes of finite types
29.24.
Dedekind finite sets
29.25.
Counting the elements of dependent function types
29.26.
Dependent pair types of finite types
29.27.
Finite discrete Σ-decompositions
29.28.
Distributivity of set truncation over finite products
29.29.
Double counting
29.30.
Injective maps
29.31.
Embeddings between standard finite types
29.32.
Equality in finite types
29.33.
Equality in the standard finite types
29.34.
Equivalences between finite types
29.35.
Equivalences of cubes
29.36.
Equivalences between standard finite types
29.37.
Ferrers diagrams (unlabeled partitions)
29.38.
Fibers of maps between finite types
29.39.
Finite choice
29.40.
Finiteness of the type of connected components
29.41.
Finite presentations of types
29.42.
Finite types
29.43.
Finitely presented types
29.44.
Finite function types
29.45.
The image of a map
29.46.
Inequality on types equipped with a counting
29.47.
Inhabited finite types
29.48.
Injective maps between finite types
29.49.
An involution on the standard finite types
29.50.
Isotopies of Latin squares
29.51.
Kuratowsky finite sets
29.52.
Latin squares
29.53.
The groupoid of main classes of Latin hypercubes
29.54.
The groupoid of main classes of Latin squares
29.55.
The maybe modality on finite types
29.56.
Necklaces
29.57.
Orientations of the complete undirected graph
29.58.
Orientations of cubes
29.59.
Partitions of finite types
29.60.
Petri-nets
29.61.
π-finite types
29.62.
The pigeonhole principle
29.63.
Finitely π-presented types
29.64.
Quotients of finite types
29.65.
Ramsey theory
29.66.
Repetitions of values
29.67.
Repetitions of values in sequences
29.68.
Retracts of finite types
29.69.
Sequences of elements in finite types
29.70.
Set quotients of index 2
29.71.
Finite Σ-decompositions of finite types
29.72.
Skipping elements in standard finite types
29.73.
Small types
29.74.
Standard finite pruned trees
29.75.
Standard finite trees
29.76.
The standard finite types
29.77.
Steiner systems
29.78.
Steiner triple systems
29.79.
Combinatorial identities of sums of natural numbers
29.80.
Surjective maps between finite types
29.81.
Symmetric difference of finite subtypes
29.82.
Finite trivial Σ-decompositions
29.83.
Type duality of finite types
29.84.
Unions of finite subtypes
29.85.
The universal property of the standard finite types
29.86.
Unlabeled partitions
29.87.
Unlabeled rooted trees
29.88.
Unlabeled trees
30.
Universal Algebra
❱
30.1.
Abstract equations over signatures
30.2.
Algebraic theories
30.3.
Algebraic theory of groups
30.4.
Algebras
30.5.
Congruences
30.6.
Homomorphisms of algebras
30.7.
Kernels of homomorphisms of algebras
30.8.
Models of signatures
30.9.
Quotient algebras
30.10.
Signatures
30.11.
Terms over signatures
Light
Rust
Coal
Navy
Ayu
Latte
Frappé
Macchiato
Mocha
agda-unimath
Agda-unimath art
The graph of mathematical concepts. Andrej Bauer and Matej Petković. 2023
The graph of mathematical concepts. Andrej Bauer and Matej Petković. 2023