SUMMARY

Overview

• Home
• Community
  • Maintainers
  • Contributors
  • Statement of inclusivity
  • Projects using agda-unimath
  • Grant acknowledgements
• Guides
  • Installing the library
  • Design principles
  • Contributing to the library
  • Structuring your file
    • File template
  • The library coding style
  • Guidelines for mixfix operators
  • Citing sources
  • Citing the library
• Library explorer
• Art
• Full list of library contents
• Formalization of results from the literature
  • Freek Wiedijk’s 100 Theorems
  • Idempotents in Intensional Type Theory
  • Sequences of the online encyclopedia of integer sequences
  • Sequential Colimits in Homotopy Type Theory

The agda-unimath library

• Category theory

  • Adjunctions between large categories
  • Adjunctions between large precategories
  • Anafunctors between categories
  • Anafunctors between precategories
  • The augmented simplex category
  • Categories
  • The category of functors and natural transformations between two categories
  • The category of functors and natural transformations from small to large categories
  • The category of maps and natural transformations between two categories
  • The category of maps and natural transformations from small to large categories
  • Commuting squares of morphisms in large precategories
  • Commuting squares of morphisms in precategories
  • Commuting squares of morphisms in set-magmoids
  • Commuting triangles of morphisms in precategories
  • Commuting triangles of morphisms in set-magmoids
  • Complete precategories
  • Composition operations on binary families of sets
  • Cones in precategories
  • Conservative functors between precategories
  • Constant functors
  • Copresheaf categories
  • Coproducts in precategories
  • Cores of categories
  • Cores of precategories
  • Coslice precategories
  • Dependent composition operations over precategories
  • Dependent products of categories
  • Dependent products of large categories
  • Dependent products of large precategories
  • Dependent products of precategories
  • Discrete categories
  • Displayed precategories
  • Embedding maps between precategories
  • Embeddings between precategories
  • Endomorphisms in categories
  • Endomorphisms in precategories
  • Epimorphism in large precategories
  • Equivalences between categories
  • Equivalences between large precategories
  • Equivalences between precategories
  • Essential fibers of functors between precategories
  • Essentially injective functors between precategories
  • Essentially surjective functors between precategories
  • Exponential objects in precategories
  • Extensions of functors between precategories
  • Faithful functors between precategories
  • Faithful maps between precategories
  • Full functors between precategories
  • Full large subcategories
  • Full large subprecategories
  • Full maps between precategories
  • Full subcategories
  • Full subprecategories
  • Fully faithful functors between precategories
  • Fully faithful maps between precategories
  • Function categories
  • Function precategories
  • Functors between categories
  • Functors from small to large categories
  • Functors from small to large precategories
  • Functors between large categories
  • Functors between large precategories
  • Functors between nonunital precategories
  • Functors between precategories
  • Functors between set-magmoids
  • Gaunt categories
  • Groupoids
  • Homotopies of natural transformations in large precategories
  • Indiscrete precategories
  • The initial category
  • Initial objects of large categories
  • Initial objects of large precategories
  • Initial objects in a precategory
  • Isomorphism induction in categories
  • Isomorphism induction in precategories
  • Isomorphisms in categories
  • Isomorphisms in large categories
  • Isomorphisms in large precategories
  • Isomorphisms in precategories
  • Isomorphisms in subprecategories
  • Large categories
  • Large function categories
  • Large function precategories
  • Large precategories
  • Large subcategories
  • Large subprecategories
  • Limits in precategories
  • Maps between categories
  • Maps from small to large categories
  • Maps from small to large precategories
  • Maps between precategories
  • Maps between set-magmoids
  • Monads on categories
  • Monads on precategories
  • Monomorphisms in large precategories
  • Natural isomorphisms between functors between categories
  • Natural isomorphisms between functors between large precategories
  • Natural isomorphisms between functors between precategories
  • Natural isomorphisms between maps between categories
  • Natural isomorphisms between maps between precategories
  • Natural numbers object in a precategory
  • Natural transformations between functors between categories
  • Natural transformations between functors from small to large categories
  • Natural transformations between functors from small to large precategories
  • Natural transformations between functors between large categories
  • Natural transformations between functors between large precategories
  • Natural transformations between functors between precategories
  • Natural transformations between maps between categories
  • Natural transformations between maps from small to large precategories
  • Natural transformations between maps between precategories
  • Nonunital precategories
  • One object precategories
  • Opposite categories
  • Opposite large precategories
  • Opposite precategories
  • Opposite preunivalent categories
  • Pointed endofunctors on categories
  • Pointed endofunctors
  • Precategories
  • Precategory of elements of a presheaf
  • The precategory of functors and natural transformations between two precategories
  • The precategory of functors and natural transformations from small to large precategories
  • The precategory of maps and natural transformations from a small to a large precategory
  • The precategory of maps and natural transformations between two precategories
  • Pregroupoids
  • Presheaf categories
  • Preunivalent categories
  • Products in precategories
  • Products of precategories
  • Pseudomonic functors between precategories
  • Pullbacks in precategories
  • Replete subprecategories
  • Representable functors between categories
  • Representable functors between large precategories
  • Representable functors between precategories
  • The representing arrow category
  • Restrictions of functors to cores of precategories
  • Right extensions in precategories
  • Right Kan extensions in precategories
  • Rigid objects in a category
  • Rigid objects in a precategory
  • Set-magmoids
  • Sieves in categories
  • The simplex category
  • Slice precategories
  • Split essentially surjective functors between precategories
  • Strict categories
  • Structure equivalences between set-magmoids
  • Subcategories
  • Subprecategories
  • Subterminal precategories
  • The terminal category
  • Terminal objects in a precategory
  • Wide subcategories
  • Wide subprecategories
  • The Yoneda lemma for categories
  • The Yoneda lemma for precategories

