SUMMARY
Overview
The agdaunimath library

 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 setmagmoids
 Composition operations on binary families of sets
 Conservative functors between precategories
 Constant functors
 Copresheaf categories
 Coproducts in precategories
 Cores of categories
 Cores of precategories
 Coslice precategories
 Dependent products of categories
 Dependent products of large categories
 Dependent products of large precategories
 Dependent products of precategories
 Discrete categories
 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
 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 setmagmoids
 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
 Maps between categories
 Maps from small to large categories
 Maps from small to large precategories
 Maps between precategories
 Maps between setmagmoids
 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
 Rigid objects in a category
 Rigid objects in a precategory
 Setmagmoids
 Sieves in categories
 The simplex category
 Slice precategories
 Split essentially surjective functors between precategories
 Strict categories
 Structure equivalences between setmagmoids
 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

 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

 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 crossmultiplication 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
 Euclidean division on the natural numbers
 Euler's totient function
 Exponentiation of natural numbers
 Factorials of natural numbers
 Falling factorials
 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 halfintegers
 The HardyRamanujan 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
 Squarefree 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
 Strictly ordered pairs of natural numbers
 The strong induction principle for the natural numbers
 Sums of natural numbers
 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 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
 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

 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 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 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 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
 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 diagonal argument
 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 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
 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 relations
 Discrete relaxed Σdecompositions
 Discrete Σdecompositions
 Discrete types
 Disjunction
 Double arrows
 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 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 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 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
 Higher homotopies of morphisms of arrows
 Hilbert's
ε
operators  Homotopies
 Homotopies of morphisms of arrows
 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
 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
 The maybe modality
 Mere embeddings
 Mere equality
 Mere equivalences
 Mere functions
 Mere logical equivalences
 Mere pathcosplit 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
 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
 Pathcosplit maps
 Pathsplit 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
 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
 Russell's paradox
 Sections
 Separated types
 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
 Transportsplit 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 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 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

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

 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
 Discrete graphs
 Displayed large reflexive 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
 Higher directed graphs
 Hypergraphs
 Large higher directed graphs
 Large reflexive graphs
 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
 Wide displayed large reflexive graphs

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

 Cartesian products of higher groups
 Conjugation in higher groups
 Cyclic higher groups
 Deloopable groups
 Deloopable Hspaces
 Deloopable types
 EilenbergMac 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

 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

 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

 Accessible elements with respect to relations
 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 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 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 meetsemilattices
 Homomorphisms of large suplattices
 Homomorphisms of meetsemilattices
 Homomorphisms of meet sup lattices
 Homomorphisms of suplattices
 Ideals in preorders
 Inhabited finite total orders
 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 sets in large 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
 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
 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
 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
 Upper sets of large posets
 Wellfounded orders
 Wellfounded relations

Orthogonal factorization systems
 Cdstructures
 Cellular maps
 The closed modalities
 Double lifts of families of elements
 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
 Fiberwise orthogonal maps
 Function classes
 Functoriality of higher modalities
 Functoriality of the pullbackhom
 Global function classes
 Higher modalities
 The identity modality
 Lifting operations
 Lifting structures on commuting squares of maps
 Lifts of families of elements
 Lifts of maps
 Local families of types
 Local maps
 Local types
 Localizations at maps
 Localizations at subuniverses
 Locally small modaloperators
 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 pullbackhom
 The raise modalities
 Reflective modalities
 Reflective subuniverses
 Regular cdstructures
 Separated types
 Σclosed modalities
 Σclosed reflective modalities
 Σclosed reflective subuniverses
 Stable orthogonal factorization systems
 Uniquely eliminating modalities
 Wide function classes
 Wide global function classes
 The zero modality

 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

 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
 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 Hspaces
 Dependent products of pointed types
 Dependent products of wild monoids
 Dependent types equipped with automorphisms
 Equivalences of Hspaces
 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 Hspaces
 Function magmas
 Function wild monoids
 Globular types
 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
 Large globular types
 Large reflexive globular types
 Large symmetric globular types
 Large transitive globular types
 Magmas
 Maps between globular types
 Maps between large globular types
 Mere equivalences of types equipped with endomorphisms
 Morphisms of Hspaces
 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 Hspaces
 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
 Reflexive globular types
 Sets equipped with automorphisms
 Small pointed types
 Symmetric elements of involutive types
 Symmetric globular types
 Symmetric Hspaces
 Transitive globular types
 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
 Wild groups
 Wild loops
 Wild monoids
 Wild quasigroups
 Wild semigroups

0
acyclic maps0
acyclic types1
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
 Dependent cocones under sequential diagrams
 Dependent cocones under spans
 Dependent coforks
 Dependent descent for the circle
 The dependent pullback property of pushouts
 Dependent pushoutproducts
 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 EckmannHilton 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 plusprinciple
 Powers of loops
 Premanifolds
 Prespectra
 The pullback property of pushouts
 Pushoutproducts
 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 mapsk
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

 Algebras for polynomial endofunctors
 Bases of directed trees
 Bases of enriched directed trees
 Binary Wtypes
 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 Wtypes
 Empty multisets
 Enriched directed trees
 Equivalences of directed trees
 Equivalences of enriched directed trees
 Extensional Wtypes
 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 Wtypes
 Hereditary 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
 Multisetindexed dependent products of types
 Multisets
 Planar binary trees
 Plane 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 trees
 The universal multiset
 The universal tree
 The Wtype of natural numbers
 The Wtype of the type of propositions
 Wtypes

 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

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

 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