A small optimization to equivalence relations

[fredrik-bakke]

• Makes equivalence relations typecheck in about half the time. I also had a look at category-of-functors-from-small-to-large-categories, and I really can't find anything wrong, so I'm a bit puzzled.
• Adds a make hook for more streamlined profiling of individual modules.

[fredrik-bakke]

I tried typechecking the whole library with the flag --lossy-unification set globally, comparing it to not having it set. Here are the details. Turns out there's not much to gain, but it did perform a little better in a few select files. I'm guessing this is likely by chance, however.

```csv name,unit,lossy-unification,no-lossy-unification memory_allocated_in_heap,MiB,1162753,1162755 memory_copied_during_GC,MiB,84076,83809 maximum_residency,MiB,1579,1576 memory_maximum_slop,KiB,1836,1666 total_memory_in_use,MiB,3160,3154 Total,ms,395798,396995 Miscellaneous,ms,13183,13206 category-theory.category-of-functors-from-small-to-large-categories,ms,10724,10818 univalent-combinatorics.orientations-complete-undirected-graph,ms,7962,7964 finite-group-theory.orbits-permutations,ms,6973,6811 foundation.equivalence-relations,ms,6711,6713 finite-group-theory.delooping-sign-homomorphism,ms,6441,6333 foundation.pullbacks,ms,5670,5630 category-theory.category-of-maps-from-small-to-large-categories,ms,5183,5288 foundation.commuting-cubes-of-maps,ms,3587,3566 finite-group-theory.transpositions,ms,3276,3301 everything,ms,3179,3275 foundation-core.pullbacks,ms,2981,2787 synthetic-homotopy-theory.universal-property-pushouts,ms,2911,2774 foundation.commuting-prisms-of-maps,ms,2593,2665 universal-algebra.quotient-algebras,ms,2511,2529 elementary-number-theory.bezouts-lemma-natural-numbers,ms,2352,2264 univalent-combinatorics.2-element-decidable-subtypes,ms,2015,2110 univalent-combinatorics.counting-dependent-pair-types,ms,2043,2101 orthogonal-factorization-systems.orthogonal-maps,ms,2034,2067 foundation-core.coherently-invertible-maps,ms,1890,2062 foundation.commuting-squares-of-maps,ms,2163,2024 foundation.functoriality-dependent-pair-types,ms,1782,1976 univalent-combinatorics.pi-finite-types,ms,1950,1876 type-theories.dependent-type-theories,ms,1825,1823 synthetic-homotopy-theory.functoriality-sequential-colimits,ms,1754,1749 univalent-combinatorics.2-element-types,ms,1597,1649 foundation.homotopies-morphisms-arrows,ms,1444,1436 finite-group-theory.simpson-delooping-sign-homomorphism,ms,1396,1410 trees.underlying-trees-elements-coalgebras-polynomial-endofunctors,ms,1407,1403 category-theory.slice-precategories,ms,1461,1394 synthetic-homotopy-theory.flattening-lemma-pushouts,ms,1205,1375 type-theories.fibered-dependent-type-theories,ms,1340,1342 foundation.yoneda-identity-types,ms,1293,1308 foundation.retracts-of-maps,ms,1442,1307 univalent-combinatorics.binomial-types,ms,1303,1289 foundation.universal-property-set-quotients,ms,1158,1266 foundation-core.commuting-squares-of-homotopies,ms,1257,1251 synthetic-homotopy-theory.26-id-pushout,ms,1209,1220 foundation.functoriality-fibers-of-maps,ms,1149,1204 type-theories.simple-type-theories,ms,1119,1196 orthogonal-factorization-systems.modal-subuniverse-induction,ms,1117,1169 synthetic-homotopy-theory.universal-cover-circle,ms,1317,1137 foundation.sigma-decompositions,ms,1143,1125 category-theory.natural-isomorphisms-functors-precategories,ms,1007,1122 foundation.functoriality-coproduct-types,ms,1089,1113 category-theory.natural-isomorphisms-functors-categories,ms,1039,1094 polytopes.abstract-polytopes,ms,1094,1090 structured-types.pointed-equivalences,ms,1081,1084 set-theory.cumulative-hierarchy,ms,1084,1073 elementary-number-theory.modular-arithmetic-standard-finite-types,ms,1048,1071 synthetic-homotopy-theory.hatchers-acyclic-type,ms,1064,993 commutative-algebra.products-ideals-commutative-rings,ms,897,972 elementary-number-theory.modular-arithmetic,ms,938,968 finite-group-theory.permutations-standard-finite-types,ms,962,963 category-theory.natural-isomorphisms-maps-precategories,ms,1020,954 category-theory.natural-isomorphisms-maps-categories,ms,994,946 synthetic-homotopy-theory.truncated-acyclic-maps,ms,932,937 foundation.surjective-maps,ms,921,930 foundation.telescopes,ms,957,916 foundation.relaxed-sigma-decompositions,ms,930,888 species.small-cauchy-composition-species-of-types-in-subuniverses,ms,777,876 finite-group-theory.transpositions-standard-finite-types,ms,866,873 foundation.coproduct-decompositions,ms,936,872 foundation.binary-functoriality-set-quotients,ms,886,867 category-theory.isomorphisms-in-large-precategories,ms,840,867 ring-theory.isomorphisms-rings,ms,839,855 foundation-core.commuting-squares-of-identifications,ms,796,854 foundation.path-algebra,ms,839,852 group-theory.quotient-groups,ms,841,836 commutative-algebra.groups-of-units-commutative-rings,ms,855,828 synthetic-homotopy-theory.suspensions-of-types,ms,788,827 ring-theory.groups-of-units-rings,ms,900,822 species.cauchy-composition-species-of-types-in-subuniverses,ms,826,819 trees.combinator-directed-trees,ms,810,818 category-theory.isomorphisms-in-precategories,ms,780,818 foundation.cartesian-products-set-quotients,ms,767,817 synthetic-homotopy-theory.26-descent,ms,762,817 foundation.higher-homotopies-morphisms-arrows,ms,799,796 trees.equivalences-enriched-directed-trees,ms,782,790 species.cauchy-products-species-of-types-in-subuniverses,ms,804,789 species.dirichlet-products-species-of-types-in-subuniverses,ms,814,783 trees.combinator-enriched-directed-trees,ms,782,782 univalent-combinatorics.cyclic-finite-types,ms,771,770 synthetic-homotopy-theory.universal-property-coequalizers,ms,767,768 synthetic-homotopy-theory.pushouts,ms,724,768 graph-theory.walks-directed-graphs,ms,769,766 finite-group-theory.sign-homomorphism,ms,714,763 synthetic-homotopy-theory.dependent-pullback-property-pushouts,ms,603,761 foundation.partitions,ms,790,753 order-theory.finitely-graded-posets,ms,770,748 category-theory.isomorphisms-in-categories,ms,769,747 trees.underlying-trees-of-elements-of-w-types,ms,748,747 univalent-combinatorics.sigma-decompositions,ms,746,743 group-theory.subgroups,ms,754,738 group-theory.normal-subgroups,ms,627,736 elementary-number-theory.fundamental-theorem-of-arithmetic,ms,709,731 foundation.fibered-maps,ms,730,729 foundation.equivalences,ms,707,724 foundation.truncations,ms,703,724 foundation-core.equivalences,ms,747,718 synthetic-homotopy-theory.dependent-universal-property-pushouts,ms,666,712 foundation-core.commuting-prisms-of-maps,ms,724,710 foundation.vectors-set-quotients,ms,706,709 ring-theory.rings,ms,674,708 graph-theory.equivalences-directed-graphs,ms,690,693 group-theory.abelian-groups,ms,690,692 synthetic-homotopy-theory.smash-products-of-pointed-types,ms,707,685 finite-group-theory.abstract-quaternion-group,ms,793,680 group-theory.subgroups-generated-by-subsets-groups,ms,741,675 commutative-algebra.joins-radical-ideals-commutative-rings,ms,667,672 synthetic-homotopy-theory.acyclic-maps,ms,673,669 foundation.coproduct-decompositions-subuniverse,ms,682,667 orthogonal-factorization-systems.modal-induction,ms,655,664 group-theory.subgroups-abelian-groups,ms,587,650 orthogonal-factorization-systems.lifting-structures-on-squares,ms,689,637 order-theory.galois-connections,ms,644,637 category-theory.isomorphisms-in-large-categories,ms,630,637 univalent-combinatorics.distributivity-of-set-truncation-over-finite-products,ms,679,636 univalent-combinatorics.finite-types,ms,661,633 synthetic-homotopy-theory.suspension-structures,ms,642,633 group-theory.homomorphisms-generated-subgroups,ms,620,632 synthetic-homotopy-theory.dependent-coforks,ms,623,629 foundation.computational-identity-types,ms,622,627 group-theory.loop-groups-sets,ms,623,626 elementary-number-theory.divisibility-integers,ms,625,625 foundation.uniqueness-image,ms,607,620 foundation.fibered-equivalences,ms,621,619 category-theory.subprecategories,ms,617,615 category-theory.subcategories,ms,611,615 group-theory.generating-elements-groups,ms,608,614 foundation.exponents-set-quotients,ms,636,611 foundation.pi-decompositions,ms,611,610 elementary-number-theory.multiplication-integers,ms,604,608 foundation-core.commuting-squares-of-maps,ms,587,605 category-theory.adjunctions-large-precategories,ms,633,603 species.cauchy-composition-species-of-types,ms,594,601 foundation.embeddings,ms,609,600 trees.directed-trees,ms,607,594 foundation.set-quotients,ms,598,591 commutative-algebra.eisenstein-integers,ms,545,591 group-theory.torsors,ms,574,590 synthetic-homotopy-theory.cocones-under-spans,ms,581,583 group-theory.normal-submonoids,ms,582,580 elementary-number-theory.rational-numbers,ms,568,575 foundation.descent-coproduct-types,ms,626,572 synthetic-homotopy-theory.circle,ms,529,572 group-theory.groups,ms,527,572 foundation.unordered-pairs,ms,580,568 foundation.decidable-equivalence-relations,ms,501,565 trees.equivalences-directed-trees,ms,563,562 species.cauchy-exponentials-species-of-types-in-subuniverses,ms,594,561 foundation.universal-property-image,ms,554,558 trees.w-types,ms,561,557 orthogonal-factorization-systems.pullback-hom,ms,573,554 order-theory.galois-connections-large-posets,ms,507,554 category-theory.precategory-of-functors,ms,541,545 category-theory.functors-precategories,ms,537,541 foundation.equivalences-maybe,ms,606,539 elementary-number-theory.bezouts-lemma-integers,ms,534,536 foundation.invertible-maps,ms,529,532 category-theory.natural-transformations-functors-from-small-to-large-precategories,ms,492,532 category-theory.precategory-of-maps-precategories,ms,516,531 foundation.slice,ms,479,528 foundation.product-decompositions-subuniverse,ms,530,527 category-theory.structure-equivalences-set-magmoids,ms,469,527 foundation.truncation-equivalences,ms,522,526 group-theory.integer-powers-of-elements-groups,ms,550,525 ring-theory.ideals-rings,ms,538,525 ring-theory.binomial-theorem-semirings,ms,527,525 species.dirichlet-exponentials-species-of-types-in-subuniverses,ms,528,524 finite-algebra.finite-rings,ms,526,524 synthetic-homotopy-theory.functoriality-suspensions,ms,524,524 category-theory.natural-transformations-maps-from-small-to-large-precategories,ms,474,523 orthogonal-factorization-systems.extensions-of-maps,ms,542,522 foundation,ms,570,511 category-theory.natural-transformations-functors-precategories,ms,507,511 foundation.set-truncations,ms,531,510 univalent-combinatorics.standard-finite-types,ms,518,502 foundation.universal-property-pullbacks,ms,517,501 category-theory.wide-subcategories,ms,503,500 group-theory.normal-submonoids-commutative-monoids,ms,493,500 ring-theory.ideals-generated-by-subsets-rings,ms,502,496 foundation-core.functoriality-dependent-pair-types,ms,517,494 category-theory.dependent-products-of-categories,ms,497,492 foundation.connected-maps,ms,498,488 commutative-algebra.euclidean-domains,ms,436,485 foundation.functoriality-set-quotients,ms,517,482 univalent-combinatorics.main-classes-of-latin-hypercubes,ms,482,482 structured-types.pointed-homotopies,ms,458,482 foundation.homotopies,ms,445,479 foundation.strictly-involutive-identity-types,ms,476,478 category-theory.fully-faithful-functors-precategories,ms,474,477 synthetic-homotopy-theory.flattening-lemma-coequalizers,ms,470,475 finite-group-theory.permutations,ms,458,472 foundation.cones-over-cospan-diagrams,ms,441,472 reflection.precategory-solver,ms,512,470 category-theory.replete-subprecategories,ms,482,470 foundation.functoriality-dependent-function-types,ms,472,470 foundation.arithmetic-law-product-and-pi-decompositions,ms,462,467 linear-algebra.vectors,ms,461,465 foundation.functoriality-set-truncation,ms,457,465 graph-theory.walks-undirected-graphs,ms,468,455 foundation.arithmetic-law-coproduct-and-sigma-decompositions,ms,517,450 ring-theory.left-ideals-generated-by-subsets-rings,ms,480,447 synthetic-homotopy-theory.dependent-cocones-under-sequential-diagrams,ms,447,447 foundation.type-arithmetic-dependent-pair-types,ms,444,447 foundation.equivalence-classes,ms,404,447 ring-theory.right-ideals-generated-by-subsets-rings,ms,446,444 set-theory.countable-sets,ms,457,442 ring-theory.cyclic-rings,ms,458,441 group-theory.cores-monoids,ms,455,440 category-theory.category-of-functors,ms,414,438 synthetic-homotopy-theory.flattening-lemma-sequential-colimits,ms,448,437 foundation.composition-algebra,ms,458,434 elementary-number-theory.addition-integers,ms,422,428 synthetic-homotopy-theory.dependent-suspension-structures,ms,391,428 finite-algebra.commutative-finite-rings,ms,444,426 orthogonal-factorization-systems.higher-modalities,ms,417,425 foundation.identity-types,ms,391,425 category-theory.category-of-maps-categories,ms,401,422 finite-group-theory.subgroups-finite-groups,ms,369,422 group-theory.equivalences-group-actions,ms,419,421 category-theory.functors-set-magmoids,ms,397,420 foundation.epimorphisms-with-respect-to-truncated-types,ms,404,418 category-theory.wide-subprecategories,ms,415,417 orthogonal-factorization-systems.function-classes,ms,415,417 commutative-algebra.commutative-rings,ms,402,412 foundation-core.fibers-of-maps,ms,415,407 trees.bases-directed-trees,ms,401,407 structured-types.morphisms-h-spaces,ms,407,405 synthetic-homotopy-theory.dependent-cocones-under-spans,ms,378,403 category-theory.function-categories,ms,401,399 group-theory.invertible-elements-monoids,ms,392,399 organic-chemistry.ethane,ms,392,392 synthetic-homotopy-theory.joins-of-types,ms,381,392 orthogonal-factorization-systems.local-types,ms,374,392 ring-theory.integer-multiples-of-elements-rings,ms,389,391 foundation.decidable-embeddings,ms,381,390 category-theory.natural-transformations-maps-precategories,ms,383,387 foundation.equality-coproduct-types,ms,379,387 synthetic-homotopy-theory.coforks,ms,383,385 commutative-algebra.integral-domains,ms,349,384 trees.extensional-w-types,ms,377,382 synthetic-homotopy-theory.sections-descent-circle,ms,377,379 group-theory.conjugation,ms,380,376 elementary-number-theory.pisano-periods,ms,360,374 finite-group-theory.finite-groups,ms,372,372 foundation.universal-property-propositional-truncation,ms,362,370 foundation.type-duality,ms,369,368 reflection.group-solver,ms,365,368 trees.functoriality-combinator-directed-trees,ms,370,367 foundation.universal-property-family-of-fibers-of-maps,ms,375,365 synthetic-homotopy-theory.sequential-colimits,ms,367,365 ring-theory.homomorphisms-rings,ms,358,362 finite-algebra.finite-fields,ms,379,361 foundation.equivalences-span-diagrams,ms,354,360 foundation.functoriality-cartesian-product-types,ms,331,358 trees.functoriality-w-types,ms,353,357 orthogonal-factorization-systems.precomposition-lifts-families-of-elements,ms,313,352 foundation-core.homotopies,ms,320,351 elementary-number-theory.well-ordering-principle-standard-finite-types,ms,339,350 group-theory.symmetric-groups,ms,351,348 ring-theory.modules-rings,ms,340,348 category-theory.natural-transformations-functors-from-small-to-large-categories,ms,338,348 commutative-algebra.products-radical-ideals-commutative-rings,ms,325,347 elementary-number-theory.divisibility-natural-numbers,ms,349,345 order-theory.meet-semilattices,ms,343,344 order-theory.nuclei-large-locales,ms,342,344 trees.ranks-of-elements-w-types,ms,339,342 trees.morphisms-enriched-directed-trees,ms,336,338 type-theories.precategories-with-attributes,ms,414,334 order-theory.closure-operators-large-locales,ms,334,333 category-theory.adjunctions-large-categories,ms,371,332 lists.permutation-vectors,ms,377,331 category-theory.categories,ms,340,330 lists.lists,ms,328,329 foundation.commuting-squares-of-homotopies,ms,328,328 order-theory.join-semilattices,ms,330,327 synthetic-homotopy-theory.eckmann-hilton-argument,ms,326,325 foundation.exclusive-disjunction,ms,323,325 univalent-combinatorics.set-quotients-of-index-two,ms,325,324 synthetic-homotopy-theory.universal-property-sequential-colimits,ms,318,324 category-theory.dependent-products-of-precategories,ms,319,323 foundation.sections,ms,317,323 category-theory.dependent-products-of-large-categories,ms,320,320 synthetic-homotopy-theory.dependent-universal-property-sequential-colimits,ms,314,319 category-theory.monads-on-precategories,ms,310,319 category-theory.dependent-products-of-large-precategories,ms,349,318 foundation-core.truncated-types,ms,313,318 category-theory.pseudomonic-functors-precategories,ms,319,316 foundation.transport-along-higher-identifications,ms,325,315 group-theory.decidable-subgroups,ms,308,315 category-theory.functors-categories,ms,327,312 category-theory.precategory-of-functors-from-small-to-large-precategories,ms,279,312 foundation.symmetric-operations,ms,307,311 elementary-number-theory.reduced-integer-fractions,ms,302,309 foundation.postcomposition-functions,ms,271,307 group-theory.quotients-abelian-groups,ms,309,306 ring-theory.localizations-rings,ms,308,306 synthetic-homotopy-theory.cocones-under-sequential-diagrams,ms,307,306 foundation.isolated-elements,ms,306,305 commutative-algebra.gaussian-integers,ms,318,304 foundation.faithful-maps,ms,294,304 elementary-number-theory.greatest-common-divisor-natural-numbers,ms,304,303 commutative-algebra.isomorphisms-commutative-rings,ms,274,302 group-theory.images-of-group-homomorphisms,ms,309,300 group-theory.abelianization-groups,ms,304,300 category-theory.copresheaf-categories,ms,273,300 foundation-core.subtypes,ms,291,299 lists.sort-by-insertion-vectors,ms,298,297 foundation.uniqueness-set-quotients,ms,340,296 trees.morphisms-coalgebras-polynomial-endofunctors,ms,299,296 trees.morphisms-algebras-polynomial-endofunctors,ms,297,296 elementary-number-theory.greatest-common-divisor-integers,ms,292,296 elementary-number-theory.universal-property-integers,ms,316,292 elementary-number-theory.inequality-natural-numbers,ms,252,292 foundation.transposition-identifications-along-equivalences,ms,297,291 orthogonal-factorization-systems.factorizations-of-maps,ms,291,291 synthetic-homotopy-theory.dependent-universal-property-coequalizers,ms,290,291 category-theory.natural-transformations-functors-categories,ms,268,290 category-theory.precategory-of-maps-from-small-to-large-precategories,ms,303,288 univalent-combinatorics.partitions,ms,286,288 foundation.equality-dependent-pair-types,ms,285,288 category-theory.presheaf-categories,ms,270,288 order-theory.order-preserving-maps-posets,ms,268,288 trees.small-multisets,ms,287,286 group-theory.isomorphisms-group-actions,ms,298,285 graph-theory.equivalences-undirected-graphs,ms,357,284 group-theory.homomorphisms-group-actions,ms,281,282 category-theory.monads-on-categories,ms,273,282 foundation.type-arithmetic-coproduct-types,ms,271,282 synthetic-homotopy-theory.dependent-pushout-products,ms,351,280 elementary-number-theory.integers,ms,289,279 trees.fibers-enriched-directed-trees,ms,270,279 univalent-combinatorics.type-duality,ms,282,277 foundation.commuting-squares-of-identifications,ms,232,274 foundation.equivalences-arrows,ms,278,273 foundation-core.invertible-maps,ms,265,273 foundation.commuting-triangles-of-identifications,ms,254,273 foundation.dependent-identifications,ms,242,273 group-theory.subgroups-generated-by-elements-groups,ms,303,272 graph-theory.equivalences-enriched-undirected-graphs,ms,265,271 category-theory.isomorphisms-in-subprecategories,ms,263,271 category-theory.groupoids,ms,252,271 synthetic-homotopy-theory.dependent-descent-circle,ms,270,269 structured-types.equivalences-types-equipped-with-endomorphisms,ms,262,269 univalent-combinatorics.pigeonhole-principle,ms,266,268 finite-algebra.homomorphisms-commutative-finite-rings,ms,289,266 foundation.decidable-equality,ms,251,266 category-theory.functors-from-small-to-large-categories,ms,227,266 trees.bases-enriched-directed-trees,ms,195,266 trees.morphisms-directed-trees,ms,262,264 foundation.dependent-binomial-theorem,ms,256,264 foundation-core.small-types,ms,253,264 group-theory.subgroups-generated-by-families-of-elements-groups,ms,289,262 ring-theory.products-subsets-rings,ms,246,262 foundation.univalence,ms,223,262 species.products-dirichlet-series-species-of-types-in-subuniverses,ms,327,261 group-theory.homomorphisms-groups,ms,270,260 lists.universal-property-lists-wild-monoids,ms,262,260 group-theory.isomorphisms-semigroups,ms,267,259 foundation.propositional-truncations,ms,252,259 foundation.repetitions-of-values,ms,220,259 foundation.perfect-images,ms,260,258 commutative-algebra.homomorphisms-commutative-rings,ms,277,257 synthetic-homotopy-theory.descent-circle-equivalence-types,ms,257,257 foundation.type-arithmetic-empty-type,ms,237,256 foundation-core.universal-property-pullbacks,ms,232,256 category-theory.functors-from-small-to-large-precategories,ms,230,256 commutative-algebra.intersections-radical-ideals-commutative-rings,ms,248,255 elementary-number-theory.based-strong-induction-natural-numbers,ms,248,255 foundation.images-subtypes,ms,230,255 synthetic-homotopy-theory.equivalences-sequential-diagrams,ms,253,253 structured-types.initial-pointed-type-equipped-with-automorphism,ms,252,253 type-theories.unityped-type-theories,ms,249,253 univalent-combinatorics.decidable-equivalence-relations,ms,258,252 ring-theory.homomorphisms-semirings,ms,257,252 species.cauchy-exponentials-species-of-types,ms,251,252 category-theory.large-function-categories,ms,245,251 elementary-number-theory.distance-natural-numbers,ms,253,250 synthetic-homotopy-theory.codiagonals-of-maps,ms,247,250 category-theory.full-subcategories,ms,248,249 lists.permutation-lists,ms,248,247 orthogonal-factorization-systems.lifts-of-maps,ms,246,245 category-theory.natural-transformations-maps-categories,ms,254,243 foundation-core.truncated-maps,ms,230,243 commutative-algebra.joins-ideals-commutative-rings,ms,239,242 ring-theory.transporting-ring-structure-along-isomorphisms-abelian-groups,ms,237,242 category-theory.full-subprecategories,ms,263,241 order-theory.order-preserving-maps-preorders,ms,233,240 category-theory.maps-precategories,ms,230,240 foundation-core.propositions,ms,225,240 univalent-combinatorics.coproduct-types,ms,240,239 orthogonal-factorization-systems.factorizations-of-maps-function-classes,ms,239,239 foundation.decidable-propositions,ms,231,238 category-theory.fully-faithful-maps-precategories,ms,216,238 finite-algebra.homomorphisms-finite-rings,ms,252,237 species.dirichlet-exponentials-species-of-types,ms,252,237 group-theory.homomorphisms-monoids,ms,236,237 trees.rooted-morphisms-directed-trees,ms,234,236 synthetic-homotopy-theory.descent-circle-dependent-pair-types,ms,164,236 univalent-combinatorics.ferrers-diagrams,ms,233,235 foundation.subtypes,ms,214,235 commutative-algebra.radicals-of-ideals-commutative-rings,ms,187,235 category-theory.composition-operations-on-binary-families-of-sets,ms,257,234 category-theory.function-precategories,ms,230,234 category-theory.large-function-precategories,ms,234,233 synthetic-homotopy-theory.universal-property-circle,ms,232,233 foundation.universal-property-fiber-products,ms,228,232 foundation.whiskering-homotopies-composition,ms,245,231 univalent-combinatorics.cartesian-product-types,ms,212,230 foundation.morphisms-arrows,ms,233,229 foundation.iterating-automorphisms,ms,224,229 category-theory.precategory-of-elements-of-a-presheaf,ms,232,228 type-theories.precategories-with-families,ms,228,227 lists.functoriality-lists,ms,225,227 group-theory.powers-of-elements-monoids,ms,254,225 foundation.function-extensionality,ms,216,225 foundation.binary-type-duality,ms,221,224 foundation.binary-relations,ms,211,224 category-theory.maps-set-magmoids,ms,195,224 order-theory.large-subframes,ms,224,223 synthetic-homotopy-theory.descent-circle-function-types,ms,222,223 ring-theory.semirings,ms,217,223 commutative-algebra.zariski-locale,ms,223,221 group-theory.normal-closures-subgroups,ms,219,221 ring-theory.congruence-relations-rings,ms,248,220 foundation.logical-equivalences,ms,211,219 univalent-combinatorics.counting-decidable-subtypes,ms,218,218 group-theory.functoriality-quotient-groups,ms,215,218 group-theory.subsemigroups,ms,218,217 elementary-number-theory.ring-of-integers,ms,197,217 group-theory.congruence-relations-groups,ms,197,215 category-theory.opposite-preunivalent-categories,ms,192,215 synthetic-homotopy-theory.infinite-cyclic-types,ms,231,214 category-theory.terminal-category,ms,215,214 lists.arrays,ms,207,214 category-theory.functors-nonunital-precategories,ms,213,213 group-theory.normal-cores-subgroups,ms,212,211 group-theory.transitive-concrete-group-actions,ms,209,210 order-theory.least-upper-bounds-posets,ms,182,209 foundation-core.identity-types,ms,209,208 synthetic-homotopy-theory.descent-circle,ms,208,208 category-theory.anafunctors-precategories,ms,205,208 foundation.universal-property-set-truncation,ms,213,207 foundation.universal-property-sequential-limits,ms,208,207 category-theory.faithful-maps-precategories,ms,206,207 foundation.transport-along-equivalences,ms,206,207 foundation.locally-small-types,ms,178,207 orthogonal-factorization-systems.functoriality-higher-modalities,ms,206,206 commutative-algebra.homomorphisms-commutative-semirings,ms,205,206 type-theories.sections-dependent-type-theories,ms,203,206 ring-theory.invertible-elements-rings,ms,230,205 trees.undirected-trees,ms,204,205 group-theory.isomorphisms-abelian-groups,ms,199,205 foundation.preunivalent-type-families,ms,216,204 univalent-combinatorics.dependent-pair-types,ms,202,204 orthogonal-factorization-systems.extensions-double-lifts-families-of-elements,ms,235,203 category-theory.pullbacks-in-precategories,ms,212,203 foundation.morphisms-cospan-diagrams,ms,202,203 foundation-core.contractible-types,ms,189,203 synthetic-homotopy-theory.pushout-products,ms,225,202 group-theory.isomorphisms-groups,ms,203,202 group-theory.substitution-functor-group-actions,ms,203,201 linear-algebra.vectors-on-euclidean-domains,ms,200,201 structured-types.involutive-type-of-h-space-structures,ms,201,200 linear-algebra.vectors-on-rings,ms,199,200 foundation.function-types,ms,206,199 foundation.symmetric-identity-types,ms,202,199 synthetic-homotopy-theory.descent-circle-subtypes,ms,198,199 lists.sorted-vectors,ms,197,199 finite-group-theory.cartier-delooping-sign-homomorphism,ms,199,198 group-theory.subgroups-concrete-groups,ms,197,198 orthogonal-factorization-systems.factorization-operations-function-classes,ms,185,198 foundation.decidable-types,ms,156,197 category-theory.gaunt-categories,ms,197,196 species.small-cauchy-composition-species-of-finite-inhabited-types,ms,196,195 foundation.universal-property-identity-types,ms,192,194 foundation.multivariable-homotopies,ms,188,192 foundation-core.universal-property-truncation,ms,189,191 synthetic-homotopy-theory.pushouts-of-pointed-types,ms,209,190 synthetic-homotopy-theory.interval-type,ms,208,190 trees.enriched-directed-trees,ms,189,189 group-theory.homomorphisms-semigroups,ms,178,189 synthetic-homotopy-theory.morphisms-sequential-diagrams,ms,182,188 ring-theory.joins-ideals-rings,ms,177,188 foundation.precomposition-functions,ms,182,187 graph-theory.morphisms-undirected-graphs,ms,194,185 finite-algebra.dependent-products-finite-rings,ms,186,185 foundation.retractions,ms,177,185 foundation-core.whiskering-identifications-concatenation,ms,163,185 foundation.equality-cartesian-product-types,ms,193,184 category-theory.restrictions-functors-cores-precategories,ms,186,184 finite-group-theory.finite-semigroups,ms,184,184 order-theory.greatest-lower-bounds-posets,ms,183,184 category-theory.indiscrete-precategories,ms,183,184 foundation.regensburg-extension-fundamental-theorem-of-identity-types,ms,180,184 foundation.equality-fibers-of-maps,ms,174,184 group-theory,ms,202,183 species.composition-cauchy-series-species-of-types,ms,193,183 elementary-number-theory.strict-inequality-natural-numbers,ms,191,182 order-theory.finite-preorders,ms,180,181 group-theory.images-of-semigroup-homomorphisms,ms,186,180 foundation.sequential-limits,ms,183,180 foundation.universal-property-truncation,ms,180,180 group-theory.addition-homomorphisms-abelian-groups,ms,194,179 ring-theory.sums-semirings,ms,180,179 set-theory.cardinalities,ms,179,178 graph-theory.morphisms-directed-graphs,ms,179,178 foundation.impredicative-encodings,ms,178,177 category-theory.cores-precategories,ms,175,177 graph-theory.fibers-directed-graphs,ms,180,176 group-theory.iterated-cartesian-products-concrete-groups,ms,178,176 foundation.symmetric-difference,ms,175,176 foundation.epimorphisms,ms,173,176 category-theory.strict-categories,ms,154,176 elementary-number-theory.standard-cyclic-rings,ms,190,175 ring-theory.joins-right-ideals-rings,ms,176,175 category-theory.large-categories,ms,175,175 foundation.decidable-subtypes,ms,174,175 ring-theory.congruence-relations-semirings,ms,161,175 foundation.functoriality-truncation,ms,185,174 foundation.unordered-tuples,ms,177,174 foundation-core.equality-dependent-pair-types,ms,156,174 foundation.subuniverses,ms,181,173 synthetic-homotopy-theory.functoriality-loop-spaces,ms,180,173 ring-theory.joins-left-ideals-rings,ms,179,173 group-theory.isomorphisms-monoids,ms,173,173 finite-algebra.dependent-products-commutative-finite-rings,ms,173,173 commutative-algebra.integer-multiples-of-elements-commutative-rings,ms,163,173 elementary-number-theory.strong-induction-natural-numbers,ms,156,173 ring-theory.homomorphisms-cyclic-rings,ms,168,172 univalent-combinatorics.fibers-of-maps,ms,166,172 foundation.sets,ms,160,172 foundation.commuting-triangles-of-maps,ms,152,172 foundation.0-connected-types,ms,187,171 synthetic-homotopy-theory.triple-loop-spaces,ms,171,171 commutative-algebra.transporting-commutative-ring-structure-isomorphisms-abelian-groups,ms,168,171 category-theory.faithful-functors-precategories,ms,168,171 elementary-number-theory.powers-of-two,ms,167,171 group-theory.congruence-relations-abelian-groups,ms,158,171 group-theory.homomorphisms-groups-equipped-with-normal-subgroups,ms,182,170 elementary-number-theory.type-arithmetic-natural-numbers,ms,180,170 group-theory.integer-multiples-of-elements-abelian-groups,ms,176,170 orthogonal-factorization-systems.factorizations-of-maps-global-function-classes,ms,160,170 group-theory.orbits-monoid-actions,ms,175,169 structured-types.pointed-types-equipped-with-automorphisms,ms,161,169 synthetic-homotopy-theory.joins-of-maps,ms,183,168 category-theory,ms,172,168 category-theory.preunivalent-categories,ms,167,168 ring-theory.dependent-products-rings,ms,163,168 foundation.cantor-schroder-bernstein-escardo,ms,176,167 foundation.images,ms,169,166 category-theory.full-large-subprecategories,ms,167,166 finite-group-theory.finite-monoids,ms,166,166 univalent-combinatorics.2-element-subtypes,ms,163,165 univalent-combinatorics.counting,ms,171,164 category-theory.functors-large-precategories,ms,150,164 structured-types.dependent-products-wild-monoids,ms,160,163 commutative-algebra.ideals-commutative-rings,ms,180,162 trees.functoriality-fiber-directed-tree,ms,163,162 orthogonal-factorization-systems.orthogonal-factorization-systems,ms,162,162 structured-types.equivalences-types-equipped-with-automorphisms,ms,160,162 elementary-number-theory.finitary-natural-numbers,ms,151,162 foundation.singleton-subtypes,ms,172,161 order-theory.large-frames,ms,164,161 group-theory.normalizer-subgroups,ms,162,161 commutative-algebra.function-commutative-rings,ms,169,160 foundation.descent-equivalences,ms,161,160 foundation-core.functoriality-dependent-function-types,ms,160,160 group-theory.homomorphisms-abelian-groups,ms,155,160 category-theory.full-large-subcategories,ms,159,159 finite-group-theory.finite-abelian-groups,ms,158,159 foundation.diagonals-of-maps,ms,154,159 foundation.descent-dependent-pair-types,ms,160,158 group-theory.cartesian-products-concrete-groups,ms,159,158 elementary-number-theory.addition-integer-fractions,ms,158,158 foundation.fiber-inclusions,ms,158,157 elementary-number-theory.congruence-natural-numbers,ms,147,157 foundation.equivalences-spans,ms,157,156 finite-group-theory.finite-type-groups,ms,157,156 foundation-core.sections,ms,112,156 ring-theory.products-rings,ms,155,155 univalent-combinatorics.sequences-finite-types,ms,150,155 category-theory.large-precategories,ms,148,155 foundation.universal-property-propositional-truncation-into-sets,ms,145,155 category-theory.products-in-precategories,ms,154,153 univalent-combinatorics.decidable-subtypes,ms,154,152 species.products-dirichlet-series-species-of-types,ms,154,152 univalent-combinatorics.equality-standard-finite-types,ms,162,151 category-theory.coproducts-in-precategories,ms,154,151 group-theory.pullbacks-subgroups,ms,142,151 foundation.action-on-higher-identifications-functions,ms,144,150 foundation-core.injective-maps,ms,148,149 foundation.action-on-identifications-binary-functions,ms,144,149 category-theory.natural-transformations-functors-large-precategories,ms,169,148 order-theory.frames,ms,156,148 group-theory.nullifying-group-homomorphisms,ms,156,148 foundation.coproduct-types,ms,153,148 synthetic-homotopy-theory.free-loops,ms,148,148 ring-theory.algebras-rings,ms,92,148 elementary-number-theory.universal-property-natural-numbers,ms,154,147 synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types,ms,154,147 foundation.iterated-cartesian-product-types,ms,148,147 elementary-number-theory.multiplication-natural-numbers,ms,147,147 foundation.morphisms-spans-families-of-types,ms,147,146 foundation.constant-maps,ms,147,145 group-theory.saturated-congruence-relations-monoids,ms,143,145 foundation.monomorphisms,ms,138,145 species.products-cauchy-series-species-of-types,ms,144,144 trees.fibers-directed-trees,ms,142,144 foundation.action-on-equivalences-type-families,ms,141,144 order-theory.large-locales,ms,144,143 commutative-algebra.dependent-products-commutative-rings,ms,141,143 elementary-number-theory.congruence-integers,ms,137,143 category-theory.yoneda-lemma-precategories,ms,136,143 foundation.connected-types,ms,150,142 finite-algebra.products-commutative-finite-rings,ms,150,142 category-theory.opposite-large-precategories,ms,147,142 foundation-core.retractions,ms,147,142 orthogonal-factorization-systems.open-modalities,ms,144,142 category-theory.opposite-precategories,ms,136,142 foundation.type-theoretic-principle-of-choice,ms,131,141 group-theory.kernels-homomorphisms-groups,ms,121,141 foundation.global-subuniverses,ms,140,140 univalent-combinatorics.embeddings-standard-finite-types,ms,131,140 group-theory.saturated-congruence-relations-commutative-monoids,ms,146,139 universal-algebra.terms-over-signatures,ms,138,139 category-theory.opposite-categories,ms,137,139 univalent-combinatorics.equivalences-cubes,ms,139,138 foundation.functional-correspondences,ms,139,138 trees.polynomial-endofunctors,ms,127,138 category-theory.precategories,ms,138,137 group-theory.submonoids,ms,137,137 order-theory.large-quotient-locales,ms,136,137 higher-group-theory.transitive-higher-group-actions,ms,136,137 orthogonal-factorization-systems.uniquely-eliminating-modalities,ms,135,137 species.morphisms-finite-species,ms,134,137 ring-theory.products-ideals-rings,ms,129,137 foundation.pairs-of-distinct-elements,ms,127,137 group-theory.dihedral-group-construction,ms,145,136 foundation.equivalence-extensionality,ms,158,135 universal-algebra.algebraic-theory-of-groups,ms,136,135 foundation.morphisms-inverse-sequential-diagrams,ms,134,135 foundation.dependent-universal-property-equivalences,ms,108,135 finite-algebra.products-finite-rings,ms,142,134 elementary-number-theory.prime-numbers,ms,128,134 elementary-number-theory.inequality-standard-finite-types,ms,127,134 foundation.raising-universe-levels,ms,136,133 foundation.involutions,ms,134,133 order-theory.order-preserving-maps-large-posets,ms,133,133 trees.induction-w-types,ms,133,133 foundation.truncation-images-of-maps,ms,132,133 commutative-algebra.commutative-semirings,ms,120,133 univalent-combinatorics.cycle-prime-decomposition-natural-numbers,ms,134,132 foundation-core.type-theoretic-principle-of-choice,ms,114,132 foundation.apartness-relations,ms,137,131 foundation.universal-property-dependent-pair-types,ms,137,131 order-theory.order-preserving-maps-large-preorders,ms,134,131 elementary-number-theory.absolute-value-integers,ms,130,131 category-theory.conservative-functors-precategories,ms,128,131 linear-algebra.vectors-on-semirings,ms,127,131 group-theory.equivalences-concrete-group-actions,ms,138,130 structured-types.h-spaces,ms,134,130 trees.rooted-morphisms-enriched-directed-trees,ms,129,130 foundation-core.equivalence-relations,ms,119,130 order-theory.large-suplattices,ms,131,129 ring-theory.ideals-semirings,ms,130,129 group-theory.submonoids-commutative-monoids,ms,130,128 ring-theory.products-right-ideals-rings,ms,129,128 univalent-combinatorics.finite-choice,ms,128,128 group-theory.homomorphisms-concrete-groups,ms,128,128 foundation.families-of-maps,ms,128,128 lists.quicksort-lists,ms,127,128 group-theory.congruence-relations-semigroups,ms,122,128 foundation.univalent-type-families,ms,139,126 order-theory.large-meet-subsemilattices,ms,134,126 group-theory.full-subgroups,ms,130,125 ring-theory.products-left-ideals-rings,ms,129,125 group-theory.homomorphisms-commutative-monoids,ms,122,125 structured-types.morphisms-types-equipped-with-endomorphisms,ms,120,125 univalent-combinatorics.surjective-maps,ms,118,125 commutative-algebra.invertible-elements-commutative-rings,ms,117,125 foundation.category-of-families-of-sets,ms,125,124 order-theory.posets,ms,125,124 commutative-algebra.radical-ideals-commutative-rings,ms,130,123 foundation.fibered-involutions,ms,124,123 structured-types.dependent-types-equipped-with-automorphisms,ms,123,123 foundation.propositional-extensionality,ms,123,123 modal-type-theory.flat-sharp-adjunction,ms,124,122 category-theory.pregroupoids,ms,123,122 orthogonal-factorization-systems.extensions-lifts-families-of-elements,ms,122,122 elementary-number-theory.equality-natural-numbers,ms,102,122 orthogonal-factorization-systems.global-function-classes,ms,121,121 order-theory.large-posets,ms,119,121 group-theory.congruence-relations-monoids,ms,114,121 foundation.binary-reflecting-maps-equivalence-relations,ms,121,120 foundation.russells-paradox,ms,120,120 ring-theory.additive-orders-of-elements-rings,ms,119,120 foundation.epimorphisms-with-respect-to-sets,ms,118,120 reflection.type-checking-monad,ms,117,120 foundation.strictly-right-unital-concatenation-identifications,ms,119,119 ring-theory.left-ideals-rings,ms,117,119 commutative-algebra.products-commutative-rings,ms,116,119 category-theory.yoneda-lemma-categories,ms,107,119 commutative-algebra.ideals-generated-by-subsets-commutative-rings,ms,121,118 foundation.equivalence-induction,ms,117,118 foundation.contractible-types,ms,116,118 species.coproducts-species-of-types-in-subuniverses,ms,127,117 orthogonal-factorization-systems.reflective-subuniverses,ms,119,117 order-theory.dependent-products-large-frames,ms,118,117 foundation.trivial-sigma-decompositions,ms,115,117 ring-theory.right-ideals-rings,ms,122,116 ring-theory.powers-of-elements-rings,ms,116,116 group-theory.nontrivial-groups,ms,116,116 foundation.discrete-sigma-decompositions,ms,116,116 lists.concatenation-lists,ms,111,116 group-theory.automorphism-groups,ms,118,115 foundation.iterating-functions,ms,110,115 elementary-number-theory.equality-integers,ms,109,115 foundation.cones-over-inverse-sequential-diagrams,ms,116,114 type-theories.pi-types-precategories-with-attributes,ms,114,114 group-theory.congruence-relations-commutative-monoids,ms,115,113 elementary-number-theory.decidable-types,ms,115,112 group-theory.concrete-groups,ms,111,112 foundation.transport-split-type-families,ms,111,112 group-theory.commutator-subgroups,ms,118,111 foundation.structure-identity-principle,ms,117,111 foundation.connected-components-universes,ms,117,111 category-theory.representing-arrow-category,ms,116,111 univalent-combinatorics.symmetric-difference,ms,112,111 order-theory.large-meet-semilattices,ms,112,111 synthetic-homotopy-theory.retracts-of-sequential-diagrams,ms,111,111 foundation.fundamental-theorem-of-identity-types,ms,119,110 group-theory.quotient-groups-concrete-groups,ms,113,110 ring-theory.dependent-products-semirings,ms,112,110 univalent-combinatorics.inhabited-finite-types,ms,111,110 type-theories.pi-types-precategories-with-families,ms,110,110 higher-group-theory.homomorphisms-higher-groups,ms,117,109 foundation.choice-of-representatives-equivalence-relation,ms,110,109 foundation.pointed-torsorial-type-families,ms,108,109 foundation.discrete-relaxed-sigma-decompositions,ms,106,109 elementary-number-theory.infinitude-of-primes,ms,105,109 commutative-algebra.sums-commutative-rings,ms,111,108 foundation.precomposition-functions-into-subuniverses,ms,108,108 order-theory.decidable-total-orders,ms,99,108 univalent-combinatorics.dependent-function-types,ms,96,108 foundation.isomorphisms-of-sets,ms,110,107 elementary-number-theory.finitely-cyclic-maps,ms,101,107 elementary-number-theory.well-ordering-principle-natural-numbers,ms,135,106 category-theory.nonunital-precategories,ms,113,106 foundation.0-maps,ms,104,106 foundation.propositional-maps,ms,103,106 foundation.reflecting-maps-equivalence-relations,ms,102,106 foundation.functoriality-function-types,ms,101,106 commutative-algebra.poset-of-radical-ideals-commutative-rings,ms,110,105 foundation.equivalences-spans-families-of-types,ms,104,105 foundation.homotopy-induction,ms,127,104 synthetic-homotopy-theory.cocones-under-spans-of-pointed-types,ms,104,104 foundation.type-arithmetic-cartesian-product-types,ms,103,104 foundation.existential-quantification,ms,98,104 foundation.1-types,ms,117,103 foundation.universal-property-dependent-function-types,ms,106,103 elementary-number-theory.inequality-integers,ms,103,102 foundation.binary-transport,ms,97,102 synthetic-homotopy-theory.induction-principle-pushouts,ms,91,102 category-theory.maps-from-small-to-large-precategories,ms,75,102 ring-theory.poset-of-ideals-rings,ms,111,101 category-theory.maps-categories,ms,104,101 group-theory.monoids,ms,103,101 graph-theory.enriched-undirected-graphs,ms,103,101 synthetic-homotopy-theory.loop-spaces,ms,103,101 orthogonal-factorization-systems.closed-modalities,ms,101,101 foundation.universal-property-cartesian-product-types,ms,101,101 foundation.cartesian-morphisms-arrows,ms,100,101 order-theory.commuting-squares-of-galois-connections-large-posets,ms,110,100 category-theory.set-magmoids,ms,105,100 group-theory.homomorphisms-concrete-group-actions,ms,105,100 synthetic-homotopy-theory.powers-of-loops,ms,104,100 ring-theory.poset-of-right-ideals-rings,ms,103,100 group-theory.intersections-subgroups-groups,ms,101,100 order-theory.dependent-products-large-locales,ms,101,100 order-theory.preorders,ms,100,100 commutative-algebra.prime-ideals-commutative-rings,ms,100,100 foundation.booleans,ms,99,100 group-theory.free-groups-with-one-generator,ms,97,100 ring-theory.subsets-rings,ms,93,100 orthogonal-factorization-systems.lifts-families-of-elements,ms,80,100 higher-group-theory.free-higher-group-actions,ms,103,99 ring-theory.poset-of-left-ideals-rings,ms,100,99 higher-group-theory.iterated-cartesian-products-higher-groups,ms,96,99 foundation.inhabited-types,ms,107,98 foundation.uniqueness-set-truncations,ms,105,98 species.products-cauchy-series-species-of-types-in-subuniverses,ms,100,98 order-theory.homomorphisms-meet-semilattices,ms,99,98 order-theory.closure-operators-large-posets,ms,99,98 group-theory.torsion-free-groups,ms,99,98 foundation.maybe,ms,98,98 foundation.coherently-invertible-maps,ms,98,98 universal-algebra.kernels,ms,97,98 synthetic-homotopy-theory.1-acyclic-types,ms,96,98 foundation.inhabited-subtypes,ms,95,98 group-theory.full-subsemigroups,ms,100,97 foundation.symmetric-binary-relations,ms,99,97 foundation.commuting-hexagons-of-identifications,ms,97,97 species.morphisms-species-of-types,ms,93,97 foundation.fibers-of-maps,ms,91,97 category-theory.maps-from-small-to-large-categories,ms,85,97 ring-theory.full-ideals-rings,ms,99,96 order-theory.similarity-of-elements-large-posets,ms,99,96 foundation.weak-function-extensionality,ms,95,96 elementary-number-theory.maximum-natural-numbers,ms,93,96 synthetic-homotopy-theory.wedges-of-pointed-types,ms,105,95 commutative-algebra.full-ideals-commutative-rings,ms,103,95 foundation.equivalence-injective-type-families,ms,100,95 lists.sorted-lists,ms,98,95 category-theory.simplex-category,ms,96,95 category-theory.representable-functors-precategories,ms,96,95 foundation.universal-property-coproduct-types,ms,95,95 univalent-combinatorics,ms,95,95 order-theory.powers-of-large-locales,ms,94,95 foundation.iterated-dependent-product-types,ms,94,95 elementary-number-theory.fibonacci-sequence,ms,90,95 elementary-number-theory.integer-fractions,ms,96,94 univalent-combinatorics.universal-property-standard-finite-types,ms,96,94 species.composition-cauchy-series-species-of-types-in-subuniverses,ms,93,93 synthetic-homotopy-theory.coequalizers,ms,93,93 foundation.type-arithmetic-unit-type,ms,91,93 elementary-number-theory.minimum-standard-finite-types,ms,67,93 group-theory.equivalences-semigroups,ms,89,92 category-theory.split-essentially-surjective-functors-precategories,ms,84,92 ring-theory.sums-rings,ms,100,91 structured-types.pointed-maps,ms,95,91 foundation.structured-type-duality,ms,94,91 foundation.subtype-identity-principle,ms,93,91 foundation.commuting-triangles-of-homotopies,ms,91,91 foundation.coslice,ms,91,91 foundation.precomposition-dependent-functions,ms,91,91 lists.reversing-lists,ms,89,91 foundation.homotopy-algebra,ms,66,91 elementary-number-theory,ms,98,90 order-theory,ms,92,90 linear-algebra.scalar-multiplication-vectors-on-rings,ms,89,90 orthogonal-factorization-systems.local-maps,ms,89,90 elementary-number-theory.minimum-natural-numbers,ms,91,89 category-theory.full-maps-precategories,ms,89,89 finite-group-theory.groups-of-order-2,ms,89,89 commutative-algebra.dependent-products-commutative-semirings,ms,87,89 ring-theory.commuting-elements-rings,ms,93,88 order-theory.subposets,ms,89,88 foundation.disjunction,ms,87,88 foundation.contractible-maps,ms,87,88 ring-theory.function-rings,ms,85,88 ring-theory.function-semirings,ms,85,88 foundation.functoriality-propositional-truncation,ms,90,87 category-theory.initial-category,ms,90,87 commutative-algebra.sums-commutative-semirings,ms,87,87 category-theory.cores-categories,ms,86,87 foundation-core.transport-along-identifications,ms,81,87 univalent-combinatorics.finitely-presented-types,ms,91,86 foundation-core.contractible-maps,ms,88,85 category-theory.isomorphism-induction-categories,ms,86,85 category-theory.representable-functors-large-precategories,ms,86,85 ring-theory.category-of-cyclic-rings,ms,84,85 foundation.repetitions-sequences,ms,82,85 foundation.truncated-maps,ms,69,85 group-theory.symmetric-concrete-groups,ms,60,85 orthogonal-factorization-systems.modal-operators,ms,85,84 foundation.category-of-sets,ms,85,84 foundation.large-locale-of-subtypes,ms,84,84 group-theory.dependent-products-abelian-groups,ms,83,84 elementary-number-theory.addition-natural-numbers,ms,81,84 species.cauchy-series-species-of-types-in-subuniverses,ms,88,83 foundation-core.sets,ms,84,83 group-theory.cartesian-products-abelian-groups,ms,83,83 order-theory.distributive-lattices,ms,83,83 modal-type-theory.sharp-modality,ms,82,83 species.exponentials-cauchy-series-of-types-in-subuniverses,ms,82,83 univalent-combinatorics.necklaces,ms,81,83 foundation.sigma-decomposition-subuniverse,ms,81,83 foundation.trivial-relaxed-sigma-decompositions,ms,80,83 foundation-core.propositional-maps,ms,79,83 univalent-combinatorics.complements-isolated-elements,ms,117,82 group-theory.pullbacks-subsemigroups,ms,103,82 order-theory.least-upper-bounds-large-posets,ms,83,82 finite-group-theory.concrete-quaternion-group,ms,83,82 trees.raising-universe-levels-directed-trees,ms,82,82 foundation.axiom-of-choice,ms,81,82 ring-theory.nilpotent-elements-semirings,ms,80,82 linear-algebra.functoriality-vectors,ms,79,82 commutative-algebra.products-subsets-commutative-rings,ms,77,82 foundation.binary-embeddings,ms,104,81 commutative-algebra.function-commutative-semirings,ms,87,81 foundation.pi-decompositions-subuniverse,ms,81,81 group-theory.group-actions,ms,81,81 synthetic-homotopy-theory.double-loop-spaces,ms,81,81 foundation.morphisms-span-diagrams,ms,79,81 finite-group-theory.finite-commutative-monoids,ms,79,81 ring-theory.intersections-ideals-rings,ms,75,81 foundation.universal-property-identity-systems,ms,63,81 foundation.products-unordered-tuples-of-types,ms,46,81 linear-algebra.vectors-on-commutative-rings,ms,82,80 elementary-number-theory.difference-integers,ms,81,80 foundation.path-split-maps,ms,79,80 foundation.truncated-types,ms,79,80 finite-group-theory.tetrahedra-in-3-space,ms,78,80 synthetic-homotopy-theory.cocartesian-morphisms-arrows,ms,78,80 category-theory.augmented-simplex-category,ms,75,80 synthetic-homotopy-theory,ms,84,79 graph-theory.trails-undirected-graphs,ms,81,79 foundation.functoriality-pullbacks,ms,79,79 commutative-algebra.binomial-theorem-commutative-rings,ms,79,79 order-theory.subpreorders,ms,79,79 foundation.equivalences-cospans,ms,78,79 order-theory.large-preorders,ms,74,79 commutative-algebra.ideals-commutative-semirings,ms,78,78 elementary-number-theory.squares-natural-numbers,ms,76,78 order-theory.large-subposets,ms,71,78 foundation.torsorial-type-families,ms,58,78 ring-theory.binomial-theorem-rings,ms,78,77 univalent-combinatorics.retracts-of-finite-types,ms,75,77 foundation.empty-types,ms,74,77 foundation.mere-equivalences,ms,74,77 foundation-core.diagonal-maps-of-types,ms,73,77 foundation-core.operations-span-diagrams,ms,72,77 modal-type-theory.flat-modality,ms,77,76 univalent-combinatorics.trivial-sigma-decompositions,ms,76,76 foundation.diagonal-maps-of-types,ms,75,76 species.species-of-types-in-subuniverses,ms,75,76 trees.inequality-w-types,ms,75,76 linear-algebra.vectors-on-commutative-semirings,ms,76,75 commutative-algebra.binomial-theorem-commutative-semirings,ms,74,75 synthetic-homotopy-theory.connected-set-bundles-circle,ms,74,75 elementary-number-theory.parity-natural-numbers,ms,73,75 order-theory.decidable-total-preorders,ms,72,75 category-theory.natural-numbers-object-precategories,ms,72,75 foundation-core.decidable-propositions,ms,71,75 synthetic-homotopy-theory.universal-property-suspensions,ms,70,75 univalent-combinatorics.decidable-dependent-function-types,ms,69,75 commutative-algebra.intersections-ideals-commutative-rings,ms,69,75 elementary-number-theory.unit-similarity-standard-finite-types,ms,81,74 foundation.split-surjective-maps,ms,75,74 foundation.equivalences-span-diagrams-families-of-types,ms,75,74 group-theory.stabilizer-groups-concrete-group-actions,ms,74,74 linear-algebra.matrices-on-rings,ms,74,74 synthetic-homotopy-theory.pullback-property-pushouts,ms,67,74 category-theory.products-of-precategories,ms,77,73 ring-theory,ms,73,73 category-theory.one-object-precategories,ms,72,73 elementary-number-theory.sums-of-natural-numbers,ms,70,73 orthogonal-factorization-systems.null-types,ms,70,73 order-theory.dependent-products-large-suplattices,ms,76,72 foundation-core.whiskering-homotopies-concatenation,ms,72,72 univalent-combinatorics.inequality-types-with-counting,ms,72,72 elementary-number-theory.relatively-prime-natural-numbers,ms,70,72 commutative-algebra.subsets-commutative-rings,ms,68,72 category-theory.natural-transformations-functors-large-categories,ms,75,71 synthetic-homotopy-theory.spectra,ms,75,71 lists.lists-discrete-types,ms,73,71 group-theory.cartesian-products-groups,ms,70,71 structured-types.pointed-cartesian-product-types,ms,74,70 order-theory.locales,ms,73,70 group-theory.category-of-group-actions,ms,71,70 order-theory.dependent-products-large-meet-semilattices,ms,71,70 graph-theory.embeddings-undirected-graphs,ms,70,70 commutative-algebra.poset-of-ideals-commutative-rings,ms,75,69 foundation.binary-homotopies,ms,71,69 foundation.multivariable-operations,ms,71,69 foundation.action-on-homotopies-functions,ms,70,69 group-theory.powers-of-elements-groups,ms,70,69 group-theory.category-of-orbits-groups,ms,70,69 group-theory.cyclic-groups,ms,70,69 ring-theory.kernels-of-ring-homomorphisms,ms,69,69 univalent-combinatorics.discrete-sigma-decompositions,ms,69,69 foundation.unordered-tuples-of-types,ms,68,69 foundation.whiskering-higher-homotopies-composition,ms,87,68 elementary-number-theory.unit-elements-standard-finite-types,ms,73,68 foundation-core.operations-spans,ms,71,68 univalent-combinatorics.decidable-propositions,ms,68,68 structured-types.wild-monoids,ms,66,68 group-theory.commutative-monoids,ms,69,67 foundation.dependent-telescopes,ms,68,67 linear-algebra.transposition-matrices,ms,68,67 order-theory.total-orders,ms,66,67 foundation.double-powersets,ms,65,67 foundation.unit-type,ms,64,67 group-theory.representations-monoids-precategories,ms,71,66 order-theory.suplattices,ms,67,66 order-theory.large-subsuplattices,ms,66,66 synthetic-homotopy-theory.cavallos-trick,ms,66,66 category-theory.pointed-endofunctors-categories,ms,66,66 modal-type-theory.sharp-codiscrete-types,ms,65,66 category-theory.exponential-objects-precategories,ms,65,66 elementary-number-theory.maximum-standard-finite-types,ms,65,66 foundation.unordered-pairs-of-types,ms,64,66 elementary-number-theory.binomial-theorem-integers,ms,58,66 higher-group-theory.cartesian-products-higher-groups,ms,68,65 order-theory.lattices,ms,67,65 structured-types.conjugation-pointed-types,ms,65,65 synthetic-homotopy-theory.cofibers,ms,64,65 foundation-core.commuting-triangles-of-maps,ms,68,64 elementary-number-theory.euclidean-division-natural-numbers,ms,66,64 foundation.universal-property-contractible-types,ms,65,64 structured-types.mere-equivalences-types-equipped-with-endomorphisms,ms,63,64 real-numbers.dedekind-real-numbers,ms,63,63 graph-theory.neighbors-undirected-graphs,ms,63,63 elementary-number-theory.squares-integers,ms,62,63 ring-theory.subsets-semirings,ms,61,63 order-theory.decidable-posets,ms,59,63 foundation.universal-property-unit-type,ms,71,62 group-theory.dependent-products-groups,ms,67,62 organic-chemistry.alcohols,ms,63,62 reflection.definitions,ms,62,62 foundation.large-binary-relations,ms,62,62 elementary-number-theory.proper-divisors-natural-numbers,ms,62,62 foundation.double-negation,ms,61,62 order-theory.principal-lower-sets-large-posets,ms,55,62 category-theory.pointed-endofunctors-precategories,ms,64,61 structured-types.pointed-universal-property-contractible-types,ms,63,61 order-theory.upper-bounds-posets,ms,63,61 foundation.action-on-identifications-functions,ms,62,61 category-theory.homotopies-natural-transformations-large-precategories,ms,61,61 univalent-combinatorics.embeddings,ms,58,61 foundation.descent-empty-types,ms,29,61 foundation.multivariable-functoriality-set-quotients,ms,59,60 elementary-number-theory.repeating-element-standard-finite-type,ms,56,60 group-theory.function-abelian-groups,ms,61,59 synthetic-homotopy-theory.multiplication-circle,ms,61,59 group-theory.powers-of-elements-commutative-monoids,ms,60,59 group-theory.centers-groups,ms,60,59 category-theory.constant-functors,ms,60,59 group-theory.semigroups,ms,60,59 foundation.commuting-tetrahedra-of-homotopies,ms,59,59 foundation.symmetric-cores-binary-relations,ms,59,59 order-theory.principal-upper-sets-large-posets,ms,58,59 foundation.products-unordered-pairs-of-types,ms,58,59 commutative-algebra,ms,58,59 elementary-number-theory.binomial-theorem-natural-numbers,ms,55,59 foundation.operations-span-diagrams,ms,96,58 structured-types.morphisms-types-equipped-with-automorphisms,ms,58,58 foundation.singleton-induction,ms,57,58 foundation.tight-apartness-relations,ms,57,58 group-theory.category-of-groups,ms,56,58 univalent-combinatorics.function-types,ms,54,58 foundation.equality-dependent-function-types,ms,61,57 organic-chemistry.hydrocarbons,ms,58,57 graph-theory.faithful-morphisms-undirected-graphs,ms,58,57 commutative-algebra.nilradical-commutative-rings,ms,56,57 higher-group-theory.homomorphisms-higher-group-actions,ms,55,57 foundation.postcomposition-dependent-functions,ms,55,57 foundation.preunivalence,ms,59,56 graph-theory.polygons,ms,58,56 modal-type-theory.flat-dependent-pair-types,ms,57,56 graph-theory.finite-graphs,ms,57,56 foundation.transport-along-homotopies,ms,56,56 foundation.identity-systems,ms,56,56 graph-theory.raising-universe-levels-directed-graphs,ms,56,56 foundation.dependent-inverse-sequential-diagrams,ms,56,56 foundation.decidable-maps,ms,55,56 orthogonal-factorization-systems.factorization-operations-global-function-classes,ms,55,56 foundation.action-on-equivalences-functions,ms,54,56 elementary-number-theory.sieve-of-eratosthenes,ms,54,56 structured-types.morphisms-wild-monoids,ms,104,55 foundation.connected-components,ms,59,55 order-theory.lower-bounds-posets,ms,58,55 structured-types.function-wild-monoids,ms,57,55 foundation-core,ms,56,55 group-theory.precategory-of-group-actions,ms,56,55 group-theory.commuting-elements-semigroups,ms,55,55 group-theory.centralizer-subgroups,ms,55,55 foundation.full-subtypes,ms,54,55 order-theory.accessible-elements-relations,ms,54,55 order-theory.finite-total-orders,ms,54,55 foundation.equivalences-inverse-sequential-diagrams,ms,53,55 group-theory.commutators-of-elements-groups,ms,52,55 univalent-combinatorics.decidable-dependent-pair-types,ms,52,55 foundation.negated-equality,ms,52,55 group-theory.endomorphism-rings-abelian-groups,ms,56,54 group-theory.category-of-semigroups,ms,55,54 group-theory.kernels-homomorphisms-abelian-groups,ms,55,54 group-theory.kernels-homomorphisms-concrete-groups,ms,55,54 category-theory.essentially-surjective-functors-precategories,ms,55,54 order-theory.homomorphisms-frames,ms,54,54 ring-theory.powers-of-elements-semirings,ms,53,54 foundation.conjunction,ms,53,54 commutative-algebra.radical-ideals-generated-by-subsets-commutative-rings,ms,53,54 orthogonal-factorization-systems.functoriality-pullback-hom,ms,52,54 elementary-number-theory.cofibonacci,ms,52,54 graph-theory.undirected-graphs,ms,59,53 foundation-core.empty-types,ms,56,53 category-theory.functors-large-categories,ms,56,53 synthetic-homotopy-theory.conjugation-loops,ms,54,53 trees.w-type-of-natural-numbers,ms,53,53 foundation.action-on-equivalences-type-families-over-subuniverses,ms,53,53 foundation.decidable-dependent-pair-types,ms,52,53 foundation-core.embeddings,ms,51,53 ring-theory.nilpotent-elements-rings,ms,51,53 higher-group-theory.equivalences-higher-groups,ms,55,52 lists.sorting-algorithms-lists,ms,54,52 synthetic-homotopy-theory.tangent-spheres,ms,54,52 order-theory.meet-suplattices,ms,54,52 univalent-combinatorics.repetitions-of-values,ms,53,52 universal-algebra.congruences,ms,53,52 category-theory.subterminal-precategories,ms,53,52 ring-theory.quotient-rings,ms,51,52 elementary-number-theory.distance-integers,ms,51,52 foundation.products-equivalence-relations,ms,51,52 commutative-algebra.powers-of-elements-commutative-rings,ms,51,52 foundation-core.path-split-maps,ms,50,52 structured-types.wild-loops,ms,50,52 group-theory.multiples-of-elements-abelian-groups,ms,80,51 group-theory.function-groups,ms,53,51 category-theory.isomorphism-induction-precategories,ms,53,51 order-theory.precategory-of-posets,ms,52,51 univalent-combinatorics.classical-finite-types,ms,52,51 order-theory.homomorphisms-meet-sup-lattices,ms,51,51 ring-theory.precategory-of-semirings,ms,51,51 group-theory.central-elements-groups,ms,51,51 commutative-algebra.subsets-commutative-semirings,ms,50,51 foundation.universal-property-maybe,ms,53,50 finite-algebra.semisimple-commutative-finite-rings,ms,53,50 elementary-number-theory.multiplication-integer-fractions,ms,52,50 category-theory.anafunctors-categories,ms,52,50 foundation.iterated-dependent-pair-types,ms,52,50 order-theory.homomorphisms-sup-lattices,ms,51,50 order-theory.large-subpreorders,ms,49,50 trees.universal-multiset,ms,49,50 foundation.whiskering-identifications-concatenation,ms,48,50 univalent-combinatorics.unions-subtypes,ms,48,50 foundation.universal-property-empty-type,ms,50,49 lists.flattening-lists,ms,49,49 group-theory.subsets-semigroups,ms,49,49 foundation.mere-equality,ms,47,49 foundation.retracts-of-types,ms,47,49 ring-theory.multiples-of-elements-rings,ms,54,48 graph-theory.directed-graphs,ms,51,48 foundation.implicit-function-types,ms,50,48 graph-theory.complete-bipartite-graphs,ms,49,48 foundation.transport-along-identifications,ms,49,48 order-theory.chains-preorders,ms,48,48 foundation.subtype-duality,ms,48,48 trees,ms,48,48 group-theory.cayleys-theorem,ms,47,48 commutative-algebra.precategory-of-commutative-semirings,ms,47,48 order-theory.similarity-of-elements-large-preorders,ms,50,47 universal-algebra.algebras-of-theories,ms,48,47 ring-theory.precategory-of-rings,ms,47,47 univalent-combinatorics.skipping-element-standard-finite-types,ms,47,47 synthetic-homotopy-theory.dependent-universal-property-suspensions,ms,47,47 foundation.pullback-squares,ms,46,47 elementary-number-theory.initial-segments-natural-numbers,ms,44,47 category-theory.full-functors-precategories,ms,48,46 category-theory.embeddings-precategories,ms,48,46 orthogonal-factorization-systems.wide-global-function-classes,ms,47,46 category-theory.epimorphisms-in-large-precategories,ms,47,46 foundation.operations-spans,ms,46,46 elementary-number-theory.monoid-of-natural-numbers-with-maximum,ms,46,46 linear-algebra.matrices,ms,45,46 univalent-combinatorics.kuratowsky-finite-sets,ms,45,46 foundation.discrete-types,ms,45,46 group-theory.category-of-abelian-groups,ms,42,46 commutative-algebra.precategory-of-commutative-rings,ms,48,45 structured-types.dependent-products-h-spaces,ms,46,45 foundation.unital-binary-operations,ms,46,45 category-theory.monomorphisms-in-large-precategories,ms,46,45 category-theory.initial-objects-precategories,ms,45,45 univalent-combinatorics.sums-of-natural-numbers,ms,45,45 synthetic-homotopy-theory.truncated-acyclic-types,ms,45,45 group-theory.monoid-actions,ms,45,45 synthetic-homotopy-theory.premanifolds,ms,47,44 foundation.span-diagrams,ms,46,44 group-theory.subsets-monoids,ms,45,44 foundation-core.1-types,ms,45,44 foundation.type-arithmetic-dependent-function-types,ms,44,44 foundation-core.univalence,ms,44,44 category-theory.natural-isomorphisms-functors-large-precategories,ms,44,44 group-theory.commuting-elements-groups,ms,44,44 foundation.mere-embeddings,ms,43,44 modal-type-theory.flat-discrete-types,ms,43,44 foundation.decidable-relations,ms,43,44 elementary-number-theory.divisibility-standard-finite-types,ms,42,44 ring-theory.central-elements-rings,ms,42,44 trees.w-type-of-propositions,ms,42,44 order-theory.upper-bounds-large-posets,ms,45,43 group-theory.equivalences-concrete-groups,ms,44,43 category-theory.large-subprecategories,ms,44,43 synthetic-homotopy-theory.groups-of-loops-in-1-types,ms,43,43 group-theory.cartesian-products-monoids,ms,43,43 order-theory.total-preorders,ms,42,43 elementary-number-theory.kolakoski-sequence,ms,41,43 order-theory.directed-families,ms,41,43 foundation.whiskering-operations,ms,65,42 univalent-combinatorics.image-of-maps,ms,46,42 group-theory.free-concrete-group-actions,ms,45,42 order-theory.chains-posets,ms,45,42 group-theory.intersections-subgroups-abelian-groups,ms,44,42 foundation.decidable-dependent-function-types,ms,43,42 order-theory.homomorphisms-large-frames,ms,43,42 order-theory.finite-posets,ms,43,42 group-theory.wild-representations-monoids,ms,42,42 foundation.universal-property-equivalences,ms,42,42 category-theory.essentially-injective-functors-precategories,ms,42,42 foundation.universal-property-booleans,ms,40,42 elementary-number-theory.addition-rational-numbers,ms,39,42 category-theory.terminal-objects-precategories,ms,62,41 graph-theory.totally-faithful-morphisms-undirected-graphs,ms,43,41 order-theory.decidable-subpreorders,ms,43,41 foundation.morphisms-spans,ms,43,41 univalent-combinatorics.equivalences,ms,42,41 foundation.whiskering-homotopies-concatenation,ms,42,41 order-theory.decidable-subposets,ms,42,41 orthogonal-factorization-systems,ms,41,41 elementary-number-theory.peano-arithmetic,ms,41,41 group-theory.dependent-products-monoids,ms,41,41 group-theory.rational-commutative-monoids,ms,40,41 order-theory.decidable-preorders,ms,40,41 elementary-number-theory.bounded-sums-arithmetic-functions,ms,40,41 order-theory.lower-bounds-large-posets,ms,39,41 order-theory.dependent-products-large-posets,ms,39,41 ring-theory.intersections-ideals-semirings,ms,38,41 order-theory.well-founded-relations,ms,42,40 group-theory.inverse-semigroups,ms,42,40 ring-theory.nil-ideals-rings,ms,41,40 order-theory.homomorphisms-large-locales,ms,41,40 order-theory.homomorphisms-large-meet-semilattices,ms,41,40 foundation.subsingleton-induction,ms,41,40 structured-types.commuting-squares-of-pointed-maps,ms,41,40 foundation.commuting-tetrahedra-of-maps,ms,40,40 ring-theory.trivial-rings,ms,40,40 univalent-combinatorics.cycle-partitions,ms,40,40 univalent-combinatorics.cubes,ms,40,40 group-theory.torsion-elements-groups,ms,39,40 synthetic-homotopy-theory.dependent-sequential-diagrams,ms,39,40 univalent-combinatorics.equality-finite-types,ms,38,40 foundation.pullbacks-subtypes,ms,38,40 elementary-number-theory.strictly-ordered-pairs-of-natural-numbers,ms,37,40 group-theory.dependent-products-commutative-monoids,ms,37,40 synthetic-homotopy-theory.prespectra,ms,43,39 commutative-algebra.multiples-of-elements-commutative-rings,ms,41,39 organic-chemistry.methane,ms,41,39 group-theory.orders-of-elements-groups,ms,41,39 foundation.unions-subtypes,ms,39,39 elementary-number-theory.poset-of-natural-numbers-ordered-by-divisibility,ms,39,39 foundation.large-locale-of-propositions,ms,39,39 elementary-number-theory.based-induction-natural-numbers,ms,39,39 structured-types.function-h-spaces,ms,39,39 group-theory.centers-monoids,ms,39,39 foundation.type-arithmetic-booleans,ms,38,39 order-theory.homomorphisms-large-suplattices,ms,38,39 species.cauchy-series-species-of-types,ms,41,38 group-theory.subsets-commutative-monoids,ms,40,38 foundation.precomposition-type-families,ms,40,38 univalent-combinatorics.injective-maps,ms,39,38 orthogonal-factorization-systems.localizations-subuniverses,ms,39,38 reflection.terms,ms,38,38 elementary-number-theory.exponentiation-natural-numbers,ms,37,38 order-theory.greatest-lower-bounds-large-posets,ms,36,38 group-theory.embeddings-groups,ms,40,37 category-theory.sieves-in-categories,ms,38,37 synthetic-homotopy-theory.acyclic-types,ms,38,37 set-theory.baire-space,ms,38,37 graph-theory.edge-coloured-undirected-graphs,ms,37,37 group-theory.commuting-elements-monoids,ms,37,37 group-theory.function-commutative-monoids,ms,37,37 ring-theory.central-elements-semirings,ms,37,37 commutative-algebra.category-of-commutative-rings,ms,36,37 foundation.powersets,ms,36,37 foundation-core.families-of-equivalences,ms,50,36 lists.sorting-algorithms-vectors,ms,37,36 higher-group-theory.higher-groups,ms,37,36 trees.rooted-undirected-trees,ms,37,36 group-theory.centers-semigroups,ms,37,36 category-theory.embedding-maps-precategories,ms,36,36 order-theory.maximal-chains-preorders,ms,36,36 graph-theory.matchings,ms,35,36 foundation.copartial-functions,ms,35,36 group-theory.precategory-of-concrete-groups,ms,35,36 orthogonal-factorization-systems.wide-function-classes,ms,34,36 graph-theory.complete-multipartite-graphs,ms,36,35 elementary-number-theory.natural-numbers,ms,36,35 category-theory.endomorphisms-in-precategories,ms,35,35 ring-theory.category-of-rings,ms,35,35 group-theory.monomorphisms-groups,ms,35,35 category-theory.endomorphisms-in-categories,ms,35,35 orthogonal-factorization-systems.localizations-maps,ms,35,35 species.exponentials-cauchy-series-of-types,ms,35,35 foundation.induction-principle-propositional-truncation,ms,34,35 structured-types.finite-multiplication-magmas,ms,34,35 univalent-combinatorics.equivalences-standard-finite-types,ms,34,35 foundation.univalence-implies-function-extensionality,ms,34,35 group-theory.embeddings-abelian-groups,ms,36,34 order-theory.dependent-products-large-preorders,ms,36,34 group-theory.function-monoids,ms,35,34 lists.sort-by-insertion-lists,ms,34,34 group-theory.surjective-group-homomorphisms,ms,34,34 foundation.intersections-subtypes,ms,34,34 graph-theory.embeddings-directed-graphs,ms,33,34 elementary-number-theory.factorials,ms,33,34 foundation.action-on-equivalences-functions-out-of-subuniverses,ms,33,34 foundation.propositions,ms,34,33 order-theory.similarity-of-order-preserving-maps-large-posets,ms,34,33 group-theory.epimorphisms-groups,ms,33,33 group-theory.cartesian-products-semigroups,ms,33,33 group-theory.precategory-of-monoids,ms,33,33 group-theory.trivial-groups,ms,33,33 synthetic-homotopy-theory.0-acyclic-maps,ms,32,33 foundation.interchange-law,ms,32,33 synthetic-homotopy-theory.descent-circle-constant-families,ms,31,33 foundation.functoriality-sequential-limits,ms,31,33 order-theory.maximal-chains-posets,ms,34,32 species.coproducts-species-of-types,ms,32,32 foundation.truncation-levels,ms,32,32 ring-theory.local-rings,ms,32,32 foundation.subterminal-types,ms,32,32 foundation.structure,ms,31,32 group-theory.large-semigroups,ms,31,32 orthogonal-factorization-systems.local-families-of-types,ms,33,31 elementary-number-theory.nonzero-integers,ms,33,31 group-theory.central-elements-semigroups,ms,32,31 univalent-combinatorics.ramsey-theory,ms,32,31 foundation.constant-type-families,ms,32,31 graph-theory.simple-undirected-graphs,ms,31,31 univalent-combinatorics.double-counting,ms,31,31 order-theory.top-elements-posets,ms,31,31 order-theory.inhabited-finite-total-orders,ms,31,31 synthetic-homotopy-theory.0-acyclic-types,ms,31,31 elementary-number-theory.divisibility-modular-arithmetic,ms,31,31 group-theory.mere-equivalences-concrete-group-actions,ms,31,31 structured-types.cyclic-types,ms,31,31 higher-group-theory.subgroups-higher-groups,ms,31,31 foundation.negation,ms,30,31 graph-theory,ms,30,31 universal-algebra.signatures,ms,30,31 foundation.complements-subtypes,ms,30,31 order-theory.finite-coverings-locales,ms,30,30 foundation.copartial-elements,ms,30,30 group-theory.characteristic-subgroups,ms,30,30 universal-algebra.homomorphisms-of-algebras,ms,30,30 commutative-algebra.zariski-topology,ms,30,30 order-theory.bottom-elements-posets,ms,30,30 organic-chemistry.saturated-carbons,ms,30,30 structured-types,ms,29,30 group-theory.surjective-semigroup-homomorphisms,ms,28,30 elementary-number-theory.squares-modular-arithmetic,ms,27,30 commutative-algebra.local-commutative-rings,ms,30,29 foundation.projective-types,ms,30,29 graph-theory.reflecting-maps-undirected-graphs,ms,30,29 foundation.endomorphisms,ms,30,29 group-theory.trivial-group-homomorphisms,ms,30,29 univalent-combinatorics.counting-maybe,ms,30,29 foundation.small-maps,ms,29,29 univalent-combinatorics.dedekind-finite-sets,ms,29,29 foundation.dependent-pair-types,ms,29,29 foundation.cantors-diagonal-argument,ms,29,29 group-theory.dependent-products-semigroups,ms,29,29 category-theory.representable-functors-categories,ms,28,29 elementary-number-theory.legendre-symbol,ms,28,29 foundation.dependent-homotopies,ms,28,29 orthogonal-factorization-systems.lifting-operations,ms,27,29 order-theory.similarity-of-order-preserving-maps-large-preorders,ms,29,28 commutative-algebra.trivial-commutative-rings,ms,28,28 order-theory.reflective-galois-connections-large-posets,ms,28,28 foundation.morphisms-binary-relations,ms,28,28 elementary-number-theory.taxicab-numbers,ms,27,28 foundation.small-types,ms,27,28 order-theory.lower-types-preorders,ms,26,28 structured-types.magmas,ms,30,27 orthogonal-factorization-systems.mere-lifting-properties,ms,30,27 structured-types.wild-quasigroups,ms,28,27 trees.elementhood-relation-coalgebras-polynomial-endofunctors,ms,28,27 univalent-combinatorics.isotopies-latin-squares,ms,27,27 foundation.binary-equivalences,ms,27,27 foundation.multisubsets,ms,27,27 elementary-number-theory.standard-cyclic-groups,ms,27,27 commutative-algebra.powers-of-elements-commutative-semirings,ms,27,27 group-theory.precategory-of-commutative-monoids,ms,27,27 foundation.iterating-involutions,ms,27,27 univalent-combinatorics.standard-finite-trees,ms,26,27 foundation.inverse-sequential-diagrams,ms,26,27 foundation.partial-functions,ms,26,27 elementary-number-theory.dirichlet-convolution,ms,24,27 univalent-combinatorics.petri-nets,ms,24,27 category-theory.equivalences-of-precategories,ms,27,26 category-theory.rigid-objects-precategories,ms,27,26 structured-types.faithful-pointed-maps,ms,27,26 trees.bounded-multisets,ms,27,26 species.equivalences-species-of-types-in-subuniverses,ms,27,26 species.hasse-weil-species,ms,26,26 graph-theory.paths-undirected-graphs,ms,26,26 graph-theory.geometric-realizations-undirected-graphs,ms,27,25 structured-types.noncoherent-h-spaces,ms,27,25 ring-theory.idempotent-elements-rings,ms,26,25 group-theory.conjugation-concrete-groups,ms,26,25 group-theory.precategory-of-groups,ms,26,25 group-theory.opposite-groups,ms,25,25 univalent-combinatorics.latin-squares,ms,25,25 graph-theory.stereoisomerism-enriched-undirected-graphs,ms,25,25 elementary-number-theory.multiplication-lists-of-natural-numbers,ms,25,25 synthetic-homotopy-theory.suspensions-of-pointed-types,ms,24,25 ring-theory.invariant-basis-property-rings,ms,24,25 group-theory.trivial-subgroups,ms,26,24 trees.elementhood-relation-w-types,ms,26,24 category-theory.discrete-categories,ms,25,24 group-theory.transitive-group-actions,ms,25,24 group-theory.products-of-elements-monoids,ms,25,24 category-theory.rigid-objects-categories,ms,25,24 foundation.lawveres-fixed-point-theorem,ms,25,24 group-theory.trivial-concrete-groups,ms,24,24 group-theory.monomorphisms-concrete-groups,ms,24,24 group-theory.subsets-abelian-groups,ms,24,24 foundation.cospans,ms,24,24 elementary-number-theory.group-of-integers,ms,23,24 foundation.morphisms-twisted-arrows,ms,23,24 commutative-algebra.nilradicals-commutative-semirings,ms,24,23 structured-types.pointed-unit-type,ms,24,23 finite-group-theory,ms,24,23 elementary-number-theory.binomial-coefficients,ms,23,23 species.precategory-of-finite-species,ms,23,23 higher-group-theory.trivial-higher-groups,ms,23,23 group-theory.products-of-tuples-of-elements-commutative-monoids,ms,23,23 foundation.effective-maps-equivalence-relations,ms,21,23 order-theory.well-founded-orders,ms,24,22 group-theory.function-semigroups,ms,23,22 foundation.hilberts-epsilon-operators,ms,23,22 univalent-combinatorics.steiner-systems,ms,23,22 ring-theory.radical-ideals-rings,ms,23,22 foundation.cartesian-product-types,ms,23,22 univalent-combinatorics.orientations-cubes,ms,22,22 category-theory.essential-fibers-of-functors-precategories,ms,22,22 foundation.noncontractible-types,ms,22,22 graph-theory.vertex-covers,ms,22,22 order-theory.coverings-locales,ms,22,22 linear-algebra.diagonal-matrices-on-rings,ms,22,22 foundation.multivariable-sections,ms,22,22 higher-group-theory.cyclic-higher-groups,ms,22,22 foundation.standard-apartness-relations,ms,22,22 species.cartesian-products-species-of-types,ms,22,22 foundation-core.function-types,ms,22,22 ring-theory.opposite-rings,ms,22,22 group-theory.precategory-of-semigroups,ms,22,22 order-theory.commuting-squares-of-order-preserving-maps-large-posets,ms,22,22 group-theory.subsets-groups,ms,22,22 elementary-number-theory.ordinal-induction-natural-numbers,ms,21,22 universal-algebra.models-of-signatures,ms,21,22 graph-theory.eulerian-circuits-undirected-graphs,ms,21,22 group-theory.elements-of-finite-order-groups,ms,23,21 group-theory.concrete-monoids,ms,22,21 structured-types.pointed-dependent-functions,ms,22,21 higher-group-theory.conjugation,ms,22,21 elementary-number-theory.inequality-integer-fractions,ms,22,21 group-theory.orbit-stabilizer-theorem-concrete-groups,ms,21,21 foundation.kernel-span-diagrams-of-maps,ms,21,21 group-theory.shriek-concrete-group-actions,ms,21,21 synthetic-homotopy-theory.spheres,ms,21,21 foundation.dependent-binary-homotopies,ms,21,21 univalent-combinatorics.small-types,ms,21,21 foundation.composite-maps-in-inverse-sequential-diagrams,ms,21,21 group-theory.central-elements-monoids,ms,21,21 univalent-combinatorics.quotients-finite-types,ms,21,21 trees.empty-multisets,ms,21,21 trees.lower-types-w-types,ms,21,21 foundation.double-negation-modality,ms,20,21 graph-theory.mere-equivalences-undirected-graphs,ms,21,20 group-theory.perfect-subgroups,ms,21,20 orthogonal-factorization-systems.cd-structures,ms,21,20 graph-theory.trails-directed-graphs,ms,21,20 elementary-number-theory.collatz-bijection,ms,20,20 foundation.morphisms-cospans,ms,20,20 structured-types.sets-equipped-with-automorphisms,ms,20,20 synthetic-homotopy-theory.suspension-prespectra,ms,19,20 univalent-combinatorics.involution-standard-finite-types,ms,19,20 order-theory.directed-complete-posets,ms,19,20 foundation-core.dependent-identifications,ms,18,20 group-theory.opposite-semigroups,ms,44,19 finite-algebra,ms,22,19 foundation-core.endomorphisms,ms,21,19 foundation.separated-types,ms,20,19 foundation.lesser-limited-principle-of-omniscience,ms,20,19 group-theory.exponents-groups,ms,19,19 group-theory.commuting-squares-of-group-homomorphisms,ms,19,19 foundation.global-choice,ms,19,19 foundation.automorphisms,ms,19,19 trees.submultisets,ms,19,19 order-theory.lower-sets-large-posets,ms,19,19 species.unlabeled-structures-species,ms,19,19 foundation.dependent-function-types,ms,19,19 species.species-of-types,ms,18,19 orthogonal-factorization-systems.identity-modality,ms,18,19 elementary-number-theory.commutative-semiring-of-natural-numbers,ms,18,19 species,ms,18,19 graph-theory.voltage-graphs,ms,17,19 synthetic-homotopy-theory.maps-of-prespectra,ms,20,18 univalent-combinatorics.main-classes-of-latin-squares,ms,19,18 graph-theory.regular-undirected-graphs,ms,18,18 higher-group-theory.higher-group-actions,ms,18,18 finite-group-theory.alternating-groups,ms,18,18 species.equivalences-species-of-types,ms,18,18 group-theory.concrete-group-actions,ms,18,18 foundation.weakly-constant-maps,ms,18,18 elementary-number-theory.relatively-prime-integers,ms,18,18 order-theory.locally-finite-posets,ms,18,18 category-theory.equivalences-of-large-precategories,ms,18,18 order-theory.top-elements-large-posets,ms,18,18 foundation.replacement,ms,18,18 elementary-number-theory.jacobi-symbol,ms,17,18 foundation.dependent-epimorphisms-with-respect-to-truncated-types,ms,17,18 elementary-number-theory.hardy-ramanujan-number,ms,17,18 foundation.discrete-reflexive-relations,ms,17,18 organic-chemistry.alkenes,ms,17,18 category-theory.commuting-squares-of-morphisms-in-large-precategories,ms,17,18 elementary-number-theory.powers-integers,ms,16,18 foundation.law-of-excluded-middle,ms,18,17 group-theory.mere-equivalences-group-actions,ms,18,17 group-theory.furstenberg-groups,ms,18,17 orthogonal-factorization-systems.raise-modalities,ms,18,17 foundation.set-presented-types,ms,18,17 order-theory.top-elements-preorders,ms,18,17 foundation.product-decompositions,ms,17,17 structured-types.wild-semigroups,ms,17,17 modal-type-theory.sharp-codiscrete-maps,ms,17,17 order-theory.bottom-elements-preorders,ms,17,17 structured-types.types-equipped-with-automorphisms,ms,17,17 elementary-number-theory.inequality-rational-numbers,ms,17,17 order-theory.precategory-of-total-orders,ms,17,17 foundation.spans,ms,17,17 reflection.boolean-reflection,ms,16,17 order-theory.precategory-of-inhabited-finite-total-orders,ms,16,17 order-theory.precategory-of-decidable-total-orders,ms,16,17 elementary-number-theory.collatz-conjecture,ms,16,17 foundation.sigma-closed-subuniverses,ms,47,16 type-theories,ms,18,16 univalent-combinatorics.finite-connected-components,ms,17,16 foundation.families-of-equivalences,ms,17,16 order-theory.precategory-of-finite-total-orders,ms,17,16 graph-theory.connected-undirected-graphs,ms,17,16 synthetic-homotopy-theory.mere-spheres,ms,17,16 trees.multisets,ms,17,16 group-theory.sheargroups,ms,17,16 elementary-number-theory.multiplication-rational-numbers,ms,17,16 foundation.dubuc-penon-compact-types,ms,17,16 structured-types.morphisms-magmas,ms,16,16 foundation.evaluation-functions,ms,16,16 structured-types.involutive-types,ms,16,16 ring-theory.free-rings-with-one-generator,ms,16,16 reflection.fixity,ms,16,16 order-theory.precategory-of-finite-posets,ms,16,16 foundation.operations-spans-families-of-types,ms,16,16 online-encyclopedia-of-integer-sequences.oeis,ms,16,16 elementary-number-theory.catalan-numbers,ms,15,16 order-theory.ideals-preorders,ms,15,16 elementary-number-theory.decidable-total-order-standard-finite-types,ms,15,16 species.dirichlet-series-species-of-finite-inhabited-types,ms,15,16 synthetic-homotopy-theory.infinite-complex-projective-space,ms,17,15 group-theory.e8-lattice,ms,17,15 category-theory.commuting-squares-of-morphisms-in-set-magmoids,ms,16,15 elementary-number-theory.nonzero-natural-numbers,ms,16,15 finite-group-theory.alternating-concrete-groups,ms,16,15 lists.predicates-on-lists,ms,16,15 elementary-number-theory.lower-bounds-natural-numbers,ms,16,15 synthetic-homotopy-theory.sequential-diagrams,ms,15,15 foundation.identity-truncated-types,ms,15,15 foundation.preidempotent-maps,ms,15,15 foundation.limited-principle-of-omniscience,ms,15,15 trees.coalgebras-polynomial-endofunctors,ms,15,15 foundation-core.precomposition-dependent-functions,ms,15,15 species.dirichlet-series-species-of-types-in-subuniverses,ms,15,15 organic-chemistry.alkynes,ms,15,15 reflection.metavariables,ms,15,15 group-theory.principal-group-actions,ms,15,15 foundation.permutations-spans-families-of-types,ms,15,15 foundation.uniqueness-truncation,ms,15,15 category-theory.equivalences-of-categories,ms,15,15 structured-types.fibers-of-pointed-maps,ms,15,15 ring-theory.characteristics-rings,ms,15,15 order-theory.upper-sets-large-posets,ms,15,15 trees.coalgebra-of-enriched-directed-trees,ms,15,15 foundation-core.coproduct-types,ms,15,15 foundation.truncation-modalities,ms,15,15 group-theory.normal-subgroups-concrete-groups,ms,15,15 set-theory.infinite-sets,ms,15,15 reflection.arguments,ms,15,15 foundation.constant-span-diagrams,ms,14,15 trees.planar-binary-trees,ms,14,15 synthetic-homotopy-theory.morphisms-descent-data-circle,ms,14,15 foundation.spans-families-of-types,ms,14,15 foundation.multivariable-decidable-relations,ms,15,14 foundation.weak-limited-principle-of-omniscience,ms,15,14 group-theory.exponents-abelian-groups,ms,15,14 group-theory.perfect-cores,ms,14,14 elementary-number-theory.products-of-natural-numbers,ms,14,14 order-theory.interval-subposets,ms,14,14 linear-algebra,ms,14,14 graph-theory.orientations-undirected-graphs,ms,14,14 elementary-number-theory.eulers-totient-function,ms,14,14 foundation.span-diagrams-families-of-types,ms,14,14 foundation.total-partial-functions,ms,14,14 orthogonal-factorization-systems.locally-small-modal-operators,ms,14,14 group-theory.perfect-groups,ms,14,14 trees.algebras-polynomial-endofunctors,ms,14,14 foundation.principle-of-omniscience,ms,14,14 set-theory.uncountable-sets,ms,14,14 group-theory.stabilizer-groups,ms,14,14 elementary-number-theory.half-integers,ms,14,14 foundation.partial-elements,ms,14,14 elementary-number-theory.goldbach-conjecture,ms,13,14 elementary-number-theory.decidable-total-order-natural-numbers,ms,13,14 group-theory.orbits-group-actions,ms,14,13 orthogonal-factorization-systems.double-lifts-families-of-elements,ms,14,13 synthetic-homotopy-theory.sequentially-compact-types,ms,14,13 linear-algebra.functoriality-matrices,ms,13,13 foundation.binary-equivalences-unordered-pairs-of-types,ms,13,13 orthogonal-factorization-systems.zero-modality,ms,13,13 foundation.dependent-epimorphisms,ms,13,13 foundation.multivariable-relations,ms,13,13 foundation.bands,ms,13,13 foundation.products-binary-relations,ms,13,13 reflection.names,ms,13,13 foundation.commuting-pentagons-of-identifications,ms,12,13 primitives.floats,ms,12,13 ring-theory.generating-elements-rings,ms,12,13 structured-types.pointed-families-of-types,ms,13,12 commutative-algebra.boolean-rings,ms,13,12 higher-group-theory.symmetric-higher-groups,ms,13,12 species.unit-cauchy-composition-species-of-types-in-subuniverses,ms,13,12 elementary-number-theory.upper-bounds-natural-numbers,ms,13,12 foundation.partial-sequences,ms,12,12 group-theory.orbits-concrete-group-actions,ms,12,12 orthogonal-factorization-systems.separated-types,ms,12,12 group-theory.generating-sets-groups,ms,12,12 structured-types.cartesian-products-types-equipped-with-endomorphisms,ms,12,12 elementary-number-theory.monoid-of-natural-numbers-with-addition,ms,12,12 reflection.literals,ms,12,12 modal-type-theory.crisp-identity-types,ms,12,12 graph-theory.hypergraphs,ms,12,12 trees.rooted-quasitrees,ms,12,12 elementary-number-theory.mersenne-primes,ms,12,12 trees.coalgebra-of-directed-trees,ms,12,12 modal-type-theory.crisp-law-of-excluded-middle,ms,12,12 structured-types.constant-maps-pointed-types,ms,12,12 lists,ms,12,12 foundation-core.discrete-types,ms,12,12 species.cauchy-products-species-of-types,ms,11,12 ring-theory.division-rings,ms,11,12 elementary-number-theory.cubes-natural-numbers,ms,10,12 reflection,ms,12,11 structured-types.contractible-pointed-types,ms,12,11 structured-types.pointed-sections,ms,12,11 category-theory.commuting-squares-of-morphisms-in-precategories,ms,12,11 foundation.injective-maps,ms,12,11 higher-group-theory,ms,12,11 foundation.cospan-diagrams,ms,11,11 trees.indexed-w-types,ms,11,11 group-theory.unordered-tuples-of-elements-commutative-monoids,ms,11,11 foundation.opposite-spans,ms,11,11 foundation.transposition-span-diagrams,ms,11,11 group-theory.dihedral-groups,ms,11,11 modal-type-theory.flat-dependent-function-types,ms,11,11 structured-types.types-equipped-with-endomorphisms,ms,11,11 foundation.propositional-resizing,ms,11,11 structured-types.pointed-dependent-pair-types,ms,11,11 set-theory.cantor-space,ms,11,11 orthogonal-factorization-systems.cellular-maps,ms,11,11 structured-types.symmetric-h-spaces,ms,11,11 foundation.reflexive-relations,ms,11,11 structured-types.central-h-spaces,ms,11,11 orthogonal-factorization-systems.sigma-closed-modalities,ms,10,11 univalent-combinatorics.maybe,ms,10,11 primitives.strings,ms,10,11 synthetic-homotopy-theory.join-powers-of-types,ms,12,10 species.cycle-index-series-species-of-types,ms,11,10 graph-theory.reflexive-graphs,ms,10,10 foundation.0-images-of-maps,ms,10,10 elementary-number-theory.multiplicative-monoid-of-natural-numbers,ms,10,10 foundation.terminal-spans-families-of-types,ms,10,10 structured-types.iterated-pointed-cartesian-product-types,ms,10,10 foundation.strongly-extensional-maps,ms,10,10 graph-theory.directed-graph-structures-on-standard-finite-sets,ms,10,10 orthogonal-factorization-systems.sigma-closed-reflective-modalities,ms,10,10 foundation.2-types,ms,10,10 foundation.truncated-equality,ms,10,10 graph-theory.undirected-graph-structures-on-standard-finite-sets,ms,,10 orthogonal-factorization-systems.reflective-modalities,ms,,10 group-theory.substitution-functor-concrete-group-actions,ms,,10 elementary-number-theory.twin-prime-conjecture,ms,10, univalent-combinatorics.standard-finite-pruned-trees,ms,10, elementary-number-theory.stirling-numbers-of-the-second-kind,ms,10, graph-theory.complete-undirected-graphs,ms,10, species.dirichlet-products-species-of-types,ms,10, ```