• Commutative algebra

  • The binomial theorem in commutative rings
  • The binomial theorem in commutative semirings
  • Boolean rings
  • The category of commutative 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
  • The group of multiplicative units of a commutative ring
  • Homomorphisms of commutative rings
  • Homomorphisms of commutative semirings
  • Ideals of commutative rings
  • Ideals of commutative semirings
  • Ideals generated by subsets of commutative rings
  • Integer multiples of elements 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
  • Multiples of elements in 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
  • Transporting commutative ring structures along isomorphisms of abelian groups
  • Trivial commutative rings
  • The Zariski locale
  • The Zariski topology on the set of prime ideals of a commutative ring

• Domain theory

  • Directed complete posets
  • Directed families in posets
  • Kleene’s fixed point theorem for ω-complete posets
  • Kleene’s fixed point theorem for posets
  • ω-Complete posets
  • ω-Continuous maps between ω-complete posets
  • ω-Continuous maps between posets
  • Reindexing directed families in posets
  • Scott-continuous maps between posets

• 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 of positive, negative, nonnegative and nonpositive integers
  • Addition on the rational numbers
  • The additive group of rational numbers
  • 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 semiring of natural numbers
  • The congruence relations on the integers
  • The congruence relations on the natural numbers
  • The cross-multiplication difference of two integer fractions
  • Cubes of natural numbers
  • Decidable dependent function types
  • The decidable total order of integers
  • The decidable total order of natural numbers
  • The decidable total order of rational numbers
  • The decidable total order of a standard finite type
  • Decidable types in elementary number theory
  • The difference between integers
  • The difference between rational numbers
  • 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
  • The Euclid–Mullin sequence
  • Euclidean division on the natural numbers
  • Euler’s totient function
  • Exponentiation of natural numbers
  • Factorials of natural numbers
  • Falling factorials
  • Fermat numbers
  • The Fibonacci sequence
  • The field of rational numbers
  • 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 half-integers
  • The Hardy-Ramanujan number
  • 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 Jacobi symbol
  • The Kolakoski sequence
  • The Legendre symbol
  • Lower bounds of type families over the natural numbers
  • Maximum on the natural numbers
  • Maximum on the standard finite types
  • The mediant fraction of two integer fractions
  • 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 on integer fractions
  • Multiplication of integers
  • Multiplication of the elements of a list of natural numbers
  • Multiplication of natural numbers
  • Multiplication of positive, negative, nonnegative and nonpositive integers
  • Multiplication on the rational numbers
  • The multiplicative group of positive rational numbers
  • The multiplicative group of rational numbers
  • Multiplicative inverses of positive integer fractions
  • The multiplicative monoid of natural numbers
  • The multiplicative monoid of rational numbers
  • Multiplicative units in the integers
  • Multiplicative units in modular arithmetic
  • Multiset coefficients
  • The type of natural numbers
  • The negative integers
  • The nonnegative integers
  • The nonpositive integers
  • Nonzero integers
  • Nonzero natural numbers
  • Nonzero rational numbers
  • The ordinal induction principle for the natural numbers
  • Parity of the natural numbers
  • Peano arithmetic
  • Pisano periods
  • The poset of natural numbers ordered by divisibility
  • The positive, negative, nonnegative and nonpositive integers
  • Positive integer fractions
  • The positive integers
  • Positive rational numbers
  • 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 ring of integers
  • The ring of rational numbers
  • The sieve of Eratosthenes
  • Square-free natural numbers
  • Squares in the integers
  • Squares in ℤₚ
  • Squares in the natural numbers
  • The standard cyclic groups
  • The standard cyclic rings
  • Stirling numbers of the second kind
  • Strict inequality on the integer fractions
  • Strict inequality on the integers
  • Strict inequality on the natural numbers
  • Strict inequality on the rational numbers
  • Strict inequality on the standard finite types
  • Strictly ordered pairs of natural numbers
  • The strong induction principle for the natural numbers
  • Sums of natural numbers
  • Sylvester’s sequence
  • Taxicab 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 integers
  • 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
  • Finite fields
  • Finite rings
  • 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
  • Abelian groups
  • Finite Commutative monoids
  • 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
  • Action on equivalences of functions
  • The action on equivalences of functions out of subuniverses
  • Action on equivalences of type families
  • Action on equivalences in type families over subuniverses
  • The action of functions on higher identifications
  • The action on homotopies of functions
  • The binary action on identifications of binary dependent functions
  • 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
  • The axiom of choice
  • Bands
  • Base changes of span diagrams
  • Bicomposition of functions
  • Binary dependent identifications
  • 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 relations with extensions
  • Binary relations with lifts
  • Binary transport
  • Binary type duality
  • The booleans
  • The Cantor–Schröder–Bernstein–Escardó theorem
  • Cantor’s theorem
  • Cartesian morphisms of arrows
  • Cartesian morphisms of span diagrams
  • Cartesian product types
  • Cartesian products of set quotients
  • The category of families of sets
  • The category of sets
  • Choice of representatives for an equivalence relation
  • Codiagonal maps of types
  • Coherently idempotent maps
  • Coherently invertible maps
  • Coinhabited pairs of types
  • Commuting cubes of maps
  • Commuting hexagons of identifications
  • Commuting pentagons of identifications
  • Commuting prisms of maps
  • Commuting squares of homotopies
  • Commuting squares of identifications
  • Commuting squares of maps
  • Commuting tetrahedra of homotopies
  • Commuting tetrahedra of maps
  • Commuting triangles of homotopies
  • Commuting triangles of identifications
  • Commuting triangles of maps
  • Commuting triangles of morphisms of arrows
  • Complements of type families
  • Complements of subtypes
  • Composite maps in inverse sequential diagrams
  • Composition algebra
  • Computational identity types
  • Cones over cospan diagrams
  • Cones over inverse sequential diagrams
  • Conjunction
  • Connected components of types
  • Connected components of universes
  • Connected maps
  • Connected types
  • Constant maps
  • Constant span diagrams
  • Constant type families
  • The continuation monad
  • Contractible maps
  • Contractible types
  • Copartial elements
  • Copartial functions
  • Coproduct decompositions
  • Coproduct decompositions in a subuniverse
  • Coproduct types
  • Coproducts of pullbacks
  • Morphisms in the coslice category of types
  • Cospan diagrams
  • Cospans of types
  • 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
  • Dependent binary homotopies
  • The dependent binomial theorem for types (distributivity of dependent function types over coproduct types)
  • Dependent epimorphisms
  • Dependent epimorphisms with respect to truncated types
  • Dependent function types
  • Dependent homotopies
  • Dependent identifications
  • Dependent inverse sequential diagrams of types
  • Dependent pair types
  • Dependent products of pullbacks
  • Dependent sequences
  • Dependent sums of pullbacks
  • Dependent telescopes
  • The dependent universal property of equivalences
  • Descent for coproduct types
  • Descent for dependent pair types
  • Descent for the empty type
  • Descent for equivalences
  • Diagonal maps into cartesian products of types
  • Diagonal maps of types
  • Diagonal span diagrams
  • Diagonals of maps
  • Diagonals of morphisms of arrows
  • Discrete binary relations
  • Discrete reflexive relations
  • Discrete relaxed Σ-decompositions
  • Discrete Σ-decompositions
  • Discrete types
  • Disjunction
  • Double arrows
  • Double negation
  • The double negation modality
  • Double negation stable propositions
  • 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 injective type families
  • Equivalence relations
  • Equivalences
  • Equivalences of arrows
  • Equivalences of cospans
  • Equivalences of double arrows
  • Equivalences of inverse sequential diagrams of types
  • Equivalences on Maybe
  • Equivalences of span diagrams
  • Equivalences of span diagrams on families of types
  • Equivalences of spans
  • Equivalences of spans of families of types
  • Evaluation of functions
  • Exclusive disjunctions
  • Exclusive sums
  • Existential quantification
  • Exponents of set quotients
  • Extensions of types
  • Faithful maps
  • Families of equivalences
  • Families of maps
  • Families of types over telescopes
  • Fiber inclusions
  • Fibered equivalences
  • Fibered involutions
  • Maps fibered over a map
  • Fibers of maps
  • Finitely coherent equivalences
  • Finitely coherently invertible maps
  • Fixed points of endofunctions
  • Full subtypes of types
  • Function extensionality
  • Function types
  • Functional correspondences
  • Functoriality of the action on identifications of functions
  • Functoriality of cartesian product types
  • Functoriality of coproduct types
  • Functoriality of dependent function types
  • Functoriality of dependent pair types
  • Functoriality of fibers of maps
  • Functoriality of function types
  • Functoriality of morphisms of arrows
  • Functoriality of propositional truncations
  • Functorialty of pullbacks
  • Functoriality of sequential limits
  • Functoriality of set quotients
  • Functoriality of set truncation
  • Functoriality of truncations
  • The fundamental theorem of identity types
  • Global choice
  • Global subuniverses
  • The globular type of dependent functions
  • The globular type of functions
  • Higher homotopies of morphisms of arrows
  • Hilbert’s ε-operators
  • Homotopies
  • Homotopies of morphisms of arrows
  • Homotopies of morphisms of cospan diagrams
  • Homotopy algebra
  • Homotopy induction
  • The homotopy preorder of types
  • Idempotent maps
  • Identity systems
  • Identity types of truncated types
  • Identity types
  • The image of a map
  • Images of subtypes
  • Implicit function types
  • Impredicative encodings of the logical operations
  • Impredicative universes
  • The induction principle for propositional truncation
  • Infinitely coherent equivalences
  • Inhabited subtypes
  • Inhabited types
  • Injective maps
  • The interchange law
  • Intersections of subtypes
  • Inverse sequential diagrams of types
  • Invertible maps
  • Involutions
  • Irrefutable propositions
  • Isolated elements
  • Isomorphisms of sets
  • Iterated cartesian product types
  • Iterated dependent pair types
  • Iterated dependent product types
  • Iterating automorphisms
  • Iterating functions
  • Iterating involutions
  • Kernel span diagrams of maps
  • Large binary relations
  • 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
  • Lifts of types
  • The limited principle of omniscience
  • Locally small types
  • Logical equivalences
  • Maps in global subuniverses
  • Maps in subuniverses
  • The maybe monad
  • Mere embeddings
  • Mere equality
  • Mere equivalences
  • Mere functions
  • Mere logical equivalences
  • Mere path-cosplit maps
  • Monomorphisms
  • Morphisms of arrows
  • Morphisms of binary relations
  • Morphisms of cospan diagrams
  • Morphisms of cospans
  • Morphisms of double arrows
  • Morphisms of inverse sequential diagrams of types
  • Morphisms of span diagrams
  • Morphisms of spans
  • Morphisms of spans on families of types
  • Morphisms of twisted arrows
  • Multisubsets
  • Multivariable correspondences
  • Multivariable decidable relations
  • Multivariable functoriality of set quotients
  • Multivariable homotopies
  • Multivariable operations
  • Multivariable relations
  • Multivariable sections
  • Negated equality
  • Negation
  • Noncontractible types
  • Null-homotopic maps
  • Operations on span diagrams
  • Operations on spans
  • Operations on spans of families of types
  • Opposite spans
  • Pairs of distinct elements
  • Partial elements
  • Partial functions
  • Partial sequences
  • Partitions
  • Path algebra
  • Path-cosplit maps
  • Path-split maps
  • Perfect images
  • Permutations of spans of families of types
  • Π-decompositions of types
  • Π-decompositions of types into types in a subuniverse
  • Pointed torsorial type families
  • Postcomposition of dependent functions
  • Postcomposition of functions
  • Postcomposition of pullbacks
  • Powersets
  • Precomposition of dependent functions
  • Precomposition of functions
  • Precomposition of functions into subuniverses
  • Precomposition of type families
  • Preimages of subtypes
  • The preunivalence axiom
  • Preunivalent type families
  • 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 pullbacks
  • 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 cones
  • Pullbacks
  • Pullbacks of subtypes
  • Quasicoherently idempotent maps
  • Raising universe levels
  • Reflecting maps for equivalence relations
  • Reflexive relations
  • The Regensburg extension of the fundamental theorem of identity types
  • Relaxed Σ-decompositions of types
  • Repetitions of values of maps
  • Repetitions in sequences
  • The type theoretic replacement axiom
  • Retractions
  • Retracts of maps
  • Retracts of types
  • Sections
  • Types separated at subuniverses
  • Sequences
  • Sequential limits
  • Set presented types
  • Set quotients
  • Set truncations
  • Sets
  • Shifting sequences
  • Σ-closed subuniverses
  • Σ-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
  • Sorial type families
  • Span diagrams
  • Span diagrams on families of types
  • Spans of types
  • Spans of families of types
  • Split idempotent maps
  • Split surjective maps
  • Standard apartness relations
  • Standard pullbacks
  • Strict symmetrization of binary relations
  • Strictly involutive identity types
  • The strictly right unital concatenation operation on identifications
  • Strongly extensional maps
  • Structure
  • The structure identity principle
  • Structured type duality
  • Subsingleton induction
  • Subterminal types
  • Subtype duality
  • The subtype identity principle
  • Subtypes
  • Subuniverses
  • Surjective maps
  • Symmetric binary relations
  • Symmetric cores of binary relations
  • Symmetric difference of subtypes
  • The symmetric identity types
  • Symmetric operations
  • Telescopes
  • Terminal spans on families of types
  • Tight apartness relations
  • Torsorial type families
  • Total partial elements
  • Total partial functions
  • Transfinite cocomposition of maps
  • Transport along equivalences
  • Transport along higher identifications
  • Transport along homotopies
  • Transport along identifications
  • Transport-split type families
  • Transposing identifications along equivalences
  • Transposing identifications along retractions
  • Transposing identifications along sections
  • Transposition of span diagrams
  • 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
  • Uniqueness of the image of a map
  • Uniqueness quantification
  • The uniqueness of set quotients
  • Uniqueness of set truncations
  • Uniqueness of the truncations
  • The unit type
  • Unital binary operations
  • The univalence axiom
  • The univalence axiom implies function extensionality
  • Univalent type families
  • The universal property of booleans
  • The universal properties of cartesian product types
  • Universal property of contractible types
  • The universal property of coproduct types
  • The universal property of dependent function types
  • The universal property of dependent pair types
  • The universal property of the empty type
  • The universal property of equivalences
  • The universal property of the family of fibers of maps
  • The universal property of fiber products
  • The universal property of identity systems
  • The universal property of identity types
  • The universal property of the image of a map
  • The universal property of the maybe monad
  • 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 sequential limits
  • The universal property of set quotients
  • The universal property of set truncations
  • The universal property of truncations
  • The universal property of the unit type
  • Universal quantification
  • 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
  • Whiskering higher homotopies with respect to composition
  • Whiskering homotopies with respect to composition
  • Whiskering homotopies with respect to concatenation
  • Whiskering identifications with respect to concatenation
  • Whiskering operations
  • The wild category of types
  • Yoneda identity types

