diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index 295040db20..fefb607157 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -35,6 +35,27 @@ repos: args: [] require_serial: false + - id: generate-namespace-index-modules + name: Generate Agda namespace index modules + entry: hooks/generate_namespace_index_modules.py + language: python + always_run: true + verbose: true + types_or: [markdown, text] + args: [] + require_serial: false + + - id: generate-main-index-file + name: Generate main index file + entry: hooks/generate_main_index_file.py + language: python + always_run: true + verbose: true + types_or: [markdown, text] + args: [] + require_serial: false + + # - repo: https://github.com/pre-commit/mirrors-prettier # rev: "v3.0.0-alpha.6" # hooks: diff --git a/MODULE-INDEX.md b/MODULE-INDEX.md new file mode 100644 index 0000000000..93ccf62fd1 --- /dev/null +++ b/MODULE-INDEX.md @@ -0,0 +1,1010 @@ +# Formalisation in Agda + +- [Category theory](category-theory.md) + - [Adjunctions between large precategories](category-theory.adjunctions-large-precategories.md) + - [Anafunctors](category-theory.anafunctors.md) + - [Categories](category-theory.categories.md) + - [Coproducts in precategories](category-theory.coproducts-precategories.md) + - [Endomorphisms of objects in categories](category-theory.endomorphisms-of-objects-categories.md) + - [Epimorphism in large precategories](category-theory.epimorphisms-large-precategories.md) + - [Equivalences between categories](category-theory.equivalences-categories.md) + - [Equivalences between large precategories](category-theory.equivalences-large-precategories.md) + - [Equivalences between precategories](category-theory.equivalences-precategories.md) + - [Exponential objects in precategories](category-theory.exponential-objects-precategories.md) + - [Functors between categories](category-theory.functors-categories.md) + - [Functors between large precategories](category-theory.functors-large-precategories.md) + - [Functors between precategories](category-theory.functors-precategories.md) + - [Groupoids](category-theory.groupoids.md) + - [Homotopies of natural transformations in large precategories](category-theory.homotopies-natural-transformations-large-precategories.md) + - [Initial objects of a precategory](category-theory.initial-objects-precategories.md) + - [Isomorphisms in categories](category-theory.isomorphisms-categories.md) + - [Isomorphisms in large precategories](category-theory.isomorphisms-large-precategories.md) + - [Isomorphisms in precategories](category-theory.isomorphisms-precategories.md) + - [Large categories](category-theory.large-categories.md) + - [Large precategories](category-theory.large-precategories.md) + - [Monomorphisms in large precategories](category-theory.monomorphisms-large-precategories.md) + - [Natural isomorphisms between functors between categories](category-theory.natural-isomorphisms-categories.md) + - [Natural isomorphisms between functors between precategories](category-theory.natural-isomorphisms-precategories.md) + - [Natural isomorphisms between functors on large precategories](category-theory.natural-isomorphisms-large-precategories.md) + - [Natural numbers object in a precategory](category-theory.natural-numbers-object-precategories.md) + - [Natural transformations between functors between categories](category-theory.natural-transformations-categories.md) + - [Natural transformations between functors between large precategories](category-theory.natural-transformations-large-precategories.md) + - [Natural transformations between functors on precategories](category-theory.natural-transformations-precategories.md) + - [Precategories](category-theory.precategories.md) + - [Pregroupoids](category-theory.pregroupoids.md) + - [Products in precategories](category-theory.products-precategories.md) + - [Pullbacks in precategories](category-theory.pullbacks-precategories.md) + - [Sieves in categories](category-theory.sieves-categories.md) + - [Slice precategories](category-theory.slice-precategories.md) + - [Terminal object of a precategory](category-theory.terminal-objects-precategories.md) + - [The discrete precategory introduced by any hSet](category-theory.discrete-precategories.md) + - [The precategory of functors and natural transformations between two fixed precategories](category-theory.precategory-of-functors.md) + +- [Commutative algebra](commutative-algebra.md) + - [Boolean rings](commutative-algebra.boolean-rings.md) + - [Commutative rings](commutative-algebra.commutative-rings.md) + - [Commutative semirings](commutative-algebra.commutative-semirings.md) + - [Discrete fields](commutative-algebra.discrete-fields.md) + - [Homomorphisms of commutative rings](commutative-algebra.homomorphisms-commutative-rings.md) + - [Ideals in commutative rings](commutative-algebra.ideals-commutative-rings.md) + - [Integral domains](commutative-algebra.integral-domains.md) + - [Invertible elements in commutative rings](commutative-algebra.invertible-elements-commutative-rings.md) + - [Isomorphisms of commutative rings](commutative-algebra.isomorphisms-commutative-rings.md) + - [Local commutative rings](commutative-algebra.local-commutative-rings.md) + - [Maximal ideals in commutative rings](commutative-algebra.maximal-ideals-commutative-rings.md) + - [Nilradical of a commutative ring](commutative-algebra.nilradical-commutative-rings.md) + - [Powers of elements in commutative rings](commutative-algebra.powers-of-elements-commutative-rings.md) + - [Powers of elements in commutative semirings](commutative-algebra.powers-of-elements-commutative-semirings.md) + - [Prime ideals in commutative rings](commutative-algebra.prime-ideals-commutative-rings.md) + - [Sums in commutative rings](commutative-algebra.sums-commutative-rings.md) + - [Sums in commutative semirings](commutative-algebra.sums-commutative-semirings.md) + - [The binomial theorem in commutative rings](commutative-algebra.binomial-theorem-commutative-rings.md) + - [The binomial theorem in commutative semirings](commutative-algebra.binomial-theorem-commutative-semirings.md) + - [The Eisenstein integers](commutative-algebra.eisenstein-integers.md) + - [The Gaussian integers](commutative-algebra.gaussian-integers.md) + - [The Zariski topology on the set of prime ideals in a commutative ring](commutative-algebra.zariski-topology.md) + +- [Elementary Number Theory](elementary-number-theory.md) + - [Addition on the integers](elementary-number-theory.addition-integers.md) + - [Addition on the natural numbers](elementary-number-theory.addition-natural-numbers.md) + - [Addition on the rationals](elementary-number-theory.addition-rationals.md) + - [Arithmetic functions](elementary-number-theory.arithmetic-functions.md) + - [Bezout's lemma](elementary-number-theory.bezouts-lemma.md) + - [Bounded sums of arithmetic functions](elementary-number-theory.bounded-sums-arithmetic-functions.md) + - [Catalan numbers](elementary-number-theory.catalan-numbers.md) + - [Decidable dependent function types](elementary-number-theory.decidable-dependent-function-types.md) + - [Decidable types in elementary number theory](elementary-number-theory.decidable-types.md) + - [Dirichlet convolution](elementary-number-theory.dirichlet-convolution.md) + - [Divisibility in modular arithmetic](elementary-number-theory.divisibility-modular-arithmetic.md) + - [Divisibility of integers](elementary-number-theory.divisibility-integers.md) + - [Divisibility of natural numbers](elementary-number-theory.divisibility-natural-numbers.md) + - [Equality of integers](elementary-number-theory.equality-integers.md) + - [Equality of natural numbers](elementary-number-theory.equality-natural-numbers.md) + - [Euclidean division on the natural numbers](elementary-number-theory.euclidean-division-natural-numbers.md) + - [Euler's totient function](elementary-number-theory.eulers-totient-function.md) + - [Exponentiation of natural numbers](elementary-number-theory.exponentiation-natural-numbers.md) + - [Factorials of natural numbers](elementary-number-theory.factorials.md) + - [Falling factorials](elementary-number-theory.falling-factorials.md) + - [Finitely cyclic maps](elementary-number-theory.finitely-cyclic-maps.md) + - [Fractions](elementary-number-theory.fractions.md) + - [Inequality of integers](elementary-number-theory.inequality-integers.md) + - [Inequality of natural numbers](elementary-number-theory.inequality-natural-numbers.md) + - [Inequality on the standard finite types](elementary-number-theory.inequality-standard-finite-types.md) + - [Integer partitions](elementary-number-theory.integer-partitions.md) + - [Lower bounds of type families over the natural numbers](elementary-number-theory.lower-bounds-natural-numbers.md) + - [Maximum on the natural numbers](elementary-number-theory.maximum-natural-numbers.md) + - [Maximum on the standard finite types](elementary-number-theory.maximum-standard-finite-types.md) + - [Mersenne primes](elementary-number-theory.mersenne-primes.md) + - [Minimum on the natural numbers](elementary-number-theory.minimum-natural-numbers.md) + - [Minimum on the standard finite types](elementary-number-theory.minimum-standard-finite-types.md) + - [Modular arithmetic](elementary-number-theory.modular-arithmetic.md) + - [Modular arithmetic on the standard finite types](elementary-number-theory.modular-arithmetic-standard-finite-types.md) + - [Multiplication of integers](elementary-number-theory.multiplication-integers.md) + - [Multiplication of natural numbers](elementary-number-theory.multiplication-natural-numbers.md) + - [Multiset coefficients](elementary-number-theory.multiset-coefficients.md) + - [Nonzero natural numbers](elementary-number-theory.nonzero-natural-numbers.md) + - [Powers of integers](elementary-number-theory.powers-integers.md) + - [Prime numbers](elementary-number-theory.prime-numbers.md) + - [Products of natural numbers](elementary-number-theory.products-of-natural-numbers.md) + - [Proper divisors of natural numbers](elementary-number-theory.proper-divisors-natural-numbers.md) + - [Pythagorean triples](elementary-number-theory.pythagorean-triples.md) + - [Relatively prime integers](elementary-number-theory.relatively-prime-integers.md) + - [Relatively prime natural numbers](elementary-number-theory.relatively-prime-natural-numbers.md) + - [Repeating an element in a standard finite type](elementary-number-theory.repeating-element-standard-finite-type.md) + - [Retracts of the type of natural numbers](elementary-number-theory.retracts-of-natural-numbers.md) + - [Square-free natural numbers](elementary-number-theory.square-free-natural-numbers.md) + - [Stirling numbers of the second kind](elementary-number-theory.stirling-numbers-of-the-second-kind.md) + - [Sums of natural numbers](elementary-number-theory.sums-of-natural-numbers.md) + - [Telephone numbers](elementary-number-theory.telephone-numbers.md) + - [The absolute value function on the integers](elementary-number-theory.absolute-value-integers.md) + - [The binomial coefficients](elementary-number-theory.binomial-coefficients.md) + - [The binomial theorem for the integers](elementary-number-theory.binomial-theorem-integers.md) + - [The binomial theorem for the natural numbers](elementary-number-theory.binomial-theorem-natural-numbers.md) + - [The Collatz bijection](elementary-number-theory.collatz-bijection.md) + - [The Collatz conjecture](elementary-number-theory.collatz-conjecture.md) + - [The commutative ring of integers](elementary-number-theory.commutative-ring-of-integers.md) + - [The commutative semiring of natural numbers](elementary-number-theory.commutative-semiring-of-natural-numbers.md) + - [The congruence relations on the integers](elementary-number-theory.congruence-integers.md) + - [The congruence relations on the natural numbers](elementary-number-theory.congruence-natural-numbers.md) + - [The difference between integers](elementary-number-theory.difference-integers.md) + - [The distance between integers](elementary-number-theory.distance-integers.md) + - [The distance between natural numbers](elementary-number-theory.distance-natural-numbers.md) + - [The divisibility relation on the standard finite types](elementary-number-theory.divisibility-standard-finite-types.md) + - [The Fibonacci sequence](elementary-number-theory.fibonacci-sequence.md) + - [The Goldbach conjecture](elementary-number-theory.goldbach-conjecture.md) + - [The greatest common divisor of integers](elementary-number-theory.greatest-common-divisor-integers.md) + - [The greatest common divisor of natural numbers](elementary-number-theory.greatest-common-divisor-natural-numbers.md) + - [The group of integers](elementary-number-theory.group-of-integers.md) + - [The groups ℤ/kℤ](elementary-number-theory.groups-of-modular-arithmetic.md) + - [The half-integers](elementary-number-theory.half-integers.md) + - [The infinitude of primes](elementary-number-theory.infinitude-of-primes.md) + - [The integers](elementary-number-theory.integers.md) + - [The natural numbers base k](elementary-number-theory.finitary-natural-numbers.md) + - [The ordinal induction principle for the natural numbers](elementary-number-theory.ordinal-induction-natural-numbers.md) + - [The rational numbers](elementary-number-theory.rational-numbers.md) + - [The strong induction principle for the natural numbers](elementary-number-theory.strong-induction-natural-numbers.md) + - [The triangular numbers](elementary-number-theory.triangular-numbers.md) + - [The Twin Prime conjecture](elementary-number-theory.twin-prime-conjecture.md) + - [The type of natural numbers](elementary-number-theory.natural-numbers.md) + - [The universal property of the natural numbers](elementary-number-theory.universal-property-natural-numbers.md) + - [The Well-Ordering Principle of the natural numbers](elementary-number-theory.well-ordering-principle-natural-numbers.md) + - [The Well-Ordering Principle of the standard finite types](elementary-number-theory.well-ordering-principle-standard-finite-types.md) + - [Unit elements in the standard finite types](elementary-number-theory.unit-elements-standard-finite-types.md) + - [Unit similarity on the standard finite types](elementary-number-theory.unit-similarity-standard-finite-types.md) + - [Upper bounds for type families over the natural numbers](elementary-number-theory.upper-bounds-natural-numbers.md) + +- [Finite group theory](finite-group-theory.md) + - [Alternating concrete groups](finite-group-theory.alternating-concrete-groups.md) + - [Alternating groups](finite-group-theory.alternating-groups.md) + - [Cartier's delooping of the sign homomorphism](finite-group-theory.cartier-delooping-sign-homomorphism.md) + - [Deloopings of the sign homomorphism](finite-group-theory.delooping-sign-homomorphism.md) + - [Finite groups](finite-group-theory.finite-groups.md) + - [Finite monoids](finite-group-theory.finite-monoids.md) + - [Finite semigroups](finite-group-theory.finite-semigroups.md) + - [Groups of order 2](finite-group-theory.groups-of-order-2.md) + - [Orbits of permutations](finite-group-theory.orbits-permutations.md) + - [Permutations](finite-group-theory.permutations.md) + - [Simpson's delooping of the sign homomorphism](finite-group-theory.simpson-delooping-sign-homomorphism.md) + - [Subgroups of finite groups](finite-group-theory.subgroups-finite-groups.md) + - [Tetrahedra in 3-dimensional space](finite-group-theory.tetrahedra-in-3-space.md) + - [The abstract quaternion group of order 8](finite-group-theory.abstract-quaternion-group.md) + - [The concrete quaternion group](finite-group-theory.concrete-quaternion-group.md) + - [The group of n-element types](finite-group-theory.finite-type-groups.md) + - [The sign homomorphism](finite-group-theory.sign-homomorphism.md) + - [Transpositions](finite-group-theory.transpositions.md) + +- [Foundation](foundation.md) + - [0-Connected types](foundation.0-connected-types.md) + - [0-Images of maps](foundation.0-images-of-maps.md) + - [0-Maps](foundation.0-maps.md) + - [1-Types](foundation.1-types.md) + - [2-Types](foundation.2-types.md) + - [Algebras for polynomial endofunctors](foundation.algebras-polynomial-endofunctors.md) + - [Apartness relations](foundation.apartness-relations.md) + - [Automorphisms of types](foundation.automorphisms.md) + - [Axiom L](foundation.axiom-l.md) + - [Bands](foundation.bands.md) + - [Binary embeddings](foundation.binary-embeddings.md) + - [Binary equivalences](foundation.binary-equivalences.md) + - [Binary equivalences on unordered pairs of types](foundation.binary-equivalences-unordered-pairs-of-types.md) + - [Binary functoriality of set quotients](foundation.binary-functoriality-set-quotients.md) + - [Binary operations on unordered pairs of types](foundation.binary-operations-unordered-pairs-of-types.md) + - [Binary reflecting maps of equivalence relations](foundation.binary-reflecting-maps-equivalence-relations.md) + - [Binary relations](foundation.binary-relations.md) + - [Binary transport](foundation.binary-transport.md) + - [Boolean Reflection](foundation.boolean-reflection.md) + - [Cantor's diagonal argument](foundation.cantors-diagonal-argument.md) + - [Cartesian product types](foundation.cartesian-product-types.md) + - [Choice of representatives for an equivalence relation](foundation.choice-of-representatives-equivalence-relation.md) + - [Coherently invertible maps](foundation.coherently-invertible-maps.md) + - [Commuting 3-simplices of homotopies](foundation.commuting-3-simplices-of-homotopies.md) + - [Commuting 3-simplices of maps](foundation.commuting-3-simplices-of-maps.md) + - [Commuting cubes of maps](foundation.commuting-cubes-of-maps.md) + - [Commuting squares of identifications](foundation.commuting-squares-of-identifications.md) + - [Commuting squares of maps](foundation.commuting-squares-of-maps.md) + - [Commuting triangles of homotopies](foundation.commuting-triangles-of-homotopies.md) + - [Commuting triangles of maps](foundation.commuting-triangles-of-maps.md) + - [Complements of subtypes](foundation.complements-subtypes.md) + - [Complements of type families](foundation.complements.md) + - [Cones on pullback diagrams](foundation.cones-pullbacks.md) + - [Conjunction of propositions](foundation.conjunction.md) + - [Connected components of types](foundation.connected-components.md) + - [Connected components of universes](foundation.connected-components-universes.md) + - [Connected maps](foundation.connected-maps.md) + - [Connected types](foundation.connected-types.md) + - [Constant maps](foundation.constant-maps.md) + - [Contractible maps](foundation.contractible-maps.md) + - [Contractible types](foundation.contractible-types.md) + - [Coproduct types](foundation.coproduct-types.md) + - [Cospans](foundation.cospans.md) + - [Decidability of dependent function types](foundation.decidable-dependent-function-types.md) + - [Decidability of dependent pair types](foundation.decidable-dependent-pair-types.md) + - [Decidable embeddings](foundation.decidable-embeddings.md) + - [Decidable equality](foundation.decidable-equality.md) + - [Decidable equivalence relations](foundation.decidable-equivalence-relations.md) + - [Decidable maps](foundation.decidable-maps.md) + - [Decidable propositions](foundation.decidable-propositions.md) + - [Decidable relations on types](foundation.decidable-relations.md) + - [Decidable subtypes](foundation.decidable-subtypes.md) + - [Decidable types](foundation.decidable-types.md) + - [Dependent pair types](foundation.dependent-pair-types.md) + - [Dependent paths](foundation.dependent-paths.md) + - [Descent for coproduct types](foundation.descent-coproduct-types.md) + - [Descent for dependent pair types](foundation.descent-dependent-pair-types.md) + - [Descent for equivalences](foundation.descent-equivalences.md) + - [Descent for the empty type](foundation.descent-empty-types.md) + - [Diagonal maps of types](foundation.diagonal-maps-of-types.md) + - [Diagonals of maps](foundation.diagonals-of-maps.md) + - [Discrete reflexive relations](foundation.discrete-reflexive-relations.md) + - [Discrete types](foundation.discrete-types.md) + - [Disjunction of propositions](foundation.disjunction.md) + - [Double negation](foundation.double-negation.md) + - [Double powersets](foundation.double-powersets.md) + - [Dubuc-Penon compact types](foundation.dubuc-penon-compact-types.md) + - [Effective maps for equivalence relations](foundation.effective-maps-equivalence-relations.md) + - [Embeddings](foundation.embeddings.md) + - [Empty types](foundation.empty-types.md) + - [endomorphisms](foundation.endomorphisms.md) + - [Epimorphisms with respect to maps into sets](foundation.epimorphisms-with-respect-to-sets.md) + - [Equality in the fibers of a map](foundation.equality-fibers-of-maps.md) + - [Equality of cartesian product types](foundation.equality-cartesian-product-types.md) + - [Equality of coproduct types](foundation.equality-coproduct-types.md) + - [Equality of dependent pair types](foundation.equality-dependent-pair-types.md) + - [Equality on dependent function types](foundation.equality-dependent-function-types.md) + - [Equational reasoning](foundation.equational-reasoning.md) + - [Equivalence classes](foundation.equivalence-classes.md) + - [Equivalence extensionality](foundation.equivalence-extensionality.md) + - [Equivalence induction](foundation.equivalence-induction.md) + - [Equivalence relations](foundation.equivalence-relations.md) + - [Equivalences](foundation.equivalences.md) + - [Equivalences on Maybe](foundation.equivalences-maybe.md) + - [Exclusive disjunction of propositions](foundation.xor.md) + - [Existential quantification](foundation.existential-quantification.md) + - [Exponents of set quotients](foundation.exponents-set-quotients.md) + - [Faithful maps](foundation.faithful-maps.md) + - [Fiber inclusions](foundation.fiber-inclusions.md) + - [Fibered equivalences](foundation.fibered-equivalences.md) + - [Fibered involutions](foundation.fibered-involutions.md) + - [Fibers of maps](foundation.fibers-of-maps.md) + - [Full subtypes of types](foundation.full-subtypes.md) + - [Function extensionality](foundation.function-extensionality.md) + - [Functional correspondences](foundation.functional-correspondences.md) + - [Functions](foundation.functions.md) + - [Functoriality of `fib`](foundation.functoriality-fibers-of-maps.md) + - [Functoriality of cartesian product types](foundation.functoriality-cartesian-product-types.md) + - [Functoriality of coproduct types](foundation.functoriality-coproduct-types.md) + - [Functoriality of dependent function types](foundation.functoriality-dependent-function-types.md) + - [Functoriality of dependent pair types](foundation.functoriality-dependent-pair-types.md) + - [Functoriality of function types](foundation.functoriality-function-types.md) + - [Functoriality of propositional truncations](foundation.functoriality-propositional-truncation.md) + - [Functoriality of set quotients](foundation.functoriality-set-quotients.md) + - [Functoriality of set truncation](foundation.functoriality-set-truncation.md) + - [Functoriality of truncations](foundation.functoriality-truncation.md) + - [Global choice](foundation.global-choice.md) + - [Hexagons of identifications](foundation.hexagons-of-identifications.md) + - [Hilbert's ε-operators](foundation.hilberts-epsilon-operators.md) + - [Homotopies](foundation.homotopies.md) + - [Homotopies of binary operations](foundation.binary-homotopies.md) + - [Identity systems](foundation.identity-systems.md) + - [Identity types](foundation.identity-types.md) + - [Identity types of truncated types](foundation.identity-truncated-types.md) + - [Images of subtypes](foundation.images-subtypes.md) + - [Impredicative encodings of the logical operations](foundation.impredicative-encodings.md) + - [Impredicative universes](foundation.impredicative-universes.md) + - [Inhabited subtypes](foundation.inhabited-subtypes.md) + - [Inhabited types](foundation.inhabited-types.md) + - [Injective maps](foundation.injective-maps.md) + - [Intersection of subtypes](foundation.intersections-subtypes.md) + - [Involutions](foundation.involutions.md) + - [Isolated points](foundation.isolated-points.md) + - [Isomorphisms of sets](foundation.isomorphisms-of-sets.md) + - [Iterating automorphisms](foundation.iterating-automorphisms.md) + - [Iterating functions](foundation.iterating-functions.md) + - [Iterating involutions](foundation.iterating-involutions.md) + - [Lawvere's fixed point theorem](foundation.lawveres-fixed-point-theorem.md) + - [Locally small types](foundation.locally-small-types.md) + - [Logical equivalences](foundation.logical-equivalences.md) + - [Maps fibered over a map](foundation.fibered-maps.md) + - [Mere embeddings](foundation.mere-embeddings.md) + - [Mere equality](foundation.mere-equality.md) + - [Mere equivalences](foundation.mere-equivalences.md) + - [Monomorphisms](foundation.monomorphisms.md) + - [Morphisms in the coslice category of types](foundation.coslice.md) + - [Morphisms of cospans](foundation.morphisms-cospans.md) + - [Morphisms of the slice category of types](foundation.slice.md) + - [Multisubsets](foundation.multisubsets.md) + - [Multivariable correspondences](foundation.multivariable-correspondences.md) + - [Multivariable decidable relations](foundation.multivariable-decidable-relations.md) + - [Multivariable relations](foundation.multivariable-relations.md) + - [Negation](foundation.negation.md) + - [Non-contractible types](foundation.noncontractible-types.md) + - [Pairs of distinct elements](foundation.pairs-of-distinct-elements.md) + - [Partial elements](foundation.partial-elements.md) + - [Partitions](foundation.partitions.md) + - [Path algebra](foundation.path-algebra.md) + - [Path-split maps](foundation.path-split-maps.md) + - [Perfect Images](foundation.perfect-images.md) + - [Polynomial endofunctors](foundation.polynomial-endofunctors.md) + - [Powersets](foundation.powersets.md) + - [Preimages of subtypes](foundation.preimages-of-subtypes.md) + - [Products of tuples of types](foundation.products-of-tuples-of-types.md) + - [Products of unordered pairs of types](foundation.products-unordered-pairs-of-types.md) + - [Products of unordered tuples of types](foundation.products-unordered-tuples-of-types.md) + - [Projective types](foundation.projective-types.md) + - [Proper subsets](foundation.proper-subtypes.md) + - [Propositional extensionality](foundation.propositional-extensionality.md) + - [Propositional maps](foundation.propositional-maps.md) + - [Propositional resizing](foundation.propositional-resizing.md) + - [Propositional truncations](foundation.propositional-truncations.md) + - [Propositions](foundation.propositions.md) + - [Pullbacks](foundation.pullbacks.md) + - [Raising universe levels](foundation.raising-universe-levels.md) + - [Reflecting maps for equivalence relations](foundation.reflecting-maps-equivalence-relations.md) + - [Reflexive relations](foundation.reflexive-relations.md) + - [Repetitions in sequences](foundation.repetitions-sequences.md) + - [Repetitions of values of maps](foundation.repetitions.md) + - [Retractions](foundation.retractions.md) + - [Russell's paradox](foundation.russells-paradox.md) + - [Sections](foundation.sections.md) + - [Sequences](foundation.sequences.md) + - [Set presented types](foundation.set-presented-types.md) + - [Set quotients](foundation.set-quotients.md) + - [Set truncations](foundation.set-truncations.md) + - [Sets](foundation.sets.md) + - [Shifting sequences](foundation.shifting-sequences.md) + - [Singleton induction](foundation.singleton-induction.md) + - [Singleton subtypes](foundation.singleton-subtypes.md) + - [Small maps](foundation.small-maps.md) + - [Small types](foundation.small-types.md) + - [Small universes](foundation.small-universes.md) + - [Split surjective maps](foundation.split-surjective-maps.md) + - [Standard apartness relations](foundation.standard-apartness-relations.md) + - [Strongly extensional maps](foundation.strongly-extensional-maps.md) + - [Structure](foundation.structure.md) + - [Subterminal types](foundation.subterminal-types.md) + - [Subtypes](foundation.subtypes.md) + - [Subuniverse](foundation.subuniverses.md) + - [Surjective maps](foundation.surjective-maps.md) + - [Symmetric difference of subtypes](foundation.symmetric-difference.md) + - [Symmetric operations](foundation.symmetric-operations.md) + - [The axiom of choice](foundation.axiom-of-choice.md) + - [The booleans](foundation.booleans.md) + - [The Cantor-Schröder-Bernstein-Escardó theorem](foundation.cantor-schroder-bernstein-escardo.md) + - [The dependent binomial theorem for types (Distributivity of dependent function types over coproduct types)](foundation.dependent-binomial-theorem.md) + - [The fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md) + - [The image of a map](foundation.images.md) + - [The induction principle for propositional truncation](foundation.induction-principle-propositional-truncation.md) + - [The interchange law](foundation.interchange-law.md) + - [The law of excluded middle](foundation.law-of-excluded-middle.md) + - [The lesser limited principle of omniscience](foundation.lesser-limited-principle-of-omniscience.md) + - [The limited principle of omniscience (LPO)](foundation.limited-principle-of-omniscience.md) + - [The maybe modality](foundation.maybe.md) + - [The principle of omniscience](foundation.principle-of-omniscience.md) + - [The replacement axiom for type theory](foundation.replacement.md) + - [The structure identity principle](foundation.structure-identity-principle.md) + - [The subtype identity principle](foundation.subtype-identity-principle.md) + - [The symmetric identity types](foundation.symmetric-identity-types.md) + - [The type theoretic principle of choice](foundation.type-theoretic-principle-of-choice.md) + - [The uniqueness of set quotients](foundation.uniqueness-set-quotients.md) + - [The unit type](foundation.unit-type.md) + - [The univalence axiom](foundation.univalence.md) + - [The univalence axiom implies function extensionality](foundation.univalence-implies-function-extensionality.md) + - [The universal propert of cartesian product types](foundation.universal-property-cartesian-product-types.md) + - [The universal property of booleans](foundation.universal-property-booleans.md) + - [The universal property of coproduct types](foundation.universal-property-coproduct-types.md) + - [The universal property of dependent pair types](foundation.universal-property-dependent-pair-types.md) + - [The universal property of fiber products](foundation.universal-property-fiber-products.md) + - [The universal property of identity types](foundation.universal-property-identity-types.md) + - [The universal property of maybe](foundation.universal-property-maybe.md) + - [The universal property of propositional truncations](foundation.universal-property-propositional-truncation.md) + - [The universal property of propositional truncations with respect to sets](foundation.universal-property-propositional-truncation-into-sets.md) + - [The universal property of pullbacks](foundation.universal-property-pullbacks.md) + - [The universal property of set quotients](foundation.universal-property-set-quotients.md) + - [The universal property of set truncations](foundation.universal-property-set-truncation.md) + - [The universal property of the empty type](foundation.universal-property-empty-type.md) + - [The universal property of the image of a map](foundation.universal-property-image.md) + - [The universal property of the unit type](foundation.universal-property-unit-type.md) + - [The universal property of truncations](foundation.universal-property-truncation.md) + - [The weak limited principle of omniscience](foundation.weak-limited-principle-of-omniscience.md) + - [Tight apartness relations](foundation.tight-apartness-relations.md) + - [Transport](foundation.transport.md) + - [Truncated equality](foundation.truncated-equality.md) + - [Truncated maps](foundation.truncated-maps.md) + - [Truncated types](foundation.truncated-types.md) + - [Truncation images of maps](foundation.truncation-images-of-maps.md) + - [Truncation levels](foundation.truncation-levels.md) + - [Truncations](foundation.truncations.md) + - [Tuples of types](foundation.tuples-of-types.md) + - [Type arithmetic for cartesian product types](foundation.type-arithmetic-cartesian-product-types.md) + - [Type arithmetic for coproduct types](foundation.type-arithmetic-coproduct-types.md) + - [Type arithmetic for dependent pair types](foundation.type-arithmetic-dependent-pair-types.md) + - [Type arithmetic with dependent function types](foundation.type-arithmetic-dependent-function-types.md) + - [Type arithmetic with the booleans](foundation.type-arithmetic-booleans.md) + - [Type arithmetic with the empty type](foundation.type-arithmetic-empty-type.md) + - [Type arithmetic with the unit type](foundation.type-arithmetic-unit-type.md) + - [Type duality](foundation.type-duality.md) + - [Union of subtypes](foundation.unions-subtypes.md) + - [Unique existence](foundation.unique-existence.md) + - [Uniqueness of set truncations](foundation.uniqueness-set-truncations.md) + - [Uniqueness of the image of a map](foundation.uniqueness-image.md) + - [Uniqueness of the truncations](foundation.uniqueness-truncation.md) + - [Unital binary operations](foundation.unital-binary-operations.md) + - [Univalent type families](foundation.univalent-type-families.md) + - [Universe levels](foundation.universe-levels.md) + - [Unordered n-tuples of elements in a type](foundation.unordered-tuples.md) + - [Unordered pairs of elements in a type](foundation.unordered-pairs.md) + - [Unordered pairs of types](foundation.unordered-pairs-of-types.md) + - [Unordered tuples of types](foundation.unordered-tuples-of-types.md) + - [Weak function extensionality](foundation.weak-function-extensionality.md) + - [Weakly constant maps](foundation.weakly-constant-maps.md) + - [Σ-decompositions of types](foundation.sigma-decompositions.md) + +- [Foundation Core](foundation-core.md) + - [0-Maps](foundation-core.0-maps.md) + - [1-Types](foundation-core.1-types.md) + - [Automorphisms](foundation-core.automorphisms.md) + - [Cartesian product types](foundation-core.cartesian-product-types.md) + - [Coherently invertible maps](foundation-core.coherently-invertible-maps.md) + - [Commuting 3-simplices of homotopies](foundation-core.commuting-3-simplices-of-homotopies.md) + - [Commuting 3-simplices of maps](foundation-core.commuting-3-simplices-of-maps.md) + - [Commuting cubes of maps](foundation-core.commuting-cubes-of-maps.md) + - [Commuting squares of maps](foundation-core.commuting-squares-of-maps.md) + - [Commuting triangles of homotopies](foundation-core.commuting-triangles-of-homotopies.md) + - [Commuting triangles of maps](foundation-core.commuting-triangles-of-maps.md) + - [Cones on pullback diagrams](foundation-core.cones-pullbacks.md) + - [Constant maps](foundation-core.constant-maps.md) + - [Contractible maps](foundation-core.contractible-maps.md) + - [Contractible types](foundation-core.contractible-types.md) + - [Coproduct types](foundation-core.coproduct-types.md) + - [Cospans](foundation-core.cospans.md) + - [Decidable propositions](foundation-core.decidable-propositions.md) + - [Dependent pair types](foundation-core.dependent-pair-types.md) + - [Diagonal maps of types](foundation-core.diagonal-maps-of-types.md) + - [Discrete types](foundation-core.discrete-types.md) + - [Embeddings](foundation-core.embeddings.md) + - [Empty types](foundation-core.empty-types.md) + - [Endomorphisms](foundation-core.endomorphisms.md) + - [Equality in the fibers of a map](foundation-core.equality-fibers-of-maps.md) + - [Equality of cartesian product types](foundation-core.equality-cartesian-product-types.md) + - [Equality of dependent pair types](foundation-core.equality-dependent-pair-types.md) + - [Equivalence induction](foundation-core.equivalence-induction.md) + - [Equivalence relations](foundation-core.equivalence-relations.md) + - [Equivalences](foundation-core.equivalences.md) + - [Faithful maps](foundation-core.faithful-maps.md) + - [Fibers of maps](foundation-core.fibers-of-maps.md) + - [Function extensionality](foundation-core.function-extensionality.md) + - [Functions](foundation-core.functions.md) + - [Functoriality of dependent function types](foundation-core.functoriality-dependent-function-types.md) + - [Functoriality of dependent pair types](foundation-core.functoriality-dependent-pair-types.md) + - [Functoriality of function types](foundation-core.functoriality-function-types.md) + - [Homotopies](foundation-core.homotopies.md) + - [Identity systems](foundation-core.identity-systems.md) + - [Identity types](foundation-core.identity-types.md) + - [Injective maps](foundation-core.injective-maps.md) + - [Involutions](foundation-core.involutions.md) + - [Logical equivalences](foundation-core.logical-equivalences.md) + - [Morphisms of cospans](foundation-core.morphisms-cospans.md) + - [Negation](foundation-core.negation.md) + - [Path-split maps](foundation-core.path-split-maps.md) + - [Propositional maps](foundation-core.propositional-maps.md) + - [Propositions](foundation-core.propositions.md) + - [Pullbacks](foundation-core.pullbacks.md) + - [Retractions](foundation-core.retractions.md) + - [Sections](foundation-core.sections.md) + - [Sets](foundation-core.sets.md) + - [Singleton induction](foundation-core.singleton-induction.md) + - [Small types](foundation-core.small-types.md) + - [Subtypes](foundation-core.subtypes.md) + - [The functoriality of `fib`](foundation-core.functoriality-fibers-of-maps.md) + - [The fundamental theorem of identity types](foundation-core.fundamental-theorem-of-identity-types.md) + - [The subtype identity principle](foundation-core.subtype-identity-principle.md) + - [The univalence axiom](foundation-core.univalence.md) + - [The universal property of pullbacks](foundation-core.universal-property-pullbacks.md) + - [The universal property of truncations](foundation-core.universal-property-truncation.md) + - [Truncated maps](foundation-core.truncated-maps.md) + - [Truncated types](foundation-core.truncated-types.md) + - [Truncation levels](foundation-core.truncation-levels.md) + - [Type arithmetic for cartesian product types](foundation-core.type-arithmetic-cartesian-product-types.md) + - [Type arithmetic for dependent pair types](foundation-core.type-arithmetic-dependent-pair-types.md) + - [Universe levels](foundation-core.universe-levels.md) + +- [Graph theory](graph-theory.md) + - [Circuits in undirected graphs](graph-theory.circuits-undirected-graphs.md) + - [Closed walks in undirected graphs](graph-theory.closed-walks-undirected-graphs.md) + - [Complete bipartite graphs](graph-theory.complete-bipartite-graphs.md) + - [Complete multipartite graphs](graph-theory.complete-multipartite-graphs.md) + - [Complete undirected graphs](graph-theory.complete-undirected-graphs.md) + - [Connected graphs](graph-theory.connected-undirected-graphs.md) + - [Cycles in undirected graphs](graph-theory.cycles-undirected-graphs.md) + - [Directed graph structures on standard finite sets](graph-theory.directed-graph-structures-on-standard-finite-sets.md) + - [Edge-coloured undirected graphs](graph-theory.edge-coloured-undirected-graphs.md) + - [Embeddings of directed graphs](graph-theory.embeddings-directed-graphs.md) + - [Embeddings of undirected graphs](graph-theory.embeddings-undirected-graphs.md) + - [Enriched undirected graphs](graph-theory.enriched-undirected-graphs.md) + - [Equivalences of directed graphs](graph-theory.equivalences-directed-graphs.md) + - [Equivalences of enriched undirected graphs](graph-theory.equivalences-enriched-undirected-graphs.md) + - [Equivalences of undirected graphs](graph-theory.equivalences-undirected-graphs.md) + - [Eulerian circuits in undirected graphs](graph-theory.eulerian-circuits-undirected-graphs.md) + - [Faithful morphisms of undirected graphs](graph-theory.faithful-morphisms-undirected-graphs.md) + - [Finite graphs](graph-theory.finite-graphs.md) + - [Geometric realizations of undirected graphs](graph-theory.geometric-realizations-undirected-graphs.md) + - [Graphs](graph-theory.directed-graphs.md) + - [Hypergraphs](graph-theory.hypergraphs.md) + - [Incidence in undirected graphs](graph-theory.neighbors-undirected-graphs.md) + - [Matchings](graph-theory.matchings.md) + - [Mere equivalences of undirected graphs](graph-theory.mere-equivalences-undirected-graphs.md) + - [Morphisms of directed graphs](graph-theory.morphisms-directed-graphs.md) + - [Morphisms of undirected graphs](graph-theory.morphisms-undirected-graphs.md) + - [Orientations of undirected graphs](graph-theory.orientations-undirected-graphs.md) + - [Paths in undirected graphs](graph-theory.paths-undirected-graphs.md) + - [Polygons](graph-theory.polygons.md) + - [Reflecting maps of undirected graphs](graph-theory.reflecting-maps-undirected-graphs.md) + - [Reflexive graphs](graph-theory.reflexive-graphs.md) + - [Regular undirected graph](graph-theory.regular-undirected-graphs.md) + - [Simple undirected graphs](graph-theory.simple-undirected-graphs.md) + - [Stereoisomerism for enriched undirected graphs](graph-theory.stereoisomerism-enriched-undirected-graphs.md) + - [Totally faithful morphisms of undirected graphs](graph-theory.totally-faithful-morphisms-undirected-graphs.md) + - [Trails in directed graphs](graph-theory.trails-directed-graphs.md) + - [Trails in undirected graphs](graph-theory.trails-undirected-graphs.md) + - [Undirected graph structures on standard finite sets](graph-theory.undirected-graph-structures-on-standard-finite-sets.md) + - [Undirected graphs](graph-theory.undirected-graphs.md) + - [Vertex covers](graph-theory.vertex-covers.md) + - [Voltage graphs](graph-theory.voltage-graphs.md) + - [Walks in directed graphs](graph-theory.walks-directed-graphs.md) + - [Walks in undirected graphs](graph-theory.walks-undirected-graphs.md) + +- [Group theory](group-theory.md) + - [Abelian groups](group-theory.abelian-groups.md) + - [Abstract groups](group-theory.groups.md) + - [Automorphism groups](group-theory.automorphism-groups.md) + - [Cartesian products of abelian groups](group-theory.cartesian-products-abelian-groups.md) + - [Cartesian products of groups](group-theory.cartesian-products-groups.md) + - [Cartesian products of monoids](group-theory.cartesian-products-monoids.md) + - [Cartesian products of semigroups](group-theory.cartesian-products-semigroups.md) + - [Cayley's theorem](group-theory.cayleys-theorem.md) + - [Commutative monoids](group-theory.commutative-monoids.md) + - [Commutators of elements in groups](group-theory.commutators-groups.md) + - [Concrete automorphism groups on sets](group-theory.loop-groups-sets.md) + - [Concrete group actions](group-theory.concrete-group-actions.md) + - [Concrete groups](group-theory.concrete-groups.md) + - [Congruence relations on abelian groups](group-theory.congruence-relations-abelian-groups.md) + - [Congruence relations on groups](group-theory.congruence-relations-groups.md) + - [Congruence relations on monoids](group-theory.congruence-relations-monoids.md) + - [Congruence relations on semigroups](group-theory.congruence-relations-semigroups.md) + - [Conjugation in groups](group-theory.conjugation.md) + - [Contravariant pushforwards of concrete group actions](group-theory.contravariant-pushforward-concrete-group-actions.md) + - [Decidable subgroups of groups](group-theory.decidable-subgroups.md) + - [Embeddings of abelian groups](group-theory.embeddings-abelian-groups.md) + - [Embeddings of groups](group-theory.embeddings-groups.md) + - [Epimorphisms in groups](group-theory.epimorphisms-groups.md) + - [Equivalences between semigroups](group-theory.equivalences-semigroups.md) + - [Equivalences of concrete group actions](group-theory.equivalences-concrete-group-actions.md) + - [Equivalences of concrete groups](group-theory.equivalences-concrete-groups.md) + - [Equivalences of group actions](group-theory.equivalences-group-actions.md) + - [Equivalences of higher groups](group-theory.equivalences-higher-groups.md) + - [Fixed points of higher group actions](group-theory.fixed-points-higher-group-actions.md) + - [Free concrete group actions](group-theory.free-concrete-group-actions.md) + - [Free groups with one generator](group-theory.free-groups-with-one-generator.md) + - [Free higher group actions](group-theory.free-higher-group-actions.md) + - [Furstenberg groups](group-theory.furstenberg-groups.md) + - [Group actions](group-theory.group-actions.md) + - [Group solver](group-theory.group-solver.md) + - [Higher group actions](group-theory.higher-group-actions.md) + - [Higher groups](group-theory.higher-groups.md) + - [Homomorphisms of abelian groups](group-theory.homomorphisms-abelian-groups.md) + - [Homomorphisms of concrete groups](group-theory.homomorphisms-concrete-groups.md) + - [Homomorphisms of generated subgroups](group-theory.homomorphisms-generated-subgroups.md) + - [Homomorphisms of group actions](group-theory.homomorphisms-group-actions.md) + - [Homomorphisms of groups](group-theory.homomorphisms-groups.md) + - [Homomorphisms of higher group actions](group-theory.homomorphisms-higher-group-actions.md) + - [Homomorphisms of higher groups](group-theory.homomorphisms-higher-groups.md) + - [Homomorphisms of monoids](group-theory.homomorphisms-monoids.md) + - [Homomorphisms of semigroups](group-theory.homomorphisms-semigroups.md) + - [Inverse semigroups](group-theory.inverse-semigroups.md) + - [Invertible elements in monoids](group-theory.invertible-elements-monoids.md) + - [Isomorphisms of abelian groups](group-theory.isomorphisms-abelian-groups.md) + - [Isomorphisms of concrete groups](group-theory.isomorphisms-concrete-groups.md) + - [Isomorphisms of group actions](group-theory.isomorphisms-group-actions.md) + - [Isomorphisms of groups](group-theory.isomorphisms-groups.md) + - [Isomorphisms of semigroups](group-theory.isomorphisms-semigroups.md) + - [Kernels](group-theory.kernels.md) + - [Kernels of homomorphisms of concrete groups](group-theory.kernels-homomorphisms-concrete-groups.md) + - [Mere equivalences of concrete group actions](group-theory.mere-equivalences-concrete-group-actions.md) + - [Mere equivalences of group actions](group-theory.mere-equivalences-group-actions.md) + - [Monoid actions](group-theory.monoid-actions.md) + - [Monoids](group-theory.monoids.md) + - [Monomorphisms in groups](group-theory.monomorphisms-groups.md) + - [Monomorphisms of concrete groups](group-theory.monomorphisms-concrete-groups.md) + - [Morphisms of concrete group actions](group-theory.homomorphisms-concrete-group-actions.md) + - [Normal subgroups](group-theory.normal-subgroups.md) + - [Normal subgroups of concrete groups](group-theory.normal-subgroups-concrete-groups.md) + - [Orbits of concrete group actions](group-theory.orbits-concrete-group-actions.md) + - [Orbits of group actions](group-theory.orbits-group-actions.md) + - [Orbits of higher group actions](group-theory.orbits-higher-group-actions.md) + - [Pointwise addition of morphisms of abelian groups](group-theory.addition-homomorphisms-abelian-groups.md) + - [Principal group actions](group-theory.principal-group-actions.md) + - [Principal torsors of concrete groups](group-theory.principal-torsors-concrete-groups.md) + - [Products of tuples of elements in commutative monoids](group-theory.products-of-tuples-of-elements-commutative-monoids.md) + - [Quotient groups](group-theory.quotient-groups.md) + - [Quotient groups of concrete groups](group-theory.quotient-groups-concrete-groups.md) + - [Quotients of abelian groups](group-theory.quotients-abelian-groups.md) + - [Representations of monoids](group-theory.representations-monoids.md) + - [Semigroups](group-theory.semigroups.md) + - [Sheargroups](group-theory.sheargroups.md) + - [Shriek of concrete group homomorphisms](group-theory.shriek-concrete-group-actions.md) + - [Stabilizer groups](group-theory.stabilizer-groups.md) + - [Stabilizers of concrete group actions](group-theory.stabilizer-groups-concrete-group-actions.md) + - [Subgroups](group-theory.subgroups.md) + - [Subgroups generated by subsets of groups](group-theory.subgroups-generated-by-subsets-groups.md) + - [Subgroups of abelian groups](group-theory.subgroups-abelian-groups.md) + - [Subgroups of concrete groups](group-theory.subgroups-concrete-groups.md) + - [Subgroups of higher groups](group-theory.subgroups-higher-groups.md) + - [Submonoids](group-theory.submonoids.md) + - [Subsemigroups](group-theory.subsemigroups.md) + - [Symmetric concrete groups](group-theory.symmetric-concrete-groups.md) + - [Symmetric groups](group-theory.symmetric-groups.md) + - [Symmetric higher groups](group-theory.symmetric-higher-groups.md) + - [The category of concrete groups](group-theory.category-of-concrete-groups.md) + - [The category of groups](group-theory.category-of-groups.md) + - [The category of semigroups](group-theory.category-of-semigroups.md) + - [The center of a group](group-theory.centers-groups.md) + - [The dihedral group construction](group-theory.dihedral-group-construction.md) + - [The dihedral groups](group-theory.dihedral-groups.md) + - [The endomorphism rings of abelian groups](group-theory.endomorphism-rings-abelian-groups.md) + - [The E₈-lattice](group-theory.e8-lattice.md) + - [The full subgroup of a group](group-theory.full-subgroups.md) + - [The higher group of integers](group-theory.integers-higher-group.md) + - [The opposite of a group](group-theory.opposite-groups.md) + - [The orbit-stabilizer theorem for concrete groups](group-theory.orbit-stabilizer-theorem-concrete-groups.md) + - [The order of an element in a group](group-theory.orders-of-elements-groups.md) + - [The precategory of concrete groups](group-theory.precategory-of-concrete-groups.md) + - [The precategory of group actions](group-theory.precategory-of-group-actions.md) + - [The precategory of groups](group-theory.precategory-of-groups.md) + - [The precategory of orbits of a monoid action](group-theory.orbits-monoid-actions.md) + - [The precategory of semigroups](group-theory.precategory-of-semigroups.md) + - [The substitution functor of concrete group actions](group-theory.substitution-functor-concrete-group-actions.md) + - [The substitution functor of group actions](group-theory.substitution-functor-group-actions.md) + - [Torsors of abstract groups](group-theory.torsors.md) + - [Transitive concrete group actions](group-theory.transitive-concrete-group-actions.md) + - [Transitive group actions](group-theory.transitive-group-actions.md) + - [Trivial subgroups](group-theory.trivial-subgroups.md) + - [Unordered tuples of elements in commutative monoids](group-theory.unordered-tuples-of-elements-commutative-monoids.md) + +- [Linear algebra](linear-algebra.md) + - [Constant matrices](linear-algebra.constant-matrices.md) + - [Diagonal matrices on rings](linear-algebra.diagonal-matrices-on-rings.md) + - [Diagonal vectors](linear-algebra.constant-vectors.md) + - [Functoriality of matrices](linear-algebra.functoriality-matrices.md) + - [Functoriality of the type of vectors](linear-algebra.functoriality-vectors.md) + - [Matrices](linear-algebra.matrices.md) + - [Matrices on rings](linear-algebra.matrices-on-rings.md) + - [Multiplication of matrices](linear-algebra.multiplication-matrices.md) + - [Scalar multiplication of vectors](linear-algebra.scalar-multiplication-vectors.md) + - [Scalar multiplication of vectors on rings](linear-algebra.scalar-multiplication-vectors-on-rings.md) + - [Scalar multiplication on matrices](linear-algebra.scalar-multiplication-matrices.md) + - [Transposition of matrices](linear-algebra.transposition-matrices.md) + - [Vectors](linear-algebra.vectors.md) + - [Vectors on commutative rings](linear-algebra.vectors-on-commutative-rings.md) + - [Vectors on commutative semirings](linear-algebra.vectors-on-commutative-semirings.md) + - [Vectors on rings](linear-algebra.vectors-on-rings.md) + - [Vectors on semirings](linear-algebra.vectors-on-semirings.md) + +- [Order theory](order-theory.md) + - [Chains in posets](order-theory.chains-posets.md) + - [Chains in preorders](order-theory.chains-preorders.md) + - [Decidable subposets](order-theory.decidable-subposets.md) + - [Decidable subpreorders](order-theory.decidable-subpreorders.md) + - [Directed complete posets](order-theory.directed-complete-posets.md) + - [Directed families in posets](order-theory.directed-families.md) + - [Distributive Lattices](order-theory.distributive-lattices.md) + - [Finite posets](order-theory.finite-posets.md) + - [Finite preorders](order-theory.finite-preorders.md) + - [Finitely graded posets](order-theory.finitely-graded-posets.md) + - [Frames](order-theory.frames.md) + - [Greatest lower bounds in posets](order-theory.greatest-lower-bounds-posets.md) + - [Homomorphisms Frames](order-theory.homomorphisms-frames.md) + - [Homomorphisms Meet Semilattices](order-theory.homomorphisms-meet-semilattices.md) + - [Homomorphisms Meet Sup Lattice](order-theory.homomorphisms-meet-sup-lattices.md) + - [Homomorphisms Sup Lattices](order-theory.homomorphisms-sup-lattices.md) + - [Ideals in preorders](order-theory.ideals-preorders.md) + - [Infinite distributive law](order-theory.infinite-distributive-law.md) + - [Interval subposets](order-theory.interval-subposets.md) + - [Join-semilattices](order-theory.join-semilattices.md) + - [Large Posets](order-theory.large-posets.md) + - [Large preorders](order-theory.large-preorders.md) + - [Largest elements in posets](order-theory.largest-elements-posets.md) + - [Largest elements in preorders](order-theory.largest-elements-preorders.md) + - [Lattices](order-theory.lattices.md) + - [Least elements in posets](order-theory.least-elements-posets.md) + - [Least elements in preorders](order-theory.least-elements-preorders.md) + - [Least upper bounds in posets](order-theory.least-upper-bounds-posets.md) + - [Locally finite posets](order-theory.locally-finite-posets.md) + - [Lower types in preorders](order-theory.lower-types-preorders.md) + - [Maximal chains in posets](order-theory.maximal-chains-posets.md) + - [Maximal chains in preorders](order-theory.maximal-chains-preorders.md) + - [Meet-semilattices](order-theory.meet-semilattices.md) + - [Order preserving maps on posets](order-theory.order-preserving-maps-posets.md) + - [Order preserving maps on preorders](order-theory.order-preserving-maps-preorders.md) + - [Planar binary trees](order-theory.planar-binary-trees.md) + - [Posets](order-theory.posets.md) + - [Preorders](order-theory.preorders.md) + - [Subposets](order-theory.subposets.md) + - [Subpreorders](order-theory.subpreorders.md) + - [Sup Lattices](order-theory.sup-lattices.md) + - [Total preorders](order-theory.total-preorders.md) + - [Totally ordered posets](order-theory.total-posets.md) + +- [Organic Chemistry](organic-chemistry.md) + - [Alcohols](organic-chemistry.alcohols.md) + - [Alkanes](organic-chemistry.alkanes.md) + - [Alkenes](organic-chemistry.alkenes.md) + - [Alkynes](organic-chemistry.alkynes.md) + - [Ethane](organic-chemistry.ethane.md) + - [Hydrocarbons](organic-chemistry.hydrocarbons.md) + - [Methane](organic-chemistry.methane.md) + - [Saturated carbons](organic-chemistry.saturated-carbons.md) + +- [Orthogonal factorization systems](orthogonal-factorization-systems.md) + - [Extensions of maps](orthogonal-factorization-systems.extensions-of-maps.md) + - [Factorization operations](orthogonal-factorization-systems.factorization-operations.md) + - [Factorizations of maps](orthogonal-factorization-systems.factorizations-of-maps.md) + - [Function classes](orthogonal-factorization-systems.function-classes.md) + - [Higher modalities](orthogonal-factorization-systems.higher-modalities.md) + - [Lifting operations](orthogonal-factorization-systems.lifting-operations.md) + - [Lifting squares](orthogonal-factorization-systems.lifting-squares.md) + - [Lifts of maps](orthogonal-factorization-systems.lifts-of-maps.md) + - [Local types](orthogonal-factorization-systems.local-types.md) + - [Mere lifting properties](orthogonal-factorization-systems.mere-lifting-properties.md) + - [Modal operators](orthogonal-factorization-systems.modal-operators.md) + - [Orthogonal factorization systems](orthogonal-factorization-systems.orthogonal-factorization-systems.md) + - [Orthogonal maps](orthogonal-factorization-systems.orthogonal-maps.md) + - [Pullback-hom](orthogonal-factorization-systems.pullback-hom.md) + - [Reflective subuniverses](orthogonal-factorization-systems.reflective-subuniverses.md) + - [Uniquely eliminating modalities](orthogonal-factorization-systems.uniquely-eliminating-modalities.md) + - [Wide function classes](orthogonal-factorization-systems.wide-function-classes.md) + +- [Polytopes](polytopes.md) + - [Abstract polytopes](polytopes.abstract-polytopes.md) + +- [Ring theory](ring-theory.md) + - [Algebras over rings](ring-theory.algebras-rings.md) + - [Congruence relations on rings](ring-theory.congruence-relations-rings.md) + - [Congruence relations on semirings](ring-theory.congruence-relations-semirings.md) + - [Dependent products of rings](ring-theory.dependent-products-rings.md) + - [Division rings](ring-theory.division-rings.md) + - [Ideals generated by subsets of rings](ring-theory.ideals-generated-by-subsets-rings.md) + - [Ideals in rings](ring-theory.ideals-rings.md) + - [Idempotent elements in rings](ring-theory.idempotent-elements-rings.md) + - [Invertible elements in rings](ring-theory.invertible-elements-rings.md) + - [Isomorphisms of rings](ring-theory.isomorphisms-rings.md) + - [Local rings](ring-theory.local-rings.md) + - [Localizations of rings](ring-theory.localizations-rings.md) + - [Maximal ideals in rings](ring-theory.maximal-ideals-rings.md) + - [Modules over rings](ring-theory.modules-rings.md) + - [Nil ideals](ring-theory.nil-ideals-rings.md) + - [Nilpotent elements in rings](ring-theory.nilpotent-elements-rings.md) + - [Nontrivial rings](ring-theory.nontrivial-rings.md) + - [Opposite rings](ring-theory.opposite-rings.md) + - [Powers of elements in rings](ring-theory.powers-of-elements-rings.md) + - [Powers of elements in semirings](ring-theory.powers-of-elements-semirings.md) + - [Products of rings](ring-theory.products-rings.md) + - [Qutoient Rings](ring-theory.quotient-rings.md) + - [Radical ideals in rings](ring-theory.radical-ideals-rings.md) + - [Ring homomorphisms](ring-theory.homomorphisms-rings.md) + - [Rings](ring-theory.rings.md) + - [Semirings](ring-theory.semirings.md) + - [Subsets of rings](ring-theory.subsets-rings.md) + - [Sums of elements in rings](ring-theory.sums-rings.md) + - [Sums of elements in semirings](ring-theory.sums-semirings.md) + - [The binomial theorem for rings](ring-theory.binomial-theorem-rings.md) + - [The binomial theorem for semirings](ring-theory.binomial-theorem-semirings.md) + - [The invariant basis property of rings](ring-theory.invariant-basis-property-rings.md) + +- [Set theory](set-theory.md) + - [Baire space](set-theory.baire-space.md) + - [Cantor space](set-theory.cantor-space.md) + - [Cardinalities of sets](set-theory.cardinalities.md) + - [Countable sets](set-theory.countable-sets.md) + - [Cumulative hierarchy](set-theory.cumulative-hierarchy.md) + - [Infinite sets](set-theory.infinite-sets.md) + - [Uncountable sets](set-theory.uncountable-sets.md) + +- [Structured types](structured-types.md) + - [Central H-spaces](structured-types.central-h-spaces.md) + - [Coherent H-spaces](structured-types.coherent-h-spaces.md) + - [Constant maps of pointed types](structured-types.constant-maps-pointed-types.md) + - [Contractible pointed types](structured-types.contractible-pointed-types.md) + - [Equivalences of types equipped with endomorphisms](structured-types.equivalences-types-equipped-with-endomorphisms.md) + - [Faithful pointed maps](structured-types.faithful-pointed-maps.md) + - [Fibers of pointed maps](structured-types.fibers-of-pointed-maps.md) + - [Finite multiplication in magmas](structured-types.finite-multiplication-magmas.md) + - [H-spaces](structured-types.h-spaces.md) + - [Involutive types](structured-types.involutive-types.md) + - [Magmas](structured-types.magmas.md) + - [Mere equivalences of types equipped with endomorphisms](structured-types.mere-equivalences-types-equipped-with-endomorphisms.md) + - [Morphisms of coherent H-spaces](structured-types.morphisms-coherent-h-spaces.md) + - [Morphisms of magmas](structured-types.morphisms-magmas.md) + - [Morphisms of types equipped with endomorphisms](structured-types.morphisms-types-equipped-with-endomorphisms.md) + - [Pointed dependent functions](structured-types.pointed-dependent-functions.md) + - [Pointed equivalences](structured-types.pointed-equivalences.md) + - [Pointed families of types](structured-types.pointed-families-of-types.md) + - [Pointed homotopies](structured-types.pointed-homotopies.md) + - [Pointed maps](structured-types.pointed-maps.md) + - [Pointed sections of pointed maps](structured-types.pointed-sections.md) + - [Pointed types](structured-types.pointed-types.md) + - [Pointed types equipped with automorphisms](structured-types.pointed-types-equipped-with-automorphisms.md) + - [Symmetric elements of involutive types](structured-types.symmetric-elements-involutive-types.md) + - [Symmetric H-spaces](structured-types.symmetric-h-spaces.md) + - [The initial pointed type equipped with an automorphism](structured-types.initial-pointed-type-equipped-with-automorphism.md) + - [The involutive type of H-Space structures on a pointed type](structured-types.involutive-type-of-h-space-structures.md) + - [The universal property of lists with respect to wild monoids](structured-types.universal-property-lists-wild-monoids.md) + - [Types equipped with automorphisms](structured-types.types-equipped-with-automorphisms.md) + - [Types equipped with endomorphisms](structured-types.types-equipped-with-endomorphisms.md) + - [Unpointed maps between pointed types](structured-types.unpointed-maps.md) + - [Wild groups](structured-types.wild-groups.md) + - [Wild loops](structured-types.wild-loops.md) + - [Wild monoids](structured-types.wild-monoids.md) + - [Wild quasigroups](structured-types.wild-quasigroups.md) + - [Wild semigroups](structured-types.wild-semigroups.md) + +- [Synthetic homotopy theory](synthetic-homotopy-theory.md) + - [Cocones for pushouts](synthetic-homotopy-theory.cocones-pushouts.md) + - [Cofibers](synthetic-homotopy-theory.cofibers.md) + - [Double loop spaces](synthetic-homotopy-theory.double-loop-spaces.md) + - [Formalisation of the Symmetry Book - 24 pushouts](synthetic-homotopy-theory.24-pushouts.md) + - [Formalisation of the Symmetry Book - 26 descent](synthetic-homotopy-theory.26-descent.md) + - [Formalisation of the Symmetry Book - 26 id pushout](synthetic-homotopy-theory.26-id-pushout.md) + - [Formalisation of the Symmetry Book - 27 sequences](synthetic-homotopy-theory.27-sequences.md) + - [Free loops](synthetic-homotopy-theory.free-loops.md) + - [Functoriality of the loop space operation](synthetic-homotopy-theory.functoriality-loop-spaces.md) + - [Groups of loops in 1-types](synthetic-homotopy-theory.groups-of-loops-in-1-types.md) + - [Infinite cyclic types](synthetic-homotopy-theory.infinite-cyclic-types.md) + - [Iterated loop spaces](synthetic-homotopy-theory.iterated-loop-spaces.md) + - [Joins of types](synthetic-homotopy-theory.joins-of-types.md) + - [Loop spaces](synthetic-homotopy-theory.loop-spaces.md) + - [Prespectra](synthetic-homotopy-theory.prespectra.md) + - [Pushouts](synthetic-homotopy-theory.pushouts.md) + - [Spectra](synthetic-homotopy-theory.spectra.md) + - [Spheres](synthetic-homotopy-theory.spheres.md) + - [Suspensions of types](synthetic-homotopy-theory.suspensions-of-types.md) + - [The circle](synthetic-homotopy-theory.circle.md) + - [The descent property of the circle](synthetic-homotopy-theory.descent-circle.md) + - [The infinite complex projective space](synthetic-homotopy-theory.infinite-complex-projective-space.md) + - [The interval](synthetic-homotopy-theory.interval-type.md) + - [The multiplication operation on the circle](synthetic-homotopy-theory.multiplication-circle.md) + - [The universal cover of the circle](synthetic-homotopy-theory.universal-cover-circle.md) + - [The universal property of pushouts](synthetic-homotopy-theory.universal-property-pushouts.md) + - [The universal property of the circle](synthetic-homotopy-theory.universal-property-circle.md) + - [Triple loop spaces](synthetic-homotopy-theory.triple-loop-spaces.md) + - [Wedges of types](synthetic-homotopy-theory.wedges-of-pointed-types.md) + +- [Trees](trees.md) + - [Directed trees](trees.directed-trees.md) + - [Enriched directed trees](trees.enriched-directed-trees.md) + - [Equivalences of directed trees](trees.equivalences-directed-trees.md) + - [Equivalences of enriched directed trees](trees.equivalences-enriched-directed-trees.md) + - [Extensional W-types](trees.extensional-w-types.md) + - [Functoriality of W-types](trees.functoriality-w-types.md) + - [Indexed W-types](trees.indexed-w-types.md) + - [Induction principles on W-types](trees.induction-w-types.md) + - [Inequality on W-types](trees.inequality-w-types.md) + - [Lower types of elements in W-types](trees.lower-types-w-types.md) + - [Multisets](trees.multisets.md) + - [Ranks of elements in W-types](trees.ranks-of-elements-w-types.md) + - [Rooted quasitrees](trees.rooted-quasitrees.md) + - [Rooted undirected trees](trees.rooted-undirected-trees.md) + - [Small multisets](trees.small-multisets.md) + - [Submultisets](trees.submultisets.md) + - [The elementhood relation on W-types](trees.elementhood-relation-w-types.md) + - [The underlying graphs of elements of W-types](trees.underlying-graphs-of-elements-w-types.md) + - [The universal multiset](trees.universal-multiset.md) + - [The W-type of natural numbers](trees.w-type-of-natural-numbers.md) + - [The W-type of the type of propositions](trees.w-type-of-propositions.md) + - [Transitive multisets](trees.transitive-multisets.md) + - [Undirected rees](trees.undirected-trees.md) + - [W-types](trees.w-types.md) + +- [Type theories](type-theories.md) + - [Comprehension of fibered type theories](type-theories.comprehension-type-theories.md) + - [Dependent type theories](type-theories.dependent-type-theories.md) + - [Fibered dependent type theories](type-theories.fibered-dependent-type-theories.md) + - [Sections of dependent type theories](type-theories.sections-dependent-type-theories.md) + - [Simple type theories](type-theories.simple-type-theories.md) + - [Unityped type theories](type-theories.unityped-type-theories.md) + +- [Univalent Combinatorics](univalent-combinatorics.md) + - [2-element decidable subtypes](univalent-combinatorics.2-element-decidable-subtypes.md) + - [2-element subtypes](univalent-combinatorics.2-element-subtypes.md) + - [2-element types](univalent-combinatorics.2-element-types.md) + - [An involution on the standard finite types](univalent-combinatorics.involution-standard-finite-types.md) + - [Bracelets](univalent-combinatorics.bracelets.md) + - [Cartesian products of finite types](univalent-combinatorics.cartesian-product-types.md) + - [Cartesian products of species](univalent-combinatorics.cartesian-products-species.md) + - [Combinatorial identities of sums of natural numbers](univalent-combinatorics.sums-of-natural-numbers.md) + - [Complements of isolated points of finite types](univalent-combinatorics.complements-isolated-points.md) + - [Composition of species](univalent-combinatorics.composition-species.md) + - [Coproducts of finite types](univalent-combinatorics.coproduct-types.md) + - [Coproducts of species](univalent-combinatorics.coproducts-species.md) + - [Counting in type theory](univalent-combinatorics.counting.md) + - [Counting the elements in Maybe](univalent-combinatorics.counting-maybe.md) + - [Counting the elements of decidable subtypes](univalent-combinatorics.counting-decidable-subtypes.md) + - [Counting the elements of dependent function types](univalent-combinatorics.dependent-function-types.md) + - [Counting the elements of dependent pair types](univalent-combinatorics.counting-dependent-pair-types.md) + - [Counting the elements of the fiber of a map](univalent-combinatorics.counting-fibers-of-maps.md) + - [Cubes](univalent-combinatorics.cubes.md) + - [Cycle index series of species](univalent-combinatorics.cycle-index-series-species.md) + - [Cycle partitions of finite types](univalent-combinatorics.cycle-partitions.md) + - [Cyclic types](univalent-combinatorics.cyclic-types.md) + - [Decidability of dependent pair types](univalent-combinatorics.decidable-dependent-pair-types.md) + - [Decidable dependent function types](univalent-combinatorics.decidable-dependent-function-types.md) + - [Decidable equivalence relations on finite types](univalent-combinatorics.decidable-equivalence-relations.md) + - [Decidable propositions](univalent-combinatorics.decidable-propositions.md) + - [Decidable subtypes of finite types](univalent-combinatorics.decidable-subtypes.md) + - [Dedekind finite sets](univalent-combinatorics.dedekind-finite-sets.md) + - [Dependent sums of finite types](univalent-combinatorics.dependent-sum-finite-types.md) + - [Derivatives of species](univalent-combinatorics.derivatives-species.md) + - [Distributivity of set truncation over finite products](univalent-combinatorics.distributivity-of-set-truncation-over-finite-products.md) + - [Double counting](univalent-combinatorics.double-counting.md) + - [Embeddings between standard finite types](univalent-combinatorics.embeddings-standard-finite-types.md) + - [Equality in finite types](univalent-combinatorics.equality-finite-types.md) + - [Equality in the standard finite types](univalent-combinatorics.equality-standard-finite-types.md) + - [Equivalences between finite types](univalent-combinatorics.equivalences.md) + - [Equivalences between standard finite types](univalent-combinatorics.equivalences-standard-finite-types.md) + - [Equivalences of cubes](univalent-combinatorics.equivalences-cubes.md) + - [Equivalences of species](univalent-combinatorics.equivalences-species.md) + - [Exponents of species](univalent-combinatorics.exponents-species.md) + - [Ferrers diagrams (unlabeled partitions)](univalent-combinatorics.ferrers-diagrams.md) + - [Fibers of maps between finite types](univalent-combinatorics.fibers-of-maps.md) + - [Finite choice](univalent-combinatorics.finite-choice.md) + - [Finite function types](univalent-combinatorics.function-types.md) + - [Finite presentations of types](univalent-combinatorics.finite-presentations.md) + - [Finite species](univalent-combinatorics.finite-species.md) + - [Finite types](univalent-combinatorics.finite-types.md) + - [Finite Σ-decompositions of finite types](univalent-combinatorics.sigma-decompositions.md) + - [Finitely presented types](univalent-combinatorics.finitely-presented-types.md) + - [Finitely π-presented types](univalent-combinatorics.presented-pi-finite-types.md) + - [Finiteness of the type of connected components](univalent-combinatorics.finite-connected-components.md) + - [Inequality on types equipped with a counting](univalent-combinatorics.inequality-types-with-counting.md) + - [Inhabited finite types](univalent-combinatorics.inhabited-finite-types.md) + - [Injective maps](univalent-combinatorics.embeddings.md) + - [Injective maps between finite types](univalent-combinatorics.injective-maps.md) + - [Isotopies of Latin squares](univalent-combinatorics.isotopies-latin-squares.md) + - [Kuratowsky finite sets](univalent-combinatorics.kuratowsky-finite-sets.md) + - [Latin squares](univalent-combinatorics.latin-squares.md) + - [Lists](univalent-combinatorics.lists.md) + - [Morphisms of finite species](univalent-combinatorics.morphisms-finite-species.md) + - [Morphisms of species](univalent-combinatorics.morphisms-species.md) + - [Necklaces](univalent-combinatorics.necklaces.md) + - [Orientations of cubes](univalent-combinatorics.orientations-cubes.md) + - [Orientations of the complete undirected graph](univalent-combinatorics.orientations-complete-undirected-graph.md) + - [Partitions of finite types](univalent-combinatorics.partitions.md) + - [Petri-nets](univalent-combinatorics.petri-nets.md) + - [Pointing of species](univalent-combinatorics.pointing-species.md) + - [Quotients of finite types](univalent-combinatorics.quotients-finite-types.md) + - [Ramsey theory](univalent-combinatorics.ramsey-theory.md) + - [Retracts of finite types](univalent-combinatorics.retracts-of-finite-types.md) + - [Sequences of elements in finite types](univalent-combinatorics.sequences-finite-types.md) + - [Set quotients of index 2](univalent-combinatorics.set-quotients-of-index-two.md) + - [Skipping elements in standard finite types](univalent-combinatorics.skipping-element-standard-finite-types.md) + - [Species](univalent-combinatorics.species.md) + - [Standard finite pruned trees](univalent-combinatorics.standard-finite-pruned-trees.md) + - [Standard finite trees](univalent-combinatorics.standard-finite-trees.md) + - [Steiner systems](univalent-combinatorics.steiner-systems.md) + - [Steiner triple systems](univalent-combinatorics.steiner-triple-systems.md) + - [Surjective maps between finite types](univalent-combinatorics.surjective-maps.md) + - [Symmetric difference of finite subtypes](univalent-combinatorics.symmetric-difference.md) + - [The binomial types](univalent-combinatorics.binomial-types.md) + - [The classical definition of the standard finite types](univalent-combinatorics.classical-finite-types.md) + - [The groupoid of main classes of Latin hypercubes](univalent-combinatorics.main-classes-of-latin-hypercubes.md) + - [The groupoid of main classes of Latin squares](univalent-combinatorics.main-classes-of-latin-squares.md) + - [The image of a map](univalent-combinatorics.image-of-maps.md) + - [The maybe modality on finite types](univalent-combinatorics.maybe.md) + - [The pigeonhole principle](univalent-combinatorics.pigeonhole-principle.md) + - [The precategory of finite species](univalent-combinatorics.precategory-of-finite-species.md) + - [The standard finite types](univalent-combinatorics.standard-finite-types.md) + - [The universal property of the standard finite types](univalent-combinatorics.universal-property-standard-finite-types.md) + - [Unlabeled partitions](univalent-combinatorics.unlabeled-partitions.md) + - [Unlabeled structures of a species](univalent-combinatorics.unlabeled-structures-species.md) + - [Unlabelled rooted trees](univalent-combinatorics.unlabeled-rooted-trees.md) + - [Unlabelled trees](univalent-combinatorics.unlabeled-trees.md) + - [π-finite types](univalent-combinatorics.pi-finite-types.md) diff --git a/SUMMARY.md b/SUMMARY.md index b1e74c2af0..33090154d2 100644 --- a/SUMMARY.md +++ b/SUMMARY.md @@ -20,1007 +20,4 @@ --- -# Formalisation in Agda - -- [Category theory](category-theory.md) - - [Adjunctions large precategories](category-theory.adjunctions-large-precategories.md) - - [Anafunctors](category-theory.anafunctors.md) - - [Categories](category-theory.categories.md) - - [Coproducts precategories](category-theory.coproducts-precategories.md) - - [Discrete precategories](category-theory.discrete-precategories.md) - - [Endomorphisms of objects categories](category-theory.endomorphisms-of-objects-categories.md) - - [Epimorphisms large precategories](category-theory.epimorphisms-large-precategories.md) - - [Equivalences categories](category-theory.equivalences-categories.md) - - [Equivalences large precategories](category-theory.equivalences-large-precategories.md) - - [Equivalences precategories](category-theory.equivalences-precategories.md) - - [Exponential objects precategories](category-theory.exponential-objects-precategories.md) - - [Functors categories](category-theory.functors-categories.md) - - [Functors large precategories](category-theory.functors-large-precategories.md) - - [Functors precategories](category-theory.functors-precategories.md) - - [Groupoids](category-theory.groupoids.md) - - [Homotopies natural transformations large precategories](category-theory.homotopies-natural-transformations-large-precategories.md) - - [Initial objects precategories](category-theory.initial-objects-precategories.md) - - [Isomorphisms categories](category-theory.isomorphisms-categories.md) - - [Isomorphisms large precategories](category-theory.isomorphisms-large-precategories.md) - - [Isomorphisms precategories](category-theory.isomorphisms-precategories.md) - - [Large categories](category-theory.large-categories.md) - - [Large precategories](category-theory.large-precategories.md) - - [Monomorphisms large precategories](category-theory.monomorphisms-large-precategories.md) - - [Natural isomorphisms categories](category-theory.natural-isomorphisms-categories.md) - - [Natural isomorphisms large precategories](category-theory.natural-isomorphisms-large-precategories.md) - - [Natural isomorphisms precategories](category-theory.natural-isomorphisms-precategories.md) - - [Natural numbers object precategories](category-theory.natural-numbers-object-precategories.md) - - [Natural transformations categories](category-theory.natural-transformations-categories.md) - - [Natural transformations large precategories](category-theory.natural-transformations-large-precategories.md) - - [Natural transformations precategories](category-theory.natural-transformations-precategories.md) - - [Precategories](category-theory.precategories.md) - - [Precategory of functors](category-theory.precategory-of-functors.md) - - [Pregroupoids](category-theory.pregroupoids.md) - - [Products precategories](category-theory.products-precategories.md) - - [Pullbacks precategories](category-theory.pullbacks-precategories.md) - - [Sieves categories](category-theory.sieves-categories.md) - - [Slice precategories](category-theory.slice-precategories.md) - - [Terminal objects precategories](category-theory.terminal-objects-precategories.md) - -- [Commutative algebra](commutative-algebra.md) - - [Binomial theorem for commutative rings](commutative-algebra.binomial-theorem-commutative-rings.md) - - [Binomial theorem for commutative semirings](commutative-algebra.binomial-theorem-commutative-semirings.md) - - [Boolean rings](commutative-algebra.boolean-rings.md) - - [Commutative rings](commutative-algebra.commutative-rings.md) - - [Commutative semirings](commutative-algebra.commutative-semirings.md) - - [Discrete fields](commutative-algebra.discrete-fields.md) - - [Eisenstein integers](commutative-algebra.eisenstein-integers.md) - - [Gaussian integers](commutative-algebra.gaussian-integers.md) - - [Homomorphisms of commutative rings](commutative-algebra.homomorphisms-commutative-rings.md) - - [Ideals in commutative rings](commutative-algebra.ideals-commutative-rings.md) - - [Integral domains](commutative-algebra.integral-domains.md) - - [Invertible elements in commutative rings](commutative-algebra.invertible-elements-commutative-rings.md) - - [Isomorphisms of commutative rings](commutative-algebra.isomorphisms-commutative-rings.md) - - [Local commutative rings](commutative-algebra.local-commutative-rings.md) - - [Maximal ideals in commutative rings](commutative-algebra.maximal-ideals-commutative-rings.md) - - [Nilradicals of commutative rings](commutative-algebra.nilradical-commutative-rings.md) - - [Powers of elements in commutative rings](commutative-algebra.powers-of-elements-commutative-rings.md) - - [Powers of elements in commutative semirings](commutative-algebra.powers-of-elements-commutative-semirings.md) - - [Prime ideals in commutative rings](commutative-algebra.prime-ideals-commutative-rings.md) - - [Sums of elements in commutative rings](commutative-algebra.sums-commutative-rings.md) - - [Sums of elements in commutative semirings](commutative-algebra.sums-commutative-semirings.md) - - [Zariski topology](commutative-algebra.zariski-topology.md) - -- [Elementary number theory](elementary-number-theory.md) - - [Absolute value integers](elementary-number-theory.absolute-value-integers.md) - - [Addition integers](elementary-number-theory.addition-integers.md) - - [Addition natural numbers](elementary-number-theory.addition-natural-numbers.md) - - [Arithmetic functions](elementary-number-theory.arithmetic-functions.md) - - [Bezouts lemma](elementary-number-theory.bezouts-lemma.md) - - [Binomial coefficients](elementary-number-theory.binomial-coefficients.md) - - [Binomial theorem for the integers](elementary-number-theory.binomial-theorem-integers.md) - - [Binomial theorem for natural numbers](elementary-number-theory.binomial-theorem-natural-numbers.md) - - [Bounded sums arithmetic functions](elementary-number-theory.bounded-sums-arithmetic-functions.md) - - [Catalan numbers](elementary-number-theory.catalan-numbers.md) - - [Collatz bijection](elementary-number-theory.collatz-bijection.md) - - [Collatz conjecture](elementary-number-theory.collatz-conjecture.md) - - [Commutative ring of integers](elementary-number-theory.commutative-ring-of-integers.md) - - [Commutative semiring of natural numbers](elementary-number-theory.commutative-semiring-of-natural-numbers.md) - - [Congruence integers](elementary-number-theory.congruence-integers.md) - - [Congruence natural numbers](elementary-number-theory.congruence-natural-numbers.md) - - [Decidable dependent function types](elementary-number-theory.decidable-dependent-function-types.md) - - [Decidable types](elementary-number-theory.decidable-types.md) - - [Difference integers](elementary-number-theory.difference-integers.md) - - [Dirichlet convolution](elementary-number-theory.dirichlet-convolution.md) - - [Distance integers](elementary-number-theory.distance-integers.md) - - [Distance natural numbers](elementary-number-theory.distance-natural-numbers.md) - - [Divisibility integers](elementary-number-theory.divisibility-integers.md) - - [Divisibility modular arithmetic](elementary-number-theory.divisibility-modular-arithmetic.md) - - [Divisibility natural numbers](elementary-number-theory.divisibility-natural-numbers.md) - - [Divisibility standard finite types](elementary-number-theory.divisibility-standard-finite-types.md) - - [Equality integers](elementary-number-theory.equality-integers.md) - - [Equality natural numbers](elementary-number-theory.equality-natural-numbers.md) - - [Euclidean division natural numbers](elementary-number-theory.euclidean-division-natural-numbers.md) - - [Eulers totient function](elementary-number-theory.eulers-totient-function.md) - - [Exponentiation natural numbers](elementary-number-theory.exponentiation-natural-numbers.md) - - [Factorials](elementary-number-theory.factorials.md) - - [Falling factorials](elementary-number-theory.falling-factorials.md) - - [Fibonacci sequence](elementary-number-theory.fibonacci-sequence.md) - - [Finitary natural numbers](elementary-number-theory.finitary-natural-numbers.md) - - [Finitely cyclic maps](elementary-number-theory.finitely-cyclic-maps.md) - - [Fractions](elementary-number-theory.fractions.md) - - [Goldbach conjecture](elementary-number-theory.goldbach-conjecture.md) - - [Greatest common divisor integers](elementary-number-theory.greatest-common-divisor-integers.md) - - [Greatest common divisor natural numbers](elementary-number-theory.greatest-common-divisor-natural-numbers.md) - - [Group of integers](elementary-number-theory.group-of-integers.md) - - [Groups of modular arithmetic](elementary-number-theory.groups-of-modular-arithmetic.md) - - [Half integers](elementary-number-theory.half-integers.md) - - [Inequality integers](elementary-number-theory.inequality-integers.md) - - [Inequality natural numbers](elementary-number-theory.inequality-natural-numbers.md) - - [Inequality standard finite types](elementary-number-theory.inequality-standard-finite-types.md) - - [Infinitude of primes](elementary-number-theory.infinitude-of-primes.md) - - [Integer partitions](elementary-number-theory.integer-partitions.md) - - [Integers](elementary-number-theory.integers.md) - - [Lower bounds natural numbers](elementary-number-theory.lower-bounds-natural-numbers.md) - - [Maximum natural numbers](elementary-number-theory.maximum-natural-numbers.md) - - [Maximum standard finite types](elementary-number-theory.maximum-standard-finite-types.md) - - [Mersenne primes](elementary-number-theory.mersenne-primes.md) - - [Minimum natural numbers](elementary-number-theory.minimum-natural-numbers.md) - - [Minimum standard finite types](elementary-number-theory.minimum-standard-finite-types.md) - - [Modular arithmetic standard finite types](elementary-number-theory.modular-arithmetic-standard-finite-types.md) - - [Modular arithmetic](elementary-number-theory.modular-arithmetic.md) - - [Multiplication integers](elementary-number-theory.multiplication-integers.md) - - [Multiplication natural numbers](elementary-number-theory.multiplication-natural-numbers.md) - - [Multiset coefficients](elementary-number-theory.multiset-coefficients.md) - - [Natural numbers](elementary-number-theory.natural-numbers.md) - - [Nonzero natural numbers](elementary-number-theory.nonzero-natural-numbers.md) - - [Ordinal induction natural numbers](elementary-number-theory.ordinal-induction-natural-numbers.md) - - [Powers of integers](elementary-number-theory.powers-integers.md) - - [Prime numbers](elementary-number-theory.prime-numbers.md) - - [Products of natural numbers](elementary-number-theory.products-of-natural-numbers.md) - - [Proper divisors natural numbers](elementary-number-theory.proper-divisors-natural-numbers.md) - - [Pythagorean triples](elementary-number-theory.pythagorean-triples.md) - - [Rational numbers](elementary-number-theory.rational-numbers.md) - - [Relatively prime integers](elementary-number-theory.relatively-prime-integers.md) - - [Relatively prime natural numbers](elementary-number-theory.relatively-prime-natural-numbers.md) - - [Repeating element standard finite type](elementary-number-theory.repeating-element-standard-finite-type.md) - - [Retracts of natural numbers](elementary-number-theory.retracts-of-natural-numbers.md) - - [Square free natural numbers](elementary-number-theory.square-free-natural-numbers.md) - - [Stirling numbers of the second kind](elementary-number-theory.stirling-numbers-of-the-second-kind.md) - - [Strong induction natural numbers](elementary-number-theory.strong-induction-natural-numbers.md) - - [Sums of natural numbers](elementary-number-theory.sums-of-natural-numbers.md) - - [Telephone numbers](elementary-number-theory.telephone-numbers.md) - - [Triangular numbers](elementary-number-theory.triangular-numbers.md) - - [Twin prime conjecture](elementary-number-theory.twin-prime-conjecture.md) - - [Unit elements standard finite types](elementary-number-theory.unit-elements-standard-finite-types.md) - - [Unit similarity standard finite types](elementary-number-theory.unit-similarity-standard-finite-types.md) - - [Universal property natural numbers](elementary-number-theory.universal-property-natural-numbers.md) - - [Upper bounds natural numbers](elementary-number-theory.upper-bounds-natural-numbers.md) - - [Well ordering principle natural numbers](elementary-number-theory.well-ordering-principle-natural-numbers.md) - - [Well ordering principle standard finite types](elementary-number-theory.well-ordering-principle-standard-finite-types.md) - -- [Finite group theory](finite-group-theory.md) - - [Abstract quaternion group](finite-group-theory.abstract-quaternion-group.md) - - [Alternating concrete groups](finite-group-theory.alternating-concrete-groups.md) - - [Alternating groups](finite-group-theory.alternating-groups.md) - - [Cartier delooping sign homomorphism](finite-group-theory.cartier-delooping-sign-homomorphism.md) - - [Concrete quaternion group](finite-group-theory.concrete-quaternion-group.md) - - [Delooping sign homomorphism](finite-group-theory.delooping-sign-homomorphism.md) - - [Finite groups](finite-group-theory.finite-groups.md) - - [Finite monoids](finite-group-theory.finite-monoids.md) - - [Finite semigroups](finite-group-theory.finite-semigroups.md) - - [Finite type groups](finite-group-theory.finite-type-groups.md) - - [Groups of order 2](finite-group-theory.groups-of-order-2.md) - - [Orbits permutations](finite-group-theory.orbits-permutations.md) - - [Permutations](finite-group-theory.permutations.md) - - [Sign homomorphism](finite-group-theory.sign-homomorphism.md) - - [Simpson delooping sign homomorphism](finite-group-theory.simpson-delooping-sign-homomorphism.md) - - [Subgroups finite groups](finite-group-theory.subgroups-finite-groups.md) - - [Tetrahedra in-3-space](finite-group-theory.tetrahedra-in-3-space.md) - - [Transpositions](finite-group-theory.transpositions.md) - -- [Foundation](Foundation.md) - - [0-connected types](foundation.0-connected-types.md) - - [0-images of maps](foundation.0-images-of-maps.md) - - [0-maps](foundation.0-maps.md) - - [1-types](foundation.1-types.md) - - [2-types](foundation.2-types.md) - - [Algebras polynomial endofunctors](foundation.algebras-polynomial-endofunctors.md) - - [Apartness relations](foundation.apartness-relations.md) - - [Automorphisms](foundation.automorphisms.md) - - [Axiom L](foundation.axiom-l.md) - - [Axiom of choice](foundation.axiom-of-choice.md) - - [Bands](foundation.bands.md) - - [Binary embeddings](foundation.binary-embeddings.md) - - [Binary equivalences unordered pairs of types](foundation.binary-equivalences-unordered-pairs-of-types.md) - - [Binary equivalences](foundation.binary-equivalences.md) - - [Binary operations unordered pairs of types](foundation.binary-operations-unordered-pairs-of-types.md) - - [Binary reflecting maps equivalence relations](foundation.binary-reflecting-maps-equivalence-relations.md) - - [Binary relations](foundation.binary-relations.md) - - [Boolean reflection](foundation.boolean-reflection.md) - - [Booleans](foundation.booleans.md) - - [Cantor-Schröder-Bernstein-Escardó](foundation.cantor-schroder-bernstein-escardo.md) - - [Cantors diagonal argument](foundation.cantors-diagonal-argument.md) - - [Cartesian product types](foundation.cartesian-product-types.md) - - [Choice of representatives equivalence relation](foundation.choice-of-representatives-equivalence-relation.md) - - [Coherently invertible maps](foundation.coherently-invertible-maps.md) - - [Commuting 3-simplices of homotopies](foundation.commuting-3-simplices-of-homotopies.md) - - [Commuting 3-simplices of maps](foundation.commuting-3-simplices-of-maps.md) - - [Commuting cubes of maps](foundation.commuting-cubes-of-maps.md) - - [Commuting squares of identifications](foundation.commuting-squares-of-identifications.md) - - [Commuting squares of maps](foundation.commuting-squares-of-maps.md) - - [Commuting triangles of homotopies](foundation.commuting-triangles-of-homotopies.md) - - [Commuting triangles of maps](foundation.commuting-triangles-of-maps.md) - - [Complements subtypes](foundation.complements-subtypes.md) - - [Complements](foundation.complements.md) - - [Cones pullbacks](foundation.cones-pullbacks.md) - - [Conjunction](foundation.conjunction.md) - - [Connected components universes](foundation.connected-components-universes.md) - - [Connected components](foundation.connected-components.md) - - [Connected maps](foundation.connected-maps.md) - - [Connected types](foundation.connected-types.md) - - [Constant maps](foundation.constant-maps.md) - - [Contractible maps](foundation.contractible-maps.md) - - [Contractible types](foundation.contractible-types.md) - - [Coproduct types](foundation.coproduct-types.md) - - [Coslice](foundation.coslice.md) - - [Cospans](foundation.cospans.md) - - [Decidable dependent function types](foundation.decidable-dependent-function-types.md) - - [Decidable dependent pair types](foundation.decidable-dependent-pair-types.md) - - [Decidable embeddings](foundation.decidable-embeddings.md) - - [Decidable equality](foundation.decidable-equality.md) - - [Decidable equivalence relations](foundation.decidable-equivalence-relations.md) - - [Decidable maps](foundation.decidable-maps.md) - - [Decidable propositions](foundation.decidable-propositions.md) - - [Decidable relations](foundation.decidable-relations.md) - - [Decidable subtypes](foundation.decidable-subtypes.md) - - [Decidable types](foundation.decidable-types.md) - - [Dependent binomial theorem](foundation.dependent-binomial-theorem.md) - - [Dependent pair types](foundation.dependent-pair-types.md) - - [Dependent paths](foundation.dependent-paths.md) - - [Descent coproduct types](foundation.descent-coproduct-types.md) - - [Descent dependent pair types](foundation.descent-dependent-pair-types.md) - - [Descent empty types](foundation.descent-empty-types.md) - - [Descent equivalences](foundation.descent-equivalences.md) - - [Diagonal maps of types](foundation.diagonal-maps-of-types.md) - - [Diagonals of maps](foundation.diagonals-of-maps.md) - - [Discrete reflexive relations](foundation.discrete-reflexive-relations.md) - - [Discrete types](foundation.discrete-types.md) - - [Disjunction](foundation.disjunction.md) - - [Double negation](foundation.double-negation.md) - - [Double powersets](foundation.double-powersets.md) - - [Dubuc penon compact types](foundation.dubuc-penon-compact-types.md) - - [Effective maps equivalence relations](foundation.effective-maps-equivalence-relations.md) - - [Embeddings](foundation.embeddings.md) - - [Empty types](foundation.empty-types.md) - - [Endomorphisms](foundation.endomorphisms.md) - - [Epimorphisms with respect to sets](foundation.epimorphisms-with-respect-to-sets.md) - - [Equality cartesian product types](foundation.equality-cartesian-product-types.md) - - [Equality coproduct types](foundation.equality-coproduct-types.md) - - [Equality dependent function types](foundation.equality-dependent-function-types.md) - - [Equality dependent pair types](foundation.equality-dependent-pair-types.md) - - [Equality fibers of maps](foundation.equality-fibers-of-maps.md) - - [Equational reasoning](foundation.equational-reasoning.md) - - [Equivalence classes](foundation.equivalence-classes.md) - - [Equivalence induction](foundation.equivalence-induction.md) - - [Equivalence relations](foundation.equivalence-relations.md) - - [Equivalences maybe](foundation.equivalences-maybe.md) - - [Equivalences](foundation.equivalences.md) - - [Existential quantification](foundation.existential-quantification.md) - - [Exponents set quotients](foundation.exponents-set-quotients.md) - - [Faithful maps](foundation.faithful-maps.md) - - [Fiber inclusions](foundation.fiber-inclusions.md) - - [Fibered equivalences](foundation.fibered-equivalences.md) - - [Fibered involutions](foundation.fibered-involutions.md) - - [Fibered maps](foundation.fibered-maps.md) - - [Fibers of maps](foundation.fibers-of-maps.md) - - [Full subtypes](foundation.full-subtypes.md) - - [Function extensionality](foundation.function-extensionality.md) - - [Functional correspondences](foundation.functional-correspondences.md) - - [Functions](foundation.functions.md) - - [Functoriality cartesian product types](foundation.functoriality-cartesian-product-types.md) - - [Functoriality coproduct types](foundation.functoriality-coproduct-types.md) - - [Functoriality dependent function types](foundation.functoriality-dependent-function-types.md) - - [Functoriality dependent pair types](foundation.functoriality-dependent-pair-types.md) - - [Functoriality fibers of maps](foundation.functoriality-fibers-of-maps.md) - - [Functoriality function types](foundation.functoriality-function-types.md) - - [Functoriality propositional truncation](foundation.functoriality-propositional-truncation.md) - - [Functoriality set quotients](foundation.functoriality-set-quotients.md) - - [Functoriality set truncation](foundation.functoriality-set-truncation.md) - - [Functoriality truncation](foundation.functoriality-truncation.md) - - [Fundamental theorem of identity types](foundation.fundamental-theorem-of-identity-types.md) - - [Global choice](foundation.global-choice.md) - - [Hexagons of identifications](foundation.hexagons-of-identifications.md) - - [Hilberts epsilon operators](foundation.hilberts-epsilon-operators.md) - - [Homotopies](foundation.homotopies.md) - - [Identity systems](foundation.identity-systems.md) - - [Identity truncated types](foundation.identity-truncated-types.md) - - [Identity types](foundation.identity-types.md) - - [Images subtypes](foundation.images-subtypes.md) - - [Images](foundation.images.md) - - [Impredicative encodings](foundation.impredicative-encodings.md) - - [Impredicative universes](foundation.impredicative-universes.md) - - [Induction principle propositional truncation](foundation.induction-principle-propositional-truncation.md) - - [Inhabited subtypes](foundation.inhabited-subtypes.md) - - [Inhabited types](foundation.inhabited-types.md) - - [Injective maps](foundation.injective-maps.md) - - [Interchange law](foundation.interchange-law.md) - - [Intersections subtypes](foundation.intersections-subtypes.md) - - [Involutions](foundation.involutions.md) - - [Isolated points](foundation.isolated-points.md) - - [Isomorphisms of sets](foundation.isomorphisms-of-sets.md) - - [Iterating automorphisms](foundation.iterating-automorphisms.md) - - [Iterating functions](foundation.iterating-functions.md) - - [Iterating involutions](foundation.iterating-involutions.md) - - [Law of excluded middle](foundation.law-of-excluded-middle.md) - - [Lawveres fixed point theorem](foundation.lawveres-fixed-point-theorem.md) - - [Lesser limited principle of omniscience](foundation.lesser-limited-principle-of-omniscience.md) - - [Limited principle of omniscience](foundation.limited-principle-of-omniscience.md) - - [Locally small types](foundation.locally-small-types.md) - - [Logical equivalences](foundation.logical-equivalences.md) - - [Maybe](foundation.maybe.md) - - [Mere embeddings](foundation.mere-embeddings.md) - - [Mere equality](foundation.mere-equality.md) - - [Mere equivalences](foundation.mere-equivalences.md) - - [Monomorphisms](foundation.monomorphisms.md) - - [Morphisms cospans](foundation.morphisms-cospans.md) - - [Multisubsets](foundation.multisubsets.md) - - [Multivariable correspondences](foundation.multivariable-correspondences.md) - - [Multivariable decidable relations](foundation.multivariable-decidable-relations.md) - - [Multivariable relations](foundation.multivariable-relations.md) - - [Negation](foundation.negation.md) - - [Noncontractible types](foundation.noncontractible-types.md) - - [Pairs of distinct elements](foundation.pairs-of-distinct-elements.md) - - [Partial elements](foundation.partial-elements.md) - - [Partitions](foundation.partitions.md) - - [Path algebra](foundation.path-algebra.md) - - [Path split maps](foundation.path-split-maps.md) - - [Perfect images](foundation.perfect-images.md) - - [Polynomial endofunctors](foundation.polynomial-endofunctors.md) - - [Powersets](foundation.powersets.md) - - [Preimages of subtypes](foundation.preimages-of-subtypes.md) - - [Principle of omniscience](foundation.principle-of-omniscience.md) - - [Products of tuples of types](foundation.products-of-tuples-of-types.md) - - [Products unordered pairs of types](foundation.products-unordered-pairs-of-types.md) - - [Products unordered tuples of types](foundation.products-unordered-tuples-of-types.md) - - [Projective types](foundation.projective-types.md) - - [Proper subtypes](foundation.proper-subtypes.md) - - [Propositional extensionality](foundation.propositional-extensionality.md) - - [Propositional maps](foundation.propositional-maps.md) - - [Propositional resizing](foundation.propositional-resizing.md) - - [Propositional truncations](foundation.propositional-truncations.md) - - [Propositions](foundation.propositions.md) - - [Pullbacks](foundation.pullbacks.md) - - [Raising universe levels](foundation.raising-universe-levels.md) - - [Reflecting maps equivalence relations](foundation.reflecting-maps-equivalence-relations.md) - - [Reflexive relations](foundation.reflexive-relations.md) - - [Repetitions sequences](foundation.repetitions-sequences.md) - - [Repetitions](foundation.repetitions.md) - - [Replacement](foundation.replacement.md) - - [Retractions](foundation.retractions.md) - - [Russells paradox](foundation.russells-paradox.md) - - [Sections](foundation.sections.md) - - [Sequences](foundation.sequences.md) - - [Set presented types](foundation.set-presented-types.md) - - [Set quotients](foundation.set-quotients.md) - - [Set truncations](foundation.set-truncations.md) - - [Sets](foundation.sets.md) - - [Shifting sequences](foundation.shifting-sequences.md) - - [Sigma decompositions](foundation.sigma-decompositions.md) - - [Singleton induction](foundation.singleton-induction.md) - - [Singleton subtypes](foundation.singleton-subtypes.md) - - [Slice](foundation.slice.md) - - [Small maps](foundation.small-maps.md) - - [Small types](foundation.small-types.md) - - [Small universes](foundation.small-universes.md) - - [Split surjective maps](foundation.split-surjective-maps.md) - - [Standard apartness relations](foundation.standard-apartness-relations.md) - - [Strongly extensional maps](foundation.strongly-extensional-maps.md) - - [Structure identity principle](foundation.structure-identity-principle.md) - - [Structure](foundation.structure.md) - - [Subterminal types](foundation.subterminal-types.md) - - [Subtype identity principle](foundation.subtype-identity-principle.md) - - [Subtypes](foundation.subtypes.md) - - [Subuniverses](foundation.subuniverses.md) - - [Surjective maps](foundation.surjective-maps.md) - - [Symmetric difference](foundation.symmetric-difference.md) - - [Symmetric identity types](foundation.symmetric-identity-types.md) - - [Symmetric operations](foundation.symmetric-operations.md) - - [Tight apartness relations](foundation.tight-apartness-relations.md) - - [Transport](foundation.transport.md) - - [Truncated equality](foundation.truncated-equality.md) - - [Truncated maps](foundation.truncated-maps.md) - - [Truncated types](foundation.truncated-types.md) - - [Truncation images of maps](foundation.truncation-images-of-maps.md) - - [Truncation levels](foundation.truncation-levels.md) - - [Truncations](foundation.truncations.md) - - [Tuples of types](foundation.tuples-of-types.md) - - [Type arithmetic booleans](foundation.type-arithmetic-booleans.md) - - [Type arithmetic cartesian product types](foundation.type-arithmetic-cartesian-product-types.md) - - [Type arithmetic coproduct types](foundation.type-arithmetic-coproduct-types.md) - - [Type arithmetic dependent function types](foundation.type-arithmetic-dependent-function-types.md) - - [Type arithmetic dependent pair types](foundation.type-arithmetic-dependent-pair-types.md) - - [Type arithmetic empty type](foundation.type-arithmetic-empty-type.md) - - [Type arithmetic unit type](foundation.type-arithmetic-unit-type.md) - - [Type duality](foundation.type-duality.md) - - [Type theoretic principle of choice](foundation.type-theoretic-principle-of-choice.md) - - [Unions subtypes](foundation.unions-subtypes.md) - - [Unique existence](foundation.unique-existence.md) - - [Uniqueness image](foundation.uniqueness-image.md) - - [Uniqueness set quotients](foundation.uniqueness-set-quotients.md) - - [Uniqueness set truncations](foundation.uniqueness-set-truncations.md) - - [Uniqueness truncation](foundation.uniqueness-truncation.md) - - [Unit type](foundation.unit-type.md) - - [Unital binary operations](foundation.unital-binary-operations.md) - - [Univalence implies function extensionality](foundation.univalence-implies-function-extensionality.md) - - [Univalence](foundation.univalence.md) - - [Univalent type families](foundation.univalent-type-families.md) - - [Universal property booleans](foundation.universal-property-booleans.md) - - [Universal property cartesian product types](foundation.universal-property-cartesian-product-types.md) - - [Universal property coproduct types](foundation.universal-property-coproduct-types.md) - - [Universal property dependent pair types](foundation.universal-property-dependent-pair-types.md) - - [Universal property empty type](foundation.universal-property-empty-type.md) - - [Universal property fiber products](foundation.universal-property-fiber-products.md) - - [Universal property identity types](foundation.universal-property-identity-types.md) - - [Universal property image](foundation.universal-property-image.md) - - [Universal property maybe](foundation.universal-property-maybe.md) - - [Universal property propositional truncation into sets](foundation.universal-property-propositional-truncation-into-sets.md) - - [Universal property propositional truncation](foundation.universal-property-propositional-truncation.md) - - [Universal property pullbacks](foundation.universal-property-pullbacks.md) - - [Universal property set quotients](foundation.universal-property-set-quotients.md) - - [Universal property set truncation](foundation.universal-property-set-truncation.md) - - [Universal property truncation](foundation.universal-property-truncation.md) - - [Universal property unit type](foundation.universal-property-unit-type.md) - - [Universe levels](foundation.universe-levels.md) - - [Unordered pairs of types](foundation.unordered-pairs-of-types.md) - - [Unordered pairs](foundation.unordered-pairs.md) - - [Unordered tuples of types](foundation.unordered-tuples-of-types.md) - - [Unordered tuples](foundation.unordered-tuples.md) - - [Weak function extensionality](foundation.weak-function-extensionality.md) - - [Weak limited principle of omniscience](foundation.weak-limited-principle-of-omniscience.md) - - [Weakly constant maps](foundation.weakly-constant-maps.md) - - [Xor](foundation.xor.md) - -- [Foundation core](foundation-core.md) - - [0-maps](foundation-core.0-maps.md) - - [1-types](foundation-core.1-types.md) - - [Automorphisms](foundation-core.automorphisms.md) - - [Cartesian product types](foundation-core.cartesian-product-types.md) - - [Coherently invertible maps](foundation-core.coherently-invertible-maps.md) - - [Commuting 3-simplices of homotopies](foundation-core.commuting-3-simplices-of-homotopies.md) - - [Commuting 3-simplices of maps](foundation-core.commuting-3-simplices-of-maps.md) - - [Commuting cubes of maps](foundation-core.commuting-cubes-of-maps.md) - - [Commuting squares of maps](foundation-core.commuting-squares-of-maps.md) - - [Commuting triangles of homotopies](foundation-core.commuting-triangles-of-homotopies.md) - - [Commuting triangles of maps](foundation-core.commuting-triangles-of-maps.md) - - [Cones pullbacks](foundation-core.cones-pullbacks.md) - - [Constant maps](foundation-core.constant-maps.md) - - [Contractible maps](foundation-core.contractible-maps.md) - - [Contractible types](foundation-core.contractible-types.md) - - [Coproduct types](foundation-core.coproduct-types.md) - - [Cospans](foundation-core.cospans.md) - - [Decidable propositions](foundation-core.decidable-propositions.md) - - [Dependent pair types](foundation-core.dependent-pair-types.md) - - [Diagonal maps of types](foundation-core.diagonal-maps-of-types.md) - - [Discrete types](foundation-core.discrete-types.md) - - [Embeddings](foundation-core.embeddings.md) - - [Empty types](foundation-core.empty-types.md) - - [Endomorphisms](foundation-core.endomorphisms.md) - - [Equality cartesian product types](foundation-core.equality-cartesian-product-types.md) - - [Equality dependent pair types](foundation-core.equality-dependent-pair-types.md) - - [Equality fibers of maps](foundation-core.equality-fibers-of-maps.md) - - [Equivalence induction](foundation-core.equivalence-induction.md) - - [Equivalences](foundation-core.equivalences.md) - - [Faithful maps](foundation-core.faithful-maps.md) - - [Fibers of maps](foundation-core.fibers-of-maps.md) - - [Function extensionality](foundation-core.function-extensionality.md) - - [Functions](foundation-core.functions.md) - - [Functoriality dependent function types](foundation-core.functoriality-dependent-function-types.md) - - [Functoriality dependent pair types](foundation-core.functoriality-dependent-pair-types.md) - - [Functoriality fibers of maps](foundation-core.functoriality-fibers-of-maps.md) - - [Functoriality function types](foundation-core.functoriality-function-types.md) - - [Fundamental theorem of identity types](foundation-core.fundamental-theorem-of-identity-types.md) - - [Homotopies](foundation-core.homotopies.md) - - [Identity systems](foundation-core.identity-systems.md) - - [Identity types](foundation-core.identity-types.md) - - [Injective maps](foundation-core.injective-maps.md) - - [Involutions](foundation-core.involutions.md) - - [Logical equivalences](foundation-core.logical-equivalences.md) - - [Morphisms cospans](foundation-core.morphisms-cospans.md) - - [Negation](foundation-core.negation.md) - - [Path split maps](foundation-core.path-split-maps.md) - - [Propositional maps](foundation-core.propositional-maps.md) - - [Propositions](foundation-core.propositions.md) - - [Pullbacks](foundation-core.pullbacks.md) - - [Retractions](foundation-core.retractions.md) - - [Sections](foundation-core.sections.md) - - [Sets](foundation-core.sets.md) - - [Singleton induction](foundation-core.singleton-induction.md) - - [Small types](foundation-core.small-types.md) - - [Subtype identity principle](foundation-core.subtype-identity-principle.md) - - [Subtypes](foundation-core.subtypes.md) - - [Truncated maps](foundation-core.truncated-maps.md) - - [Truncated types](foundation-core.truncated-types.md) - - [Truncation levels](foundation-core.truncation-levels.md) - - [Type arithmetic cartesian product types](foundation-core.type-arithmetic-cartesian-product-types.md) - - [Type arithmetic dependent pair types](foundation-core.type-arithmetic-dependent-pair-types.md) - - [Univalence](foundation-core.univalence.md) - - [Universal property pullbacks](foundation-core.universal-property-pullbacks.md) - - [Universal property truncation](foundation-core.universal-property-truncation.md) - - [Universe levels](foundation-core.universe-levels.md) - -- [Graph theory](graph-theory.md) - - [Circuits undirected graphs](graph-theory.circuits-undirected-graphs.md) - - [Closed walks undirected graphs](graph-theory.closed-walks-undirected-graphs.md) - - [Complete bipartite graphs](graph-theory.complete-bipartite-graphs.md) - - [Complete multipartite graphs](graph-theory.complete-multipartite-graphs.md) - - [Complete undirected graphs](graph-theory.complete-undirected-graphs.md) - - [Connected undirected graphs](graph-theory.connected-undirected-graphs.md) - - [Cycles undirected graphs](graph-theory.cycles-undirected-graphs.md) - - [Directed graph structures on standard finite sets](graph-theory.directed-graph-structures-on-standard-finite-sets.md) - - [Directed graphs](graph-theory.directed-graphs.md) - - [Edge coloured undirected graphs](graph-theory.edge-coloured-undirected-graphs.md) - - [Embeddings directed graphs](graph-theory.embeddings-directed-graphs.md) - - [Embeddings undirected graphs](graph-theory.embeddings-undirected-graphs.md) - - [Enriched undirected graphs](graph-theory.enriched-undirected-graphs.md) - - [Equivalences directed graphs](graph-theory.equivalences-directed-graphs.md) - - [Equivalences enriched undirected graphs](graph-theory.equivalences-enriched-undirected-graphs.md) - - [Equivalences undirected graphs](graph-theory.equivalences-undirected-graphs.md) - - [Eulerian circuits undirected graphs](graph-theory.eulerian-circuits-undirected-graphs.md) - - [Faithful morphisms undirected graphs](graph-theory.faithful-morphisms-undirected-graphs.md) - - [Finite graphs](graph-theory.finite-graphs.md) - - [Geometric realizations undirected graphs](graph-theory.geometric-realizations-undirected-graphs.md) - - [Hypergraphs](graph-theory.hypergraphs.md) - - [Matchings](graph-theory.matchings.md) - - [Mere equivalences undirected graphs](graph-theory.mere-equivalences-undirected-graphs.md) - - [Morphisms directed graphs](graph-theory.morphisms-directed-graphs.md) - - [Morphisms undirected graphs](graph-theory.morphisms-undirected-graphs.md) - - [Neighbors undirected graphs](graph-theory.neighbors-undirected-graphs.md) - - [Orientations undirected graphs](graph-theory.orientations-undirected-graphs.md) - - [Paths undirected graphs](graph-theory.paths-undirected-graphs.md) - - [Polygons](graph-theory.polygons.md) - - [Reflecting maps undirected graphs](graph-theory.reflecting-maps-undirected-graphs.md) - - [Reflexive graphs](graph-theory.reflexive-graphs.md) - - [Regular undirected graphs](graph-theory.regular-undirected-graphs.md) - - [Simple undirected graphs](graph-theory.simple-undirected-graphs.md) - - [Stereoisomerism enriched undirected graphs](graph-theory.stereoisomerism-enriched-undirected-graphs.md) - - [Totally faithful morphisms undirected graphs](graph-theory.totally-faithful-morphisms-undirected-graphs.md) - - [Trails directed graphs](graph-theory.trails-directed-graphs.md) - - [Trails undirected graphs](graph-theory.trails-undirected-graphs.md) - - [Undirected graph structures on standard finite sets](graph-theory.undirected-graph-structures-on-standard-finite-sets.md) - - [Undirected graphs](graph-theory.undirected-graphs.md) - - [Vertex covers](graph-theory.vertex-covers.md) - - [Voltage graphs](graph-theory.voltage-graphs.md) - - [Walks directed graphs](graph-theory.walks-directed-graphs.md) - - [Walks undirected graphs](graph-theory.walks-undirected-graphs.md) - -- [Group theory](group-theory.md) - - [Abelian groups](group-theory.abelian-groups.md) - - [Addition of homomorphisms of abelian groups](group-theory.addition-homomorphisms-abelian-groups.md) - - [Automorphism of groups](group-theory.automorphism-groups.md) - - [Cartesian products of abelian groups](group-theory.cartesian-products-abelian-groups.md) - - [Cartesian products of groups](group-theory.cartesian-products-groups.md) - - [Cartesian products of monoids](group-theory.cartesian-products-monoids.md) - - [Cartesian products of semigroups](group-theory.cartesian-products-semigroups.md) - - [Category of concrete groups](group-theory.category-of-concrete-groups.md) - - [Category of groups](group-theory.category-of-groups.md) - - [Category of semigroups](group-theory.category-of-semigroups.md) - - [Cayley's theorem](group-theory.cayleys-theorem.md) - - [Centers of groups](group-theory.centers-groups.md) - - [Commutative monoids](group-theory.commutative-monoids.md) - - [Commutators in groups](group-theory.commutators-groups.md) - - [Concrete group actions](group-theory.concrete-group-actions.md) - - [Concrete groups](group-theory.concrete-groups.md) - - [Congruence relations of abelian groups](group-theory.congruence-relations-abelian-groups.md) - - [Congruence relations of groups](group-theory.congruence-relations-groups.md) - - [Congruence relations of monoids](group-theory.congruence-relations-monoids.md) - - [Congruence relations of semigroups](group-theory.congruence-relations-semigroups.md) - - [Conjugation](group-theory.conjugation.md) - - [Contravariant pushforward concrete group actions](group-theory.contravariant-pushforward-concrete-group-actions.md) - - [Decidable subgroups](group-theory.decidable-subgroups.md) - - [Dihedral group construction](group-theory.dihedral-group-construction.md) - - [Dihedral groups](group-theory.dihedral-groups.md) - - [E8-lattice](group-theory.e8-lattice.md) - - [Embeddings of abelian groups](group-theory.embeddings-abelian-groups.md) - - [Embeddings of groups](group-theory.embeddings-groups.md) - - [Endomorphism rings of abelian groups](group-theory.endomorphism-rings-abelian-groups.md) - - [Epimorphisms of groups](group-theory.epimorphisms-groups.md) - - [Equivalences of concrete group actions](group-theory.equivalences-concrete-group-actions.md) - - [Equivalences of concrete groups](group-theory.equivalences-concrete-groups.md) - - [Equivalences of group actions](group-theory.equivalences-group-actions.md) - - [Equivalences of higher groups](group-theory.equivalences-higher-groups.md) - - [Equivalences of semigroups](group-theory.equivalences-semigroups.md) - - [Fixed points of higher group actions](group-theory.fixed-points-higher-group-actions.md) - - [Free concrete group actions](group-theory.free-concrete-group-actions.md) - - [Free groups with one generator](group-theory.free-groups-with-one-generator.md) - - [Free higher group actions](group-theory.free-higher-group-actions.md) - - [Full subgroups](group-theory.full-subgroups.md) - - [Furstenberg groups](group-theory.furstenberg-groups.md) - - [Group actions](group-theory.group-actions.md) - - [Group solver](group-theory.group-solver.md) - - [Groups](group-theory.groups.md) - - [Higher group actions](group-theory.higher-group-actions.md) - - [Higher groups](group-theory.higher-groups.md) - - [Homomorphisms of abelian groups](group-theory.homomorphisms-abelian-groups.md) - - [Homomorphisms of concrete group actions](group-theory.homomorphisms-concrete-group-actions.md) - - [Homomorphisms of concrete groups](group-theory.homomorphisms-concrete-groups.md) - - [Homomorphisms of generated subgroups](group-theory.homomorphisms-generated-subgroups.md) - - [Homomorphisms of group actions](group-theory.homomorphisms-group-actions.md) - - [Homomorphisms of groups](group-theory.homomorphisms-groups.md) - - [Homomorphisms of higher group actions](group-theory.homomorphisms-higher-group-actions.md) - - [Homomorphisms of higher groups](group-theory.homomorphisms-higher-groups.md) - - [Homomorphisms of monoids](group-theory.homomorphisms-monoids.md) - - [Homomorphisms of semigroups](group-theory.homomorphisms-semigroups.md) - - [Integers as a higher group](group-theory.integers-higher-group.md) - - [Inverse semigroups](group-theory.inverse-semigroups.md) - - [Invertible elements in monoids](group-theory.invertible-elements-monoids.md) - - [Isomorphisms of abelian groups](group-theory.isomorphisms-abelian-groups.md) - - [Isomorphisms of concrete groups](group-theory.isomorphisms-concrete-groups.md) - - [Isomorphisms of group actions](group-theory.isomorphisms-group-actions.md) - - [Isomorphisms of groups](group-theory.isomorphisms-groups.md) - - [Isomorphisms of semigroups](group-theory.isomorphisms-semigroups.md) - - [Loop groups of sets](group-theory.loop-groups-sets.md) - - [Kernels](group-theory.kernels.md) - - [Kernels of homomorphisms of concrete groups](group-theory.kernels-homomorphisms-concrete-groups.md) - - [Mere equivalences of concrete group actions](group-theory.mere-equivalences-concrete-group-actions.md) - - [Mere equivalences of group actions](group-theory.mere-equivalences-group-actions.md) - - [Monoid actions](group-theory.monoid-actions.md) - - [Monoids](group-theory.monoids.md) - - [Monomorphisms of concrete groups](group-theory.monomorphisms-concrete-groups.md) - - [Monomorphisms of groups](group-theory.monomorphisms-groups.md) - - [Normal subgroups](group-theory.normal-subgroups.md) - - [Normal subgroups of concrete groups](group-theory.normal-subgroups-concrete-groups.md) - - [Opposite groups](group-theory.opposite-groups.md) - - [Orbit stabilizer theorem of concrete groups](group-theory.orbit-stabilizer-theorem-concrete-groups.md) - - [Orbits of concrete group actions](group-theory.orbits-concrete-group-actions.md) - - [Orbits of group actions](group-theory.orbits-group-actions.md) - - [Orbits of higher group actions](group-theory.orbits-higher-group-actions.md) - - [Orbits of monoid actions](group-theory.orbits-monoid-actions.md) - - [Orders of elements groups](group-theory.orders-of-elements-groups.md) - - [Precategory of concrete groups](group-theory.precategory-of-concrete-groups.md) - - [Precategory of group actions](group-theory.precategory-of-group-actions.md) - - [Precategory of groups](group-theory.precategory-of-groups.md) - - [Precategory of semigroups](group-theory.precategory-of-semigroups.md) - - [Principal group actions](group-theory.principal-group-actions.md) - - [Principal torsors of concrete groups](group-theory.principal-torsors-concrete-groups.md) - - [Products of tuples of elements in commutative monoids](group-theory.products-of-tuples-of-elements-commutative-monoids.md) - - [Quotient groups](group-theory.quotient-groups.md) - - [Quotient groups of concrete groups](group-theory.quotient-groups-concrete-groups.md) - - [Quotients of abelian groups](group-theory.quotients-abelian-groups.md) - - [Representations of monoids](group-theory.representations-monoids.md) - - [Semigroups](group-theory.semigroups.md) - - [Sheargroups](group-theory.sheargroups.md) - - [Shriek operation on concrete group actions](group-theory.shriek-concrete-group-actions.md) - - [Stabilizer groups](group-theory.stabilizer-groups.md) - - [Stabilizer groups of concrete group actions](group-theory.stabilizer-groups-concrete-group-actions.md) - - [Subgroups](group-theory.subgroups.md) - - [Subgroups of abelian groups](group-theory.subgroups-abelian-groups.md) - - [Subgroups of concrete groups](group-theory.subgroups-concrete-groups.md) - - [Subgroups generated by subsets of groups](group-theory.subgroups-generated-by-subsets-groups.md) - - [Subgroups of higher groups](group-theory.subgroups-higher-groups.md) - - [Submonoids](group-theory.submonoids.md) - - [Subsemigroups](group-theory.subsemigroups.md) - - [Substitution functor on concrete group actions](group-theory.substitution-functor-concrete-group-actions.md) - - [Substitution functor on group actions](group-theory.substitution-functor-group-actions.md) - - [Symmetric concrete groups](group-theory.symmetric-concrete-groups.md) - - [Symmetric groups](group-theory.symmetric-groups.md) - - [Symmetric higher groups](group-theory.symmetric-higher-groups.md) - - [Torsors](group-theory.torsors.md) - - [Transitive concrete group actions](group-theory.transitive-concrete-group-actions.md) - - [Transitive group actions](group-theory.transitive-group-actions.md) - - [Trivial subgroups](group-theory.trivial-subgroups.md) - - [Unordered tuples of elements in commutative monoids](group-theory.unordered-tuples-of-elements-commutative-monoids.md) - -- [Linear algebra](linear-algebra.md) - - [Constant matrices](linear-algebra.constant-matrices.md) - - [Constant vectors](linear-algebra.constant-vectors.md) - - [Diagonal matrices on rings](linear-algebra.diagonal-matrices-on-rings.md) - - [Functoriality matrices](linear-algebra.functoriality-matrices.md) - - [Functoriality vectors](linear-algebra.functoriality-vectors.md) - - [Matrices on rings](linear-algebra.matrices-on-rings.md) - - [Matrices](linear-algebra.matrices.md) - - [Multiplication of matrices](linear-algebra.multiplication-matrices.md) - - [Scalar multiplication of matrices](linear-algebra.scalar-multiplication-matrices.md) - - [Scalar multiplication of vectors](linear-algebra.scalar-multiplication-vectors.md) - - [Scalar multiplication of vectors on rings](linear-algebra.scalar-multiplication-vectors-on-rings.md) - - [Transposition of matrices](linear-algebra.transposition-matrices.md) - - [Vectors](linear-algebra.vectors.md) - - [Vectors on commutative rings](linear-algebra.vectors-on-commutative-rings.md) - - [Vectors on commutative semirings](linear-algebra.vectors-on-commutative-semirings.md) - - [Vectors on rings](linear-algebra.vectors-on-rings.md) - - [Vectors on semirings](linear-algebra.vectors-on-semirings.md) - -- [Order theory](order-theory.md) - - [Chains posets](order-theory.chains-posets.md) - - [Chains preorders](order-theory.chains-preorders.md) - - [Decidable subposets](order-theory.decidable-subposets.md) - - [Decidable subpreorders](order-theory.decidable-subpreorders.md) - - [Directed complete posets](order-theory.directed-complete-posets.md) - - [Directed families](order-theory.directed-families.md) - - [Distributive lattices](order-theory.distributive-lattices.md) - - [Finite posets](order-theory.finite-posets.md) - - [Finite preorders](order-theory.finite-preorders.md) - - [Finitely graded posets](order-theory.finitely-graded-posets.md) - - [Frames](order-theory.frames.md) - - [Greatest lower bounds posets](order-theory.greatest-lower-bounds-posets.md) - - [Homomorphisms frames](order-theory.homomorphisms-frames.md) - - [Homomorphisms meet semilattices](order-theory.homomorphisms-meet-semilattices.md) - - [Homomorphisms meet sup lattices](order-theory.homomorphisms-meet-sup-lattices.md) - - [Homomorphisms sup lattices](order-theory.homomorphisms-sup-lattices.md) - - [Ideals preorders](order-theory.ideals-preorders.md) - - [Infinite distributive law](order-theory.infinite-distributive-law.md) - - [Interval subposets](order-theory.interval-subposets.md) - - [Join semilattices](order-theory.join-semilattices.md) - - [Large posets](order-theory.large-posets.md) - - [Large preorders](order-theory.large-preorders.md) - - [Largest elements posets](order-theory.largest-elements-posets.md) - - [Largest elements preorders](order-theory.largest-elements-preorders.md) - - [Lattices](order-theory.lattices.md) - - [Least elements posets](order-theory.least-elements-posets.md) - - [Least elements preorders](order-theory.least-elements-preorders.md) - - [Least upper bounds posets](order-theory.least-upper-bounds-posets.md) - - [Locally finite posets](order-theory.locally-finite-posets.md) - - [Lower types preorders](order-theory.lower-types-preorders.md) - - [Maximal chains posets](order-theory.maximal-chains-posets.md) - - [Maximal chains preorders](order-theory.maximal-chains-preorders.md) - - [Meet semilattices](order-theory.meet-semilattices.md) - - [Order preserving maps posets](order-theory.order-preserving-maps-posets.md) - - [Order preserving maps preorders](order-theory.order-preserving-maps-preorders.md) - - [Planar binary trees](order-theory.planar-binary-trees.md) - - [Posets](order-theory.posets.md) - - [Preorders](order-theory.preorders.md) - - [Subposets](order-theory.subposets.md) - - [Subpreorders](order-theory.subpreorders.md) - - [Sup lattices](order-theory.sup-lattices.md) - - [Total posets](order-theory.total-posets.md) - - [Total preorders](order-theory.total-preorders.md) - -- [Organic chemistry](organic-chemistry.md) - - [Alcohols](organic-chemistry.alcohols.md) - - [Alkanes](organic-chemistry.alkanes.md) - - [Alkenes](organic-chemistry.alkenes.md) - - [Alkynes](organic-chemistry.alkynes.md) - - [Ethane](organic-chemistry.ethane.md) - - [Hydrocarbons](organic-chemistry.hydrocarbons.md) - - [Methane](organic-chemistry.methane.md) - - [Saturated carbons](organic-chemistry.saturated-carbons.md) - -- [Orthogonal factorization systems](orthogonal-factorization-systems.md) - - [Extensions of maps](orthogonal-factorization-systems.extensions-of-maps.md) - - [Factorization operations](orthogonal-factorization-systems.factorization-operations.md) - - [Factorizations of maps](orthogonal-factorization-systems.factorizations-of-maps.md) - - [Function classes](orthogonal-factorization-systems.function-classes.md) - - [Higher modalities](orthogonal-factorization-systems.higher-modalities.md) - - [Lifting operations](orthogonal-factorization-systems.lifting-operations.md) - - [Lifting squares](orthogonal-factorization-systems.lifting-squares.md) - - [Lifts of maps](orthogonal-factorization-systems.lifts-of-maps.md) - - [Local types](orthogonal-factorization-systems.local-types.md) - - [Mere lifting properties](orthogonal-factorization-systems.mere-lifting-properties.md) - - [Modal operators](orthogonal-factorization-systems.modal-operators.md) - - [Orthogonal factorization systems](orthogonal-factorization-systems.orthogonal-factorization-systems.md) - - [Orthogonal maps](orthogonal-factorization-systems.orthogonal-maps.md) - - [Pullback-hom](orthogonal-factorization-systems.pullback-hom.md) - - [Reflective subuniverses](orthogonal-factorization-systems.reflective-subuniverses.md) - - [Uniquely eliminating modalities](orthogonal-factorization-systems.uniquely-eliminating-modalities.md) - - [Wide function classes](orthogonal-factorization-systems.wide-function-classes.md) - -- [Polytopes](polytopes.md) - - [Abstract polytopes](polytopes.abstract-polytopes.md) - -- [Ring theory](ring-theory.md) - - [Algebras of rings](ring-theory.algebras-rings.md) - - [Binomial theorem for rings](ring-theory.binomial-theorem-rings.md) - - [Binomial theorem for semirings](ring-theory.binomial-theorem-semirings.md) - - [Congruence relations on rings](ring-theory.congruence-relations-rings.md) - - [Congruence relations on semirings](ring-theory.congruence-relations-semirings.md) - - [Dependent products of rings](ring-theory.dependent-products-rings.md) - - [Division rings](ring-theory.division-rings.md) - - [Homomorphisms of rings](ring-theory.homomorphisms-rings.md) - - [Ideals generated by subsets of rings](ring-theory.ideals-generated-by-subsets-rings.md) - - [Ideals in rings](ring-theory.ideals-rings.md) - - [Idempotent elements in rings](ring-theory.idempotent-elements-rings.md) - - [Invariant basis property of rings](ring-theory.invariant-basis-property-rings.md) - - [Invertible elements in rings](ring-theory.invertible-elements-rings.md) - - [Isomorphisms of rings](ring-theory.isomorphisms-rings.md) - - [Local rings](ring-theory.local-rings.md) - - [Localizations of rings](ring-theory.localizations-rings.md) - - [Maximal ideals in rings](ring-theory.maximal-ideals-rings.md) - - [Modules of rings](ring-theory.modules-rings.md) - - [Nil ideals in rings](ring-theory.nil-ideals-rings.md) - - [Nilpotent elements in rings](ring-theory.nilpotent-elements-rings.md) - - [Nontrivial rings](ring-theory.nontrivial-rings.md) - - [Opposite rings](ring-theory.opposite-rings.md) - - [Powers of elements in rings](ring-theory.powers-of-elements-rings.md) - - [Powers of elements in semirings](ring-theory.powers-of-elements-semirings.md) - - [Products rings](ring-theory.products-rings.md) - - [Quotient rings](ring-theory.quotient-rings.md) - - [Radical ideals in rings](ring-theory.radical-ideals-rings.md) - - [Rings](ring-theory.rings.md) - - [Semirings](ring-theory.semirings.md) - - [Subsets of rings](ring-theory.subsets-rings.md) - - [Sums of elements in rings](ring-theory.sums-rings.md) - - [Sums of elements in semirings](ring-theory.sums-semirings.md) - -- [Set theory](set-theory.md) - - [Baire space](set-theory.baire-space.md) - - [Cantor space](set-theory.cantor-space.md) - - [Cardinalities](set-theory.cardinalities.md) - - [Countable sets](set-theory.countable-sets.md) - - [Cumulative hierarchy](set-theory.cumulative-hierarchy.md) - - [Infinite sets](set-theory.infinite-sets.md) - - [Uncountable sets](set-theory.uncountable-sets.md) - -- [Structured types](structured-types.md) - - [Central h-spaces](structured-types.central-h-spaces.md) - - [Coherent h-spaces](structured-types.coherent-h-spaces.md) - - [Constant maps pointed types](structured-types.constant-maps-pointed-types.md) - - [Contractible pointed types](structured-types.contractible-pointed-types.md) - - [Equivalences types equipped with endomorphisms](structured-types.equivalences-types-equipped-with-endomorphisms.md) - - [Faithful pointed maps](structured-types.faithful-pointed-maps.md) - - [Fibers of pointed maps](structured-types.fibers-of-pointed-maps.md) - - [Finite multiplication magmas](structured-types.finite-multiplication-magmas.md) - - [h-spaces](structured-types.h-spaces.md) - - [Initial pointed type equipped with automorphism](structured-types.initial-pointed-type-equipped-with-automorphism.md) - - [Involutive type of h-space structures](structured-types.involutive-type-of-h-space-structures.md) - - [Involutive types](structured-types.involutive-types.md) - - [Magmas](structured-types.magmas.md) - - [Mere equivalences types equipped with endomorphisms](structured-types.mere-equivalences-types-equipped-with-endomorphisms.md) - - [Morphisms coherent h-spaces](structured-types.morphisms-coherent-h-spaces.md) - - [Morphisms magmas](structured-types.morphisms-magmas.md) - - [Morphisms types equipped with endomorphisms](structured-types.morphisms-types-equipped-with-endomorphisms.md) - - [Pointed dependent functions](structured-types.pointed-dependent-functions.md) - - [Pointed equivalences](structured-types.pointed-equivalences.md) - - [Pointed families of types](structured-types.pointed-families-of-types.md) - - [Pointed homotopies](structured-types.pointed-homotopies.md) - - [Pointed maps](structured-types.pointed-maps.md) - - [Pointed sections](structured-types.pointed-sections.md) - - [Pointed types equipped with automorphisms](structured-types.pointed-types-equipped-with-automorphisms.md) - - [Pointed types](structured-types.pointed-types.md) - - [Symmetric elements involutive types](structured-types.symmetric-elements-involutive-types.md) - - [Symmetric h-spaces](structured-types.symmetric-h-spaces.md) - - [Types equipped with automorphisms](structured-types.types-equipped-with-automorphisms.md) - - [Types equipped with endomorphisms](structured-types.types-equipped-with-endomorphisms.md) - - [Universal property lists wild monoids](structured-types.universal-property-lists-wild-monoids.md) - - [Unpointed maps](structured-types.unpointed-maps.md) - - [Wild groups](structured-types.wild-groups.md) - - [Wild loops](structured-types.wild-loops.md) - - [Wild monoids](structured-types.wild-monoids.md) - - [Wild quasigroups](structured-types.wild-quasigroups.md) - - [Wild semigroups](structured-types.wild-semigroups.md) - -- [Synthetic homotopy theory](synthetic-homotopy-theory.md) - - [24-pushouts](synthetic-homotopy-theory.24-pushouts.md) - - [26-descent](synthetic-homotopy-theory.26-descent.md) - - [26-id pushout](synthetic-homotopy-theory.26-id-pushout.md) - - [27-sequences](synthetic-homotopy-theory.27-sequences.md) - - [Circle](synthetic-homotopy-theory.circle.md) - - [Cocones pushouts](synthetic-homotopy-theory.cocones-pushouts.md) - - [Cofibers](synthetic-homotopy-theory.cofibers.md) - - [Descent circle](synthetic-homotopy-theory.descent-circle.md) - - [Double loop spaces](synthetic-homotopy-theory.double-loop-spaces.md) - - [Free loops](synthetic-homotopy-theory.free-loops.md) - - [Functoriality loop spaces](synthetic-homotopy-theory.functoriality-loop-spaces.md) - - [Groups of loops in-1-types](synthetic-homotopy-theory.groups-of-loops-in-1-types.md) - - [Infinite complex projective space](synthetic-homotopy-theory.infinite-complex-projective-space.md) - - [Infinite cyclic types](synthetic-homotopy-theory.infinite-cyclic-types.md) - - [Interval type](synthetic-homotopy-theory.interval-type.md) - - [Iterated loop spaces](synthetic-homotopy-theory.iterated-loop-spaces.md) - - [Joins of types](synthetic-homotopy-theory.joins-of-types.md) - - [Loop spaces](synthetic-homotopy-theory.loop-spaces.md) - - [Multiplication circle](synthetic-homotopy-theory.multiplication-circle.md) - - [Prespectra](synthetic-homotopy-theory.prespectra.md) - - [Pushouts](synthetic-homotopy-theory.pushouts.md) - - [Spectra](synthetic-homotopy-theory.spectra.md) - - [Spheres](synthetic-homotopy-theory.spheres.md) - - [Suspensions of types](synthetic-homotopy-theory.suspensions-of-types.md) - - [Triple loop spaces](synthetic-homotopy-theory.triple-loop-spaces.md) - - [Universal cover circle](synthetic-homotopy-theory.universal-cover-circle.md) - - [Universal property circle](synthetic-homotopy-theory.universal-property-circle.md) - - [Universal property pushouts](synthetic-homotopy-theory.universal-property-pushouts.md) - - [Wedges of pointed types](synthetic-homotopy-theory.wedges-of-pointed-types.md) - -- [Trees](trees.md) - - [Directed trees](trees.directed-trees.md) - - [Elementhood relation W-types](trees.elementhood-relation-w-types.md) - - [Enriched directed trees](trees.enriched-directed-trees.md) - - [Equivalences directed trees](trees.equivalences-directed-trees.md) - - [Equivalences enriched directed trees](trees.equivalences-enriched-directed-trees.md) - - [Extensional W-types](trees.extensional-w-types.md) - - [Functoriality W-types](trees.functoriality-w-types.md) - - [Indexed W-types](trees.indexed-w-types.md) - - [Induction W-types](trees.induction-w-types.md) - - [Inequality W-types](trees.inequality-w-types.md) - - [Lower types W-types](trees.lower-types-w-types.md) - - [Multisets](trees.multisets.md) - - [Ranks of elements W-types](trees.ranks-of-elements-w-types.md) - - [Rooted quasitrees](trees.rooted-quasitrees.md) - - [Rooted undirected trees](trees.rooted-undirected-trees.md) - - [Small multisets](trees.small-multisets.md) - - [Submultisets](trees.submultisets.md) - - [Transitive multisets](trees.transitive-multisets.md) - - [Underlying graphs of elements W-types](trees.underlying-graphs-of-elements-w-types.md) - - [Undirected trees](trees.undirected-trees.md) - - [Universal multiset](trees.universal-multiset.md) - - [W-type of natural numbers](trees.w-type-of-natural-numbers.md) - - [W-type of propositions](trees.w-type-of-propositions.md) - - [W-types](trees.w-types.md) - -- [Type theories](type-theories.md) - - [Comprehension type theories](type-theories.comprehension-type-theories.md) - - [Dependent type theories](type-theories.dependent-type-theories.md) - - [Fibered dependent type theories](type-theories.fibered-dependent-type-theories.md) - - [Sections dependent type theories](type-theories.sections-dependent-type-theories.md) - - [Simple type theories](type-theories.simple-type-theories.md) - - [Unityped type theories](type-theories.unityped-type-theories.md) - -- [Univalent combinatorics](univalent-combinatorics.md) - - [2-element decidable subtypes](univalent-combinatorics.2-element-decidable-subtypes.md) - - [2-element subtypes](univalent-combinatorics.2-element-subtypes.md) - - [2-element types](univalent-combinatorics.2-element-types.md) - - [Binomial types](univalent-combinatorics.binomial-types.md) - - [Bracelets](univalent-combinatorics.bracelets.md) - - [Cartesian product types](univalent-combinatorics.cartesian-product-types.md) - - [Cartesian products species](univalent-combinatorics.cartesian-products-species.md) - - [Classical finite types](univalent-combinatorics.classical-finite-types.md) - - [Complements isolated points](univalent-combinatorics.complements-isolated-points.md) - - [Composition species](univalent-combinatorics.composition-species.md) - - [Coproduct types](univalent-combinatorics.coproduct-types.md) - - [Coproducts species](univalent-combinatorics.coproducts-species.md) - - [Counting decidable subtypes](univalent-combinatorics.counting-decidable-subtypes.md) - - [Counting dependent pair types](univalent-combinatorics.counting-dependent-pair-types.md) - - [Counting fibers of maps](univalent-combinatorics.counting-fibers-of-maps.md) - - [Counting maybe](univalent-combinatorics.counting-maybe.md) - - [Counting](univalent-combinatorics.counting.md) - - [Cubes](univalent-combinatorics.cubes.md) - - [Cycle index series species](univalent-combinatorics.cycle-index-series-species.md) - - [Cycle partitions](univalent-combinatorics.cycle-partitions.md) - - [Cyclic types](univalent-combinatorics.cyclic-types.md) - - [Decidable dependent function types](univalent-combinatorics.decidable-dependent-function-types.md) - - [Decidable dependent pair types](univalent-combinatorics.decidable-dependent-pair-types.md) - - [Decidable equivalence relations](univalent-combinatorics.decidable-equivalence-relations.md) - - [Decidable propositions](univalent-combinatorics.decidable-propositions.md) - - [Decidable subtypes](univalent-combinatorics.decidable-subtypes.md) - - [Dedekind finite sets](univalent-combinatorics.dedekind-finite-sets.md) - - [Dependent function types](univalent-combinatorics.dependent-function-types.md) - - [Dependent sum finite types](univalent-combinatorics.dependent-sum-finite-types.md) - - [Derivatives species](univalent-combinatorics.derivatives-species.md) - - [Distributivity of set truncation over finite products](univalent-combinatorics.distributivity-of-set-truncation-over-finite-products.md) - - [Double counting](univalent-combinatorics.double-counting.md) - - [Embeddings standard finite types](univalent-combinatorics.embeddings-standard-finite-types.md) - - [Embeddings](univalent-combinatorics.embeddings.md) - - [Equality finite types](univalent-combinatorics.equality-finite-types.md) - - [Equality standard finite types](univalent-combinatorics.equality-standard-finite-types.md) - - [Equivalences cubes](univalent-combinatorics.equivalences-cubes.md) - - [Equivalences species](univalent-combinatorics.equivalences-species.md) - - [Equivalences standard finite types](univalent-combinatorics.equivalences-standard-finite-types.md) - - [Equivalences](univalent-combinatorics.equivalences.md) - - [Exponents species](univalent-combinatorics.exponents-species.md) - - [Ferrers diagrams](univalent-combinatorics.ferrers-diagrams.md) - - [Fibers of maps](univalent-combinatorics.fibers-of-maps.md) - - [Finite choice](univalent-combinatorics.finite-choice.md) - - [Finite connected components](univalent-combinatorics.finite-connected-components.md) - - [Finite presentations](univalent-combinatorics.finite-presentations.md) - - [Finite species](univalent-combinatorics.finite-species.md) - - [Finite types](univalent-combinatorics.finite-types.md) - - [Finitely presented types](univalent-combinatorics.finitely-presented-types.md) - - [Function types](univalent-combinatorics.function-types.md) - - [Image of maps](univalent-combinatorics.image-of-maps.md) - - [Inequality types with counting](univalent-combinatorics.inequality-types-with-counting.md) - - [Inhabited finite types](univalent-combinatorics.inhabited-finite-types.md) - - [Injective maps](univalent-combinatorics.injective-maps.md) - - [Involution on the standard finite types](univalent-combinatorics.involution-standard-finite-types.md) - - [Isotopies latin squares](univalent-combinatorics.isotopies-latin-squares.md) - - [Kuratowsky finite sets](univalent-combinatorics.kuratowsky-finite-sets.md) - - [Latin squares](univalent-combinatorics.latin-squares.md) - - [Lists](univalent-combinatorics.lists.md) - - [Main classes of latin hypercubes](univalent-combinatorics.main-classes-of-latin-hypercubes.md) - - [Main classes of latin squares](univalent-combinatorics.main-classes-of-latin-squares.md) - - [Maybe](univalent-combinatorics.maybe.md) - - [Morphisms finite species](univalent-combinatorics.morphisms-finite-species.md) - - [Morphisms species](univalent-combinatorics.morphisms-species.md) - - [Necklaces](univalent-combinatorics.necklaces.md) - - [Orientations complete undirected graph](univalent-combinatorics.orientations-complete-undirected-graph.md) - - [Orientations cubes](univalent-combinatorics.orientations-cubes.md) - - [Partitions](univalent-combinatorics.partitions.md) - - [Petri nets](univalent-combinatorics.petri-nets.md) - - [Pi finite types](univalent-combinatorics.pi-finite-types.md) - - [Pigeonhole principle](univalent-combinatorics.pigeonhole-principle.md) - - [Pointing species](univalent-combinatorics.pointing-species.md) - - [Precategory of finite species](univalent-combinatorics.precategory-of-finite-species.md) - - [Presented pi finite types](univalent-combinatorics.presented-pi-finite-types.md) - - [Quotients finite types](univalent-combinatorics.quotients-finite-types.md) - - [Ramsey theory](univalent-combinatorics.ramsey-theory.md) - - [Retracts of finite types](univalent-combinatorics.retracts-of-finite-types.md) - - [Sequences finite types](univalent-combinatorics.sequences-finite-types.md) - - [Set quotients of index two](univalent-combinatorics.set-quotients-of-index-two.md) - - [Sigma decompositions of finite types](univalent-combinatorics.sigma-decompositions.md) - - [Skipping element standard finite types](univalent-combinatorics.skipping-element-standard-finite-types.md) - - [Species](univalent-combinatorics.species.md) - - [Standard finite pruned trees](univalent-combinatorics.standard-finite-pruned-trees.md) - - [Standard finite trees](univalent-combinatorics.standard-finite-trees.md) - - [Standard finite types](univalent-combinatorics.standard-finite-types.md) - - [Steiner systems](univalent-combinatorics.steiner-systems.md) - - [Steiner triple systems](univalent-combinatorics.steiner-triple-systems.md) - - [Sums of natural numbers](univalent-combinatorics.sums-of-natural-numbers.md) - - [Surjective maps](univalent-combinatorics.surjective-maps.md) - - [Symmetric difference](univalent-combinatorics.symmetric-difference.md) - - [Universal property standard finite types](univalent-combinatorics.universal-property-standard-finite-types.md) - - [Unlabeled partitions](univalent-combinatorics.unlabeled-partitions.md) - - [Unlabeled rooted trees](univalent-combinatorics.unlabeled-rooted-trees.md) - - [Unlabeled structures species](univalent-combinatorics.unlabeled-structures-species.md) - - [Unlabeled trees](univalent-combinatorics.unlabeled-trees.md) +{{#include MODULE-INDEX.md}} diff --git a/hooks/generate_main_index_file.py b/hooks/generate_main_index_file.py new file mode 100755 index 0000000000..2a36290322 --- /dev/null +++ b/hooks/generate_main_index_file.py @@ -0,0 +1,79 @@ +#!/usr/bin/env python3 +# Run this script: +# $ python3 hooks/generate_main_index_file.py + +import os +import sys +import utils + +STATUS_FLAG_NO_TITLE = 1 +STATUS_FLAG_DUPLICATE_TITLE = 2 + +entry_template = '- [{title}]({mdfile})' + +def generate_namespace_entry_list(namespace): + status = 0 + modules = sorted(os.listdir(os.path.join(root, namespace))) + module_titles = tuple(map(lambda m: utils.get_lagda_file_title( + os.path.join(root, namespace, m)), modules)) + module_mdfiles = tuple( + map(lambda m: utils.get_module_mdfile(namespace, m), modules)) + + # Check for missing titles + for title, module in zip(module_titles, modules): + if title is None: + status |= STATUS_FLAG_NO_TITLE + print(f"WARNING! {namespace}.{module} no title was found") + + # Check duplicate titles + equal_titles = utils.get_equivalence_classes( + lambda tf1, tf2: tf1[0] == tf2[0], zip(module_titles, modules)) + equal_titles = tuple(filter(lambda ec: len( + ec) > 1 and ec[0][0] is not None, equal_titles)) + + if (len(equal_titles) > 0): + status |= STATUS_FLAG_DUPLICATE_TITLE + print(f"WARNING! Duplicate titles in {namespace}:") + for ec in equal_titles: + print( + f" Title '{ec[0][0]}': {', '.join(m[1][:m.rfind('.lagda.md')] for m in ec)}") + + module_titles_and_mdfiles = sorted( + zip(module_titles, module_mdfiles), key=lambda tm: (tm[0].casefold(), tm[1])) + + entry_list = (' ' + entry_template.format(title=t, mdfile=md) + for t, md in module_titles_and_mdfiles) + + namespace_title = utils.get_lagda_file_title( + os.path.join(root, namespace) + ".lagda.md") + namespace_entry = entry_template.format( + title=namespace_title, mdfile=namespace + ".md") + + namespace_entry_list = namespace_entry + "\n" + "\n".join(entry_list) + return namespace_entry_list, status + +def generate_index(root, header): + status = 0 + entry_lists = [] + for namespace in sorted(utils.get_subdirectories_recursive(root)): + entry_list, s = generate_namespace_entry_list(namespace) + entry_lists.append(entry_list) + status |= s + + index = f"{header}\n\n" + "\n\n".join(entry_lists) + "\n" + return index, status + +if __name__ == "__main__": + + status = 0 + root = "src" + + index_path = "MODULE-INDEX.md" + index_header = "# Formalisation in Agda" + + index_content, status = generate_index(root, index_header) + + with open(index_path, "w") as index_file: + index_file.write(index_content) + + sys.exit(status) diff --git a/hooks/generate_namespace_index_modules.py b/hooks/generate_namespace_index_modules.py new file mode 100755 index 0000000000..b8a3fde7f7 --- /dev/null +++ b/hooks/generate_namespace_index_modules.py @@ -0,0 +1,79 @@ +#!/usr/bin/env python3 +# Run this script: +# $ python3 hooks/generate_namespace_index_modules.py + +import os +import pathlib +import sys +import utils + +def generate_title(namespace): + return "# " + namespace.capitalize().replace("-", " ") + "\n" + +def generate_imports(root, namespace): + namespace_path = os.path.join(root, namespace) + agda_file_filter = lambda f: utils.isAgdaFile(pathlib.Path(os.path.join(namespace_path, f))) + namespace_files = filter(agda_file_filter, os.listdir(namespace_path)) + + import_statements = (utils.get_import_statement(namespace, module_file, public=True) for module_file in namespace_files) + return "\n".join(sorted(import_statements)) + +agda_block_template = \ + '''```agda +module {namespace} where + +{imports} +``` +''' + +def generate_agda_block(root, namespace): + return agda_block_template.format(namespace=namespace, imports=generate_imports(root, namespace)) + +if __name__ == "__main__": + + status = 0 + root = "src" + + for namespace in utils.get_subdirectories_recursive(root): + namespace_filename = os.path.join(root, namespace) + ".lagda.md" + with open(namespace_filename, "a+") as namespace_file: + pass + with open(namespace_filename, "r+") as namespace_file: + contents = namespace_file.read() + + oldcontents = contents + + title_index = contents.find("# ") + if title_index > 0: + print( + f"Warning! Namespace file {namespace_filename} has title after first line.") + elif title_index == -1: # Missing title. Generate it + contents = generate_title(namespace) + contents + + agda_block_start = contents.rfind("```agda\n") + + if agda_block_start == -1: + # Must add agda block + # Add at the end of the file + contents += "\n" + generate_agda_block(root, namespace) + else: + agda_block_end = contents.find( + "\n```\n", agda_block_start + len("```agda\n")) + generated_block = generate_agda_block(root, namespace) + + if agda_block_end == -1: + # An agda block is opened but not closed. + # This is an error, but we can fix it + print( + f"WARNING! agda-block was opened but not closed in {namespace_filename}.") + contents = contents[:agda_block_start] + generated_block + else: + agda_block_end += len("\n```\n") + contents = contents[:agda_block_start] + generated_block + contents[agda_block_end:] + + if oldcontents != contents: + status |= 1 + with open(namespace_filename, "w") as f: + f.write(contents) + + sys.exit(status) diff --git a/hooks/utils.py b/hooks/utils.py index f6f5f6fec0..90b61f528d 100644 --- a/hooks/utils.py +++ b/hooks/utils.py @@ -1,7 +1,8 @@ import pathlib as path +import os def find_index(s : str, t : str) -> list[int]: - return [p for p, c in enumerate(s) if c == t] + return [p for p, c in enumerate(s) if c == t] def isAgdaFile(f: path.Path) -> bool: return (f.match('*.lagda.md') and @@ -11,3 +12,35 @@ def isAgdaFile(f: path.Path) -> bool: def agdaFiles(files: list[str]) -> list[path.Path]: return list(filter(isAgdaFile, map(path.Path, files))) + +def get_subdirectories_recursive(startpath): + for root, dirs, files in os.walk(startpath): + yield from dirs + +def get_lagda_file_title(lagda_filepath): + with open(lagda_filepath, "r") as file: + contents = file.read() + title_index = contents.find("# ") + if title_index != 0: + return None + + title_start = title_index + len("# ") + title_end = contents.find("\n", len("# ")) + return contents[title_start:title_end] + +def get_import_statement(namespace, module_file, public=False): + return f"open import {namespace}.{module_file[:module_file.rfind('.lagda.md')]}{' public' * public}" + +def get_module_mdfile(namespace, module_file): + return namespace + "." + module_file.replace(".lagda.md", ".md") + +def get_equivalence_classes(equivalence_relation, iterable): + partitions = [] # Found partitions + for e in iterable: # Loop over each element + for p in partitions: + if equivalence_relation(e, p[0]): # Found a partition for it! + p.append(e) + break + else: # Make a new partition for it. + partitions.append([e]) + return partitions diff --git a/src/category-theory.lagda.md b/src/category-theory.lagda.md index 9efe359903..fb6f9f528b 100644 --- a/src/category-theory.lagda.md +++ b/src/category-theory.lagda.md @@ -9,6 +9,7 @@ open import category-theory.categories public open import category-theory.coproducts-precategories public open import category-theory.discrete-precategories public open import category-theory.endomorphisms-of-objects-categories public +open import category-theory.epimorphisms-large-precategories public open import category-theory.equivalences-categories public open import category-theory.equivalences-large-precategories public open import category-theory.equivalences-precategories public diff --git a/src/category-theory/exponential-objects-precategories.lagda.md b/src/category-theory/exponential-objects-precategories.lagda.md index a8f7ba485d..ff67fa8ef6 100644 --- a/src/category-theory/exponential-objects-precategories.lagda.md +++ b/src/category-theory/exponential-objects-precategories.lagda.md @@ -1,4 +1,4 @@ -# Products in precategories +# Exponential objects in precategories ```agda module category-theory.exponential-objects-precategories where diff --git a/src/elementary-number-theory.lagda.md b/src/elementary-number-theory.lagda.md index 8da1388885..6381d8243d 100644 --- a/src/elementary-number-theory.lagda.md +++ b/src/elementary-number-theory.lagda.md @@ -20,6 +20,7 @@ open import elementary-number-theory.commutative-ring-of-integers public open import elementary-number-theory.commutative-semiring-of-natural-numbers public open import elementary-number-theory.congruence-integers public open import elementary-number-theory.congruence-natural-numbers public +open import elementary-number-theory.decidable-dependent-function-types public open import elementary-number-theory.decidable-types public open import elementary-number-theory.difference-integers public open import elementary-number-theory.dirichlet-convolution public @@ -33,11 +34,13 @@ open import elementary-number-theory.equality-integers public open import elementary-number-theory.equality-natural-numbers public open import elementary-number-theory.euclidean-division-natural-numbers public open import elementary-number-theory.eulers-totient-function public +open import elementary-number-theory.exponentiation-natural-numbers public open import elementary-number-theory.factorials public open import elementary-number-theory.falling-factorials public open import elementary-number-theory.fibonacci-sequence public open import elementary-number-theory.finitary-natural-numbers public open import elementary-number-theory.finitely-cyclic-maps public +open import elementary-number-theory.fractions public open import elementary-number-theory.goldbach-conjecture public open import elementary-number-theory.greatest-common-divisor-integers public open import elementary-number-theory.greatest-common-divisor-natural-numbers public @@ -50,13 +53,14 @@ open import elementary-number-theory.inequality-standard-finite-types public open import elementary-number-theory.infinitude-of-primes public open import elementary-number-theory.integer-partitions public open import elementary-number-theory.integers public +open import elementary-number-theory.lower-bounds-natural-numbers public open import elementary-number-theory.maximum-natural-numbers public open import elementary-number-theory.maximum-standard-finite-types public open import elementary-number-theory.mersenne-primes public open import elementary-number-theory.minimum-natural-numbers public open import elementary-number-theory.minimum-standard-finite-types public -open import elementary-number-theory.modular-arithmetic-standard-finite-types public open import elementary-number-theory.modular-arithmetic public +open import elementary-number-theory.modular-arithmetic-standard-finite-types public open import elementary-number-theory.multiplication-integers public open import elementary-number-theory.multiplication-natural-numbers public open import elementary-number-theory.multiset-coefficients public @@ -76,11 +80,14 @@ open import elementary-number-theory.retracts-of-natural-numbers public open import elementary-number-theory.square-free-natural-numbers public open import elementary-number-theory.stirling-numbers-of-the-second-kind public open import elementary-number-theory.strong-induction-natural-numbers public +open import elementary-number-theory.sums-of-natural-numbers public open import elementary-number-theory.telephone-numbers public open import elementary-number-theory.triangular-numbers public open import elementary-number-theory.twin-prime-conjecture public open import elementary-number-theory.unit-elements-standard-finite-types public open import elementary-number-theory.unit-similarity-standard-finite-types public open import elementary-number-theory.universal-property-natural-numbers public +open import elementary-number-theory.upper-bounds-natural-numbers public open import elementary-number-theory.well-ordering-principle-natural-numbers public open import elementary-number-theory.well-ordering-principle-standard-finite-types public +``` diff --git a/src/finite-group-theory.lagda.md b/src/finite-group-theory.lagda.md index a03d25124a..2564b16cab 100644 --- a/src/finite-group-theory.lagda.md +++ b/src/finite-group-theory.lagda.md @@ -2,6 +2,7 @@ ```agda module finite-group-theory where + open import finite-group-theory.abstract-quaternion-group public open import finite-group-theory.alternating-concrete-groups public open import finite-group-theory.alternating-groups public diff --git a/src/foundation-core.lagda.md b/src/foundation-core.lagda.md index c604931647..29984d1fd8 100644 --- a/src/foundation-core.lagda.md +++ b/src/foundation-core.lagda.md @@ -31,6 +31,7 @@ open import foundation-core.equality-cartesian-product-types public open import foundation-core.equality-dependent-pair-types public open import foundation-core.equality-fibers-of-maps public open import foundation-core.equivalence-induction public +open import foundation-core.equivalence-relations public open import foundation-core.equivalences public open import foundation-core.faithful-maps public open import foundation-core.fibers-of-maps public diff --git a/src/foundation.lagda.md b/src/foundation.lagda.md index 36c873f20e..009273f330 100644 --- a/src/foundation.lagda.md +++ b/src/foundation.lagda.md @@ -17,6 +17,7 @@ open import foundation.bands public open import foundation.binary-embeddings public open import foundation.binary-equivalences public open import foundation.binary-equivalences-unordered-pairs-of-types public +open import foundation.binary-functoriality-set-quotients public open import foundation.binary-homotopies public open import foundation.binary-operations-unordered-pairs-of-types public open import foundation.binary-reflecting-maps-equivalence-relations public @@ -32,14 +33,16 @@ open import foundation.coherently-invertible-maps public open import foundation.commuting-3-simplices-of-homotopies public open import foundation.commuting-3-simplices-of-maps public open import foundation.commuting-cubes-of-maps public +open import foundation.commuting-squares-of-identifications public open import foundation.commuting-squares-of-maps public open import foundation.commuting-triangles-of-homotopies public open import foundation.commuting-triangles-of-maps public open import foundation.complements public open import foundation.complements-subtypes public +open import foundation.cones-pullbacks public open import foundation.conjunction public -open import foundation.connected-components-universes public open import foundation.connected-components public +open import foundation.connected-components-universes public open import foundation.connected-maps public open import foundation.connected-types public open import foundation.constant-maps public @@ -76,6 +79,7 @@ open import foundation.dubuc-penon-compact-types public open import foundation.effective-maps-equivalence-relations public open import foundation.embeddings public open import foundation.empty-types public +open import foundation.endomorphisms public open import foundation.epimorphisms-with-respect-to-sets public open import foundation.equality-cartesian-product-types public open import foundation.equality-coproduct-types public @@ -84,10 +88,11 @@ open import foundation.equality-dependent-pair-types public open import foundation.equality-fibers-of-maps public open import foundation.equational-reasoning public open import foundation.equivalence-classes public +open import foundation.equivalence-extensionality public open import foundation.equivalence-induction public open import foundation.equivalence-relations public -open import foundation.equivalences-maybe public open import foundation.equivalences public +open import foundation.equivalences-maybe public open import foundation.existential-quantification public open import foundation.exponents-set-quotients public open import foundation.faithful-maps public @@ -116,9 +121,10 @@ open import foundation.hexagons-of-identifications public open import foundation.hilberts-epsilon-operators public open import foundation.homotopies public open import foundation.identity-systems public +open import foundation.identity-truncated-types public open import foundation.identity-types public -open import foundation.images-subtypes public open import foundation.images public +open import foundation.images-subtypes public open import foundation.impredicative-encodings public open import foundation.impredicative-universes public open import foundation.induction-principle-propositional-truncation public @@ -175,10 +181,13 @@ open import foundation.pullbacks public open import foundation.raising-universe-levels public open import foundation.reflecting-maps-equivalence-relations public open import foundation.reflexive-relations public +open import foundation.repetitions public +open import foundation.repetitions-sequences public open import foundation.replacement public open import foundation.retractions public open import foundation.russells-paradox public open import foundation.sections public +open import foundation.sequences public open import foundation.set-presented-types public open import foundation.set-quotients public open import foundation.set-truncations public @@ -192,11 +201,10 @@ open import foundation.small-maps public open import foundation.small-types public open import foundation.small-universes public open import foundation.split-surjective-maps public -open import foundation.commuting-squares-of-identifications public open import foundation.standard-apartness-relations public open import foundation.strongly-extensional-maps public -open import foundation.structure-identity-principle public open import foundation.structure public +open import foundation.structure-identity-principle public open import foundation.subterminal-types public open import foundation.subtype-identity-principle public open import foundation.subtypes public @@ -230,8 +238,9 @@ open import foundation.uniqueness-set-quotients public open import foundation.uniqueness-set-truncations public open import foundation.uniqueness-truncation public open import foundation.unit-type public -open import foundation.univalence-implies-function-extensionality public +open import foundation.unital-binary-operations public open import foundation.univalence public +open import foundation.univalence-implies-function-extensionality public open import foundation.univalent-type-families public open import foundation.universal-property-booleans public open import foundation.universal-property-cartesian-product-types public @@ -242,8 +251,8 @@ open import foundation.universal-property-fiber-products public open import foundation.universal-property-identity-types public open import foundation.universal-property-image public open import foundation.universal-property-maybe public -open import foundation.universal-property-propositional-truncation-into-sets public open import foundation.universal-property-propositional-truncation public +open import foundation.universal-property-propositional-truncation-into-sets public open import foundation.universal-property-pullbacks public open import foundation.universal-property-set-quotients public open import foundation.universal-property-set-truncation public @@ -257,4 +266,5 @@ open import foundation.unordered-tuples-of-types public open import foundation.weak-function-extensionality public open import foundation.weak-limited-principle-of-omniscience public open import foundation.weakly-constant-maps public +open import foundation.xor public ``` diff --git a/src/foundation/dependent-paths.lagda.md b/src/foundation/dependent-paths.lagda.md index ae5589cc6d..c357b386cf 100644 --- a/src/foundation/dependent-paths.lagda.md +++ b/src/foundation/dependent-paths.lagda.md @@ -1,9 +1,5 @@ -<<<<<<< Updated upstream # Dependent paths -======= -# Dependent paths ->>>>>>> Stashed changes We characterize dependent paths in the family of depedent paths; define the groupoidal operators on dependent paths; define the cohrences paths: prove the operators are equivalences. diff --git a/src/foundation/functoriality-dependent-pair-types.lagda.md b/src/foundation/functoriality-dependent-pair-types.lagda.md index 9d3e67a5f0..cb7aaa4281 100644 --- a/src/foundation/functoriality-dependent-pair-types.lagda.md +++ b/src/foundation/functoriality-dependent-pair-types.lagda.md @@ -1,4 +1,4 @@ - Functoriality of dependent pair types +# Functoriality of dependent pair types ```agda module foundation.functoriality-dependent-pair-types where diff --git a/src/group-theory.lagda.md b/src/group-theory.lagda.md index 52da2a414b..e2c9a72730 100644 --- a/src/group-theory.lagda.md +++ b/src/group-theory.lagda.md @@ -19,6 +19,7 @@ open import group-theory.commutative-monoids public open import group-theory.commutators-groups public open import group-theory.concrete-group-actions public open import group-theory.concrete-groups public +open import group-theory.congruence-relations-abelian-groups public open import group-theory.congruence-relations-groups public open import group-theory.congruence-relations-monoids public open import group-theory.congruence-relations-semigroups public @@ -28,8 +29,10 @@ open import group-theory.decidable-subgroups public open import group-theory.dihedral-group-construction public open import group-theory.dihedral-groups public open import group-theory.e8-lattice public +open import group-theory.embeddings-abelian-groups public open import group-theory.embeddings-groups public open import group-theory.endomorphism-rings-abelian-groups public +open import group-theory.epimorphisms-groups public open import group-theory.equivalences-concrete-group-actions public open import group-theory.equivalences-concrete-groups public open import group-theory.equivalences-group-actions public @@ -49,6 +52,7 @@ open import group-theory.higher-groups public open import group-theory.homomorphisms-abelian-groups public open import group-theory.homomorphisms-concrete-group-actions public open import group-theory.homomorphisms-concrete-groups public +open import group-theory.homomorphisms-generated-subgroups public open import group-theory.homomorphisms-group-actions public open import group-theory.homomorphisms-groups public open import group-theory.homomorphisms-higher-group-actions public @@ -63,9 +67,9 @@ open import group-theory.isomorphisms-concrete-groups public open import group-theory.isomorphisms-group-actions public open import group-theory.isomorphisms-groups public open import group-theory.isomorphisms-semigroups public -open import group-theory.loop-groups-sets public open import group-theory.kernels public open import group-theory.kernels-homomorphisms-concrete-groups public +open import group-theory.loop-groups-sets public open import group-theory.mere-equivalences-concrete-group-actions public open import group-theory.mere-equivalences-group-actions public open import group-theory.monoid-actions public @@ -76,7 +80,6 @@ open import group-theory.normal-subgroups public open import group-theory.normal-subgroups-concrete-groups public open import group-theory.opposite-groups public open import group-theory.orbit-stabilizer-theorem-concrete-groups public -open import group-theory.orbits-monoid-actions public open import group-theory.orbits-concrete-group-actions public open import group-theory.orbits-group-actions public open import group-theory.orbits-higher-group-actions public @@ -91,6 +94,7 @@ open import group-theory.principal-torsors-concrete-groups public open import group-theory.products-of-tuples-of-elements-commutative-monoids public open import group-theory.quotient-groups public open import group-theory.quotient-groups-concrete-groups public +open import group-theory.quotients-abelian-groups public open import group-theory.representations-monoids public open import group-theory.semigroups public open import group-theory.sheargroups public diff --git a/src/linear-algebra.lagda.md b/src/linear-algebra.lagda.md index dc7da94cdd..fe3e5ea4b5 100644 --- a/src/linear-algebra.lagda.md +++ b/src/linear-algebra.lagda.md @@ -2,21 +2,22 @@ ```agda module linear-algebra where + open import linear-algebra.constant-matrices public open import linear-algebra.constant-vectors public open import linear-algebra.diagonal-matrices-on-rings public open import linear-algebra.functoriality-matrices public open import linear-algebra.functoriality-vectors public -open import linear-algebra.matrices-on-rings public open import linear-algebra.matrices public +open import linear-algebra.matrices-on-rings public open import linear-algebra.multiplication-matrices public open import linear-algebra.scalar-multiplication-matrices public open import linear-algebra.scalar-multiplication-vectors public open import linear-algebra.scalar-multiplication-vectors-on-rings public open import linear-algebra.transposition-matrices public +open import linear-algebra.vectors public open import linear-algebra.vectors-on-commutative-rings public open import linear-algebra.vectors-on-commutative-semirings public open import linear-algebra.vectors-on-rings public open import linear-algebra.vectors-on-semirings public -open import linear-algebra.vectors public ``` diff --git a/src/order-theory.lagda.md b/src/order-theory.lagda.md index e3f315fbd6..5df02c5a85 100644 --- a/src/order-theory.lagda.md +++ b/src/order-theory.lagda.md @@ -22,12 +22,15 @@ open import order-theory.homomorphisms-sup-lattices public open import order-theory.ideals-preorders public open import order-theory.infinite-distributive-law public open import order-theory.interval-subposets public +open import order-theory.join-semilattices public open import order-theory.large-posets public open import order-theory.large-preorders public open import order-theory.largest-elements-posets public open import order-theory.largest-elements-preorders public +open import order-theory.lattices public open import order-theory.least-elements-posets public open import order-theory.least-elements-preorders public +open import order-theory.least-upper-bounds-posets public open import order-theory.locally-finite-posets public open import order-theory.lower-types-preorders public open import order-theory.maximal-chains-posets public @@ -38,9 +41,9 @@ open import order-theory.order-preserving-maps-preorders public open import order-theory.planar-binary-trees public open import order-theory.posets public open import order-theory.preorders public -open import order-theory.sup-lattices public open import order-theory.subposets public open import order-theory.subpreorders public +open import order-theory.sup-lattices public open import order-theory.total-posets public open import order-theory.total-preorders public ``` diff --git a/src/organic-chemistry.lagda.md b/src/organic-chemistry.lagda.md index cdf435f032..4fc2d7f2e2 100644 --- a/src/organic-chemistry.lagda.md +++ b/src/organic-chemistry.lagda.md @@ -3,12 +3,12 @@ ```agda module organic-chemistry where -open import organic-chemistry.hydrocarbons public open import organic-chemistry.alcohols public -open import organic-chemistry.saturated-carbons public open import organic-chemistry.alkanes public open import organic-chemistry.alkenes public open import organic-chemistry.alkynes public -open import organic-chemistry.methane public open import organic-chemistry.ethane public +open import organic-chemistry.hydrocarbons public +open import organic-chemistry.methane public +open import organic-chemistry.saturated-carbons public ``` diff --git a/src/organic-chemistry/alkenes.lagda.md b/src/organic-chemistry/alkenes.lagda.md index c921af986d..4518449ac2 100644 --- a/src/organic-chemistry/alkenes.lagda.md +++ b/src/organic-chemistry/alkenes.lagda.md @@ -1,4 +1,4 @@ -# Alkynes +# Alkenes ```agda module organic-chemistry.alkenes where diff --git a/src/polytopes.lagda.md b/src/polytopes.lagda.md index a10e37e693..d6d1fa0326 100644 --- a/src/polytopes.lagda.md +++ b/src/polytopes.lagda.md @@ -2,5 +2,6 @@ ```agda module polytopes where + open import polytopes.abstract-polytopes public ``` diff --git a/src/ring-theory.lagda.md b/src/ring-theory.lagda.md index 15bb862b03..b2c67312a2 100644 --- a/src/ring-theory.lagda.md +++ b/src/ring-theory.lagda.md @@ -6,6 +6,8 @@ module ring-theory where open import ring-theory.algebras-rings public open import ring-theory.binomial-theorem-rings public open import ring-theory.binomial-theorem-semirings public +open import ring-theory.congruence-relations-rings public +open import ring-theory.congruence-relations-semirings public open import ring-theory.dependent-products-rings public open import ring-theory.division-rings public open import ring-theory.homomorphisms-rings public diff --git a/src/structured-types.lagda.md b/src/structured-types.lagda.md index 9ab5142e35..5553c12dd5 100644 --- a/src/structured-types.lagda.md +++ b/src/structured-types.lagda.md @@ -2,6 +2,7 @@ ```agda module structured-types where + open import structured-types.central-h-spaces public open import structured-types.coherent-h-spaces public open import structured-types.constant-maps-pointed-types public @@ -24,13 +25,15 @@ open import structured-types.pointed-equivalences public open import structured-types.pointed-families-of-types public open import structured-types.pointed-homotopies public open import structured-types.pointed-maps public -open import structured-types.pointed-types-equipped-with-automorphisms public +open import structured-types.pointed-sections public open import structured-types.pointed-types public +open import structured-types.pointed-types-equipped-with-automorphisms public open import structured-types.symmetric-elements-involutive-types public open import structured-types.symmetric-h-spaces public open import structured-types.types-equipped-with-automorphisms public open import structured-types.types-equipped-with-endomorphisms public open import structured-types.universal-property-lists-wild-monoids public +open import structured-types.unpointed-maps public open import structured-types.wild-groups public open import structured-types.wild-loops public open import structured-types.wild-monoids public diff --git a/src/synthetic-homotopy-theory/24-pushouts.lagda.md b/src/synthetic-homotopy-theory/24-pushouts.lagda.md index 829603f3f6..27da5fc4b3 100644 --- a/src/synthetic-homotopy-theory/24-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/24-pushouts.lagda.md @@ -1,4 +1,4 @@ -# Formalisation of the Symmetry Book +# Formalisation of the Symmetry Book - 24 pushouts ```agda module synthetic-homotopy-theory.24-pushouts where diff --git a/src/synthetic-homotopy-theory/26-descent.lagda.md b/src/synthetic-homotopy-theory/26-descent.lagda.md index 669aa33015..7711cea239 100644 --- a/src/synthetic-homotopy-theory/26-descent.lagda.md +++ b/src/synthetic-homotopy-theory/26-descent.lagda.md @@ -1,4 +1,4 @@ -# Formalisation of the Symmetry Book +# Formalisation of the Symmetry Book - 26 descent ```agda module synthetic-homotopy-theory.26-descent where diff --git a/src/synthetic-homotopy-theory/26-id-pushout.lagda.md b/src/synthetic-homotopy-theory/26-id-pushout.lagda.md index 6a366d7e74..6380ff5f9a 100644 --- a/src/synthetic-homotopy-theory/26-id-pushout.lagda.md +++ b/src/synthetic-homotopy-theory/26-id-pushout.lagda.md @@ -1,4 +1,4 @@ -# Formalisation of the Symmetry Book +# Formalisation of the Symmetry Book - 26 id pushout ```agda module synthetic-homotopy-theory.26-id-pushout where diff --git a/src/synthetic-homotopy-theory/27-sequences.lagda.md b/src/synthetic-homotopy-theory/27-sequences.lagda.md index 36071e6a40..0fc3bf2544 100644 --- a/src/synthetic-homotopy-theory/27-sequences.lagda.md +++ b/src/synthetic-homotopy-theory/27-sequences.lagda.md @@ -1,4 +1,4 @@ -# Formalisation of the Symmetry Book +# Formalisation of the Symmetry Book - 27 sequences ```agda module synthetic-homotopy-theory.27-sequences where diff --git a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md index 26974cd40d..f7be53388e 100644 --- a/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md +++ b/src/synthetic-homotopy-theory/universal-cover-circle.lagda.md @@ -1,4 +1,4 @@ -# Formalisation of the Symmetry Book +# The universal cover of the circle ```agda module synthetic-homotopy-theory.universal-cover-circle where diff --git a/src/trees.lagda.md b/src/trees.lagda.md index 3871122f14..b2654c72bd 100644 --- a/src/trees.lagda.md +++ b/src/trees.lagda.md @@ -27,3 +27,4 @@ open import trees.universal-multiset public open import trees.w-type-of-natural-numbers public open import trees.w-type-of-propositions public open import trees.w-types public +``` diff --git a/src/type-theories.lagda.md b/src/type-theories.lagda.md index cada167b77..2c7fded60a 100644 --- a/src/type-theories.lagda.md +++ b/src/type-theories.lagda.md @@ -2,7 +2,9 @@ ```agda {-# OPTIONS --guardedness #-} +``` +```agda module type-theories where open import type-theories.comprehension-type-theories public diff --git a/src/univalent-combinatorics.lagda.md b/src/univalent-combinatorics.lagda.md index df66f8545b..eb19bb4e83 100644 --- a/src/univalent-combinatorics.lagda.md +++ b/src/univalent-combinatorics.lagda.md @@ -19,11 +19,11 @@ open import univalent-combinatorics.complements-isolated-points public open import univalent-combinatorics.composition-species public open import univalent-combinatorics.coproduct-types public open import univalent-combinatorics.coproducts-species public +open import univalent-combinatorics.counting public open import univalent-combinatorics.counting-decidable-subtypes public open import univalent-combinatorics.counting-dependent-pair-types public open import univalent-combinatorics.counting-fibers-of-maps public open import univalent-combinatorics.counting-maybe public -open import univalent-combinatorics.counting public open import univalent-combinatorics.cubes public open import univalent-combinatorics.cycle-index-series-species public open import univalent-combinatorics.cycle-partitions public @@ -39,14 +39,14 @@ open import univalent-combinatorics.dependent-sum-finite-types public open import univalent-combinatorics.derivatives-species public open import univalent-combinatorics.distributivity-of-set-truncation-over-finite-products public open import univalent-combinatorics.double-counting public -open import univalent-combinatorics.embeddings-standard-finite-types public open import univalent-combinatorics.embeddings public +open import univalent-combinatorics.embeddings-standard-finite-types public open import univalent-combinatorics.equality-finite-types public open import univalent-combinatorics.equality-standard-finite-types public +open import univalent-combinatorics.equivalences public open import univalent-combinatorics.equivalences-cubes public open import univalent-combinatorics.equivalences-species public open import univalent-combinatorics.equivalences-standard-finite-types public -open import univalent-combinatorics.equivalences public open import univalent-combinatorics.exponents-species public open import univalent-combinatorics.ferrers-diagrams public open import univalent-combinatorics.fibers-of-maps public diff --git a/src/univalent-combinatorics/steiner-systems.lagda.md b/src/univalent-combinatorics/steiner-systems.lagda.md index 375ff7a34a..ce6e35e77e 100644 --- a/src/univalent-combinatorics/steiner-systems.lagda.md +++ b/src/univalent-combinatorics/steiner-systems.lagda.md @@ -1,4 +1,4 @@ -# Steiner triple systems +# Steiner systems ```agda module univalent-combinatorics.steiner-systems where