Univalent mathematics in Agda
Welcome to the website of the agdaunimath
formalization project!
The agdaunimath
library is a community formalisation project for univalent
mathematics in Agda. The library project was
created by Elisabeth Bonnevier, Jonathan PrietoCubides, 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 agdaunimath. 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
agdaunimath
library.
Citing the AgdaUniMath library
You can cite this library with the following BibTeX entry:
@software{agdaunimath,
author = {Rijke, Egbert and Bonnevier, Elisabeth and PrietoCubides, Jonathan and Bakke, Fredrik and {others}},
license = {MIT},
title = {{Univalent mathematics in Agda}},
url = {https://github.com/UniMath/agdaunimath/}
}
SUMMARY
Project
Formalisation in Agda

 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

 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

 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 halfintegers
 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
 Squarefree 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 WellOrdering Principle of the natural numbers
 The wellordering principle of the standard finite types

 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

 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 nelement 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
 The abstract quaternion group of order

0
Connected types0
Images of maps0
Maps1
Types2
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
 DubucPenon 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
 Noncontractible types
 Pairs of distinct elements
 Partial elements
 Partitions
 Path algebra
 Pathsplit 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

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
 Pathsplit 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

 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
 Edgecoloured 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

 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 orbitstabilizer 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

 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

 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

 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

 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 meetsemilattices
 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 meetsemilattices
 Homomorphisms of large suplattices
 Homomorphisms of meetsemilattices
 Homomorphisms of meet sup lattices
 Homomorphisms of suplattices
 Ideals in preorders
 Interval subposets
 Joinsemilattices
 Large frames
 Large locales
 Large meetsemilattices
 Large meetsubsemilattices
 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
 Meetsemilattices
 Meetsuplattices
 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

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 pullbackhom
 The raise modalities
 Reflective subuniverses
 Separated types
 Σclosed reflective subuniverses
 Stable orthogonal factorization systems
 Uniquely eliminating modalities
 Wide function classes
 The zero modality

 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

 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
 HasseWeil 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

 Cartesian products of types equipped with endomorphisms
 Central Hspaces
 Coherent Hspaces
 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
 Hspaces
 The initial pointed type equipped with an automorphism
 The involutive type of Hspace 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 Hspaces
 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 Hspaces
 Types equipped with automorphisms
 Types equipped with endomorphisms
 Unpointed maps between pointed types
 Wild groups
 Wild loops
 Wild monoids
 Wild quasigroups
 Wild semigroups

 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 plusprinciple
 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

 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 Wtypes
 Enriched directed trees
 Equivalences of directed trees
 Equivalences of enriched directed trees
 Extensional Wtypes
 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 Wtypes
 Indexed Wtypes
 Induction principles on Wtypes
 Inequality on Wtypes
 Lower types of elements in Wtypes
 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 Wtypes
 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 Wtypes
 Undirected rees
 The universal multiset
 The Wtype of natural numbers
 The Wtype of the type of propositions
 Wtypes

2
element decidable subtypes2
element subtypes2
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
 Petrinets
 π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
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.