• Foundation core

  • 1-Types
  • Cartesian product types
  • Coherently invertible maps
  • Commuting prisms of maps
  • Commuting squares of homotopies
  • Commuting squares of identifications
  • Commuting squares of maps
  • Commuting triangles of maps
  • Constant maps
  • Contractible maps
  • Contractible types
  • Coproduct types
  • Decidable propositions
  • Dependent identifications
  • Diagonal maps into cartesian products of types
  • Discrete types
  • Embeddings
  • Empty types
  • Endomorphisms
  • Equality of dependent pair types
  • Equivalence relations
  • Equivalences
  • Families of equivalences
  • Fibers of maps
  • Function types
  • Functoriality of dependent function types
  • Functoriality of dependent pair types
  • Homotopies
  • Identity types
  • Injective maps
  • Invertible maps
  • Negation
  • Operations on span diagrams
  • Operations on spans
  • Path-split maps
  • Postcomposition of dependent functions
  • Postcomposition of functions
  • Precomposition of dependent functions
  • Precomposition of functions
  • Propositional maps
  • Propositions
  • Pullbacks
  • Retractions
  • Retracts of types
  • Sections
  • Sets
  • Small types
  • Subtypes
  • Torsorial type families
  • Transport along identifications
  • Truncated maps
  • Truncated types
  • Truncation levels
  • The type theoretic principle of choice
  • The univalence axiom
  • The universal property of pullbacks
  • The universal property of truncations
  • Whiskering homotopies with respect to concatenation
  • Whiskering identifications with respect to concatenation

