Overview
1.
Overview
❱
1.1.
Home
1.2.
Community
❱
1.2.1.
Maintainers
1.2.2.
Contributors
1.2.3.
Statement of inclusivity
1.2.4.
Projects using Agda-Unimath
1.2.5.
Grant acknowledgements
1.3.
Guides
❱
1.3.1.
Installing the library
1.3.2.
Design principles
1.3.3.
Contributing to the library
1.3.4.
Structuring your file
❱
1.3.4.1.
File template
1.3.5.
The library coding style
1.3.6.
Guidelines for mixfix operators
1.3.7.
Citing sources
1.3.8.
Citing the library
1.4.
Library contents
1.5.
Art
The agda-unimath library
2.
Category theory
❱
2.1.
Adjunctions between large categories
2.2.
Adjunctions between large precategories
2.3.
Anafunctors between categories
2.4.
Anafunctors between precategories
2.5.
The augmented simplex category
2.6.
Categories
2.7.
The category of functors and natural transformations between two categories
2.8.
The category of functors and natural transformations from small to large categories
2.9.
The category of maps and natural transformations between two categories
2.10.
The category of maps and natural transformations from small to large categories
2.11.
Commuting squares of morphisms in large precategories
2.12.
Commuting squares of morphisms in precategories
2.13.
Commuting squares of morphisms in set-magmoids
2.14.
Composition operations on binary families of sets
2.15.
Conservative functors between precategories
2.16.
Constant functors
2.17.
Copresheaf categories
2.18.
Coproducts in precategories
2.19.
Cores of categories
2.20.
Cores of precategories
2.21.
Dependent products of categories
2.22.
Dependent products of large categories
2.23.
Dependent products of large precategories
2.24.
Dependent products of precategories
2.25.
Discrete categories
2.26.
Embedding maps between precategories
2.27.
Embeddings between precategories
2.28.
Endomorphisms in categories
2.29.
Endomorphisms in precategories
2.30.
Epimorphism in large precategories
2.31.
Equivalences between categories
2.32.
Equivalences between large precategories
2.33.
Equivalences between precategories
2.34.
Essential fibers of functors between precategories
2.35.
Essentially injective functors between precategories
2.36.
Essentially surjective functors between precategories
2.37.
Exponential objects in precategories
2.38.
Faithful functors between precategories
2.39.
Faithful maps between precategories
2.40.
Full functors between precategories
2.41.
Full large subcategories
2.42.
Full large subprecategories
2.43.
Full maps between precategories
2.44.
Full subcategories
2.45.
Full subprecategories
2.46.
Fully faithful functors between precategories
2.47.
Fully faithful maps between precategories
2.48.
Function categories
2.49.
Function precategories
2.50.
Functors between categories
2.51.
Functors from small to large categories
2.52.
Functors from small to large precategories
2.53.
Functors between large categories
2.54.
Functors between large precategories
2.55.
Functors between nonunital precategories
2.56.
Functors between precategories
2.57.
Functors between set-magmoids
2.58.
Gaunt categories
2.59.
Groupoids
2.60.
Homotopies of natural transformations in large precategories
2.61.
Indiscrete precategories
2.62.
The initial category
2.63.
Initial objects of large categories
2.64.
Initial objects of large precategories
2.65.
Initial objects in a precategory
2.66.
Isomorphism induction in categories
2.67.
Isomorphism induction in precategories
2.68.
Isomorphisms in categories
2.69.
Isomorphisms in large categories
2.70.
Isomorphisms in large precategories
2.71.
Isomorphisms in precategories
2.72.
Isomorphisms in subprecategories
2.73.
Large categories
2.74.
Large function categories
2.75.
Large function precategories
2.76.
Large precategories
2.77.
Large subcategories
2.78.
Large subprecategories
2.79.
Maps between categories
2.80.
Maps from small to large categories
2.81.
Maps from small to large precategories
2.82.
Maps between precategories
2.83.
Maps between set-magmoids
2.84.
Monads on categories
2.85.
Monads on precategories
2.86.
Monomorphisms in large precategories
2.87.
Natural isomorphisms between functors between categories
2.88.
Natural isomorphisms between functors between large precategories
2.89.
Natural isomorphisms between functors between precategories
2.90.
Natural isomorphisms between maps between categories
2.91.
Natural isomorphisms between maps between precategories
2.92.
Natural numbers object in a precategory
2.93.
Natural transformations between functors between categories
2.94.
Natural transformations between functors from small to large categories
2.95.
Natural transformations between functors from small to large precategories
2.96.
Natural transformations between functors between large categories
2.97.
Natural transformations between functors between large precategories
2.98.
Natural transformations between functors between precategories
2.99.
Natural transformations between maps between categories
2.100.
Natural transformations between maps from small to large precategories
2.101.
Natural transformations between maps between precategories
2.102.
Nonunital precategories
2.103.
One object precategories
2.104.
Opposite categories
2.105.
Opposite large precategories
2.106.
Opposite precategories
2.107.
Opposite preunivalent categories
2.108.
Pointed endofunctors on categories
2.109.
Pointed endofunctors
2.110.
Precategories
2.111.
Precategory of elements of a presheaf
2.112.
The precategory of functors and natural transformations between two precategories
2.113.
The precategory of functors and natural transformations from small to large precategories
2.114.
The precategory of maps and natural transformations from a small to a large precategory
2.115.
The precategory of maps and natural transformations between two precategories
2.116.
Pregroupoids
2.117.
Presheaf categories
2.118.
Preunivalent categories
2.119.
Products in precategories
2.120.
Products of precategories
2.121.
Pseudomonic functors between precategories
2.122.
Pullbacks in precategories
2.123.
Replete subprecategories
2.124.
Representable functors between categories
2.125.
Representable functors between large precategories
2.126.
Representable functors between precategories
2.127.
The representing arrow category
2.128.
Restrictions of functors to cores of precategories
2.129.
Rigid objects in a category
2.130.
Rigid objects in a precategory
2.131.
Set-magmoids
2.132.
Sieves in categories
2.133.
The simplex category
2.134.
Slice precategories
2.135.
Split essentially surjective functors between precategories
2.136.
Strict categories
2.137.
Structure equivalences between set-magmoids
2.138.
Subcategories
2.139.
Subprecategories
2.140.
Subterminal precategories
2.141.
The terminal category
2.142.
Terminal objects in a precategory
2.143.
Wide subcategories
2.144.
Wide subprecategories
2.145.
The Yoneda lemma for categories
2.146.
The Yoneda lemma for precategories
3.
Commutative algebra
❱
3.1.
The binomial theorem in commutative rings
3.2.
The binomial theorem in commutative semirings
3.3.
Boolean rings
3.4.
The category of commutative rings
3.5.
Commutative rings
3.6.
Commutative semirings
3.7.
Dependent products of commutative rings
3.8.
Dependent products of commutative semirings
3.9.
Discrete fields
3.10.
The Eisenstein integers
3.11.
Euclidean domains
3.12.
Full ideals of commutative rings
3.13.
Function commutative rings
3.14.
Function commutative semirings
3.15.
The Gaussian integers
3.16.
The group of multiplicative units of a commutative ring
3.17.
Homomorphisms of commutative rings
3.18.
Homomorphisms of commutative semirings
3.19.
Ideals of commutative rings
3.20.
Ideals of commutative semirings
3.21.
Ideals generated by subsets of commutative rings
3.22.
Integer multiples of elements of commutative rings
3.23.
Integral domains
3.24.
Intersections of ideals of commutative rings
3.25.
Intersections of radical ideals of commutative rings
3.26.
Invertible elements in commutative rings
3.27.
Isomorphisms of commutative rings
3.28.
Joins of ideals of commutative rings
3.29.
Joins of radical ideals of commutative rings
3.30.
Local commutative rings
3.31.
Maximal ideals of commutative rings
3.32.
Multiples of elements in commutative rings
3.33.
Nilradical of a commutative ring
3.34.
The nilradical of a commutative semiring
3.35.
The poset of ideals of a commutative ring
3.36.
The poset of radical ideals of a commutative ring
3.37.
Powers of elements in commutative rings
3.38.
Powers of elements in commutative semirings
3.39.
The precategory of commutative rings
3.40.
The precategory of commutative semirings
3.41.
Prime ideals of commutative rings
3.42.
Products of commutative rings
3.43.
Products of ideals of commutative rings
3.44.
Products of radical ideals of a commutative ring
3.45.
Products of subsets of commutative rings
3.46.
Radical ideals of commutative rings
3.47.
Radical ideals generated by subsets of commutative rings
3.48.
Radicals of ideals of commutative rings
3.49.
Subsets of commutative rings
3.50.
Subsets of commutative semirings
3.51.
Sums in commutative rings
3.52.
Sums in commutative semirings
3.53.
Transporting commutative ring structures along isomorphisms of abelian groups
3.54.
Trivial commutative rings
3.55.
The Zariski locale
3.56.
The Zariski topology on the set of prime ideals of a commutative ring
4.
Elementary number theory
❱
4.1.
The absolute value function on the integers
4.2.
The Ackermann function
4.3.
Addition on integer fractions
4.4.
Addition on the integers
4.5.
Addition on the natural numbers
4.6.
Addition of positive, negative, nonnegative and nonpositive integers
4.7.
Addition on the rational numbers
4.8.
The additive group of rational numbers
4.9.
Arithmetic functions
4.10.
The based induction principle of the natural numbers
4.11.
Based strong induction for the natural numbers
4.12.
Bezout's lemma in the integers
4.13.
Bezout's lemma on the natural numbers
4.14.
The binomial coefficients
4.15.
The binomial theorem for the integers
4.16.
The binomial theorem for the natural numbers
4.17.
Bounded sums of arithmetic functions
4.18.
Catalan numbers
4.19.
The cofibonacci sequence
4.20.
The Collatz bijection
4.21.
The Collatz conjecture
4.22.
The commutative semiring of natural numbers
4.23.
The congruence relations on the integers
4.24.
The congruence relations on the natural numbers
4.25.
The cross-multiplication difference of two integer fractions
4.26.
Cubes of natural numbers
4.27.
Decidable dependent function types
4.28.
The decidable total order of integers
4.29.
The decidable total order of natural numbers
4.30.
The decidable total order of rational numbers
4.31.
The decidable total order of a standard finite type
4.32.
Decidable types in elementary number theory
4.33.
The difference between integers
4.34.
The difference between rational numbers
4.35.
Dirichlet convolution
4.36.
The distance between integers
4.37.
The distance between natural numbers
4.38.
Divisibility of integers
4.39.
Divisibility in modular arithmetic
4.40.
Divisibility of natural numbers
4.41.
The divisibility relation on the standard finite types
4.42.
Equality of integers
4.43.
Equality of natural numbers
4.44.
Euclidean division on the natural numbers
4.45.
Euler's totient function
4.46.
Exponentiation of natural numbers
4.47.
Factorials of natural numbers
4.48.
Falling factorials
4.49.
The Fibonacci sequence
4.50.
The field of rational numbers
4.51.
The natural numbers base k
4.52.
Finitely cyclic maps
4.53.
The fundamental theorem of arithmetic
4.54.
The Goldbach conjecture
4.55.
The greatest common divisor of integers
4.56.
The greatest common divisor of natural numbers
4.57.
The group of integers
4.58.
The half-integers
4.59.
The Hardy-Ramanujan number
4.60.
Inequality on integer fractions
4.61.
Inequality on the integers
4.62.
Inequality of natural numbers
4.63.
Inequality on the rational numbers
4.64.
Inequality on the standard finite types
4.65.
The infinitude of primes
4.66.
Initial segments of the natural numbers
4.67.
Integer fractions
4.68.
Integer partitions
4.69.
The integers
4.70.
The Jacobi symbol
4.71.
The Kolakoski sequence
4.72.
The Legendre symbol
4.73.
Lower bounds of type families over the natural numbers
4.74.
Maximum on the natural numbers
4.75.
Maximum on the standard finite types
4.76.
The mediant fraction of two integer fractions
4.77.
Mersenne primes
4.78.
Minimum on the natural numbers
4.79.
Minimum on the standard finite types
4.80.
Modular arithmetic
4.81.
Modular arithmetic on the standard finite types
4.82.
The monoid of natural numbers with addition
4.83.
The monoid of the natural numbers with maximum
4.84.
Multiplication on integer fractions
4.85.
Multiplication of integers
4.86.
Multiplication of the elements of a list of natural numbers
4.87.
Multiplication of natural numbers
4.88.
Multiplication of positive, negative, nonnegative and nonpositive integers
4.89.
Multiplication on the rational numbers
4.90.
The multiplicative group of positive rational numbers
4.91.
The multiplicative group of rational numbers
4.92.
Multiplicative inverses of positive integer fractions
4.93.
The multiplicative monoid of natural numbers
4.94.
The multiplicative monoid of rational numbers
4.95.
Multiplicative units in the integers
4.96.
Multiplicative units in modular arithmetic
4.97.
Multiset coefficients
4.98.
The type of natural numbers
4.99.
The negative integers
4.100.
The nonnegative integers
4.101.
The nonpositive integers
4.102.
Nonzero integers
4.103.
Nonzero natural numbers
4.104.
Nonzero rational numbers
4.105.
The ordinal induction principle for the natural numbers
4.106.
Parity of the natural numbers
4.107.
Peano arithmetic
4.108.
Pisano periods
4.109.
The poset of natural numbers ordered by divisibility
4.110.
The positive, negative, nonnegative and nonpositive integers
4.111.
Positive integer fractions
4.112.
The positive integers
4.113.
Positive rational numbers
4.114.
Powers of integers
4.115.
Powers of two
4.116.
Prime numbers
4.117.
Products of natural numbers
4.118.
Proper divisors of natural numbers
4.119.
Pythagorean triples
4.120.
The rational numbers
4.121.
Reduced integer fractions
4.122.
Relatively prime integers
4.123.
Relatively prime natural numbers
4.124.
Repeating an element in a standard finite type
4.125.
Retracts of the type of natural numbers
4.126.
The ring of integers
4.127.
The ring of rational numbers
4.128.
The sieve of Eratosthenes
4.129.
Square-free natural numbers
4.130.
Squares in the integers
4.131.
Squares in ℤₚ
4.132.
Squares in the natural numbers
4.133.
The standard cyclic groups
4.134.
The standard cyclic rings
4.135.
Stirling numbers of the second kind
4.136.
Strict inequality on the integer fractions
4.137.
Strict inequality on the integers
4.138.
Strict inequality on the natural numbers
4.139.
Strict inequality on the rational numbers
4.140.
Strictly ordered pairs of natural numbers
4.141.
The strong induction principle for the natural numbers
4.142.
Sums of natural numbers
4.143.
Taxicab numbers
4.144.
Telephone numbers
4.145.
The triangular numbers
4.146.
The Twin Prime conjecture
4.147.
Type arithmetic with natural numbers
4.148.
Unit elements in the standard finite types
4.149.
Unit similarity on the standard finite types
4.150.
The universal property of the integers
4.151.
The universal property of the natural numbers
4.152.
Upper bounds for type families over the natural numbers
4.153.
The Well-Ordering Principle of the natural numbers
4.154.
The well-ordering principle of the standard finite types
5.
Finite algebra
❱
5.1.
Commutative finite rings
5.2.
Dependent products of commutative finit rings
5.3.
Dependent products of finite rings
5.4.
Finite fields
5.5.
Finite rings
5.6.
Homomorphisms of commutative finite rings
5.7.
Homomorphisms of finite rings
5.8.
Products of commutative finite rings
5.9.
Products of finite rings
5.10.
Semisimple commutative finite rings
6.
Finite group theory
❱
6.1.
The abstract quaternion group of order 8
6.2.
Alternating concrete groups
6.3.
Alternating groups
6.4.
Cartier's delooping of the sign homomorphism
6.5.
The concrete quaternion group
6.6.
Deloopings of the sign homomorphism
6.7.
Abelian groups
6.8.
Finite Commutative monoids
6.9.
Finite groups
6.10.
Finite monoids
6.11.
Finite semigroups
6.12.
The group of n-element types
6.13.
Groups of order 2
6.14.
Orbits of permutations
6.15.
Permutations
6.16.
Permutations of standard finite types
6.17.
The sign homomorphism
6.18.
Simpson's delooping of the sign homomorphism
6.19.
Subgroups of finite groups
6.20.
Tetrahedra in 3-dimensional space
6.21.
Transpositions
6.22.
Transpositions of standard finite types
7.
Foundation
❱
7.1.
0-Connected types
7.2.
0-Images of maps
7.3.
0-Maps
7.4.
1-Types
7.5.
2-Types
7.6.
Action on equivalences of functions
7.7.
The action on equivalences of functions out of subuniverses
7.8.
Action on equivalences of type families
7.9.
Action on equivalences in type families over subuniverses
7.10.
The action of functions on higher identifications
7.11.
The action on homotopies of functions
7.12.
The binary action on identifications of binary functions
7.13.
The action on identifications of dependent functions
7.14.
The action on identifications of functions
7.15.
Apartness relations
7.16.
Arithmetic law for coproduct decomposition and Σ-decomposition
7.17.
Arithmetic law for product decomposition and Π-decomposition
7.18.
Automorphisms
7.19.
The axiom of choice
7.20.
Bands
7.21.
Base changes of span diagrams
7.22.
Binary embeddings
7.23.
Binary equivalences
7.24.
Binary equivalences on unordered pairs of types
7.25.
Binary functoriality of set quotients
7.26.
Homotopies of binary operations
7.27.
Binary operations on unordered pairs of types
7.28.
Binary reflecting maps of equivalence relations
7.29.
Binary relations
7.30.
Transitive Closures
7.31.
Binary relations with extensions
7.32.
Binary relations with lifts
7.33.
Binary transport
7.34.
Binary type duality
7.35.
The booleans
7.36.
The Cantor–Schröder–Bernstein–Escardó theorem
7.37.
Cantor's diagonal argument
7.38.
Cartesian morphisms of arrows
7.39.
Cartesian morphisms of span diagrams
7.40.
Cartesian product types
7.41.
Cartesian products of set quotients
7.42.
The category of families of sets
7.43.
The category of sets
7.44.
Choice of representatives for an equivalence relation
7.45.
Codiagonal maps of types
7.46.
Coherently invertible maps
7.47.
Coinhabited pairs of types
7.48.
Commuting cubes of maps
7.49.
Commuting hexagons of identifications
7.50.
Commuting pentagons of identifications
7.51.
Commuting prisms of maps
7.52.
Commuting squares of homotopies
7.53.
Commuting squares of identifications
7.54.
Commuting squares of maps
7.55.
Commuting tetrahedra of homotopies
7.56.
Commuting tetrahedra of maps
7.57.
Commuting triangles of homotopies
7.58.
Commuting triangles of identifications
7.59.
Commuting triangles of maps
7.60.
Commuting triangles of morphisms of arrows
7.61.
Complements of type families
7.62.
Complements of subtypes
7.63.
Composite maps in inverse sequential diagrams
7.64.
Composition algebra
7.65.
Computational identity types
7.66.
Cones over cospan diagrams
7.67.
Cones over inverse sequential diagrams
7.68.
Conjunction
7.69.
Connected components of types
7.70.
Connected components of universes
7.71.
Connected maps
7.72.
Connected types
7.73.
Constant maps
7.74.
Constant span diagrams
7.75.
Constant type families
7.76.
Contractible maps
7.77.
Contractible types
7.78.
Copartial elements
7.79.
Copartial functions
7.80.
Coproduct decompositions
7.81.
Coproduct decompositions in a subuniverse
7.82.
Coproduct types
7.83.
Coproducts of pullbacks
7.84.
Morphisms in the coslice category of types
7.85.
Cospan diagrams
7.86.
Cospans of types
7.87.
Decidability of dependent function types
7.88.
Decidability of dependent pair types
7.89.
Decidable embeddings
7.90.
Decidable equality
7.91.
Decidable equivalence relations
7.92.
Decidable maps
7.93.
Decidable propositions
7.94.
Decidable relations on types
7.95.
Decidable subtypes
7.96.
Decidable types
7.97.
Dependent binary homotopies
7.98.
The dependent binomial theorem for types (distributivity of dependent function types over coproduct types)
7.99.
Dependent epimorphisms
7.100.
Dependent epimorphisms with respect to truncated types
7.101.
Dependent function types
7.102.
Dependent homotopies
7.103.
Dependent identifications
7.104.
Dependent inverse sequential diagrams of types
7.105.
Dependent pair types
7.106.
Dependent products of pullbacks
7.107.
Dependent sequences
7.108.
Dependent sums of pullbacks
7.109.
Dependent telescopes
7.110.
The dependent universal property of equivalences
7.111.
Descent for coproduct types
7.112.
Descent for dependent pair types
7.113.
Descent for the empty type
7.114.
Descent for equivalences
7.115.
Diagonal maps into cartesian products of types
7.116.
Diagonal maps of types
7.117.
Diagonal span diagrams
7.118.
Diagonals of maps
7.119.
Diagonals of morphisms of arrows
7.120.
Discrete relations
7.121.
Discrete relaxed Σ-decompositions
7.122.
Discrete Σ-decompositions
7.123.
Discrete types
7.124.
Disjunction
7.125.
Double arrows
7.126.
Double negation
7.127.
The double negation modality
7.128.
Double powersets
7.129.
Dubuc-Penon compact types
7.130.
Effective maps for equivalence relations
7.131.
Embeddings
7.132.
Empty types
7.133.
Endomorphisms
7.134.
Epimorphisms
7.135.
Epimorphisms with respect to maps into sets
7.136.
Epimorphisms with respect to truncated types
7.137.
Equality of cartesian product types
7.138.
Equality of coproduct types
7.139.
Equality on dependent function types
7.140.
Equality of dependent pair types
7.141.
Equality in the fibers of a map
7.142.
Equivalence classes
7.143.
Equivalence extensionality
7.144.
Equivalence induction
7.145.
Equivalence injective type families
7.146.
Equivalence relations
7.147.
Equivalences
7.148.
Equivalences of arrows
7.149.
Equivalences of cospans
7.150.
Equivalences of double arrows
7.151.
Equivalences of inverse sequential diagrams of types
7.152.
Equivalences on Maybe
7.153.
Equivalences of span diagrams
7.154.
Equivalences of span diagrams on families of types
7.155.
Equivalences of spans
7.156.
Equivalences of spans of families of types
7.157.
Evaluation of functions
7.158.
Exclusive disjunctions
7.159.
Exclusive sums
7.160.
Existential quantification
7.161.
Exponents of set quotients
7.162.
Extensions of types
7.163.
Faithful maps
7.164.
Families of equivalences
7.165.
Families of maps
7.166.
Families of types over telescopes
7.167.
Fiber inclusions
7.168.
Fibered equivalences
7.169.
Fibered involutions
7.170.
Maps fibered over a map
7.171.
Fibers of maps
7.172.
Finitely coherent equivalences
7.173.
Finitely coherently invertible maps
7.174.
Fixed points of endofunctions
7.175.
Full subtypes of types
7.176.
Function extensionality
7.177.
Function types
7.178.
Functional correspondences
7.179.
Functoriality of cartesian product types
7.180.
Functoriality of coproduct types
7.181.
Functoriality of dependent function types
7.182.
Functoriality of dependent pair types
7.183.
Functoriality of fibers of maps
7.184.
Functoriality of function types
7.185.
Functoriality of propositional truncations
7.186.
Functorialty of pullbacks
7.187.
Functoriality of sequential limits
7.188.
Functoriality of set quotients
7.189.
Functoriality of set truncation
7.190.
Functoriality of truncations
7.191.
The fundamental theorem of identity types
7.192.
Global choice
7.193.
Global subuniverses
7.194.
Higher homotopies of morphisms of arrows
7.195.
Hilbert's ε-operators
7.196.
Homotopies
7.197.
Homotopies of morphisms of arrows
7.198.
Homotopy algebra
7.199.
Homotopy induction
7.200.
The homotopy preorder of types
7.201.
Idempotent maps
7.202.
Identity systems
7.203.
Identity types of truncated types
7.204.
Identity types
7.205.
The image of a map
7.206.
Images of subtypes
7.207.
Implicit function types
7.208.
Impredicative encodings of the logical operations
7.209.
Impredicative universes
7.210.
The induction principle for propositional truncation
7.211.
Infinitely coherent equivalences
7.212.
Inhabited subtypes
7.213.
Inhabited types
7.214.
Injective maps
7.215.
The interchange law
7.216.
Intersections of subtypes
7.217.
Inverse sequential diagrams of types
7.218.
Invertible maps
7.219.
Involutions
7.220.
Isolated elements
7.221.
Isomorphisms of sets
7.222.
Iterated cartesian product types
7.223.
Iterated dependent pair types
7.224.
Iterated dependent product types
7.225.
Iterating automorphisms
7.226.
Iterating functions
7.227.
Iterating involutions
7.228.
Kernel span diagrams of maps
7.229.
Large binary relations
7.230.
Large dependent pair types
7.231.
Large homotopies
7.232.
Large identity types
7.233.
The large locale of propositions
7.234.
The large locale of subtypes
7.235.
The law of excluded middle
7.236.
Lawvere's fixed point theorem
7.237.
The lesser limited principle of omniscience
7.238.
Lifts of types
7.239.
The limited principle of omniscience
7.240.
Locally small types
7.241.
Logical equivalences
7.242.
The maybe modality
7.243.
Mere embeddings
7.244.
Mere equality
7.245.
Mere equivalences
7.246.
Mere functions
7.247.
Mere logical equivalences
7.248.
Monomorphisms
7.249.
Morphisms of arrows
7.250.
Morphisms of binary relations
7.251.
Morphisms of cospan diagrams
7.252.
Morphisms of cospans
7.253.
Morphisms of double arrows
7.254.
Morphisms of inverse sequential diagrams of types
7.255.
Morphisms of span diagrams
7.256.
Morphisms of spans
7.257.
Morphisms of spans on families of types
7.258.
Morphisms of twisted arrows
7.259.
Multisubsets
7.260.
Multivariable correspondences
7.261.
Multivariable decidable relations
7.262.
Multivariable functoriality of set quotients
7.263.
Multivariable homotopies
7.264.
Multivariable operations
7.265.
Multivariable relations
7.266.
Multivariable sections
7.267.
Negated equality
7.268.
Negation
7.269.
Noncontractible types
7.270.
Operations on span diagrams
7.271.
Operations on spans
7.272.
Operations on spans of families of types
7.273.
Opposite spans
7.274.
Pairs of distinct elements
7.275.
Partial elements
7.276.
Partial functions
7.277.
Partial sequences
7.278.
Partitions
7.279.
Path algebra
7.280.
Path-split maps
7.281.
Perfect images
7.282.
Permutations of spans of families of types
7.283.
Π-decompositions of types
7.284.
Π-decompositions of types into types in a subuniverse
7.285.
Pointed torsorial type families
7.286.
Postcomposition of dependent functions
7.287.
Postcomposition of functions
7.288.
Postcomposition of pullbacks
7.289.
Powersets
7.290.
Precomposition of dependent functions
7.291.
Precomposition of functions
7.292.
Precomposition of functions into subuniverses
7.293.
Precomposition of type families
7.294.
Preimages of subtypes
7.295.
The preunivalence axiom
7.296.
Preunivalent type families
7.297.
The principle of omniscience
7.298.
Product decompositions
7.299.
Product decompositions of types in a subuniverse
7.300.
Products of binary relations
7.301.
Products of equivalence relataions
7.302.
Products of tuples of types
7.303.
Products of pullbacks
7.304.
Products of unordered pairs of types
7.305.
Products of unordered tuples of types
7.306.
Projective types
7.307.
Proper subsets
7.308.
Propositional extensionality
7.309.
Propositional maps
7.310.
Propositional resizing
7.311.
Propositional truncations
7.312.
Propositions
7.313.
Pullbacks
7.314.
Pullbacks of subtypes
7.315.
Quasicoherently idempotent maps
7.316.
Raising universe levels
7.317.
Reflecting maps for equivalence relations
7.318.
Reflexive relations
7.319.
The Regensburg extension of the fundamental theorem of identity types
7.320.
Relaxed Σ-decompositions of types
7.321.
Repetitions of values of maps
7.322.
Repetitions in sequences
7.323.
The type theoretic replacement axiom
7.324.
Retractions
7.325.
Retracts of maps
7.326.
Retracts of types
7.327.
Russell's paradox
7.328.
Sections
7.329.
Separated types
7.330.
Sequences
7.331.
Sequential limits
7.332.
Set presented types
7.333.
Set quotients
7.334.
Set truncations
7.335.
Sets
7.336.
Shifting sequences
7.337.
Σ-closed subuniverses
7.338.
Σ-decompositions of types into types in a subuniverse
7.339.
Σ-decompositions of types
7.340.
Singleton induction
7.341.
Singleton subtypes
7.342.
Morphisms in the slice category of types
7.343.
Small maps
7.344.
Small types
7.345.
Small universes
7.346.
Sorial type families
7.347.
Span diagrams
7.348.
Span diagrams on families of types
7.349.
Spans of types
7.350.
Spans of families of types
7.351.
Split idempotent maps
7.352.
Split surjective maps
7.353.
Standard apartness relations
7.354.
Standard pullbacks
7.355.
Strict symmetrization of binary relations
7.356.
Strictly involutive identity types
7.357.
The strictly right unital concatenation operation on identifications
7.358.
Strongly extensional maps
7.359.
Structure
7.360.
The structure identity principle
7.361.
Structured type duality
7.362.
Subsingleton induction
7.363.
Subterminal types
7.364.
Subtype duality
7.365.
The subtype identity principle
7.366.
Subtypes
7.367.
Subuniverses
7.368.
Surjective maps
7.369.
Symmetric binary relations
7.370.
Symmetric cores of binary relations
7.371.
Symmetric difference of subtypes
7.372.
The symmetric identity types
7.373.
Symmetric operations
7.374.
Telescopes
7.375.
Terminal spans on families of types
7.376.
Tight apartness relations
7.377.
Torsorial type families
7.378.
Total partial elements
7.379.
Total partial functions
7.380.
Transfinite cocomposition of maps
7.381.
Transport along equivalences
7.382.
Transport along higher identifications
7.383.
Transport along homotopies
7.384.
Transport along identifications
7.385.
Transport-split type families
7.386.
Transposing identifications along equivalences
7.387.
Transposing identifications along retractions
7.388.
Transposing identifications along sections
7.389.
Transposition of span diagrams
7.390.
Trivial relaxed Σ-decompositions
7.391.
Trivial Σ-decompositions
7.392.
Truncated equality
7.393.
Truncated maps
7.394.
Truncated types
7.395.
k-Equivalences
7.396.
Truncation images of maps
7.397.
Truncation levels
7.398.
The truncation modalities
7.399.
Truncations
7.400.
Tuples of types
7.401.
Type arithmetic with the booleans
7.402.
Type arithmetic for cartesian product types
7.403.
Type arithmetic for coproduct types
7.404.
Type arithmetic with dependent function types
7.405.
Type arithmetic for dependent pair types
7.406.
Type arithmetic with the empty type
7.407.
Type arithmetic with the unit type
7.408.
Type duality
7.409.
The type theoretic principle of choice
7.410.
Unions of subtypes
7.411.
Uniqueness of the image of a map
7.412.
Uniqueness quantification
7.413.
The uniqueness of set quotients
7.414.
Uniqueness of set truncations
7.415.
Uniqueness of the truncations
7.416.
The unit type
7.417.
Unital binary operations
7.418.
The univalence axiom
7.419.
The univalence axiom implies function extensionality
7.420.
Univalent type families
7.421.
The universal property of booleans
7.422.
The universal properties of cartesian product types
7.423.
Universal property of contractible types
7.424.
The universal property of coproduct types
7.425.
The universal property of dependent function types
7.426.
The universal property of dependent pair types
7.427.
The universal property of the empty type
7.428.
The universal property of equivalences
7.429.
The universal property of the family of fibers of maps
7.430.
The universal property of fiber products
7.431.
The universal property of identity systems
7.432.
The universal property of identity types
7.433.
The universal property of the image of a map
7.434.
The universal property of maybe
7.435.
The universal property of propositional truncations
7.436.
The universal property of propositional truncations with respect to sets
7.437.
The universal property of pullbacks
7.438.
The universal property of sequential limits
7.439.
The universal property of set quotients
7.440.
The universal property of set truncations
7.441.
The universal property of truncations
7.442.
The universal property of the unit type
7.443.
Universal quantification
7.444.
Universe levels
7.445.
Unordered pairs of elements in a type
7.446.
Unordered pairs of types
7.447.
Unordered n-tuples of elements in a type
7.448.
Unordered tuples of types
7.449.
Vectors of set quotients
7.450.
Weak function extensionality
7.451.
The weak limited principle of omniscience
7.452.
Weakly constant maps
7.453.
Whiskering higher homotopies with respect to composition
7.454.
Whiskering homotopies with respect to composition
7.455.
Whiskering homotopies with respect to concatenation
7.456.
Whiskering identifications with respect to concatenation
7.457.
Whiskering operations
7.458.
Yoneda identity types
8.
Foundation core
❱
8.1.
1-Types
8.2.
Cartesian product types
8.3.
Coherently invertible maps
8.4.
Commuting prisms of maps
8.5.
Commuting squares of homotopies
8.6.
Commuting squares of identifications
8.7.
Commuting squares of maps
8.8.
Commuting triangles of maps
8.9.
Constant maps
8.10.
Contractible maps
8.11.
Contractible types
8.12.
Coproduct types
8.13.
Decidable propositions
8.14.
Dependent identifications
8.15.
Diagonal maps into cartesian products of types
8.16.
Discrete types
8.17.
Embeddings
8.18.
Empty types
8.19.
Endomorphisms
8.20.
Equality of dependent pair types
8.21.
Equivalence relations
8.22.
Equivalences
8.23.
Families of equivalences
8.24.
Fibers of maps
8.25.
Function types
8.26.
Functoriality of dependent function types
8.27.
Functoriality of dependent pair types
8.28.
Homotopies
8.29.
Identity types
8.30.
Injective maps
8.31.
Invertible maps
8.32.
Negation
8.33.
Operations on span diagrams
8.34.
Operations on spans
8.35.
Path-split maps
8.36.
Postcomposition of dependent functions
8.37.
Postcomposition of functions
8.38.
Precomposition of dependent functions
8.39.
Precomposition of functions
8.40.
Propositional maps
8.41.
Propositions
8.42.
Pullbacks
8.43.
Retractions
8.44.
Retracts of types
8.45.
Sections
8.46.
Sets
8.47.
Small types
8.48.
Subtypes
8.49.
Torsorial type families
8.50.
Transport along identifications
8.51.
Truncated maps
8.52.
Truncated types
8.53.
Truncation levels
8.54.
The type theoretic principle of choice
8.55.
The univalence axiom
8.56.
The universal property of pullbacks
8.57.
The universal property of truncations
8.58.
Whiskering homotopies with respect to concatenation
8.59.
Whiskering identifications with respect to concatenation
9.
Graph theory
❱
9.1.
Acyclic undirected graphs
9.2.
Circuits in undirected graphs
9.3.
Closed walks in undirected graphs
9.4.
Complete bipartite graphs
9.5.
Complete multipartite graphs
9.6.
Complete undirected graphs
9.7.
Connected graphs
9.8.
Cycles in undirected graphs
9.9.
Directed graph structures on standard finite sets
9.10.
Directed graphs
9.11.
Discrete graphs
9.12.
Displayed large reflexive graphs
9.13.
Edge-coloured undirected graphs
9.14.
Embeddings of directed graphs
9.15.
Embeddings of undirected graphs
9.16.
Enriched undirected graphs
9.17.
Equivalences of directed graphs
9.18.
Equivalences of enriched undirected graphs
9.19.
Equivalences of undirected graphs
9.20.
Eulerian circuits in undirected graphs
9.21.
Faithful morphisms of undirected graphs
9.22.
Fibers of directed graphs
9.23.
Finite graphs
9.24.
Geometric realizations of undirected graphs
9.25.
Higher directed graphs
9.26.
Hypergraphs
9.27.
Large higher directed graphs
9.28.
Large reflexive graphs
9.29.
Matchings
9.30.
Mere equivalences of undirected graphs
9.31.
Morphisms of directed graphs
9.32.
Morphisms of undirected graphs
9.33.
Incidence in undirected graphs
9.34.
Orientations of undirected graphs
9.35.
Paths in undirected graphs
9.36.
Polygons
9.37.
Raising universe levels of directed graphs
9.38.
Reflecting maps of undirected graphs
9.39.
Reflexive graphs
9.40.
Regular undirected graph
9.41.
Simple undirected graphs
9.42.
Stereoisomerism for enriched undirected graphs
9.43.
Totally faithful morphisms of undirected graphs
9.44.
Trails in directed graphs
9.45.
Trails in undirected graphs
9.46.
Undirected graph structures on standard finite sets
9.47.
Undirected graphs
9.48.
Vertex covers
9.49.
Voltage graphs
9.50.
Walks in directed graphs
9.51.
Walks in undirected graphs
9.52.
Wide displayed large reflexive graphs
10.
Group theory
❱
10.1.
Abelian groups
10.2.
Abelianization of groups
10.3.
Pointwise addition of morphisms of abelian groups
10.4.
Automorphism groups
10.5.
Cartesian products of abelian groups
10.6.
Cartesian products of concrete groups
10.7.
Cartesian products of groups
10.8.
Cartesian products of monoids
10.9.
Cartesian products of semigroups
10.10.
The category of abelian groups
10.11.
The category of concrete groups
10.12.
The category of group actions
10.13.
The category of groups
10.14.
The orbit category of a group
10.15.
The category of semigroups
10.16.
Cayley's theorem
10.17.
The center of a group
10.18.
Center of a monoid
10.19.
Center of a semigroup
10.20.
Central elements of groups
10.21.
Central elements of monoids
10.22.
Central elements of semirings
10.23.
Centralizer subgroups
10.24.
Characteristic subgroups
10.25.
Commutative monoids
10.26.
Commutator subgroups
10.27.
Commutators of elements in groups
10.28.
Commuting elements of groups
10.29.
Commuting elements of monoids
10.30.
Commuting elements of semigroups
10.31.
Commuting squares of group homomorphisms
10.32.
Concrete group actions
10.33.
Concrete groups
10.34.
Concrete monoids
10.35.
Congruence relations on abelian groups
10.36.
Congruence relations on commutative monoids
10.37.
Congruence relations on groups
10.38.
Congruence relations on monoids
10.39.
Congruence relations on semigroups
10.40.
Conjugation in groups
10.41.
Conjugation on concrete groups
10.42.
Contravariant pushforwards of concrete group actions
10.43.
Cores of monoids
10.44.
Cyclic groups
10.45.
Decidable subgroups of groups
10.46.
Dependent products of abelian groups
10.47.
Dependent products of commutative monoids
10.48.
Dependent products of groups
10.49.
Dependent products of monoids
10.50.
Dependent products of semigroups
10.51.
The dihedral group construction
10.52.
The dihedral groups
10.53.
The E₈-lattice
10.54.
Elements of finite order
10.55.
Embeddings of abelian groups
10.56.
Embeddings of groups
10.57.
The endomorphism rings of abelian groups
10.58.
Epimorphisms in groups
10.59.
Equivalences of concrete group actions
10.60.
Equivalences of concrete groups
10.61.
Equivalences of group actions
10.62.
Equivalences between semigroups
10.63.
Exponents of abelian groups
10.64.
Exponents of groups
10.65.
Free concrete group actions
10.66.
Free groups with one generator
10.67.
The full subgroup of a group
10.68.
The full subsemigroup of a semigroup
10.69.
Function groups of abelian groups
10.70.
Function commutative monoids
10.71.
Function groups
10.72.
Function monoids
10.73.
Function semigroups
10.74.
Functoriality of quotient groups
10.75.
Furstenberg groups
10.76.
Generating elements of groups
10.77.
Generating sets of groups
10.78.
Group actions
10.79.
Abstract groups
10.80.
Homomorphisms of abelian groups
10.81.
Homomorphisms of commutative monoids
10.82.
Morphisms of concrete group actions
10.83.
Homomorphisms of concrete groups
10.84.
Homomorphisms of generated subgroups
10.85.
Homomorphisms of group actions
10.86.
Homomorphisms of groups
10.87.
Homomorphisms of groups equipped with normal subgroups
10.88.
Homomorphisms of monoids
10.89.
Homomorphisms of semigroups
10.90.
Images of group homomorphisms
10.91.
Images of semigroup homomorphisms
10.92.
Integer multiples of elements in abelian groups
10.93.
Integer powers of elements of groups
10.94.
Intersections of subgroups of abelian groups
10.95.
Intersections of subgroups of groups
10.96.
Inverse semigroups
10.97.
Invertible elements in monoids
10.98.
Isomorphisms of abelian groups
10.99.
Isomorphisms of concrete groups
10.100.
Isomorphisms of group actions
10.101.
Isomorphisms of groups
10.102.
Isomorphisms of monoids
10.103.
Isomorphisms of semigroups
10.104.
Iterated cartesian products of concrete groups
10.105.
Kernels of homomorphisms between abelian groups
10.106.
Kernels of homomorphisms of concrete groups
10.107.
Kernels of homomorphisms of groups
10.108.
Large semigroups
10.109.
Concrete automorphism groups on sets
10.110.
Mere equivalences of concrete group actions
10.111.
Mere equivalences of group actions
10.112.
Monoid actions
10.113.
Monoids
10.114.
Monomorphisms of concrete groups
10.115.
Monomorphisms in the category of groups
10.116.
Multiples of elements in abelian groups
10.117.
Nontrivial groups
10.118.
Normal closures of subgroups
10.119.
Normal cores of subgroups
10.120.
Normal subgroups
10.121.
Normal subgroups of concrete groups
10.122.
Normal submonoids
10.123.
Normal submonoids of commutative monoids
10.124.
Normalizer subgroups
10.125.
Nullifying group homomorphisms
10.126.
The opposite of a group
10.127.
The opposite of a semigroup
10.128.
The orbit-stabilizer theorem for concrete groups
10.129.
Orbits of concrete group actions
10.130.
Orbits of group actions
10.131.
The order of an element in a group
10.132.
Perfect cores
10.133.
Perfect groups
10.134.
Perfect subgroups
10.135.
Powers of elements in commutative monoids
10.136.
Powers of elements in groups
10.137.
Powers of elements in monoids
10.138.
The precategory of commutative monoids
10.139.
The precategory of concrete groups
10.140.
The precategory of group actions
10.141.
The precategory of groups
10.142.
The precategory of monoids
10.143.
The precategory of orbits of a monoid action
10.144.
The precategory of semigroups
10.145.
Principal group actions
10.146.
Principal torsors of concrete groups
10.147.
Products of elements in a monoid
10.148.
Products of tuples of elements in commutative monoids
10.149.
Pullbacks of subgroups
10.150.
Pullbacks of subsemigroups
10.151.
Quotient groups
10.152.
Quotient groups of concrete groups
10.153.
Quotients of abelian groups
10.154.
Rational commutative monoids
10.155.
Representations of monoids in precategories
10.156.
Saturated congruence relations on commutative monoids
10.157.
Saturated congruence relations on monoids
10.158.
Semigroups
10.159.
Sheargroups
10.160.
Shriek of concrete group homomorphisms
10.161.
Stabilizer groups
10.162.
Stabilizers of concrete group actions
10.163.
Subgroups
10.164.
Subgroups of abelian groups
10.165.
Subgroups of concrete groups
10.166.
Subgroups generated by elements of a group
10.167.
Subgroups generated by families of elements
10.168.
Subgroups generated by subsets of groups
10.169.
Submonoids
10.170.
Submonoids of commutative monoids
10.171.
Subsemigroups
10.172.
Subsets of abelian groups
10.173.
Subsets of commutative monoids
10.174.
Subsets of groups
10.175.
Subsets of monoids
10.176.
Subsets of semigroups
10.177.
The substitution functor of concrete group actions
10.178.
The substitution functor of group actions
10.179.
Surjective group homomorphisms
10.180.
Surjective semigroup homomorphisms
10.181.
Symmetric concrete groups
10.182.
Symmetric groups
10.183.
Torsion elements of groups
10.184.
Torsion-free groups
10.185.
Torsors of abstract groups
10.186.
Transitive concrete group actions
10.187.
Transitive group actions
10.188.
Trivial concrete groups
10.189.
Trivial group homomorphisms
10.190.
Trivial groups
10.191.
Trivial subgroups
10.192.
Unordered tuples of elements in commutative monoids
10.193.
Wild representations of monoids
11.
Higher group theory
❱
11.1.
Cartesian products of higher groups
11.2.
Conjugation in higher groups
11.3.
Cyclic higher groups
11.4.
Deloopable groups
11.5.
Deloopable H-spaces
11.6.
Deloopable types
11.7.
Eilenberg-Mac Lane spaces
11.8.
Equivalences of higher groups
11.9.
Fixed points of higher group actions
11.10.
Free higher group actions
11.11.
Higher group actions
11.12.
Higher groups
11.13.
Homomorphisms of higher group actions
11.14.
Homomorphisms of higher groups
11.15.
The higher group of integers
11.16.
Iterated cartesian products of higher groups
11.17.
Iterated deloopings of pointed types
11.18.
Orbits of higher group actions
11.19.
Small ∞-groups
11.20.
Subgroups of higher groups
11.21.
Symmetric higher groups
11.22.
Transitive higher group actions
11.23.
Trivial higher groups
12.
Linear algebra
❱
12.1.
Constant matrices
12.2.
Diagonal vectors
12.3.
Diagonal matrices on rings
12.4.
Functoriality of the type of matrices
12.5.
Functoriality of the type of vectors
12.6.
Matrices
12.7.
Matrices on rings
12.8.
Multiplication of matrices
12.9.
Scalar multiplication on matrices
12.10.
Scalar multiplication of vectors
12.11.
Scalar multiplication of vectors on rings
12.12.
Transposition of matrices
12.13.
Vectors
12.14.
Vectors on commutative rings
12.15.
Vectors on commutative semirings
12.16.
Vectors on euclidean domains
12.17.
Vectors on rings
12.18.
Vectors on semirings
13.
Lists
❱
13.1.
Arrays
13.2.
Concatenation of lists
13.3.
Flattening of lists
13.4.
Functoriality of the list operation
13.5.
Lists
13.6.
Lists of elements in discrete types
13.7.
Lists subtypes
13.8.
Permutations of lists
13.9.
Permutations of vectors
13.10.
Predicates on lists
13.11.
Quicksort for lists
13.12.
Reversing lists
13.13.
Sort by insertion for lists
13.14.
Sort by insertion for vectors
13.15.
Sorted lists
13.16.
Sorted vectors
13.17.
Sorting algorithms for lists
13.18.
Sorting algorithms for vectors
13.19.
The universal property of lists with respect to wild monoids
14.
Modal logic
❱
14.1.
Modal logic axioms
14.2.
Canonical model theorem
14.3.
Canonical threories
14.4.
Closed under subformulas theories
14.5.
Modal logic completeness
14.6.
Completeness of K
14.7.
Completeness of S5
14.8.
Modal logic decision
14.9.
Modal logic deduction
14.10.
Filtrated Kripke Classes
14.11.
Kripke models filtrations theorem
14.12.
Finite approximability
14.13.
Modal logic formulas
14.14.
Formulas deduction
14.15.
Kripke models filtrations
14.16.
Krikpe semantics
14.17.
L-complete theories
14.18.
L-consistent theories
14.19.
Lindenbaum's lemma
14.20.
Minimal Kripke filtration
14.21.
Minimal transitive Kripke filtration
14.22.
Modal logic K
14.23.
Modal logic S5
14.24.
Modal logic soundness
14.25.
Modal logic subformulas
14.26.
Weak deduction
15.
Modal type theory
❱
15.1.
Crisp identity types
15.2.
The crisp law of excluded middle
15.3.
Flat dependent function types
15.4.
Flat dependent pair types
15.5.
Flat discrete types
15.6.
The flat modality
15.7.
The flat-sharp adjunction
15.8.
Sharp codiscrete maps
15.9.
Sharp codiscrete types
15.10.
The sharp modality
16.
Online encyclopedia of integer sequences
❱
16.1.
Sequences of the online encyclopedia of integer sequences
17.
Order theory
❱
17.1.
Accessible elements with respect to relations
17.2.
Bottom elements in posets
17.3.
Bottom elements in preorders
17.4.
Chains in posets
17.5.
Chains in preorders
17.6.
Closure operators on large locales
17.7.
Closure operators on large posets
17.8.
Commuting squares of Galois connections between large posets
17.9.
Commuting squares of order preserving maps of large posets
17.10.
Coverings in locales
17.11.
Decidable posets
17.12.
Decidable preorders
17.13.
Decidable subposets
17.14.
Decidable subpreorders
17.15.
Decidable total orders
17.16.
Decidable total preorders
17.17.
Dependent products of large frames
17.18.
Dependent products of large locales
17.19.
Dependent products of large meet-semilattices
17.20.
Dependent products of large posets
17.21.
Dependent products large preorders
17.22.
Dependent products of large suplattices
17.23.
Directed complete posets
17.24.
Directed families in posets
17.25.
Distributive lattices
17.26.
Finite coverings in locales
17.27.
Finite posets
17.28.
Finite preorders
17.29.
Finite total orders
17.30.
Finitely graded posets
17.31.
Frames
17.32.
Galois connections
17.33.
Galois connections between large posets
17.34.
Greatest lower bounds in large posets
17.35.
Greatest lower bounds in posets
17.36.
Homomorphisms of frames
17.37.
Homomorphisms of large frames
17.38.
Homomorphisms of large locales
17.39.
Homomorphisms of large meet-semilattices
17.40.
Homomorphisms of large suplattices
17.41.
Homomorphisms of meet-semilattices
17.42.
Homomorphisms of meet sup lattices
17.43.
Homomorphisms of suplattices
17.44.
Ideals in preorders
17.45.
Inhabited finite total orders
17.46.
Interval subposets
17.47.
Join-semilattices
17.48.
Large frames
17.49.
Large locales
17.50.
Large meet-semilattices
17.51.
Large meet-subsemilattices
17.52.
Large posets
17.53.
Large preorders
17.54.
Large quotient locales
17.55.
Large subframes
17.56.
Large subposets
17.57.
Large subpreorders
17.58.
Large subsuplattices
17.59.
Large suplattices
17.60.
Lattices
17.61.
Least upper bounds in large posets
17.62.
Least upper bounds in posets
17.63.
Locales
17.64.
Locally finite posets
17.65.
Lower bounds in large posets
17.66.
Lower bounds in posets
17.67.
Lower sets in large posets
17.68.
Lower types in preorders
17.69.
Maximal chains in posets
17.70.
Maximal chains in preorders
17.71.
Maximal elements in posets
17.72.
Meet-semilattices
17.73.
Meet-suplattices
17.74.
Nuclei on large locales
17.75.
Order preserving maps between large posets
17.76.
Order preserving maps between large preorders
17.77.
Order preserving maps on posets
17.78.
Order preserving maps on preorders
17.79.
Posets
17.80.
Powers of large locales
17.81.
The precategory of decidable total orders
17.82.
The precategory of finite posets
17.83.
The precategory of finite total orders
17.84.
The precategory of inhabited finite total orders
17.85.
The precategory of posets
17.86.
The precategory of total orders
17.87.
Preorders
17.88.
Principal lower sets of large posets
17.89.
Principal upper sets of large posets
17.90.
Reflective Galois connections between large posets
17.91.
Similarity of elements in large posets
17.92.
Similarity of elements in large preorders
17.93.
Similarity of order preserving maps between large posets
17.94.
Similarity of order preserving maps between large preorders
17.95.
Subposets
17.96.
Subpreorders
17.97.
Subtypes leq Posets
17.98.
Suplattices
17.99.
Top elements in large posets
17.100.
Top elements in posets
17.101.
Top elements in preorders
17.102.
Total orders
17.103.
Total preorders
17.104.
Upper bounds of chains in posets
17.105.
Upper bounds in large posets
17.106.
Upper bounds in posets
17.107.
Upper sets of large posets
17.108.
Well-founded orders
17.109.
Well-founded relations
17.110.
Zorn's lemma
18.
Organic Chemistry
❱
18.1.
Alcohols
18.2.
Alkanes
18.3.
Alkenes
18.4.
Alkynes
18.5.
Ethane
18.6.
Hydrocarbons
18.7.
Methane
18.8.
Saturated carbons
19.
Orthogonal factorization systems
❱
19.1.
Cd-structures
19.2.
Cellular maps
19.3.
The closed modalities
19.4.
Double lifts of families of elements
19.5.
Extensions of double lifts of families of elements
19.6.
Extensions of families of elements
19.7.
Extensions of maps
19.8.
Factorization operations
19.9.
Factorization operations into function classes
19.10.
Factorization operations into global function classes
19.11.
Factorizations of maps
19.12.
Factorizations of maps into function classes
19.13.
Factorizations of maps into global function classes
19.14.
Function classes
19.15.
Functoriality of higher modalities
19.16.
Functoriality of the pullback-hom
19.17.
Global function classes
19.18.
Higher modalities
19.19.
The identity modality
19.20.
Lifting operations
19.21.
Lifting structures on commuting squares of maps
19.22.
Lifts of families of elements
19.23.
Lifts of maps
19.24.
Local families of types
19.25.
Local maps
19.26.
Local types
19.27.
Localizations at maps
19.28.
Localizations at subuniverses
19.29.
Locally small modal-operators
19.30.
Mere lifting properties
19.31.
Modal induction
19.32.
Modal operators
19.33.
Modal subuniverse induction
19.34.
Null families of types
19.35.
Null maps
19.36.
Null types
19.37.
The open modalities
19.38.
Orthogonal factorization systems
19.39.
Orthogonal maps
19.40.
Precomposition of lifts of families of elements by maps
19.41.
The pullback-hom
19.42.
The raise modalities
19.43.
Reflective modalities
19.44.
Reflective subuniverses
19.45.
Regular cd-structures
19.46.
Separated types
19.47.
Σ-closed modalities
19.48.
Σ-closed reflective modalities
19.49.
Σ-closed reflective subuniverses
19.50.
Stable orthogonal factorization systems
19.51.
Uniquely eliminating modalities
19.52.
Wide function classes
19.53.
Wide global function classes
19.54.
The zero modality
20.
Polytopes
❱
20.1.
Abstract polytopes
21.
Primitives
❱
21.1.
Characters
21.2.
Floats
21.3.
Machine integers
21.4.
Strings
22.
Real numbers
❱
22.1.
Dedekind real numbers
22.2.
Rational real numbers
23.
Reflection
❱
23.1.
Abstractions
23.2.
Arguments
23.3.
Boolean reflection
23.4.
Definitions
23.5.
Erasing equality
23.6.
Fixity
23.7.
Group solver
23.8.
Literals
23.9.
Metavariables
23.10.
Names
23.11.
Precategory solver
23.12.
Rewriting
23.13.
Terms
23.14.
The type checking monad
24.
Ring theory
❱
24.1.
Additive orders of elements of rings
24.2.
Algebras over rings
24.3.
The binomial theorem for rings
24.4.
The binomial theorem for semirings
24.5.
The category of cyclic rings
24.6.
The category of rings
24.7.
Central elements of rings
24.8.
Central elements of semirings
24.9.
Characteristics of rings
24.10.
Commuting elements of rings
24.11.
Congruence relations on rings
24.12.
Congruence relations on semirings
24.13.
Cyclic rings
24.14.
Dependent products of rings
24.15.
Dependent products of semirings
24.16.
Division rings
24.17.
The free ring with one generator
24.18.
Full ideals of rings
24.19.
Function rings
24.20.
Function semirings
24.21.
Generating elements of rings
24.22.
The group of multiplicative units of a ring
24.23.
Homomorphisms of cyclic rings
24.24.
Homomorphisms of rings
24.25.
Homomorphisms of semirings
24.26.
Ideals generated by subsets of rings
24.27.
Ideals of rings
24.28.
Ideals of semirings
24.29.
Idempotent elements in rings
24.30.
Initial rings
24.31.
Integer multiples of elements of rings
24.32.
Intersections of ideals of rings
24.33.
Intersections of ideals of semirings
24.34.
The invariant basis property of rings
24.35.
Invertible elements in rings
24.36.
Isomorphisms of rings
24.37.
Joins of ideals of rings
24.38.
Joins of left ideals of rings
24.39.
Joins of right ideals of rings
24.40.
Kernels of ring homomorphisms
24.41.
Left ideals generated by subsets of rings
24.42.
Left ideals of rings
24.43.
Local rings
24.44.
Localizations of rings
24.45.
Maximal ideals of rings
24.46.
Modules over rings
24.47.
Multiples of elements in rings
24.48.
Multiplicative orders of elements of rings
24.49.
Nil ideals of rings
24.50.
Nilpotent elements in rings
24.51.
Nilpotent elements in semirings
24.52.
Opposite rings
24.53.
The poset of cyclic rings
24.54.
The poset of ideals of a ring
24.55.
The poset of left ideals of a ring
24.56.
The poset of right ideals of a ring
24.57.
Powers of elements in rings
24.58.
Powers of elements in semirings
24.59.
The precategory of rings
24.60.
The precategory of semirings
24.61.
Products of ideals of rings
24.62.
Products of left ideals of rings
24.63.
Products of right ideals of rings
24.64.
Products of rings
24.65.
Products of subsets of rings
24.66.
Quotient rings
24.67.
Radical ideals of rings
24.68.
Right ideals generated by subsets of rings
24.69.
Right ideals of rings
24.70.
Rings
24.71.
Semirings
24.72.
Subsets of rings
24.73.
Subsets of semirings
24.74.
Sums of elements in rings
24.75.
Sums of elements in semirings
24.76.
Transporting ring structures along isomorphisms of abelian groups
24.77.
Trivial rings
25.
Set theory
❱
25.1.
Baire space
25.2.
Cantor space
25.3.
Cardinalities of sets
25.4.
Countable sets
25.5.
Cumulative hierarchy
25.6.
Infinite sets
25.7.
Uncountable sets
26.
Species
❱
26.1.
Cartesian exponents of species
26.2.
Cartesian products of species of types
26.3.
Cauchy composition of species of types
26.4.
Cauchy composition of species of types in a subuniverse
26.5.
Cauchy exponentials of species of types
26.6.
Cauchy exponentials of species of types in a subuniverse
26.7.
Cauchy products of species of types
26.8.
Cauchy products of species of types in a subuniverse
26.9.
Cauchy series of species of types
26.10.
Cauchy series of species of types in a subuniverse
26.11.
Composition of Cauchy series of species of types
26.12.
Composition of Cauchy series of species of types in subuniverses
26.13.
Coproducts of species of types
26.14.
Coproducts of species of types in subuniverses
26.15.
Cycle index series of species
26.16.
Derivatives of species
26.17.
Dirichlet exponentials of a species of types
26.18.
Dirichlet exponentials of species of types in a subuniverse
26.19.
Dirichlet products of species of types
26.20.
Dirichlet products of species of types in subuniverses
26.21.
Dirichlet series of species of finite inhabited types
26.22.
Dirichlet series of species of types
26.23.
Dirichlet series of species of types in subuniverses
26.24.
Equivalences of species of types
26.25.
Equivalences of species of types in subuniverses
26.26.
Exponential of Cauchy series of species of types
26.27.
Exponential of Cauchy series of species of types in subuniverses
26.28.
Hasse-Weil species
26.29.
Morphisms of finite species
26.30.
Morphisms of species of types
26.31.
Pointing of species of types
26.32.
The precategory of finite species
26.33.
Products of Cauchy series of species of types
26.34.
Products of Cauchy series of species of types in subuniverses
26.35.
Products of Dirichlet series of species of finite inhabited types
26.36.
Products of Dirichlet series of species of types
26.37.
Products of Dirichlet series of species of types in subuniverses
26.38.
Small Composition of species of finite inhabited types
26.39.
Small Cauchy composition of species types in subuniverses
26.40.
Species of finite inhabited types
26.41.
Species of finite types
26.42.
Species of inhabited types
26.43.
Species of types
26.44.
Species of types in subuniverses
26.45.
The unit of Cauchy composition of types
26.46.
The unit of Cauchy composition of species of types in subuniverses
26.47.
Unlabeled structures of finite species
27.
Structured types
❱
27.1.
Cartesian products of types equipped with endomorphisms
27.2.
Central H-spaces
27.3.
Commuting squares of pointed homotopies
27.4.
Commuting squares of pointed maps
27.5.
Commuting triangles of pointed maps
27.6.
Conjugation of pointed types
27.7.
Constant pointed maps
27.8.
Contractible pointed types
27.9.
Cyclic types
27.10.
Dependent products of H-spaces
27.11.
Dependent products of pointed types
27.12.
Dependent products of wild monoids
27.13.
Dependent types equipped with automorphisms
27.14.
Equivalences of H-spaces
27.15.
Equivalences of pointed arrows
27.16.
Equivalences of types equipped with automorphisms
27.17.
Equivalences of types equipped with endomorphisms
27.18.
Faithful pointed maps
27.19.
Fibers of pointed maps
27.20.
Finite multiplication in magmas
27.21.
Function H-spaces
27.22.
Function magmas
27.23.
Function wild monoids
27.24.
Globular types
27.25.
H-spaces
27.26.
The initial pointed type equipped with an automorphism
27.27.
The involutive type of H-space structures on a pointed type
27.28.
Involutive types
27.29.
Iterated cartesian products of types equipped with endomorphisms
27.30.
Iterated cartesian products of pointed types
27.31.
Large globular types
27.32.
Large reflexive globular types
27.33.
Large symmetric globular types
27.34.
Large transitive globular types
27.35.
Magmas
27.36.
Mere equivalences of types equipped with endomorphisms
27.37.
Morphisms of H-spaces
27.38.
Morphisms of magmas
27.39.
Morphisms of pointed arrows
27.40.
Morphisms of twisted pointed arrows
27.41.
Morphisms of types equipped with automorphisms
27.42.
Morphisms of types equipped with endomorphisms
27.43.
Morphisms of wild monoids
27.44.
Noncoherent H-spaces
27.45.
Opposite pointed spans
27.46.
Pointed 2-homotopies
27.47.
Pointed cartesian product types
27.48.
Pointed dependent functions
27.49.
Pointed dependent pair types
27.50.
Pointed equivalences
27.51.
Pointed families of types
27.52.
Pointed homotopies
27.53.
Pointed isomorphisms
27.54.
Pointed maps
27.55.
Pointed retractions of pointed maps
27.56.
Pointed sections of pointed maps
27.57.
Pointed span diagrams
27.58.
Pointed spans
27.59.
Pointed types
27.60.
Pointed types equipped with automorphisms
27.61.
The pointed unit type
27.62.
Universal property of contractible types with respect to pointed types and maps
27.63.
Postcomposition of pointed maps
27.64.
Precomposition of pointed maps
27.65.
Reflexive globular types
27.66.
Sets equipped with automorphisms
27.67.
Small pointed types
27.68.
Symmetric elements of involutive types
27.69.
Symmetric globular types
27.70.
Symmetric H-spaces
27.71.
Transitive globular types
27.72.
Transposition of pointed span diagrams
27.73.
Types equipped with automorphisms
27.74.
Types equipped with endomorphisms
27.75.
Uniform pointed homotopies
27.76.
The universal property of pointed equivalences
27.77.
Unpointed maps between pointed types
27.78.
Whiskering pointed homotopies with respect to concatenation
27.79.
Whiskering of pointed homotopies with respect to composition of pointed maps
27.80.
Wild groups
27.81.
Wild loops
27.82.
Wild monoids
27.83.
Wild quasigroups
27.84.
Wild semigroups
28.
Synthetic homotopy theory
❱
28.1.
0-acyclic maps
28.2.
0-acyclic types
28.3.
1-acyclic types
28.4.
Formalization of the Symmetry book - 26 id pushout
28.5.
Acyclic maps
28.6.
Acyclic types
28.7.
The category of connected set bundles over the circle
28.8.
Cavallo's trick
28.9.
The circle
28.10.
Cocartesian morphisms of arrows
28.11.
Cocones under pointed span diagrams
28.12.
Cocones under sequential diagrams
28.13.
Cocones under spans
28.14.
Codiagonals of maps
28.15.
Coequalizers
28.16.
Cofibers
28.17.
Coforks
28.18.
Correspondence between cocones under sequential diagrams and certain coforks
28.19.
Conjugation of loops
28.20.
Connected set bundles over the circle
28.21.
Dependent cocones under sequential diagrams
28.22.
Dependent cocones under spans
28.23.
Dependent coforks
28.24.
Dependent descent for the circle
28.25.
The dependent pullback property of pushouts
28.26.
Dependent pushout-products
28.27.
Dependent sequential diagrams
28.28.
Dependent suspension structures
28.29.
The dependent universal property of coequalizers
28.30.
The dependent universal property of pushouts
28.31.
The dependent universal property of sequential colimits
28.32.
Dependent universal property of suspensions
28.33.
The descent property of the circle
28.34.
Descent data for constant type families over the circle
28.35.
Descent data for families of dependent pair types over the circle
28.36.
Descent data for families of equivalence types over the circle
28.37.
Descent data for families of function types over the circle
28.38.
Subtypes of descent data for the circle
28.39.
Descent data for pushouts
28.40.
Descent data for sequential colimits
28.41.
Descent property of pushouts
28.42.
Descent property of sequential colimits
28.43.
Double loop spaces
28.44.
The Eckmann-Hilton argument
28.45.
Equifibered sequential diagrams
28.46.
Equivalences of cocones under sequential diagrams
28.47.
Equivalences of coforks
28.48.
Equivalances of dependent sequential diagrams
28.49.
Equivalences of descent data for pushouts
28.50.
Equivalences of sequential diagrams
28.51.
Families with descent data for pushouts
28.52.
Families with descent data for sequential colimits
28.53.
The flattening lemma for coequalizers
28.54.
The flattening lemma for pushouts
28.55.
The flattening lemma for sequential colimits
28.56.
Free loops
28.57.
Functoriality of the loop space operation
28.58.
Functoriality of sequential colimits
28.59.
Functoriality of suspensions
28.60.
Groups of loops in 1-types
28.61.
Hatcher's acyclic type
28.62.
The induction principle of pushouts
28.63.
The infinite complex projective space
28.64.
Infinite cyclic types
28.65.
The interval
28.66.
Iterated loop spaces
28.67.
Iterated suspensions of pointed types
28.68.
Join powers of types
28.69.
Joins of maps
28.70.
Joins of types
28.71.
Loop spaces
28.72.
Maps of prespectra
28.73.
Mere spheres
28.74.
Morphisms of cocones under morphisms of sequential diagrams
28.75.
Morphisms of coforks
28.76.
Morphisms of dependent sequential diagrams
28.77.
Morphisms of descent data of the circle
28.78.
Morphisms of descent data for pushouts
28.79.
Morphisms of sequential diagrams
28.80.
The multiplication operation on the circle
28.81.
Null cocones under pointed span diagrams
28.82.
The plus-principle
28.83.
Powers of loops
28.84.
Premanifolds
28.85.
Prespectra
28.86.
The pullback property of pushouts
28.87.
Pushout-products
28.88.
Pushouts
28.89.
Pushouts of pointed types
28.90.
The recursion principle of pushouts
28.91.
Retracts of sequential diagrams
28.92.
Rewriting rules for pushouts
28.93.
Sections of families over the circle
28.94.
Sequential colimits
28.95.
Sequential diagrams
28.96.
Sequentially compact types
28.97.
Shifts of sequential diagrams
28.98.
Smash products of pointed types
28.99.
Spectra
28.100.
The sphere prespectrum
28.101.
Spheres
28.102.
Suspension prespectra
28.103.
Suspension Structures
28.104.
Suspensions of pointed types
28.105.
Suspensions of types
28.106.
Tangent spheres
28.107.
Total cocones of type families over cocones under sequential diagrams
28.108.
Total sequential diagrams of dependent sequential diagrams
28.109.
Triple loop spaces
28.110.
k-acyclic maps
28.111.
k-acyclic types
28.112.
The universal cover of the circle
28.113.
The universal property of the circle
28.114.
The universal property of coequalizers
28.115.
The universal property of pushouts
28.116.
The universal property of sequential colimits
28.117.
Universal property of suspensions
28.118.
Universal Property of suspensions of pointed types
28.119.
Wedges of pointed types
28.120.
Zigzags between sequential diagrams
29.
Trees
❱
29.1.
Algebras for polynomial endofunctors
29.2.
Bases of directed trees
29.3.
Bases of enriched directed trees
29.4.
Binary W-types
29.5.
Bounded multisets
29.6.
The coalgebra of directed trees
29.7.
The coalgebra of enriched directed trees
29.8.
Coalgebras of polynomial endofunctors
29.9.
The combinator of directed trees
29.10.
Combinators of enriched directed trees
29.11.
Directed trees
29.12.
The elementhood relation on coalgebras of polynomial endofunctors
29.13.
The elementhood relation on W-types
29.14.
Empty multisets
29.15.
Enriched directed trees
29.16.
Equivalences of directed trees
29.17.
Equivalences of enriched directed trees
29.18.
Extensional W-types
29.19.
Fibers of directed trees
29.20.
Fibers of enriched directed trees
29.21.
Full binary trees
29.22.
Functoriality of the combinator of directed trees
29.23.
Functoriality of the fiber operation on directed trees
29.24.
Functoriality of W-types
29.25.
Hereditary W-types
29.26.
Indexed W-types
29.27.
Induction principles on W-types
29.28.
Inequality on W-types
29.29.
Lower types of elements in W-types
29.30.
Morphisms of algebras of polynomial endofunctors
29.31.
Morphisms of coalgebras of polynomial endofunctors
29.32.
Morphisms of directed trees
29.33.
Morphisms of enriched directed trees
29.34.
Multiset-indexed dependent products of types
29.35.
Multisets
29.36.
Planar binary trees
29.37.
Plane trees
29.38.
Polynomial endofunctors
29.39.
Raising universe levels of directed trees
29.40.
Ranks of elements in W-types
29.41.
Rooted morphisms of directed trees
29.42.
Rooted morphisms of enriched directed trees
29.43.
Rooted quasitrees
29.44.
Rooted undirected trees
29.45.
Small multisets
29.46.
Submultisets
29.47.
Transitive multisets
29.48.
The underlying trees of elements of coalgebras of polynomial endofunctors
29.49.
The underlying trees of elements of W-types
29.50.
Undirected trees
29.51.
The universal multiset
29.52.
The universal tree
29.53.
The W-type of natural numbers
29.54.
The W-type of the type of propositions
29.55.
W-types
30.
Type theories
❱
30.1.
Comprehension of fibered type theories
30.2.
Dependent type theories
30.3.
Fibered dependent type theories
30.4.
Π-types in precategories with attributes
30.5.
Π-types in precategories with families
30.6.
Precategories with attributes
30.7.
Precategories with families
30.8.
Sections of dependent type theories
30.9.
Simple type theories
30.10.
Unityped type theories
31.
Univalent combinatorics
❱
31.1.
2-element decidable subtypes
31.2.
2-element subtypes
31.3.
2-element types
31.4.
The binomial types
31.5.
Bracelets
31.6.
Cartesian products of finite types
31.7.
The classical definition of the standard finite types
31.8.
Complements of isolated elements of finite types
31.9.
Coproducts of finite types
31.10.
Counting in type theory
31.11.
Counting the elements of decidable subtypes
31.12.
Counting the elements of dependent pair types
31.13.
Counting the elements of the fiber of a map
31.14.
Counting the elements in Maybe
31.15.
Cubes
31.16.
Cycle partitions of finite types
31.17.
Cycle prime decompositions of natural numbers
31.18.
Cyclic finite types
31.19.
Decidable dependent function types
31.20.
Decidability of dependent pair types
31.21.
Decidable equivalence relations on finite types
31.22.
Decidable propositions
31.23.
Decidable subtypes of finite types
31.24.
Dedekind finite sets
31.25.
Counting the elements of dependent function types
31.26.
Dependent pair types of finite types
31.27.
Finite discrete Σ-decompositions
31.28.
Distributivity of set truncation over finite products
31.29.
Double counting
31.30.
Injective maps
31.31.
Embeddings between standard finite types
31.32.
Equality in finite types
31.33.
Equality in the standard finite types
31.34.
Equivalences between finite types
31.35.
Equivalences of cubes
31.36.
Equivalences between standard finite types
31.37.
Ferrers diagrams (unlabeled partitions)
31.38.
Fibers of maps between finite types
31.39.
Finite choice
31.40.
Finiteness of the type of connected components
31.41.
Finite presentations of types
31.42.
Finite types
31.43.
Finitely presented types
31.44.
Finite function types
31.45.
The image of a map
31.46.
Inequality on types equipped with a counting
31.47.
Inhabited finite types
31.48.
Injective maps between finite types
31.49.
An involution on the standard finite types
31.50.
Isotopies of Latin squares
31.51.
Kuratowsky finite sets
31.52.
Latin squares
31.53.
The groupoid of main classes of Latin hypercubes
31.54.
The groupoid of main classes of Latin squares
31.55.
The maybe modality on finite types
31.56.
Necklaces
31.57.
Orientations of the complete undirected graph
31.58.
Orientations of cubes
31.59.
Partitions of finite types
31.60.
Petri-nets
31.61.
π-finite types
31.62.
The pigeonhole principle
31.63.
Finitely π-presented types
31.64.
Quotients of finite types
31.65.
Ramsey theory
31.66.
Repetitions of values
31.67.
Repetitions of values in sequences
31.68.
Retracts of finite types
31.69.
Sequences of elements in finite types
31.70.
Set quotients of index 2
31.71.
Finite Σ-decompositions of finite types
31.72.
Skipping elements in standard finite types
31.73.
Small types
31.74.
Standard finite pruned trees
31.75.
Standard finite trees
31.76.
The standard finite types
31.77.
Steiner systems
31.78.
Steiner triple systems
31.79.
Subfinite types
31.80.
Combinatorial identities of sums of natural numbers
31.81.
Surjective maps between finite types
31.82.
Symmetric difference of finite subtypes
31.83.
Finite trivial Σ-decompositions
31.84.
Type duality of finite types
31.85.
Unions of finite subtypes
31.86.
The universal property of the standard finite types
31.87.
Unlabeled partitions
31.88.
Unlabeled rooted trees
31.89.
Unlabeled trees
32.
Universal Algebra
❱
32.1.
Abstract equations over signatures
32.2.
Algebraic theories
32.3.
Algebraic theory of groups
32.4.
Algebras
32.5.
Congruences
32.6.
Homomorphisms of algebras
32.7.
Kernels of homomorphisms of algebras
32.8.
Models of signatures
32.9.
Quotient algebras
32.10.
Signatures
32.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