Project
1.
Agda-UniMath
❱
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.3.
How-to
❱
1.3.1.
Install
1.3.2.
Cite the library
1.4.
Guidelines
❱
1.4.1.
Structure your file
❱
1.4.1.1.
TEMPLATE.lagda.md
1.4.2.
Library coding style
1.4.3.
Design principles
1.5.
Everything
Formalisation in Agda
2.
Category theory
❱
2.1.
Adjunctions between large precategories
2.2.
Anafunctors
2.3.
Categories
2.4.
Coproducts in precategories
2.5.
Discrete categories
2.6.
Endomorphisms of objects in categories
2.7.
Epimorphism in large precategories
2.8.
Equivalences between categories
2.9.
Equivalences between large precategories
2.10.
Equivalences between precategories
2.11.
Exponential objects in precategories
2.12.
Functors between categories
2.13.
Functors between large precategories
2.14.
Functors between precategories
2.15.
Groupoids
2.16.
Homotopies of natural transformations in large precategories
2.17.
Initial objects of a precategory
2.18.
Isomorphisms in categories
2.19.
Isomorphisms in large precategories
2.20.
Isomorphisms in precategories
2.21.
Large categories
2.22.
Large precategories
2.23.
Monomorphisms in large precategories
2.24.
Natural isomorphisms between functors between categories
2.25.
Natural isomorphisms between functors on large precategories
2.26.
Natural isomorphisms between functors between precategories
2.27.
Natural numbers object in a precategory
2.28.
Natural transformations between functors between categories
2.29.
Natural transformations between functors between large precategories
2.30.
Natural transformations between functors on precategories
2.31.
Opposite precategories
2.32.
Precategories
2.33.
The precategory of functors and natural transformations between two fixed precategories
2.34.
Pregroupoids
2.35.
Products of precategories
2.36.
Products in precategories
2.37.
Pullbacks in precategories
2.38.
Sieves in categories
2.39.
Slice precategories
2.40.
Terminal object of a precategory
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.
Commutative rings
3.5.
Commutative semirings
3.6.
Dependent products of commutative rings
3.7.
Dependent products of commutative semirings
3.8.
Discrete fields
3.9.
The Eisenstein integers
3.10.
Euclidean domains
3.11.
Function commutative rings
3.12.
Function commutative semirings
3.13.
The Gaussian integers
3.14.
Homomorphisms of commutative rings
3.15.
Homomorphisms of commutative semirings
3.16.
Ideals in commutative rings
3.17.
Ideals in commutative semirings
3.18.
Ideals generated by subsets of commutative rings
3.19.
Integral domains
3.20.
Invertible elements in commutative rings
3.21.
Isomorphisms of commutative rings
3.22.
Local commutative rings
3.23.
Maximal ideals in commutative rings
3.24.
Nilradical of a commutative ring
3.25.
The nilradical of a commutative semiring
3.26.
Powers of elements in commutative rings
3.27.
Powers of elements in commutative semirings
3.28.
The precategory of commutative rings
3.29.
The precategory of commutative semirings
3.30.
Prime ideals in commutative rings
3.31.
Radical ideals in commutative rings
3.32.
Radicals of ideals in commutative rings
3.33.
Subsets of commutative rings
3.34.
Subsets of commutative semirings
3.35.
Sums in commutative rings
3.36.
Sums in commutative semirings
3.37.
Trivial commutative rings
3.38.
The Zariski topology on the set of prime ideals in 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 rationals
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 of integers
4.74.
Multiplication of the elements of a list of natural numbers
4.75.
Multiplication of natural numbers
4.76.
Multiset coefficients
4.77.
The type of natural numbers
4.78.
Nonzero natural numbers
4.79.
The ordinal induction principle for the natural numbers
4.80.
Parity of the natural numbers
4.81.
Pisano periods
4.82.
Powers of integers
4.83.
Powers of Two
4.84.
Prime numbers
4.85.
Products of natural numbers
4.86.
Proper divisors of natural numbers
4.87.
Pythagorean triples
4.88.
The rational numbers
4.89.
Reduced integer fractions
4.90.
Relatively prime integers
4.91.
Relatively prime natural numbers
4.92.
Repeating an element in a standard finite type
4.93.
Retracts of the type of natural numbers
4.94.
The sieve of Eratosthenes
4.95.
Square-free natural numbers
4.96.
Stirling numbers of the second kind
4.97.
Strict inequality natural numbers
4.98.
Strictly ordered pairs of natural numbers
4.99.
The strong induction principle for the natural numbers
4.100.
Sums of natural numbers
4.101.
Telephone numbers
4.102.
The triangular numbers
4.103.
The Twin Prime conjecture
4.104.
Type arithmetic with natural numbers
4.105.
Unit elements in the standard finite types
4.106.
Unit similarity on the standard finite types
4.107.
The universal property of the natural numbers
4.108.
Upper bounds for type families over the natural numbers
4.109.
The Well-Ordering Principle of the natural numbers
4.110.
The Well-Ordering Principle of the standard finite types
5.
Finite group theory
❱
5.1.
The abstract quaternion group of order 8
5.2.
Alternating concrete groups
5.3.
Alternating groups
5.4.
Cartier's delooping of the sign homomorphism
5.5.
The concrete quaternion group
5.6.
Deloopings of the sign homomorphism
5.7.
Finite groups
5.8.
Finite monoids
5.9.
Finite semigroups
5.10.
The group of n-element types
5.11.
Groups of order 2
5.12.
Orbits of permutations
5.13.
Permutations
5.14.
Permutations of standard finite types
5.15.
The sign homomorphism
5.16.
Simpson's delooping of the sign homomorphism
5.17.
Subgroups of finite groups
5.18.
Tetrahedra in 3-dimensional space
5.19.
Transpositions
5.20.
Transpositions of standard finite types
6.
Foundation
❱
6.1.
0-Connected types
6.2.
0-Images of maps
6.3.
0-Maps
6.4.
1-Types
6.5.
2-Types
6.6.
Apartness relations
6.7.
Arithmetic law for coproduct decomposition and Σ-decomposition
6.8.
Automorphisms of types
6.9.
Axiom L
6.10.
The axiom of choice
6.11.
Bands
6.12.
Binary embeddings
6.13.
Binary equivalences
6.14.
Binary equivalences on unordered pairs of types
6.15.
Binary functoriality of set quotients
6.16.
Homotopies of binary operations
6.17.
Binary operations on unordered pairs of types
6.18.
Binary reflecting maps of equivalence relations
6.19.
Binary relations
6.20.
Binary transport
6.21.
The booleans
6.22.
The Cantor–Schröder–Bernstein–Escardó theorem
6.23.
Cantor's diagonal argument
6.24.
Cartesian product types
6.25.
Cartesian products of set quotients
6.26.
The category of sets
6.27.
Choice of representatives for an equivalence relation
6.28.
Coherently invertible maps
6.29.
Commuting 3-simplices of homotopies
6.30.
Commuting 3-simplices of maps
6.31.
Commuting cubes of maps
6.32.
Commuting squares of identifications
6.33.
Commuting squares of maps
6.34.
Commuting triangles of homotopies
6.35.
Commuting triangles of maps
6.36.
Complements of type families
6.37.
Complements of subtypes
6.38.
Cones on pullback diagrams
6.39.
Conjunction of propositions
6.40.
Connected components of types
6.41.
Connected components of universes
6.42.
Connected maps
6.43.
Connected types
6.44.
Constant maps
6.45.
Contractible maps
6.46.
Contractible types
6.47.
Coproduct decompositions
6.48.
Coproduct decompositions in a subuniverse
6.49.
Coproduct types
6.50.
Morphisms in the coslice category of types
6.51.
Cospans
6.52.
Decidability of dependent function types
6.53.
Decidability of dependent pair types
6.54.
Decidable embeddings
6.55.
Decidable equality
6.56.
Decidable equivalence relations
6.57.
Decidable maps
6.58.
Decidable propositions
6.59.
Decidable relations on types
6.60.
Decidable subtypes
6.61.
Decidable types
6.62.
The dependent binomial theorem for types (Distributivity of dependent function types over coproduct types)
6.63.
Dependent pair types
6.64.
Dependent paths
6.65.
Descent for coproduct types
6.66.
Descent for dependent pair types
6.67.
Descent for the empty type
6.68.
Descent for equivalences
6.69.
Diagonal maps of types
6.70.
Diagonals of maps
6.71.
Discrete reflexive relations
6.72.
Discrete relaxed Σ-decompositions
6.73.
Discrete Σ-Decompositions
6.74.
Discrete types
6.75.
Disjunction of propositions
6.76.
Double negation
6.77.
Double powersets
6.78.
Dubuc-Penon compact types
6.79.
Effective maps for equivalence relations
6.80.
Embeddings
6.81.
Empty types
6.82.
Endomorphisms
6.83.
Epimorphisms
6.84.
Epimorphisms with respect to maps into sets
6.85.
Epimorphisms with respect to truncated types
6.86.
Equality of cartesian product types
6.87.
Equality of coproduct types
6.88.
Equality on dependent function types
6.89.
Equality of dependent pair types
6.90.
Equality in the fibers of a map
6.91.
Equivalence classes
6.92.
Equivalence extensionality
6.93.
Equivalence induction
6.94.
Equivalence relations
6.95.
Equivalences
6.96.
Equivalences on Maybe
6.97.
Exclusive disjunction of propositions
6.98.
Existential quantification
6.99.
Exponents of set quotients
6.100.
Faithful maps
6.101.
Fiber inclusions
6.102.
Fibered equivalences
6.103.
Fibered involutions
6.104.
Maps fibered over a map
6.105.
Fibers of maps
6.106.
Full subtypes of types
6.107.
Function extensionality
6.108.
Functional correspondences
6.109.
Functions
6.110.
Functoriality of cartesian product types
6.111.
Functoriality of coproduct types
6.112.
Functoriality of dependent function types
6.113.
Functoriality of dependent pair types
6.114.
Functoriality of fib
6.115.
Functoriality of function types
6.116.
Functoriality of propositional truncations
6.117.
Functoriality of set quotients
6.118.
Functoriality of set truncation
6.119.
Functoriality of truncations
6.120.
The fundamental theorem of identity types
6.121.
Global choice
6.122.
Hexagons of identifications
6.123.
Hilbert's ε-operators
6.124.
Homotopies
6.125.
Identity systems
6.126.
Identity types of truncated types
6.127.
Identity types
6.128.
The image of a map
6.129.
Images of subtypes
6.130.
Impredicative encodings of the logical operations
6.131.
Impredicative universes
6.132.
The induction principle for propositional truncation
6.133.
Inhabited subtypes
6.134.
Inhabited types
6.135.
Injective maps
6.136.
The interchange law
6.137.
Intersection of subtypes
6.138.
Involutions
6.139.
Isolated points
6.140.
Isomorphisms of sets
6.141.
Iterated cartesian product types
6.142.
Iterating automorphisms
6.143.
Iterating functions
6.144.
Iterating involutions
6.145.
Large dependent pair types
6.146.
Large homotopies
6.147.
Large identity types
6.148.
The large locale of propositions
6.149.
The large locale of subtypes
6.150.
The law of excluded middle
6.151.
Lawvere's fixed point theorem
6.152.
The lesser limited principle of omniscience
6.153.
The limited principle of omniscience (LPO)
6.154.
Locally small types
6.155.
Logical equivalences
6.156.
The maybe modality
6.157.
Mere embeddings
6.158.
Mere equality
6.159.
Mere equivalences
6.160.
Monomorphisms
6.161.
Morphisms of cospans
6.162.
Multisubsets
6.163.
Multivariable correspondences
6.164.
Multivariable decidable relations
6.165.
Multivariable functoriality of set quotients
6.166.
Multivariable operations
6.167.
Multivariable relations
6.168.
Negation
6.169.
Non-contractible types
6.170.
Pairs of distinct elements
6.171.
Partial elements
6.172.
Partitions
6.173.
Path algebra
6.174.
Path-split maps
6.175.
Perfect images
6.176.
Powersets
6.177.
Preidempotent maps
6.178.
Preimages of subtypes
6.179.
The principle of omniscience
6.180.
Product decompositions
6.181.
Products of binary relataions
6.182.
Products of equivalence relataions
6.183.
Products of tuples of types
6.184.
Products of unordered pairs of types
6.185.
Products of unordered tuples of types
6.186.
Projective types
6.187.
Proper subsets
6.188.
Propositional extensionality
6.189.
Propositional maps
6.190.
Propositional resizing
6.191.
Propositional truncations
6.192.
Propositions
6.193.
Pullback squares
6.194.
Pullbacks
6.195.
Raising universe levels
6.196.
Reflecting maps for equivalence relations
6.197.
Reflexive relations
6.198.
Relaxed Σ-decompositions of types
6.199.
Repetitions of values of maps
6.200.
Repetitions in sequences
6.201.
The replacement axiom for type theory
6.202.
Retractions
6.203.
Russell's paradox
6.204.
Sections
6.205.
Sequences
6.206.
Set presented types
6.207.
Set quotients
6.208.
Set truncations
6.209.
Sets
6.210.
Shifting sequences
6.211.
Σ-decompositions of types into types in a subuniverse
6.212.
Σ-decompositions of types
6.213.
Singleton induction
6.214.
Singleton subtypes
6.215.
Morphisms of the slice category of types
6.216.
Small maps
6.217.
Small types
6.218.
Small universes
6.219.
Split surjective maps
6.220.
Standard apartness relations
6.221.
Strongly extensional maps
6.222.
Structure
6.223.
The structure identity principle
6.224.
Structured type duality
6.225.
Subterminal types
6.226.
Subtype duality
6.227.
The subtype identity principle
6.228.
Subtypes
6.229.
Subuniverse
6.230.
Surjective maps
6.231.
Symmetric difference of subtypes
6.232.
The symmetric identity types
6.233.
Symmetric operations
6.234.
Tight apartness relations
6.235.
Transport
6.236.
Trivial relaxed Σ-Decompositions
6.237.
Trivial Σ-Decompositions
6.238.
Truncated equality
6.239.
Truncated maps
6.240.
Truncated types
6.241.
k-Equivalences
6.242.
Truncation images of maps
6.243.
Truncation levels
6.244.
Truncations
6.245.
Tuples of types
6.246.
Type arithmetic with the booleans
6.247.
Type arithmetic for cartesian product types
6.248.
Type arithmetic for coproduct types
6.249.
Type arithmetic with dependent function types
6.250.
Type arithmetic for dependent pair types
6.251.
Type arithmetic with the empty type
6.252.
Type arithmetic with the unit type
6.253.
Type duality
6.254.
The type theoretic principle of choice
6.255.
Union of subtypes
6.256.
Unique existence
6.257.
Uniqueness of the image of a map
6.258.
The uniqueness of set quotients
6.259.
Uniqueness of set truncations
6.260.
Uniqueness of the truncations
6.261.
The unit type
6.262.
Unital binary operations
6.263.
The univalence axiom
6.264.
Univalent action on equivalences
6.265.
The univalence axiom implies function extensionality
6.266.
Univalent type families
6.267.
The universal property of booleans
6.268.
The universal propert of cartesian product types
6.269.
The universal property of coproduct types
6.270.
The universal property of dependent pair types
6.271.
The universal property of the empty type
6.272.
The universal property of fiber products
6.273.
The universal property of identity types
6.274.
The universal property of the image of a map
6.275.
The universal property of maybe
6.276.
The universal property of propositional truncations
6.277.
The universal property of propositional truncations with respect to sets
6.278.
The universal property of pullbacks
6.279.
The universal property of set quotients
6.280.
The universal property of set truncations
6.281.
The universal property of truncations
6.282.
The universal property of the unit type
6.283.
Universe levels
6.284.
Unordered pairs of elements in a type
6.285.
Unordered pairs of types
6.286.
Unordered n-tuples of elements in a type
6.287.
Unordered tuples of types
6.288.
Vectors of set quotients
6.289.
Weak function extensionality
6.290.
The weak limited principle of omniscience
6.291.
Weakly constant maps
7.
Foundation core
❱
7.1.
0-Maps
7.2.
1-Types
7.3.
Automorphisms
7.4.
Cartesian product types
7.5.
Coherently invertible maps
7.6.
Commuting 3-simplices of homotopies
7.7.
Commuting 3-simplices of maps
7.8.
Commuting cubes of maps
7.9.
Commuting squares of maps
7.10.
Commuting triangles of homotopies
7.11.
Commuting triangles of maps
7.12.
Cones on pullback diagrams
7.13.
Constant maps
7.14.
Contractible maps
7.15.
Contractible types
7.16.
Coproduct types
7.17.
Cospans
7.18.
Decidable propositions
7.19.
Dependent pair types
7.20.
Diagonal maps of types
7.21.
Discrete types
7.22.
Embeddings
7.23.
Empty types
7.24.
Endomorphisms
7.25.
Equality of cartesian product types
7.26.
Equality of dependent pair types
7.27.
Equality in the fibers of a map
7.28.
Equivalence induction
7.29.
Equivalence relations
7.30.
Equivalences
7.31.
Faithful maps
7.32.
Fibers of maps
7.33.
Function extensionality
7.34.
Functions
7.35.
Functoriality of dependent function types
7.36.
Functoriality of dependent pair types
7.37.
The functoriality of fib
7.38.
Functoriality of function types
7.39.
The fundamental theorem of identity types
7.40.
Homotopies
7.41.
Identity systems
7.42.
Identity types
7.43.
Injective maps
7.44.
Involutions
7.45.
Logical equivalences
7.46.
Morphisms of cospans
7.47.
Negation
7.48.
Path-split maps
7.49.
Propositional maps
7.50.
Propositions
7.51.
Pullbacks
7.52.
Retractions
7.53.
Sections
7.54.
Sets
7.55.
Singleton induction
7.56.
Small types
7.57.
The subtype identity principle
7.58.
Subtypes
7.59.
Truncated maps
7.60.
Truncated types
7.61.
Truncation levels
7.62.
Type arithmetic for cartesian product types
7.63.
Type arithmetic for dependent pair types
7.64.
The univalence axiom
7.65.
The universal property of pullbacks
7.66.
The universal property of truncations
7.67.
Universe levels
8.
Graph theory
❱
8.1.
Acyclic undirected graphs
8.2.
Circuits in undirected graphs
8.3.
Closed walks in undirected graphs
8.4.
Complete bipartite graphs
8.5.
Complete multipartite graphs
8.6.
Complete undirected graphs
8.7.
Connected graphs
8.8.
Cycles in undirected graphs
8.9.
Directed graph structures on standard finite sets
8.10.
Directed graphs
8.11.
Edge-coloured undirected graphs
8.12.
Embeddings of directed graphs
8.13.
Embeddings of undirected graphs
8.14.
Enriched undirected graphs
8.15.
Equivalences of directed graphs
8.16.
Equivalences of enriched undirected graphs
8.17.
Equivalences of undirected graphs
8.18.
Eulerian circuits in undirected graphs
8.19.
Faithful morphisms of undirected graphs
8.20.
Fibers of directed graphs
8.21.
Finite graphs
8.22.
Geometric realizations of undirected graphs
8.23.
Hypergraphs
8.24.
Matchings
8.25.
Mere equivalences of undirected graphs
8.26.
Morphisms of directed graphs
8.27.
Morphisms of undirected graphs
8.28.
Incidence in undirected graphs
8.29.
Orientations of undirected graphs
8.30.
Paths in undirected graphs
8.31.
Polygons
8.32.
Raising universe levels of directed graphs
8.33.
Reflecting maps of undirected graphs
8.34.
Reflexive graphs
8.35.
Regular undirected graph
8.36.
Simple undirected graphs
8.37.
Stereoisomerism for enriched undirected graphs
8.38.
Totally faithful morphisms of undirected graphs
8.39.
Trails in directed graphs
8.40.
Trails in undirected graphs
8.41.
Undirected graph structures on standard finite sets
8.42.
Undirected graphs
8.43.
Vertex covers
8.44.
Voltage graphs
8.45.
Walks in directed graphs
8.46.
Walks in undirected graphs
9.
Group theory
❱
9.1.
Abelian groups
9.2.
Pointwise addition of morphisms of abelian groups
9.3.
Automorphism groups
9.4.
Cartesian products of abelian groups
9.5.
Cartesian products of concrete groups
9.6.
Cartesian products of groups
9.7.
Cartesian products of monoids
9.8.
Cartesian products of semigroups
9.9.
The category of concrete groups
9.10.
The category of groups
9.11.
The category of semigroups
9.12.
Cayley's theorem
9.13.
The center of a group
9.14.
Center of a monoid
9.15.
Center of a semigroup
9.16.
Central elements of groups
9.17.
Central elements of monoids
9.18.
Central elements of semirings
9.19.
Commutative monoids
9.20.
Commutators of elements in groups
9.21.
Concrete group actions
9.22.
Concrete groups
9.23.
Congruence relations on abelian groups
9.24.
Congruence relations on commutative monoids
9.25.
Congruence relations on groups
9.26.
Congruence relations on monoids
9.27.
Congruence relations on semigroups
9.28.
Conjugation in groups
9.29.
Contravariant pushforwards of concrete group actions
9.30.
Decidable subgroups of groups
9.31.
Dependent products of abelian groups
9.32.
Dependent products of commutative monoids
9.33.
Dependent products of groups
9.34.
Dependent products of monoids
9.35.
Dependent products of semigroups
9.36.
The dihedral group construction
9.37.
The dihedral groups
9.38.
The E₈-lattice
9.39.
Embeddings of abelian groups
9.40.
Embeddings of groups
9.41.
The endomorphism rings of abelian groups
9.42.
Epimorphisms in groups
9.43.
Equivalences of concrete group actions
9.44.
Equivalences of concrete groups
9.45.
Equivalences of group actions
9.46.
Equivalences between semigroups
9.47.
Free concrete group actions
9.48.
Free groups with one generator
9.49.
The full subgroup of a group
9.50.
Function groups of abelian groups
9.51.
Function commutative monoids
9.52.
Function groups
9.53.
Function monoids
9.54.
Function semigroups
9.55.
Furstenberg groups
9.56.
Group actions
9.57.
Abstract groups
9.58.
Homomorphisms of abelian groups
9.59.
Homomorphisms of commutative monoids
9.60.
Morphisms of concrete group actions
9.61.
Homomorphisms of concrete groups
9.62.
Homomorphisms of generated subgroups
9.63.
Homomorphisms of group actions
9.64.
Homomorphisms of groups
9.65.
Homomorphisms of monoids
9.66.
Homomorphisms of semigroups
9.67.
Inverse semigroups
9.68.
Invertible elements in monoids
9.69.
Isomorphisms of abelian groups
9.70.
Isomorphisms of concrete groups
9.71.
Isomorphisms of group actions
9.72.
Isomorphisms of groups
9.73.
Isomorphisms of semigroups
9.74.
Iterated cartesian products of concrete groups
9.75.
Kernels
9.76.
Kernels of homomorphisms of concrete groups
9.77.
Large semigroups
9.78.
Concrete automorphism groups on sets
9.79.
Mere equivalences of concrete group actions
9.80.
Mere equivalences of group actions
9.81.
Monoid actions
9.82.
Monoids
9.83.
Monomorphisms of concrete groups
9.84.
Monomorphisms in the category of groups
9.85.
Normal subgroups
9.86.
Normal subgroups of concrete groups
9.87.
Normal submonoids
9.88.
Normal submonoids of commutative monoids
9.89.
The opposite of a group
9.90.
The orbit-stabilizer theorem for concrete groups
9.91.
Orbits of concrete group actions
9.92.
Orbits of group actions
9.93.
The precategory of orbits of a monoid action
9.94.
The order of an element in a group
9.95.
The precategory of abelian groups
9.96.
The precategory of commutative monoids
9.97.
The precategory of concrete groups
9.98.
The precategory of group actions
9.99.
The precategory of groups
9.100.
The precategory of monoids
9.101.
The precategory of semigroups
9.102.
Principal group actions
9.103.
Principal torsors of concrete groups
9.104.
Products of elements in a monoid
9.105.
Products of tuples of elements in commutative monoids
9.106.
Quotient groups
9.107.
Quotient groups of concrete groups
9.108.
Quotients of abelian groups
9.109.
Representations of monoids
9.110.
Saturated congruence relations on commutative monoids
9.111.
Saturated congruence relations on monoids
9.112.
Semigroups
9.113.
Sheargroups
9.114.
Shriek of concrete group homomorphisms
9.115.
Stabilizer groups
9.116.
Stabilizers of concrete group actions
9.117.
Subgroups
9.118.
Subgroups of abelian groups
9.119.
Subgroups of concrete groups
9.120.
Subgroups generated by subsets of groups
9.121.
Submonoids
9.122.
Submonoids of commutative monoids
9.123.
Subsemigroups
9.124.
Subsets of commutative monoids
9.125.
Subsets of monoids
9.126.
The substitution functor of concrete group actions
9.127.
The substitution functor of group actions
9.128.
Symmetric concrete groups
9.129.
Symmetric groups
9.130.
Torsors of abstract groups
9.131.
Transitive concrete group actions
9.132.
Transitive group actions
9.133.
Trivial subgroups
9.134.
Unordered tuples of elements in commutative monoids
10.
Higher group theory
❱
10.1.
Cartesian products of higher groups
10.2.
Equivalences of higher groups
10.3.
Fixed points of higher group actions
10.4.
Free higher group actions
10.5.
Higher group actions
10.6.
Higher groups
10.7.
Homomorphisms of higher group actions
10.8.
Homomorphisms of higher groups
10.9.
The higher group of integers
10.10.
Iterated cartesian products of higher groups
10.11.
Orbits of higher group actions
10.12.
Subgroups of higher groups
10.13.
Symmetric higher groups
11.
Linear algebra
❱
11.1.
Constant matrices
11.2.
Diagonal vectors
11.3.
Diagonal matrices on rings
11.4.
Functoriality of matrices
11.5.
Functoriality of the type of vectors
11.6.
Matrices
11.7.
Matrices on rings
11.8.
Multiplication of matrices
11.9.
Scalar multiplication on matrices
11.10.
Scalar multiplication of vectors
11.11.
Scalar multiplication of vectors on rings
11.12.
Transposition of matrices
11.13.
Vectors
11.14.
Vectors on commutative rings
11.15.
Vectors on commutative semirings
11.16.
Vectors on euclidean domains
11.17.
Vectors on rings
11.18.
Vectors on semirings
12.
Lists
❱
12.1.
Arrays
12.2.
Concatenation of lists
12.3.
Flattening of lists
12.4.
Functoriality of the list operation
12.5.
Lists
12.6.
Lists of elements in discrete types
12.7.
Permutations of lists
12.8.
Permutations of vectors
12.9.
Predicates on lists
12.10.
Quicksort for lists
12.11.
Reversing lists
12.12.
Sort by insertion for lists
12.13.
Sort by insertion for vectors
12.14.
Sorted lists
12.15.
Sorted vectors
12.16.
Sorting algorithms for lists
12.17.
Sorting algorithms for vectors
12.18.
The universal property of lists with respect to wild monoids
13.
Online encyclopedia of integer sequences
❱
13.1.
Sequences of the online encyclopedia of integer sequences
14.
Order theory
❱
14.1.
Bottom elements in posets
14.2.
Bottom elements in preorders
14.3.
Chains in posets
14.4.
Chains in preorders
14.5.
Decidable posets
14.6.
Decidable preorders
14.7.
Decidable subposets
14.8.
Decidable subpreorders
14.9.
Decidable total orders
14.10.
Decidable total preorders
14.11.
Dependent products of large frames
14.12.
Dependent products of large locales
14.13.
Dependent products of large meet-semilattices
14.14.
Dependent products of large posets
14.15.
Dependent products large preorders
14.16.
Dependent products of large suplattices
14.17.
Directed complete posets
14.18.
Directed families in posets
14.19.
Distributive lattices
14.20.
Finite posets
14.21.
Finite preorders
14.22.
Finitely graded posets
14.23.
Frames
14.24.
Galois connections
14.25.
Galois connections between large posets
14.26.
Greatest lower bounds in large posets
14.27.
Greatest lower bounds in posets
14.28.
Homomorphisms of frames
14.29.
Homomorphisms of large frames
14.30.
Homomorphisms of large locales
14.31.
Homomorphisms of large meet-semilattices
14.32.
Homomorphisms of large suplattices
14.33.
Homomorphisms of meet-semilattices
14.34.
Homomorphisms of meet sup lattices
14.35.
Homomorphisms of suplattices
14.36.
Ideals in preorders
14.37.
Interval subposets
14.38.
Join-semilattices
14.39.
Large frames
14.40.
Large locales
14.41.
Large meet-semilattices
14.42.
Large meet-subsemilattices
14.43.
Large posets
14.44.
Large preorders
14.45.
Large quotient locales
14.46.
Large subframes
14.47.
Large subposets
14.48.
Large subpreorders
14.49.
Large subsuplattices
14.50.
Large suplattices
14.51.
Lattices
14.52.
Least upper bounds in large posets
14.53.
Least upper bounds in posets
14.54.
Locales
14.55.
Locally finite posets
14.56.
Lower bounds in large posets
14.57.
Lower bounds in posets
14.58.
Lower types in preorders
14.59.
Maximal chains in posets
14.60.
Maximal chains in preorders
14.61.
Meet-semilattices
14.62.
Meet-suplattices
14.63.
Nuclei on large locales
14.64.
Order preserving maps between large posets
14.65.
Order preserving maps between large preorders
14.66.
Order preserving maps on posets
14.67.
Order preserving maps on preorders
14.68.
Posets
14.69.
Powers of large locales
14.70.
Preorders
14.71.
Subposets
14.72.
Subpreorders
14.73.
Suplattices
14.74.
Top elements in large posets
14.75.
Top elements in posets
14.76.
Top elements in preorders
14.77.
Total orders
14.78.
Total preorders
14.79.
Upper bounds in large posets
14.80.
Upper bounds in posets
15.
Organic Chemistry
❱
15.1.
Alcohols
15.2.
Alkanes
15.3.
Alkenes
15.4.
Alkynes
15.5.
Ethane
15.6.
Hydrocarbons
15.7.
Methane
15.8.
Saturated carbons
16.
Orthogonal factorization systems
❱
16.1.
Extensions of maps
16.2.
Factorization operations
16.3.
Factorization operations into function classes
16.4.
Factorizations of maps
16.5.
Function classes
16.6.
Higher modalities
16.7.
Lifting operations
16.8.
Lifting squares
16.9.
Lifts of maps
16.10.
Local types
16.11.
Mere lifting properties
16.12.
Modal operators
16.13.
Null types
16.14.
Orthogonal factorization systems
16.15.
Orthogonal maps
16.16.
The pullback-hom
16.17.
Reflective subuniverses
16.18.
Σ-closed reflective subuniverses
16.19.
Stable orthogonal factorization systems
16.20.
Uniquely eliminating modalities
16.21.
Wide function classes
17.
Polytopes
❱
17.1.
Abstract polytopes
18.
Primitives
❱
18.1.
Characters
18.2.
Floats
18.3.
Machine integers
18.4.
Strings
19.
Real numbers
❱
19.1.
Dedekind real numbers
20.
Reflection
❱
20.1.
Abstractions
20.2.
Arguments
20.3.
Boolean reflection
20.4.
Definitions
20.5.
Fixity
20.6.
Group solver
20.7.
Literals
20.8.
Metavariables
20.9.
Names
20.10.
Precategory solver
20.11.
Terms
20.12.
The type checking monad
21.
Ring theory
❱
21.1.
Algebras over rings
21.2.
The binomial theorem for rings
21.3.
The binomial theorem for semirings
21.4.
Central elements of rings
21.5.
Central elements of semirings
21.6.
Congruence relations on rings
21.7.
Congruence relations on semirings
21.8.
Dependent products of rings
21.9.
Dependent products of semirings
21.10.
Division rings
21.11.
Function rings
21.12.
Function semirings
21.13.
Homomorphisms of rings
21.14.
Homomorphisms of semirings
21.15.
Ideals generated by subsets of rings
21.16.
Ideals in rings
21.17.
Ideals in semirings
21.18.
Idempotent elements in rings
21.19.
The invariant basis property of rings
21.20.
Invertible elements in rings
21.21.
Isomorphisms of rings
21.22.
Local rings
21.23.
Localizations of rings
21.24.
Maximal ideals in rings
21.25.
Modules over rings
21.26.
Nil ideals
21.27.
Nilpotent elements in rings
21.28.
Nilpotent elements in semirings
21.29.
Opposite rings
21.30.
Powers of elements in rings
21.31.
Powers of elements in semirings
21.32.
The precategory of rings
21.33.
The precategory of semirings
21.34.
Products of rings
21.35.
Quotient rings
21.36.
Radical ideals in rings
21.37.
Rings
21.38.
Semirings
21.39.
Subsets of rings
21.40.
Subsets of semirings
21.41.
Sums of elements in rings
21.42.
Sums of elements in semirings
21.43.
Trivial rings
22.
Set theory
❱
22.1.
Baire space
22.2.
Cantor space
22.3.
Cardinalities of sets
22.4.
Countable sets
22.5.
Cumulative hierarchy
22.6.
Infinite sets
22.7.
Uncountable sets
23.
Species
❱
23.1.
Cartesian exponents of species
23.2.
Cartesian products of species of types
23.3.
Cauchy composition of species of types
23.4.
Cauchy composition of species of types in a subuniverse
23.5.
Cauchy exponentials of species of types
23.6.
Cauchy exponentials of species of types in a subuniverse
23.7.
Cauchy products of species of types
23.8.
Cauchy products of species of types in a subuniverse
23.9.
Cauchy series of species of types
23.10.
Cauchy series of species of types in a subuniverse
23.11.
Composition of Cauchy series of species of types
23.12.
Composition of Cauchy series of species of types in subuniverses
23.13.
Coproducts of species of types
23.14.
Coproducts of species of types in subuniverses
23.15.
Cycle index series of species
23.16.
Derivatives of species
23.17.
Dirichlet products of species of types in subuniverses
23.18.
Dirichlet series of species of finite inhabited types
23.19.
Dirichlet series of species of types in subuniverses
23.20.
Equivalences of species of types
23.21.
Equivalences of species of types in subuniverses
23.22.
Exponential of Cauchy series of species of types
23.23.
Exponential of Cauchy series of species of types in subuniverses
23.24.
Morphisms of finite species
23.25.
Morphisms of species of types
23.26.
Pointing of species of types
23.27.
The precategory of finite species
23.28.
Products of Cauchy series of species of types
23.29.
Products of Cauchy series of species of types in subuniverses
23.30.
Products of Dirichlet series of species of finite inhabited types
23.31.
Products of Dirichlet series of species of types in subuniverses
23.32.
Small Composition of species of finite inhabited types
23.33.
Small Cauchy composition of species types in subuniverses
23.34.
Species of finite inhabited types
23.35.
Species of finite types
23.36.
Species of inhabited types
23.37.
Species of types
23.38.
Species of types in subuniverses
23.39.
The unit of Cauchy composition of types
23.40.
The unit of Cauchy composition of species of types in subuniverses
23.41.
Unlabeled structures of finite species
24.
Structured types
❱
24.1.
Cartesian products of types equipped with endomorphisms
24.2.
Central H-spaces
24.3.
Coherent H-spaces
24.4.
Commuting squares of pointed maps
24.5.
Constant maps of pointed types
24.6.
Contractible pointed types
24.7.
Equivalences of types equipped with endomorphisms
24.8.
Faithful pointed maps
24.9.
Fibers of pointed maps
24.10.
Finite multiplication in magmas
24.11.
Function magmas
24.12.
H-spaces
24.13.
The initial pointed type equipped with an automorphism
24.14.
The involutive type of H-Space structures on a pointed type
24.15.
Involutive types
24.16.
Iterated cartesian products of types equipped with endomorphisms
24.17.
Iterated cartesian products of pointed types
24.18.
Magmas
24.19.
Mere equivalences of types equipped with endomorphisms
24.20.
Morphisms of coherent H-spaces
24.21.
Morphisms of magmas
24.22.
Morphisms of types equipped with endomorphisms
24.23.
Pointed cartesian product types
24.24.
Pointed dependent functions
24.25.
Pointed dependent pair types
24.26.
Pointed equivalences
24.27.
Pointed families of types
24.28.
Pointed homotopies
24.29.
Pointed maps
24.30.
Pointed sections of pointed maps
24.31.
Pointed types
24.32.
Pointed types equipped with automorphisms
24.33.
The pointed unit type
24.34.
Symmetric elements of involutive types
24.35.
Symmetric H-spaces
24.36.
Types equipped with automorphisms
24.37.
Types equipped with endomorphisms
24.38.
Unpointed maps between pointed types
24.39.
Wild groups
24.40.
Wild loops
24.41.
Wild monoids
24.42.
Wild quasigroups
24.43.
Wild semigroups
25.
Synthetic homotopy theory
❱
25.1.
Formalisation of the Symmetry Book - 24 pushouts
25.2.
Formalisation of the Symmetry Book - 26 descent
25.3.
Formalisation of the Symmetry Book - 26 id pushout
25.4.
Formalisation of the Symmetry Book - 27 sequences
25.5.
Acyclic maps
25.6.
Acyclic types
25.7.
Cavallo's trick
25.8.
The circle
25.9.
Cocones under spans
25.10.
Cocones under spans of pointed types
25.11.
Cofibers
25.12.
The descent property of the circle
25.13.
Double loop spaces
25.14.
Free loops
25.15.
Functoriality of the loop space operation
25.16.
Groups of loops in 1-types
25.17.
Hatcher's acyclic type
25.18.
The infinite complex projective space
25.19.
Infinite cyclic types
25.20.
The interval
25.21.
Iterated loop spaces
25.22.
Joins of types
25.23.
Loop spaces
25.24.
The multiplication operation on the circle
25.25.
The plus-principle
25.26.
Powers of loops
25.27.
Prespectra
25.28.
Pushouts
25.29.
Pushouts of pointed types
25.30.
Smash products of pointed types
25.31.
Spectra
25.32.
Spheres
25.33.
Suspensions of types
25.34.
Triple loop spaces
25.35.
The universal cover of the circle
25.36.
The universal property of the circle
25.37.
The universal property of pushouts
25.38.
Wedges of pointed types
26.
Trees
❱
26.1.
Algebras for polynomial endofunctors
26.2.
Bases of directed trees
26.3.
Bases of enriched directed trees
26.4.
The coalgebra of directed trees
26.5.
The coalgebra of enriched directed trees
26.6.
Coalgebras of polynomial endofunctors
26.7.
The combinator of directed trees
26.8.
Combinators of enriched directed trees
26.9.
Directed trees
26.10.
The elementhood relation on coalgebras of polynomial endofunctors
26.11.
The elementhood relation on W-types
26.12.
Enriched directed trees
26.13.
Equivalences of directed trees
26.14.
Equivalences of enriched directed trees
26.15.
Extensional W-types
26.16.
Fibers of directed trees
26.17.
Fibers of enriched directed trees
26.18.
Functoriality of the combinator of directed trees
26.19.
Functoriality of the fiber operation on directed trees
26.20.
Functoriality of W-types
26.21.
Indexed W-types
26.22.
Induction principles on W-types
26.23.
Inequality on W-types
26.24.
Lower types of elements in W-types
26.25.
Morphisms of algebras of polynomial endofunctors
26.26.
Morphisms of coalgebras of polynomial endofunctors
26.27.
Morphisms of directed trees
26.28.
Morphisms of enriched directed trees
26.29.
Multisets
26.30.
Planar binary trees
26.31.
Polynomial endofunctors
26.32.
Raising universe levels of directed trees
26.33.
Ranks of elements in W-types
26.34.
Rooted morphisms of directed trees
26.35.
Rooted morphisms of enriched directed trees
26.36.
Rooted quasitrees
26.37.
Rooted undirected trees
26.38.
Small multisets
26.39.
Submultisets
26.40.
Transitive multisets
26.41.
The underlying trees of elements of coalgebras of polynomial endofunctors
26.42.
The underlying trees of elements of W-types
26.43.
Undirected rees
26.44.
The universal multiset
26.45.
The W-type of natural numbers
26.46.
The W-type of the type of propositions
26.47.
W-types
27.
Type theories
❱
27.1.
Comprehension of fibered type theories
27.2.
Dependent type theories
27.3.
Fibered dependent type theories
27.4.
Sections of dependent type theories
27.5.
Simple type theories
27.6.
Unityped type theories
28.
Univalent combinatorics
❱
28.1.
2-element decidable subtypes
28.2.
2-element subtypes
28.3.
2-element types
28.4.
The binomial types
28.5.
Bracelets
28.6.
Cartesian products of finite types
28.7.
The classical definition of the standard finite types
28.8.
Complements of isolated points of finite types
28.9.
Coproducts of finite types
28.10.
Counting in type theory
28.11.
Counting the elements of decidable subtypes
28.12.
Counting the elements of dependent pair types
28.13.
Counting the elements of the fiber of a map
28.14.
Counting the elements in Maybe
28.15.
Cubes
28.16.
Cycle partitions of finite types
28.17.
Cycle prime decompositions of natural numbers
28.18.
Cyclic types
28.19.
Decidable dependent function types
28.20.
Decidability of dependent pair types
28.21.
Decidable equivalence relations on finite types
28.22.
Decidable propositions
28.23.
Decidable subtypes of finite types
28.24.
Dedekind finite sets
28.25.
Counting the elements of dependent function types
28.26.
Dependent pair types of finite types
28.27.
Finite discrete Σ-Decompositions
28.28.
Distributivity of set truncation over finite products
28.29.
Double counting
28.30.
Injective maps
28.31.
Embeddings between standard finite types
28.32.
Equality in finite types
28.33.
Equality in the standard finite types
28.34.
Equivalences between finite types
28.35.
Equivalences of cubes
28.36.
Equivalences between standard finite types
28.37.
Ferrers diagrams (unlabeled partitions)
28.38.
Fibers of maps between finite types
28.39.
Finite choice
28.40.
Finiteness of the type of connected components
28.41.
Finite presentations of types
28.42.
Finite types
28.43.
Finitely presented types
28.44.
Finite function types
28.45.
The image of a map
28.46.
Inequality on types equipped with a counting
28.47.
Inhabited finite types
28.48.
Injective maps between finite types
28.49.
An involution on the standard finite types
28.50.
Isotopies of Latin squares
28.51.
Kuratowsky finite sets
28.52.
Latin squares
28.53.
The groupoid of main classes of Latin hypercubes
28.54.
The groupoid of main classes of Latin squares
28.55.
The maybe modality on finite types
28.56.
Necklaces
28.57.
Orientations of the complete undirected graph
28.58.
Orientations of cubes
28.59.
Partitions of finite types
28.60.
Petri-nets
28.61.
π-finite types
28.62.
The pigeonhole principle
28.63.
Finitely π-presented types
28.64.
Quotients of finite types
28.65.
Ramsey theory
28.66.
Repetitions of values
28.67.
Repetitions of values in sequences
28.68.
Retracts of finite types
28.69.
Sequences of elements in finite types
28.70.
Set quotients of index 2
28.71.
Finite Σ-decompositions of finite types
28.72.
Skipping elements in standard finite types
28.73.
Small types
28.74.
Standard finite pruned trees
28.75.
Standard finite trees
28.76.
The standard finite types
28.77.
Steiner systems
28.78.
Steiner triple systems
28.79.
Combinatorial identities of sums of natural numbers
28.80.
Surjective maps between finite types
28.81.
Symmetric difference of finite subtypes
28.82.
Finite trivial Σ-Decompositions
28.83.
Type duality of finite types
28.84.
Union of finite subtypes
28.85.
The universal property of the standard finite types
28.86.
Unlabeled partitions
28.87.
Unlabelled rooted trees
28.88.
Unlabelled trees
29.
Universal Algebra
❱
29.1.
Abstract equations over signatures
29.2.
Algebraic theories
29.3.
Algebraic theory of groups
29.4.
Algebras
29.5.
Congruences
29.6.
Homomorphisms of algebras
29.7.
Kernels of homomorphisms of algebras
29.8.
Models of signatures
29.9.
Quotient algebras
29.10.
Signatures
29.11.
Terms over signatures
Light
Rust
Coal
Navy
Ayu
Latte
Frappé
Macchiato
Mocha
Agda-UniMath
Identity systems
module
foundation.identity-systems
where
Imports
open
import
foundation-core.identity-systems
public