• Globular types

  • Base change of dependent globular types
  • Base change of dependent reflexive globular types
  • Binary dependent globular types
  • Binary dependent reflexive globular types
  • Binary globular maps
  • Colax reflexive globular maps
  • Colax transitive globular maps
  • Composition structure on globular types
  • Constant globular types
  • Dependent globular types
  • Dependent reflexive globular types
  • Dependent sums of globular types
  • Discrete dependent reflexive globular types
  • Discrete globular types
  • Discrete reflexive globular types
  • Empty globular types
  • Equality of globular types
  • Exponentials of globular types
  • Fibers of globular maps
  • Equivalences between globular types
  • Maps between globular types
  • Globular types
  • Large colax reflexive globular maps
  • Large colax transitive globular maps
  • Maps between large globular types
  • Large globular types
  • Large lax reflexive globular maps
  • Large lax transitive globular maps
  • Large reflexive globular maps
  • Large reflexive globular types
  • Large symmetric globular types
  • Large transitive globular maps
  • Large transitive globular types
  • Lax reflexive globular maps
  • Lax transitive globular maps
  • Points of globular types
  • Points of reflexive globular types
  • Pointwise extensions of binary families of globular types
  • Pointwise extensions of binary families of reflexive globular types
  • Pointwise extensions of families of globular types
  • Pointwise extensions of families of reflexive globular types
  • Products of families of globular types
  • Reflexive globular equivalences
  • Reflexive globular maps
  • Reflexive globular types
  • Sections of dependent globular types
  • Superglobular types
  • Symmetric globular types
  • Terminal globular types
  • Transitive globular maps
  • Transitive globular types
  • The unit globular type
  • The unit reflexive globular type
  • The universal globular type
  • The universal reflexive globular type

