Univalent mathematics in Agda

Welcome to the website of the agda-unimath formalization project!

The agda-unimath library is a community formalisation project for univalent mathematics in Agda. The library project was created by Elisabeth Bonnevier, Jonathan Prieto-Cubides, and Egbert Rijke, and is currently also being maintained by Fredrik Bakke. Our goal is to formalize an extensive curriculum of mathematics from the univalent point of view. Furthermore, we think libraries of formalized mathematics have the potential to be useful, and informative resources for mathematicians. Our library is designed to work towards this goal, and we welcome contributions to the library within any topic in mathematics.

The library is built in Agda 2.6.3. It can be compiled by running make check from the main folder of the repository.

See the list of all Agda modules in the library here.

Joining the project

Great, you want to contribute something! The best way to start is to find us in our chat channels on the Univalent Agda discord, which is a discord servers shared between the 1Lab, cubical Agda, and agda-unimath. We have a vibing community there, and you're more than welcome to join us just to hang out.

Once you've decided what you want to contribute, the best way to proceed is to make your own fork of the library. Within your fork, make a separate branch in which you will be making your contributions. And after following our installation guide, you're ready to start your project! When you've completed your formalization you can proceed by making a pull request. Then we will review your contributions, and merge it when it is ready for the agda-unimath library.

Citing the Agda-UniMath library

You can cite this library with the following BibTeX entry:

