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.

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,