• Graph theory

  • Acyclic undirected graphs
  • Base change of dependent directed graphs
  • Base change of dependent reflexive graphs
  • Cartesian products of directed graphs
  • Cartesian products of reflexive 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
  • Dependent directed graphs
  • Dependent products of directed graphs
  • Dependent products of reflexive graphs
  • Dependent reflexive graphs
  • Dependent sums directed graphs
  • Dependent sums reflexive graphs
  • Directed graph duality
  • Directed graph structures on standard finite sets
  • Directed graphs
  • Discrete dependent reflexive graphs
  • Discrete directed graphs
  • Discrete reflexive graphs
  • Displayed large reflexive graphs
  • Edge-coloured undirected graphs
  • Embeddings of directed graphs
  • Embeddings of undirected graphs
  • Enriched undirected graphs
  • Equivalences of dependent directed graphs
  • Equivalences of dependent reflexive graphs
  • Equivalences of directed graphs
  • Equivalences of enriched undirected graphs
  • Equivalences of reflexive graphs
  • Equivalences of undirected graphs
  • Eulerian circuits in undirected graphs
  • Faithful morphisms of undirected graphs
  • Fibers of directed graphs
  • Fibers of morphisms into directed graphs
  • Fibers of morphisms into reflexive graphs
  • Finite graphs
  • Geometric realizations of undirected graphs
  • Higher directed graphs
  • Hypergraphs
  • Internal homs of directed graphs
  • Large higher directed graphs
  • Large reflexive graphs
  • Matchings
  • Mere equivalences of undirected graphs
  • Morphisms of dependent directed graphs
  • Morphisms of directed graphs
  • Morphisms of reflexive 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
  • Sections of dependent directed graphs
  • Sections of dependent reflexive graphs
  • Simple undirected graphs
  • Stereoisomerism for enriched undirected graphs
  • Terminal directed graphs
  • Terminal reflexive graphs
  • Totally faithful morphisms of undirected graphs
  • Trails in directed graphs
  • Trails in undirected graphs
  • Undirected graph structures on standard finite sets
  • Undirected graphs
  • The universal directed graph
  • The universal reflexive graph
  • Vertex covers
  • Voltage graphs
  • Walks in directed graphs
  • Walks in undirected graphs
  • Wide displayed large reflexive graphs

• Group theory

  • Abelian groups
  • Abelianization of 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 abelian groups
  • The category of concrete groups
  • The category of group actions
  • The category of groups
  • The orbit category of a group
  • 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
  • Centralizer subgroups
  • Characteristic subgroups
  • Commutative monoids
  • Commutator subgroups
  • Commutators of elements in groups
  • Commuting elements of groups
  • Commuting elements of monoids
  • Commuting elements of semigroups
  • Commuting squares of group homomorphisms
  • Concrete group actions
  • Concrete groups
  • Concrete monoids
  • 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
  • Conjugation on concrete groups
  • Contravariant pushforwards of concrete group actions
  • Cores of monoids
  • Cyclic groups
  • 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
  • Elements of finite order
  • 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
  • Exponents of abelian groups
  • Exponents of groups
  • Free concrete group actions
  • Free groups with one generator
  • The full subgroup of a group
  • The full subsemigroup of a semigroup
  • Function groups of abelian groups
  • Function commutative monoids
  • Function groups
  • Function monoids
  • Function semigroups
  • Functoriality of quotient groups
  • Furstenberg groups
  • Generating elements of 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 groups equipped with normal subgroups
  • Homomorphisms of monoids
  • Homomorphisms of semigroups
  • Images of group homomorphisms
  • Images of semigroup homomorphisms
  • Integer multiples of elements in abelian groups
  • Integer powers of elements of groups
  • 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 monoids
  • Isomorphisms of semigroups
  • Iterated cartesian products of concrete groups
  • Kernels of homomorphisms between abelian groups
  • Kernels of homomorphisms of concrete groups
  • Kernels of homomorphisms of 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
  • Multiples of elements in abelian groups
  • Nontrivial groups
  • Normal closures of subgroups
  • Normal cores of subgroups
  • Normal subgroups
  • Normal subgroups of concrete groups
  • Normal submonoids
  • Normal submonoids of commutative monoids
  • Normalizer subgroups
  • Nullifying group homomorphisms
  • The opposite of a group
  • The opposite of a semigroup
  • The orbit-stabilizer theorem for concrete groups
  • Orbits of concrete group actions
  • Orbits of group actions
  • The order of an element in a group
  • Perfect cores
  • Perfect groups
  • Perfect subgroups
  • Powers of elements in commutative monoids
  • Powers of elements in groups
  • Powers of elements in monoids
  • 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 orbits of a monoid action
  • 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
  • Pullbacks of subgroups
  • Pullbacks of subsemigroups
  • Quotient groups
  • Quotient groups of concrete groups
  • Quotients of abelian groups
  • Rational commutative monoids
  • Representations of monoids in precategories
  • 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 elements of a group
  • Subgroups generated by families of elements
  • 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
  • Subsets of semigroups
  • The substitution functor of concrete group actions
  • The substitution functor of group actions
  • Surjective group homomorphisms
  • Surjective semigroup homomorphisms
  • Symmetric concrete groups
  • Symmetric groups
  • Torsion elements of groups
  • Torsion-free groups
  • Torsors of abstract groups
  • Transitive concrete group actions
  • Transitive group actions
  • Trivial concrete groups
  • Trivial group homomorphisms
  • Trivial groups
  • Trivial subgroups
  • Unordered tuples of elements in commutative monoids
  • Wild representations of monoids