@software{agda-unimath,
  author = {Rijke, Egbert and Bonnevier, Elisabeth and Prieto-Cubides, Jonathan and Bakke, Fredrik and {others}},
  license = {MIT},
  title = {{Univalent mathematics in Agda}},
  url = {https://github.com/UniMath/agda-unimath/}
}

SUMMARY

Project

• Agda-UniMath
  • Home
  • Community
    • Maintainers
    • Contributors
    • Statement of inclusivity
    • Projects using Agda-Unimath
  • How-to
    • Install
    • Cite the library
  • Guidelines
    • Structure your file
      • TEMPLATE.lagda.md
    • Library coding style
    • Design principles
  • Everything

Formalisation in Agda

• Category theory

  • Adjunctions between large precategories
  • Anafunctors
  • Categories
  • Coproducts in precategories
  • Discrete categories
  • Endomorphisms of objects in categories
  • Epimorphism in large precategories
  • Equivalences between categories
  • Equivalences between large precategories
  • Equivalences between precategories
  • Exponential objects in precategories
  • Functors between categories
  • Functors between large precategories
  • Functors between precategories
  • Groupoids
  • Homotopies of natural transformations in large precategories
  • Initial objects of a precategory
  • Isomorphisms in categories
  • Isomorphisms in large precategories
  • Isomorphisms in precategories
  • Large categories
  • Large precategories
  • Monomorphisms in large precategories
  • Natural isomorphisms between functors between categories
  • Natural isomorphisms between functors on large precategories
  • Natural isomorphisms between functors between precategories
  • Natural numbers object in a precategory
  • Natural transformations between functors between categories
  • Natural transformations between functors between large precategories
  • Natural transformations between functors on precategories
  • Opposite precategories
  • Precategories
  • The precategory of functors and natural transformations between two fixed precategories
  • Pregroupoids
  • Products of precategories
  • Products in precategories
  • Pullbacks in precategories
  • Representable functors between precategories
  • Sieves in categories
  • Slice precategories
  • Terminal object of a precategory
  • The Yoneda lemma for precategories

• Commutative algebra

  • The binomial theorem in commutative rings
  • The binomial theorem in commutative semirings
  • Boolean rings
  • Commutative rings
  • Commutative semirings
  • Dependent products of commutative rings
  • Dependent products of commutative semirings
  • Discrete fields
  • The Eisenstein integers
  • Euclidean domains
  • Full ideals of commutative rings
  • Function commutative rings
  • Function commutative semirings
  • The Gaussian integers
  • Homomorphisms of commutative rings
  • Homomorphisms of commutative semirings
  • Ideals of commutative rings
  • Ideals of commutative semirings
  • Ideals generated by subsets of commutative rings
  • Integral domains
  • Intersections of ideals of commutative rings
  • Intersections of radical ideals of commutative rings
  • Invertible elements in commutative rings
  • Isomorphisms of commutative rings
  • Joins of ideals of commutative rings
  • Joins of radical ideals of commutative rings
  • Local commutative rings
  • Maximal ideals of commutative rings
  • Nilradical of a commutative ring
  • The nilradical of a commutative semiring
  • The poset of ideals of a commutative ring
  • The poset of radical ideals of a commutative ring
  • Powers of elements in commutative rings
  • Powers of elements in commutative semirings
  • The precategory of commutative rings
  • The precategory of commutative semirings
  • Prime ideals of commutative rings
  • Products of commutative rings
  • Products of ideals of commutative rings
  • Products of radical ideals of a commutative ring
  • Products of subsets of commutative rings
  • Radical ideals of commutative rings
  • Radical ideals generated by subsets of commutative rings
  • Radicals of ideals of commutative rings
  • Subsets of commutative rings
  • Subsets of commutative semirings
  • Sums in commutative rings
  • Sums in commutative semirings
  • Trivial commutative rings
  • The Zariski locale
  • The Zariski topology on the set of prime ideals of a commutative ring

• Elementary number theory

  • The absolute value function on the integers
  • The Ackermann function
  • Addition on integer fractions
  • Addition on the integers
  • Addition on the natural numbers
  • Addition on the rationals
  • Arithmetic functions
  • The based induction principle of the natural numbers
  • Based strong induction for the natural numbers
  • Bezout's lemma in the integers
  • Bezout's lemma on the natural numbers
  • The binomial coefficients
  • The binomial theorem for the integers
  • The binomial theorem for the natural numbers
  • Bounded sums of arithmetic functions
  • Catalan numbers
  • The cofibonacci sequence
  • The Collatz bijection
  • The Collatz conjecture
  • The commutative ring of integers
  • The commutative semiring of natural numbers
  • The congruence relations on the integers
  • The congruence relations on the natural numbers
  • Decidable dependent function types
  • Natural numbers are a total decidable poset
  • Decidable types in elementary number theory
  • The difference between integers
  • Dirichlet convolution
  • The distance between integers
  • The distance between natural numbers
  • Divisibility of integers
  • Divisibility in modular arithmetic
  • Divisibility of natural numbers
  • The divisibility relation on the standard finite types
  • Equality of integers
  • Equality of natural numbers
  • Euclidean division on the natural numbers
  • Euler's totient function
  • Exponentiation of natural numbers
  • Factorials of natural numbers
  • Falling factorials
  • The Fibonacci sequence
  • The natural numbers base k
  • Finitely cyclic maps
  • The fundamental theorem of arithmetic
  • The Goldbach conjecture
  • The greatest common divisor of integers
  • The greatest common divisor of natural numbers
  • The group of integers
  • The groups ℤ/kℤ
  • The half-integers
  • Inequality on integer fractions
  • Inequality on the integers
  • Inequality of natural numbers
  • Inequality on the rational numbers
  • Inequality on the standard finite types
  • The infinitude of primes
  • Initial segments of the natural numbers
  • Integer fractions
  • Integer partitions
  • The integers
  • The Kolakoski sequence
  • Lower bounds of type families over the natural numbers
  • Maximum on the natural numbers
  • Maximum on the standard finite types
  • Mersenne primes
  • Minimum on the natural numbers
  • Minimum on the standard finite types
  • Modular arithmetic
  • Modular arithmetic on the standard finite types
  • The monoid of natural numbers with addition
  • The monoid of the natural numbers with maximum
  • Multiplication of integers
  • Multiplication of the elements of a list of natural numbers
  • Multiplication of natural numbers
  • Multiset coefficients
  • The type of natural numbers
  • Nonzero natural numbers
  • The ordinal induction principle for the natural numbers
  • Parity of the natural numbers
  • Pisano periods
  • Powers of integers
  • Powers of two
  • Prime numbers
  • Products of natural numbers
  • Proper divisors of natural numbers
  • Pythagorean triples
  • The rational numbers
  • Reduced integer fractions
  • Relatively prime integers
  • Relatively prime natural numbers
  • Repeating an element in a standard finite type
  • Retracts of the type of natural numbers
  • The sieve of Eratosthenes
  • Square-free natural numbers
  • Stirling numbers of the second kind
  • Strict inequality natural numbers
  • Strictly ordered pairs of natural numbers
  • The strong induction principle for the natural numbers
  • Sums of natural numbers
  • Telephone numbers
  • The triangular numbers
  • The Twin Prime conjecture
  • Type arithmetic with natural numbers
  • Unit elements in the standard finite types
  • Unit similarity on the standard finite types
  • The universal property of the natural numbers
  • Upper bounds for type families over the natural numbers
  • The Well-Ordering Principle of the natural numbers
  • The well-ordering principle of the standard finite types

• Finite algebra

  • Commutative finite rings
  • Dependent products of commutative finit rings
  • Dependent products of finite rings
  • Abelian groups
  • Finite Commutative monoids
  • Finite fields
  • Abstract finite groups
  • Finite monoids
  • Finite rings
  • Finite semigroups
  • Homomorphisms of commutative finite rings
  • Homomorphisms of finite rings
  • Products of commutative finite rings
  • Products of finite rings
  • Semisimple commutative finite rings

• Finite group theory

  • The abstract quaternion group of order 8
  • Alternating concrete groups
  • Alternating groups
  • Cartier's delooping of the sign homomorphism
  • The concrete quaternion group
  • Deloopings of the sign homomorphism
  • Finite groups
  • Finite monoids
  • Finite semigroups
  • The group of n-element types
  • Groups of order 2
  • Orbits of permutations
  • Permutations
  • Permutations of standard finite types
  • The sign homomorphism
  • Simpson's delooping of the sign homomorphism
  • Subgroups of finite groups
  • Tetrahedra in 3-dimensional space
  • Transpositions
  • Transpositions of standard finite types

• Foundation

  • 0-Connected types
  • 0-Images of maps
  • 0-Maps
  • 1-Types
  • 2-Types
  • The binary action on identifications of binary functions
  • The action on identifications of dependent functions
  • The action on identifications of functions
  • Apartness relations
  • Arithmetic law for coproduct decomposition and Σ-decomposition
  • Arithmetic law for product decomposition and Π-decomposition
  • Automorphisms
  • Axiom L
  • The axiom of choice
  • Bands
  • Binary embeddings
  • Binary equivalences
  • Binary equivalences on unordered pairs of types
  • Binary functoriality of set quotients
  • Homotopies of binary operations
  • Binary operations on unordered pairs of types
  • Binary reflecting maps of equivalence relations
  • Binary relations
  • Binary transport
  • The booleans
  • The Cantor–Schröder–Bernstein–Escardó theorem
  • Cantor's diagonal argument
  • Cartesian product types
  • Cartesian products of set quotients
  • The category of sets
  • Choice of representatives for an equivalence relation
  • Coherently invertible maps
  • Commuting 3-simplices of homotopies
  • Commuting 3-simplices of maps
  • Commuting cubes of maps
  • Commuting squares of identifications
  • Commuting squares of maps
  • Commuting triangles of homotopies
  • Commuting triangles of maps
  • Complements of type families
  • Complements of subtypes
  • Cones over cospans
  • Conjunction of propositions
  • Connected components of types
  • Connected components of universes
  • Connected maps
  • Connected types
  • Constant maps
  • Constant type families
  • Contractible maps
  • Contractible types
  • Coproduct decompositions
  • Coproduct decompositions in a subuniverse
  • Coproduct types
  • Morphisms in the coslice category of types
  • Cospans
  • Decidability of dependent function types
  • Decidability of dependent pair types
  • Decidable embeddings
  • Decidable equality
  • Decidable equivalence relations
  • Decidable maps
  • Decidable propositions
  • Decidable relations on types
  • Decidable subtypes
  • Decidable types
  • The dependent binomial theorem for types (distributivity of dependent function types over coproduct types)
  • Dependent pair types
  • Dependent paths
  • Descent for coproduct types
  • Descent for dependent pair types
  • Descent for the empty type
  • Descent for equivalences
  • Diagonal maps of types
  • Diagonals of maps
  • Discrete reflexive relations
  • Discrete relaxed Σ-decompositions
  • Discrete Σ-decompositions
  • Discrete types
  • Disjunction of propositions
  • Double negation
  • The double negation modality
  • Double powersets
  • Dubuc-Penon compact types
  • Effective maps for equivalence relations
  • Embeddings
  • Empty types
  • Endomorphisms
  • Epimorphisms
  • Epimorphisms with respect to maps into sets
  • Epimorphisms with respect to truncated types
  • Equality of cartesian product types
  • Equality of coproduct types
  • Equality on dependent function types
  • Equality of dependent pair types
  • Equality in the fibers of a map
  • Equivalence classes
  • Equivalence extensionality
  • Equivalence induction
  • Equivalence relations
  • Equivalences
  • Equivalences on Maybe
  • Exclusive disjunction of propositions
  • Existential quantification
  • Exponents of set quotients
  • Faithful maps
  • Fiber inclusions
  • Fibered equivalences
  • Fibered involutions
  • Maps fibered over a map
  • Fibers of maps
  • Full subtypes of types
  • Function extensionality
  • Functional correspondences
  • Functions
  • Functoriality of cartesian product types
  • Functoriality of coproduct types
  • Functoriality of dependent function types
  • Functoriality of dependent pair types
  • The functoriality of fib
  • Functoriality of function types
  • Functoriality of propositional truncations
  • Functoriality of set quotients
  • Functoriality of set truncation
  • Functoriality of truncations
  • The fundamental theorem of identity types
  • Global choice
  • Hexagons of identifications
  • Hilbert's ε-operators
  • Homotopies
  • Identity systems
  • Identity types of truncated types
  • Identity types
  • The image of a map
  • Images of subtypes
  • Impredicative encodings of the logical operations
  • Impredicative universes
  • The induction principle for propositional truncation
  • Inhabited subtypes
  • Inhabited types
  • Injective maps
  • The interchange law
  • Intersections of subtypes
  • Involutions
  • Isolated points
  • Isomorphisms of sets
  • Iterated cartesian product types
  • Iterating automorphisms
  • Iterating functions
  • Iterating involutions
  • Large dependent pair types
  • Large homotopies
  • Large identity types
  • The large locale of propositions
  • The large locale of subtypes
  • The law of excluded middle
  • Lawvere's fixed point theorem
  • The lesser limited principle of omniscience
  • The limited principle of omniscience
  • Locally small types
  • Logical equivalences
  • The maybe modality
  • Mere embeddings
  • Mere equality
  • Mere equivalences
  • Monomorphisms
  • Morphisms of cospans
  • Multisubsets
  • Multivariable correspondences
  • Multivariable decidable relations
  • Multivariable functoriality of set quotients
  • Multivariable operations
  • Multivariable relations
  • Negation
  • Non-contractible types
  • Pairs of distinct elements
  • Partial elements
  • Partitions
  • Path algebra
  • Path-split maps
  • Perfect images
  • Π-decompositions of types
  • Π-decompositions of types into types in a subuniverse
  • Powersets
  • Preidempotent maps
  • Preimages of subtypes
  • The principle of omniscience
  • Product decompositions
  • Product decompositions of types in a subuniverse
  • Products of binary relations
  • Products of equivalence relataions
  • Products of tuples of types
  • Products of unordered pairs of types
  • Products of unordered tuples of types
  • Projective types
  • Proper subsets
  • Propositional extensionality
  • Propositional maps
  • Propositional resizing
  • Propositional truncations
  • Propositions
  • Pullback squares
  • Pullbacks
  • Raising universe levels
  • Reflecting maps for equivalence relations
  • Reflexive relations
  • Relaxed Σ-decompositions of types
  • Repetitions of values of maps
  • Repetitions in sequences
  • The replacement axiom for type theory
  • Retractions
  • Russell's paradox
  • Sections
  • Sequences
  • Set presented types
  • Set quotients
  • Set truncations
  • Sets
  • Shifting sequences
  • Σ-decompositions of types into types in a subuniverse
  • Σ-decompositions of types
  • Singleton induction
  • Singleton subtypes
  • Morphisms in the slice category of types
  • Small maps
  • Small types
  • Small universes
  • Split surjective maps
  • Standard apartness relations
  • Strongly extensional maps
  • Structure
  • The structure identity principle
  • Structured type duality
  • Subterminal types
  • Subtype duality
  • The subtype identity principle
  • Subtypes
  • Subuniverses
  • Surjective maps
  • Symmetric difference of subtypes
  • The symmetric identity types
  • Symmetric operations
  • Tight apartness relations
  • Transport
  • Trivial relaxed Σ-decompositions
  • Trivial Σ-decompositions
  • Truncated equality
  • Truncated maps
  • Truncated types
  • k-Equivalences
  • Truncation images of maps
  • Truncation levels
  • The truncation modalities
  • Truncations
  • Tuples of types
  • Type arithmetic with the booleans
  • Type arithmetic for cartesian product types
  • Type arithmetic for coproduct types
  • Type arithmetic with dependent function types
  • Type arithmetic for dependent pair types
  • Type arithmetic with the empty type
  • Type arithmetic with the unit type
  • Type duality
  • The type theoretic principle of choice
  • Unions of subtypes
  • Unique existence
  • Uniqueness of the image of a map
  • The uniqueness of set quotients
  • Uniqueness of set truncations
  • Uniqueness of the truncations
  • The unit type
  • Unital binary operations
  • The univalence axiom
  • Univalent action on equivalences
  • The univalence axiom implies function extensionality
  • Univalent type families
  • The universal property of booleans
  • The universal propert of cartesian product types
  • The universal property of coproduct types
  • The universal property of dependent pair types
  • The universal property of the empty type
  • The universal property of fiber products
  • The universal property of identity types
  • The universal property of the image of a map
  • The universal property of maybe
  • The universal property of propositional truncations
  • The universal property of propositional truncations with respect to sets
  • The universal property of pullbacks
  • The universal property of set quotients
  • The universal property of set truncations
  • The universal property of truncations
  • The universal property of the unit type
  • Universe levels
  • Unordered pairs of elements in a type
  • Unordered pairs of types
  • Unordered n-tuples of elements in a type
  • Unordered tuples of types
  • Vectors of set quotients
  • Weak function extensionality
  • The weak limited principle of omniscience
  • Weakly constant maps

• Foundation core

  • 1-Types
  • Cartesian product types
  • Coherently invertible maps
  • Commuting cubes of maps
  • Commuting squares of maps
  • Commuting triangles of maps
  • Constant maps
  • Contractible maps
  • Contractible types
  • Coproduct types
  • Decidable propositions
  • Dependent paths
  • Diagonal maps of types
  • Discrete types
  • Embeddings
  • Empty types
  • Endomorphisms
  • Equality of dependent pair types
  • Equivalence induction
  • Equivalence relations
  • Equivalences
  • Fibers of maps
  • Function extensionality
  • Functoriality of dependent function types
  • Functoriality of dependent pair types
  • Functoriality of function types
  • Homotopies
  • Identity types
  • Injective maps
  • Involutions
  • Logical equivalences
  • Negation
  • Path-split maps
  • Propositional maps
  • Propositions
  • Pullbacks
  • Retractions
  • Sections
  • Sets
  • Singleton induction
  • Small types
  • Subtypes
  • Transport
  • Truncated maps
  • Truncated types
  • Truncation levels
  • The univalence axiom
  • The universal property of pullbacks
  • The universal property of truncations

• Graph theory

  • Acyclic undirected graphs
  • Circuits in undirected graphs
  • Closed walks in undirected graphs
  • Complete bipartite graphs
  • Complete multipartite graphs
  • Complete undirected graphs
  • Connected graphs
  • Cycles in undirected graphs
  • Directed graph structures on standard finite sets
  • Directed graphs
  • Edge-coloured undirected graphs
  • Embeddings of directed graphs
  • Embeddings of undirected graphs
  • Enriched undirected graphs
  • Equivalences of directed graphs
  • Equivalences of enriched undirected graphs
  • Equivalences of undirected graphs
  • Eulerian circuits in undirected graphs
  • Faithful morphisms of undirected graphs
  • Fibers of directed graphs
  • Finite graphs
  • Geometric realizations of undirected graphs
  • Hypergraphs
  • Matchings
  • Mere equivalences of undirected graphs
  • Morphisms of directed graphs
  • Morphisms of undirected graphs
  • Incidence in undirected graphs
  • Orientations of undirected graphs
  • Paths in undirected graphs
  • Polygons
  • Raising universe levels of directed graphs
  • Reflecting maps of undirected graphs
  • Reflexive graphs
  • Regular undirected graph
  • Simple undirected graphs
  • Stereoisomerism for enriched undirected graphs
  • Totally faithful morphisms of undirected graphs
  • Trails in directed graphs
  • Trails in undirected graphs
  • Undirected graph structures on standard finite sets
  • Undirected graphs
  • Vertex covers
  • Voltage graphs
  • Walks in directed graphs
  • Walks in undirected graphs

• Group theory

  • Abelian groups
  • Pointwise addition of morphisms of abelian groups
  • Automorphism groups
  • Cartesian products of abelian groups
  • Cartesian products of concrete groups
  • Cartesian products of groups
  • Cartesian products of monoids
  • Cartesian products of semigroups
  • The category of concrete groups
  • The category of groups
  • The category of semigroups
  • Cayley's theorem
  • The center of a group
  • Center of a monoid
  • Center of a semigroup
  • Central elements of groups
  • Central elements of monoids
  • Central elements of semirings
  • Commutative monoids
  • Commutators of elements in groups
  • Concrete group actions
  • Concrete groups
  • Congruence relations on abelian groups
  • Congruence relations on commutative monoids
  • Congruence relations on groups
  • Congruence relations on monoids
  • Congruence relations on semigroups
  • Conjugation in groups
  • Contravariant pushforwards of concrete group actions
  • Decidable subgroups of groups
  • Dependent products of abelian groups
  • Dependent products of commutative monoids
  • Dependent products of groups
  • Dependent products of monoids
  • Dependent products of semigroups
  • The dihedral group construction
  • The dihedral groups
  • The E₈-lattice
  • Embeddings of abelian groups
  • Embeddings of groups
  • The endomorphism rings of abelian groups
  • Epimorphisms in groups
  • Equivalences of concrete group actions
  • Equivalences of concrete groups
  • Equivalences of group actions
  • Equivalences between semigroups
  • Free concrete group actions
  • Free groups with one generator
  • The full subgroup of a group
  • Function groups of abelian groups
  • Function commutative monoids
  • Function groups
  • Function monoids
  • Function semigroups
  • Furstenberg groups
  • Generating sets of groups
  • Group actions
  • Abstract groups
  • Homomorphisms of abelian groups
  • Homomorphisms of commutative monoids
  • Morphisms of concrete group actions
  • Homomorphisms of concrete groups
  • Homomorphisms of generated subgroups
  • Homomorphisms of group actions
  • Homomorphisms of groups
  • Homomorphisms of monoids
  • Homomorphisms of semigroups
  • Intersections of subgroups of abelian groups
  • Intersections of subgroups of groups
  • Inverse semigroups
  • Invertible elements in monoids
  • Isomorphisms of abelian groups
  • Isomorphisms of concrete groups
  • Isomorphisms of group actions
  • Isomorphisms of groups
  • Isomorphisms of semigroups
  • Iterated cartesian products of concrete groups
  • Kernels
  • Kernels of homomorphisms of concrete groups
  • Large semigroups
  • Concrete automorphism groups on sets
  • Mere equivalences of concrete group actions
  • Mere equivalences of group actions
  • Monoid actions
  • Monoids
  • Monomorphisms of concrete groups
  • Monomorphisms in the category of groups
  • Normal subgroups
  • Normal subgroups of concrete groups
  • Normal submonoids
  • Normal submonoids of commutative monoids
  • The opposite of a group
  • The orbit-stabilizer theorem for concrete groups
  • Orbits of concrete group actions
  • Orbits of group actions
  • The precategory of orbits of a monoid action
  • The order of an element in a group
  • The precategory of abelian groups
  • The precategory of commutative monoids
  • The precategory of concrete groups
  • The precategory of group actions
  • The precategory of groups
  • The precategory of monoids
  • The precategory of semigroups
  • Principal group actions
  • Principal torsors of concrete groups
  • Products of elements in a monoid
  • Products of tuples of elements in commutative monoids
  • Quotient groups
  • Quotient groups of concrete groups
  • Quotients of abelian groups
  • Representations of monoids
  • Saturated congruence relations on commutative monoids
  • Saturated congruence relations on monoids
  • Semigroups
  • Sheargroups
  • Shriek of concrete group homomorphisms
  • Stabilizer groups
  • Stabilizers of concrete group actions
  • Subgroups
  • Subgroups of abelian groups
  • Subgroups of concrete groups
  • Subgroups generated by subsets of groups
  • Submonoids
  • Submonoids of commutative monoids
  • Subsemigroups
  • Subsets of abelian groups
  • Subsets of commutative monoids
  • Subsets of groups
  • Subsets of monoids
  • The substitution functor of concrete group actions
  • The substitution functor of group actions
  • Symmetric concrete groups
  • Symmetric groups
  • Torsors of abstract groups
  • Transitive concrete group actions
  • Transitive group actions
  • Trivial subgroups
  • Unordered tuples of elements in commutative monoids

• Higher group theory

  • Cartesian products of higher groups
  • Equivalences of higher groups
  • Fixed points of higher group actions
  • Free higher group actions
  • Higher group actions
  • Higher groups
  • Homomorphisms of higher group actions
  • Homomorphisms of higher groups
  • The higher group of integers
  • Iterated cartesian products of higher groups
  • Orbits of higher group actions
  • Subgroups of higher groups
  • Symmetric higher groups

• Linear algebra

  • Constant matrices
  • Diagonal vectors
  • Diagonal matrices on rings
  • Functoriality of matrices
  • Functoriality of the type of vectors
  • Matrices
  • Matrices on rings
  • Multiplication of matrices
  • Scalar multiplication on matrices
  • Scalar multiplication of vectors
  • Scalar multiplication of vectors on rings
  • Transposition of matrices
  • Vectors
  • Vectors on commutative rings
  • Vectors on commutative semirings
  • Vectors on euclidean domains
  • Vectors on rings
  • Vectors on semirings

• Lists

  • Arrays
  • Concatenation of lists
  • Flattening of lists
  • Functoriality of the list operation
  • Lists
  • Lists of elements in discrete types
  • Permutations of lists
  • Permutations of vectors
  • Predicates on lists
  • Quicksort for lists
  • Reversing lists
  • Sort by insertion for lists
  • Sort by insertion for vectors
  • Sorted lists
  • Sorted vectors
  • Sorting algorithms for lists
  • Sorting algorithms for vectors
  • The universal property of lists with respect to wild monoids

• Online encyclopedia of integer sequences

  • Sequences of the online encyclopedia of integer sequences

• Order theory

  • Bottom elements in posets
  • Bottom elements in preorders
  • Chains in posets
  • Chains in preorders
  • Closure operators on large locales
  • Closure operators on large posets
  • Decidable posets
  • Decidable preorders
  • Decidable subposets
  • Decidable subpreorders
  • Decidable total orders
  • Decidable total preorders
  • Dependent products of large frames
  • Dependent products of large locales
  • Dependent products of large meet-semilattices
  • Dependent products of large posets
  • Dependent products large preorders
  • Dependent products of large suplattices
  • Directed complete posets
  • Directed families in posets
  • Distributive lattices
  • Finite posets
  • Finite preorders
  • Finitely graded posets
  • Frames
  • Galois connections
  • Galois connections between large posets
  • Greatest lower bounds in large posets
  • Greatest lower bounds in posets
  • Homomorphisms of frames
  • Homomorphisms of large frames
  • Homomorphisms of large locales
  • Homomorphisms of large meet-semilattices
  • Homomorphisms of large suplattices
  • Homomorphisms of meet-semilattices
  • Homomorphisms of meet sup lattices
  • Homomorphisms of suplattices
  • Ideals in preorders
  • Interval subposets
  • Join-semilattices
  • Large frames
  • Large locales
  • Large meet-semilattices
  • Large meet-subsemilattices
  • Large posets
  • Large preorders
  • Large quotient locales
  • Large subframes
  • Large subposets
  • Large subpreorders
  • Large subsuplattices
  • Large suplattices
  • Lattices
  • Least upper bounds in large posets
  • Least upper bounds in posets
  • Locales
  • Locally finite posets
  • Lower bounds in large posets
  • Lower bounds in posets
  • Lower types in preorders
  • Maximal chains in posets
  • Maximal chains in preorders
  • Meet-semilattices
  • Meet-suplattices
  • Nuclei on large locales
  • Order preserving maps between large posets
  • Order preserving maps between large preorders
  • Order preserving maps on posets
  • Order preserving maps on preorders
  • Posets
  • Powers of large locales
  • Preorders
  • Reflective Galois connections between large posets
  • Similarity of elements in large posets
  • Similarity of elements in large preorders
  • Subposets
  • Subpreorders
  • Suplattices
  • Top elements in large posets
  • Top elements in posets
  • Top elements in preorders
  • Total orders
  • Total preorders
  • Upper bounds in large posets
  • Upper bounds in posets

• Organic Chemistry

  • Alcohols
  • Alkanes
  • Alkenes
  • Alkynes
  • Ethane
  • Hydrocarbons
  • Methane
  • Saturated carbons

• Orthogonal factorization systems

  • The closed modalities
  • Extensions of maps
  • Factorization operations
  • Factorization operations into function classes
  • Factorizations of maps
  • Function classes
  • Higher modalities
  • The identity modality
  • Lifting operations
  • Lifting squares
  • Lifts of maps
  • Local types
  • Mere lifting properties
  • Modal operators
  • Null types
  • The open modalities
  • Orthogonal factorization systems
  • Orthogonal maps
  • The pullback-hom
  • The raise modalities
  • Reflective subuniverses
  • Separated types
  • Σ-closed reflective subuniverses
  • Stable orthogonal factorization systems
  • Uniquely eliminating modalities
  • Wide function classes
  • The zero modality

• Polytopes

  • Abstract polytopes

• Primitives

  • Characters
  • Floats
  • Machine integers
  • Strings

• Real numbers

  • Dedekind real numbers

• Reflection

  • Abstractions
  • Arguments
  • Boolean reflection
  • Definitions
  • Fixity
  • Group solver
  • Literals
  • Metavariables
  • Names
  • Precategory solver
  • Terms
  • The type checking monad

• Ring theory

  • Algebras over rings
  • The binomial theorem for rings
  • The binomial theorem for semirings
  • Central elements of rings
  • Central elements of semirings
  • Congruence relations on rings
  • Congruence relations on semirings
  • Dependent products of rings
  • Dependent products of semirings
  • Division rings
  • Full ideals of rings
  • Function rings
  • Function semirings
  • Homomorphisms of rings
  • Homomorphisms of semirings
  • Ideals generated by subsets of rings
  • Ideals of rings
  • Ideals of semirings
  • Idempotent elements in rings
  • Intersections of ideals of rings
  • Intersections of ideals of semirings
  • The invariant basis property of rings
  • Invertible elements in rings
  • Isomorphisms of rings
  • Joins of ideals of rings
  • Joins of left ideals of rings
  • Joins of right ideals of rings
  • Left ideals generated by subsets of rings
  • Left ideals of rings
  • Local rings
  • Localizations of rings
  • Maximal ideals of rings
  • Modules over rings
  • Nil ideals of rings
  • Nilpotent elements in rings
  • Nilpotent elements in semirings
  • Opposite rings
  • The poset of ideals of a ring
  • The poset of left ideals of a ring
  • The poset of right ideals of a ring
  • Powers of elements in rings
  • Powers of elements in semirings
  • The precategory of rings
  • The precategory of semirings
  • Products of ideals of rings
  • Products of left ideals of rings
  • Products of right ideals of rings
  • Products of rings
  • Products of subsets of rings
  • Quotient rings
  • Radical ideals of rings
  • Right ideals generated by subsets of rings
  • Right ideals of rings
  • Rings
  • Semirings
  • Subsets of rings
  • Subsets of semirings
  • Sums of elements in rings
  • Sums of elements in semirings
  • Trivial rings

• Set theory

  • Baire space
  • Cantor space
  • Cardinalities of sets
  • Countable sets
  • Cumulative hierarchy
  • Infinite sets
  • Uncountable sets

• Species

  • Cartesian exponents of species
  • Cartesian products of species of types
  • Cauchy composition of species of types
  • Cauchy composition of species of types in a subuniverse
  • Cauchy exponentials of species of types
  • Cauchy exponentials of species of types in a subuniverse
  • Cauchy products of species of types
  • Cauchy products of species of types in a subuniverse
  • Cauchy series of species of types
  • Cauchy series of species of types in a subuniverse
  • Composition of Cauchy series of species of types
  • Composition of Cauchy series of species of types in subuniverses
  • Coproducts of species of types
  • Coproducts of species of types in subuniverses
  • Cycle index series of species
  • Derivatives of species
  • Dirichlet exponentials of a species of types
  • Dirichlet exponentials of species of types in a subuniverse
  • Dirichlet products of species of types
  • Dirichlet products of species of types in subuniverses
  • Dirichlet series of species of finite inhabited types
  • Dirichlet series of species of types
  • Dirichlet series of species of types in subuniverses
  • Equivalences of species of types
  • Equivalences of species of types in subuniverses
  • Exponential of Cauchy series of species of types
  • Exponential of Cauchy series of species of types in subuniverses
  • Hasse-Weil species
  • Morphisms of finite species
  • Morphisms of species of types
  • Pointing of species of types
  • The precategory of finite species
  • Products of Cauchy series of species of types
  • Products of Cauchy series of species of types in subuniverses
  • Products of Dirichlet series of species of finite inhabited types
  • Products of Dirichlet series of species of types
  • Products of Dirichlet series of species of types in subuniverses
  • Small Composition of species of finite inhabited types
  • Small Cauchy composition of species types in subuniverses
  • Species of finite inhabited types
  • Species of finite types
  • Species of inhabited types
  • Species of types
  • Species of types in subuniverses
  • The unit of Cauchy composition of types
  • The unit of Cauchy composition of species of types in subuniverses
  • Unlabeled structures of finite species

• Structured types

  • Cartesian products of types equipped with endomorphisms
  • Central H-spaces
  • Coherent H-spaces
  • Commuting squares of pointed maps
  • Constant maps of pointed types
  • Contractible pointed types
  • Equivalences of types equipped with endomorphisms
  • Faithful pointed maps
  • Fibers of pointed maps
  • Finite multiplication in magmas
  • Function magmas
  • H-spaces
  • The initial pointed type equipped with an automorphism
  • The involutive type of H-space structures on a pointed type
  • Involutive types
  • Iterated cartesian products of types equipped with endomorphisms
  • Iterated cartesian products of pointed types
  • Magmas
  • Mere equivalences of types equipped with endomorphisms
  • Morphisms of coherent H-spaces
  • Morphisms of magmas
  • Morphisms of types equipped with endomorphisms
  • Pointed cartesian product types
  • Pointed dependent functions
  • Pointed dependent pair types
  • Pointed equivalences
  • Pointed families of types
  • Pointed homotopies
  • Pointed maps
  • Pointed sections of pointed maps
  • Pointed types
  • Pointed types equipped with automorphisms
  • The pointed unit type
  • Symmetric elements of involutive types
  • Symmetric H-spaces
  • Types equipped with automorphisms
  • Types equipped with endomorphisms
  • Unpointed maps between pointed types
  • Wild groups
  • Wild loops
  • Wild monoids
  • Wild quasigroups
  • Wild semigroups

• Synthetic homotopy theory

  • Formalisation of the Symmetry Book - 26 descent
  • Formalisation of the Symmetry Book - 26 id pushout
  • Formalisation of the Symmetry Book - 27 sequences
  • Acyclic maps
  • Acyclic types
  • Cavallo's trick
  • The circle
  • Cocones under spans
  • Cocones under spans of pointed types
  • Cofibers
  • Dependent cocones under spans
  • The dependent pullback property of pushouts
  • The dependent universal property of pushouts
  • The descent property of the circle
  • Double loop spaces
  • Free loops
  • Functoriality of the loop space operation
  • Groups of loops in 1-types
  • Hatcher's acyclic type
  • The induction principle of pushouts
  • The infinite complex projective space
  • Infinite cyclic types
  • The interval
  • Iterated loop spaces
  • Joins of types
  • Loop spaces
  • The multiplication operation on the circle
  • The plus-principle
  • Powers of loops
  • Prespectra
  • The pullback property of pushouts
  • Pushouts
  • Pushouts of pointed types
  • Smash products of pointed types
  • Spectra
  • Spheres
  • Suspensions of types
  • Triple loop spaces
  • The universal cover of the circle
  • The universal property of the circle
  • The universal property of pushouts
  • Wedges of pointed types

• Trees

  • Algebras for polynomial endofunctors
  • Bases of directed trees
  • Bases of enriched directed trees
  • The coalgebra of directed trees
  • The coalgebra of enriched directed trees
  • Coalgebras of polynomial endofunctors
  • The combinator of directed trees
  • Combinators of enriched directed trees
  • Directed trees
  • The elementhood relation on coalgebras of polynomial endofunctors
  • The elementhood relation on W-types
  • Enriched directed trees
  • Equivalences of directed trees
  • Equivalences of enriched directed trees
  • Extensional W-types
  • Fibers of directed trees
  • Fibers of enriched directed trees
  • Functoriality of the combinator of directed trees
  • Functoriality of the fiber operation on directed trees
  • Functoriality of W-types
  • Indexed W-types
  • Induction principles on W-types
  • Inequality on W-types
  • Lower types of elements in W-types
  • Morphisms of algebras of polynomial endofunctors
  • Morphisms of coalgebras of polynomial endofunctors
  • Morphisms of directed trees
  • Morphisms of enriched directed trees
  • Multisets
  • Planar binary trees
  • Polynomial endofunctors
  • Raising universe levels of directed trees
  • Ranks of elements in W-types
  • Rooted morphisms of directed trees
  • Rooted morphisms of enriched directed trees
  • Rooted quasitrees
  • Rooted undirected trees
  • Small multisets
  • Submultisets
  • Transitive multisets
  • The underlying trees of elements of coalgebras of polynomial endofunctors
  • The underlying trees of elements of W-types
  • Undirected rees
  • The universal multiset
  • The W-type of natural numbers
  • The W-type of the type of propositions
  • W-types

• Type theories

  • Comprehension of fibered type theories
  • Dependent type theories
  • Fibered dependent type theories
  • Sections of dependent type theories
  • Simple type theories
  • Unityped type theories

• Univalent combinatorics

  • 2-element decidable subtypes
  • 2-element subtypes
  • 2-element types
  • The binomial types
  • Bracelets
  • Cartesian products of finite types
  • The classical definition of the standard finite types
  • Complements of isolated points of finite types
  • Coproducts of finite types
  • Counting in type theory
  • Counting the elements of decidable subtypes
  • Counting the elements of dependent pair types
  • Counting the elements of the fiber of a map
  • Counting the elements in Maybe
  • Cubes
  • Cycle partitions of finite types
  • Cycle prime decompositions of natural numbers
  • Cyclic types
  • Decidable dependent function types
  • Decidability of dependent pair types
  • Decidable equivalence relations on finite types
  • Decidable propositions
  • Decidable subtypes of finite types
  • Dedekind finite sets
  • Counting the elements of dependent function types
  • Dependent pair types of finite types
  • Finite discrete Σ-decompositions
  • Distributivity of set truncation over finite products
  • Double counting
  • Injective maps
  • Embeddings between standard finite types
  • Equality in finite types
  • Equality in the standard finite types
  • Equivalences between finite types
  • Equivalences of cubes
  • Equivalences between standard finite types
  • Ferrers diagrams (unlabeled partitions)
  • Fibers of maps between finite types
  • Finite choice
  • Finiteness of the type of connected components
  • Finite presentations of types
  • Finite types
  • Finitely presented types
  • Finite function types
  • The image of a map
  • Inequality on types equipped with a counting
  • Inhabited finite types
  • Injective maps between finite types
  • An involution on the standard finite types
  • Isotopies of Latin squares
  • Kuratowsky finite sets
  • Latin squares
  • The groupoid of main classes of Latin hypercubes
  • The groupoid of main classes of Latin squares
  • The maybe modality on finite types
  • Necklaces
  • Orientations of the complete undirected graph
  • Orientations of cubes
  • Partitions of finite types
  • Petri-nets
  • π-finite types
  • The pigeonhole principle
  • Finitely π-presented types
  • Quotients of finite types
  • Ramsey theory
  • Repetitions of values
  • Repetitions of values in sequences
  • Retracts of finite types
  • Sequences of elements in finite types
  • Set quotients of index 2
  • Finite Σ-decompositions of finite types
  • Skipping elements in standard finite types
  • Small types
  • Standard finite pruned trees
  • Standard finite trees
  • The standard finite types
  • Steiner systems
  • Steiner triple systems
  • Combinatorial identities of sums of natural numbers
  • Surjective maps between finite types
  • Symmetric difference of finite subtypes
  • Finite trivial Σ-decompositions
  • Type duality of finite types
  • Unions of finite subtypes
  • The universal property of the standard finite types
  • Unlabeled partitions
  • Unlabeled rooted trees
  • Unlabeled trees

• Universal Algebra

  • Abstract equations over signatures
  • Algebraic theories
  • Algebraic theory of groups
  • Algebras
  • Congruences
  • Homomorphisms of algebras
  • Kernels of homomorphisms of algebras
  • Models of signatures
  • Quotient algebras
  • Signatures
  • Terms over signatures

Contributors

We are grateful to the following people for their contributions to the library.

• Egbert Rijke
• Fredrik Bakke
• EleonoreMangel
• Elisabeth Bonnevier
• Bryan Lu
• Jonathan Cubides
• Raymond Baker
• ElifUskuplu
• Fernando Chu
• IanRay11
• Andreas Källberg
• Matej Jazbec
• malarbol
• Amélia
• ivankobe
• daniel gratzer
• Vojtěch Štěpančík
• Alice Laroche
• masazaucer
• VictorBlanchi
• favonia
• Szumi Xie
• Åsmund Kløvstad
• Dylan Braithwaite
• Erik Schnetter
• Nathan van Doorn
• Pierre Cagne
• Tom de Jong

Help us to improve the library by contributing to the project! Contributions come in many forms, please ask us if you are not sure how to help. We are happy to help you get started.