• Higher group theory

  • Abelian higher groups
  • Cartesian products of higher groups
  • Conjugation in higher groups
  • Cyclic higher groups
  • Deloopable groups
  • Deloopable H-spaces
  • Deloopable types
  • Eilenberg-Mac Lane spaces
  • 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
  • Iterated deloopings of pointed types
  • Orbits of higher group actions
  • Small ∞-groups
  • Subgroups of higher groups
  • Symmetric higher groups
  • Transitive higher group actions
  • Trivial higher groups

• Linear algebra

  • Constant matrices
  • Diagonal vectors
  • Diagonal matrices on rings
  • Functoriality of the type 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

• Metric spaces

  • The category of metric spaces and isometries
  • The category of metric spaces and short maps
  • Cauchy approximations in metric spaces
  • Cauchy approximations in premetric spaces
  • Closed premetric structures
  • Complete metric spaces
  • Convergent Cauchy approximations in metric spaces
  • Dependent products of metric spaces
  • Discrete premetric structures
  • Equality of metric spaces
  • Equality of premetric spaces
  • Extensional premetric structures on types
  • Functions between metric spaces
  • The functor from the precategory of metric spaces and isometries to the precategory of sets
  • The inclusion of isometries into the category of metric spaces and short maps
  • Induced premetric structures on preimages
  • Isometric equivalences between premetric spaces
  • Isometries between metric spaces
  • Isometries between premetric spaces
  • Limits of Cauchy approximations in premetric spaces
  • The metric space of cauchy approximations in a metric space
  • The metric space of convergent cauchy approximations in a metric space
  • The standard metric structure on the rational numbers
  • The metric structure on the rational numbers with open neighborhoods
  • Metric spaces
  • Metric structures
  • Monotonic premetric structures on types
  • The poset of premetric structures on a type
  • The precategory of metric spaces and functions
  • The precategory of metric spaces and isometries
  • The precategory of metric spaces and short functions
  • Premetric spaces
  • Premetric structures on types
  • Pseudometric spaces
  • Pseudometric structures on a type
  • Reflexive premetric structures on types
  • Saturated metric spaces
  • Short functions between metric spaces
  • Short functions between premetric spaces
  • Subspaces of metric spaces
  • Symmetric premetric structures on types
  • Triangular premetric structures on types

• Modal type theory

  • The action on homotopies of the flat modality
  • The action on identifications of crisp functions
  • The action on identifications of the flat modality
  • Crisp cartesian product types
  • Crisp coproduct types
  • Crisp dependent function types
  • Crisp dependent pair types
  • Crisp function types
  • Crisp identity types
  • The crisp law of excluded middle
  • Crisp pullbacks
  • Crisp types
  • Dependent universal property of flat discrete crisp types
  • Flat discrete crisp types
  • The flat modality
  • The flat-sharp adjunction
  • Functoriality of the flat modality
  • Functoriality of the sharp modality
  • Sharp codiscrete maps
  • Sharp codiscrete types
  • The sharp modality
  • Transport along crisp identifications
  • The universal property of flat discrete crisp types

• Order theory

  • Accessible elements with respect to relations
  • Bottom elements in large posets
  • Bottom elements in posets
  • Bottom elements in preorders
  • Chains in posets
  • Chains in preorders
  • Closure operators on large locales
  • Closure operators on large posets
  • Commuting squares of Galois connections between large posets
  • Commuting squares of order preserving maps of large posets
  • Coverings in locales
  • 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
  • Distributive lattices
  • Finite coverings in locales
  • Finite posets
  • Finite preorders
  • Finite total orders
  • 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-suplattices
  • Homomorphisms of suplattices
  • Ideals in preorders
  • Incidence algebras
  • Inflattices
  • Inhabited chains in posets
  • Inhabited chains in preorders
  • Inhabited finite total orders
  • Interval subposets
  • Join preserving maps between posets
  • Join-semilattices
  • The Knaster–Tarski fixed point theorem
  • 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 sets in large posets
  • Lower types in preorders
  • Maximal chains in posets
  • Maximal chains in preorders
  • Meet-semilattices
  • Meet-suplattices
  • Nuclei on large locales
  • Opposite large posets
  • Opposite large preorders
  • Opposite posets
  • Opposite preorders
  • Order preserving maps between large posets
  • Order preserving maps between large preorders
  • Order preserving maps between posets
  • Order preserving maps between preorders
  • Ordinals
  • Posets
  • Powers of large locales
  • The precategory of decidable total orders
  • The precategory of finite posets
  • The precategory of finite total orders
  • The precategory of inhabited finite total orders
  • The precategory of posets
  • The precategory of total orders
  • Preorders
  • Principal lower sets of large posets
  • Principal upper sets of large posets
  • Reflective Galois connections between large posets
  • Resizing posets
  • Resizing preorders
  • Resizing suplattices
  • Similarity of elements in large posets
  • Similarity of elements in large preorders
  • Similarity of order preserving maps between large posets
  • Similarity of order preserving maps between large preorders
  • Subposets
  • Subpreorders
  • Suplattices
  • Supremum preserving maps between posets
  • Top elements in large posets
  • Top elements in posets
  • Top elements in preorders
  • Total orders
  • Total preorders
  • Upper bounds of chains in posets
  • Upper bounds in large posets
  • Upper bounds in posets
  • Upper sets of large posets
  • Well-founded orders
  • Well-founded relations
  • Zorn’s lemma

• Organic chemistry

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

• Orthogonal factorization systems

  • Cd-structures
  • Cellular maps
  • The closed modalities
  • Continuation modalities
  • Double lifts of families of elements
  • Double negation sheaves
  • Extensions of double lifts of families of elements
  • Extensions of families of elements
  • Extensions of maps
  • Factorization operations
  • Factorization operations into function classes
  • Factorization operations into global function classes
  • Factorizations of maps
  • Factorizations of maps into function classes
  • Factorizations of maps into global function classes
  • Families of types local at a map
  • Fiberwise orthogonal maps
  • Function classes
  • Functoriality of higher modalities
  • Functoriality of the pullback-hom
  • Global function classes
  • Higher modalities
  • The identity modality
  • Large Lawvere–Tierney topologies
  • Lawvere–Tierney topologies
  • Lifting operations
  • Lifting structures on commuting squares of maps
  • Lifts of families of elements
  • Lifts of maps
  • Localizations at maps
  • Localizations at subuniverses
  • Locally small modal-operators
  • Maps local at maps
  • Mere lifting properties
  • Modal induction
  • Modal operators
  • Modal subuniverse induction
  • Null families of types
  • Null maps
  • Null types
  • The open modalities
  • Orthogonal factorization systems
  • Orthogonal maps
  • Precomposition of lifts of families of elements by maps
  • The pullback-hom
  • The raise modalities
  • Reflective modalities
  • Reflective subuniverses
  • Regular cd-structures
  • Σ-closed modalities
  • Σ-closed reflective modalities
  • Σ-closed reflective subuniverses
  • Stable orthogonal factorization systems
  • Types colocal at maps
  • Types local at maps
  • Types separated at maps
  • Uniquely eliminating modalities
  • Wide function classes
  • Wide global function classes
  • The zero modality

• Polytopes

  • Abstract polytopes

• Primitives

  • Characters
  • Floats
  • Machine integers
  • Strings

• Real numbers

  • Dedekind real numbers
  • The metric space of real numbers
  • Rational real numbers

• Reflection

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

• Ring theory

  • Additive orders of elements of rings
  • Algebras over rings
  • The binomial theorem for rings
  • The binomial theorem for semirings
  • The category of cyclic rings
  • The category of rings
  • Central elements of rings
  • Central elements of semirings
  • Characteristics of rings
  • Commuting elements of rings
  • Congruence relations on rings
  • Congruence relations on semirings
  • Cyclic rings
  • Dependent products of rings
  • Dependent products of semirings
  • Division rings
  • The free ring with one generator
  • Full ideals of rings
  • Function rings
  • Function semirings
  • Generating elements of rings
  • The group of multiplicative units of a ring
  • Homomorphisms of cyclic rings
  • Homomorphisms of rings
  • Homomorphisms of semirings
  • Ideals generated by subsets of rings
  • Ideals of rings
  • Ideals of semirings
  • Idempotent elements in rings
  • Initial rings
  • Integer multiples of elements of 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
  • Kernels of ring homomorphisms
  • Left ideals generated by subsets of rings
  • Left ideals of rings
  • Local rings
  • Localizations of rings
  • Maximal ideals of rings
  • Modules over rings
  • Multiples of elements in rings
  • Multiplicative orders of elements of rings
  • Nil ideals of rings
  • Nilpotent elements in rings
  • Nilpotent elements in semirings
  • Opposite rings
  • The poset of cyclic 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
  • Transporting ring structures along isomorphisms of abelian groups
  • Trivial rings

• Set theory

  • Baire space
  • Cantor space
  • Cantor’s diagonal argument
  • Cardinalities of sets
  • Countable sets
  • Cumulative hierarchy
  • Infinite sets
  • Russell’s paradox
  • 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
  • Commuting squares of pointed homotopies
  • Commuting squares of pointed maps
  • Commuting triangles of pointed maps
  • Conjugation of pointed types
  • Constant pointed maps
  • Contractible pointed types
  • Cyclic types
  • Dependent products of H-spaces
  • Dependent products of pointed types
  • Dependent products of wild monoids
  • Dependent types equipped with automorphisms
  • Equivalences of H-spaces
  • Equivalences of pointed arrows
  • Equivalences of types equipped with automorphisms
  • Equivalences of types equipped with endomorphisms
  • Faithful pointed maps
  • Fibers of pointed maps
  • Finite multiplication in magmas
  • Function H-spaces
  • Function magmas
  • Function wild monoids
  • 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 H-spaces
  • Morphisms of magmas
  • Morphisms of pointed arrows
  • Morphisms of twisted pointed arrows
  • Morphisms of types equipped with automorphisms
  • Morphisms of types equipped with endomorphisms
  • Morphisms of wild monoids
  • Noncoherent H-spaces
  • Opposite pointed spans
  • Pointed 2-homotopies
  • Pointed cartesian product types
  • Pointed dependent functions
  • Pointed dependent pair types
  • Pointed equivalences
  • Pointed families of types
  • Pointed homotopies
  • Pointed isomorphisms
  • Pointed maps
  • Pointed retractions of pointed maps
  • Pointed sections of pointed maps
  • Pointed span diagrams
  • Pointed spans
  • Pointed types
  • Pointed types equipped with automorphisms
  • The pointed unit type
  • Universal property of contractible types with respect to pointed types and maps
  • Postcomposition of pointed maps
  • Precomposition of pointed maps
  • Sets equipped with automorphisms
  • Small pointed types
  • Symmetric elements of involutive types
  • Symmetric H-spaces
  • Transposition of pointed span diagrams
  • Types equipped with automorphisms
  • Types equipped with endomorphisms
  • Uniform pointed homotopies
  • The universal property of pointed equivalences
  • Unpointed maps between pointed types
  • Whiskering pointed homotopies with respect to concatenation
  • Whiskering of pointed homotopies with respect to composition of pointed maps
  • The wild category of pointed types
  • Wild groups
  • Wild loops
  • Wild monoids
  • Wild quasigroups
  • Wild semigroups

• Synthetic category theory

  • Cone diagrams of synthetic categories
  • Cospans of synthetic categories
  • Equivalences between synthetic categories
  • Invertible functors between synthetic categories
  • Pullbacks of synthetic categories
  • Retractions of functors between synthetic categories
  • Sections of functor between synthetic categories
  • Synthetic categories

• Synthetic homotopy theory

  • 0-acyclic maps
  • 0-acyclic types
  • 1-acyclic types
  • Acyclic maps
  • Acyclic types
  • The category of connected set bundles over the circle
  • Cavallo’s trick
  • The circle
  • Cocartesian morphisms of arrows
  • Cocones under pointed span diagrams
  • Cocones under sequential diagrams
  • Cocones under spans
  • Codiagonals of maps
  • Coequalizers
  • Cofibers
  • Coforks
  • Correspondence between cocones under sequential diagrams and certain coforks
  • Conjugation of loops
  • Connected set bundles over the circle
  • Connective prespectra
  • Connective spectra
  • Dependent cocones under sequential diagrams
  • Dependent cocones under spans
  • Dependent coforks
  • Dependent descent for the circle
  • The dependent pullback property of pushouts
  • Dependent pushout-products
  • Dependent sequential diagrams
  • Dependent suspension structures
  • The dependent universal property of coequalizers
  • The dependent universal property of pushouts
  • The dependent universal property of sequential colimits
  • Dependent universal property of suspensions
  • The descent property of the circle
  • Descent data for constant type families over the circle
  • Descent data for families of dependent pair types over the circle
  • Descent data for families of equivalence types over the circle
  • Descent data for families of function types over the circle
  • Subtypes of descent data for the circle
  • Descent data for type families of equivalence types over pushouts
  • Descent data for type families of function types over pushouts
  • Descent data for type families of identity types over pushouts
  • Descent data for pushouts
  • Descent data for sequential colimits
  • Descent property of pushouts
  • Descent property of sequential colimits
  • Double loop spaces
  • The Eckmann-Hilton argument
  • Equifibered sequential diagrams
  • Equivalences of cocones under sequential diagrams
  • Equivalences of coforks
  • Equivalances of dependent sequential diagrams
  • Equivalences of descent data for pushouts
  • Equivalences of sequential diagrams
  • Families with descent data for pushouts
  • Families with descent data for sequential colimits
  • The flattening lemma for coequalizers
  • The flattening lemma for pushouts
  • The flattening lemma for sequential colimits
  • Free loops
  • Functoriality of the loop space operation
  • Functoriality of sequential colimits
  • Functoriality of suspensions
  • Groups of loops in 1-types
  • Hatcher’s acyclic type
  • Identity systems of descent data for pushouts
  • The induction principle of pushouts
  • The infinite complex projective space
  • Infinite cyclic types
  • The interval
  • Iterated loop spaces
  • Iterated suspensions of pointed types
  • Join powers of types
  • Joins of maps
  • Joins of types
  • The loop homotopy on the circle
  • Loop spaces
  • Maps of prespectra
  • Mere spheres
  • Morphisms of cocones under morphisms of sequential diagrams
  • Morphisms of coforks
  • Morphisms of dependent sequential diagrams
  • Morphisms of descent data of the circle
  • Morphisms of descent data for pushouts
  • Morphisms of sequential diagrams
  • The multiplication operation on the circle
  • Null cocones under pointed span diagrams
  • The plus-principle
  • Powers of loops
  • Premanifolds
  • Prespectra
  • The pullback property of pushouts
  • Pushout-products
  • Pushouts
  • Pushouts of pointed types
  • The recursion principle of pushouts
  • Retracts of sequential diagrams
  • Rewriting rules for pushouts
  • Sections of families over the circle
  • Sections of descent data for pushouts
  • Sequential colimits
  • Sequential diagrams
  • Sequentially compact types
  • Shifts of sequential diagrams
  • Smash products of pointed types
  • Spectra
  • The sphere prespectrum
  • Spheres
  • Suspension prespectra
  • Suspension Structures
  • Suspensions of pointed types
  • Suspensions of types
  • Tangent spheres
  • Total cocones of type families over cocones under sequential diagrams
  • Total sequential diagrams of dependent sequential diagrams
  • Triple loop spaces
  • k-acyclic maps
  • k-acyclic types
  • The universal cover of the circle
  • The universal property of the circle
  • The universal property of coequalizers
  • The universal property of pushouts
  • The universal property of sequential colimits
  • Universal property of suspensions
  • Universal Property of suspensions of pointed types
  • Wedges of pointed types
  • Zigzags between sequential diagrams

• Trees

  • Algebras for polynomial endofunctors
  • Bases of directed trees
  • Bases of enriched directed trees
  • Binary W-types
  • Bounded multisets
  • 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
  • Empty multisets
  • Enriched directed trees
  • Equivalences of directed trees
  • Equivalences of enriched directed trees
  • Extensional W-types
  • Fibers of directed trees
  • Fibers of enriched directed trees
  • Full binary trees
  • Functoriality of the combinator of directed trees
  • Functoriality of the fiber operation on directed trees
  • Functoriality of W-types
  • Hereditary 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
  • Multiset-indexed dependent products of types
  • Multisets
  • Planar binary trees
  • Plane 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 trees
  • The universal multiset
  • The universal tree
  • 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
  • Π-types in precategories with attributes
  • Π-types in precategories with families
  • Precategories with attributes
  • Precategories with families
  • 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 elements 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 finite 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
  • Embeddings
  • 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
  • Finite presentations of types
  • Finite types
  • Finiteness of the type of connected components
  • 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
  • Kuratowski finite sets
  • Latin squares
  • Locally finite types
  • The groupoid of main classes of Latin hypercubes
  • The groupoid of main classes of Latin squares
  • The maybe monad 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

• Wild category theory

  • Colax functors between large noncoherent wild higher precategories
  • Colax functors between noncoherent wild higher precategories
  • Isomorphisms in noncoherent large wild higher precategories
  • Isomorphisms in noncoherent wild higher precategories
  • Maps between noncoherent large wild higher precategories
  • Maps between noncoherent wild higher precategories
  • Noncoherent large wild higher precategories
  • Noncoherent wild higher precategories