Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Profile typechecking performance #1031

Merged
merged 18 commits into from
Feb 22, 2024
Merged

Conversation

fredrik-bakke
Copy link
Collaborator

@fredrik-bakke fredrik-bakke commented Feb 17, 2024

  • Set up make-hook for profiling
  • Set up GitHub workflow for profiling
  • Generate pretty graphs based on profiling data
  • Host graphs on a webpage

I'm not yet completely sure I set up the workflow correctly. Also note that 4GB memory is not enough for this profiler to work (#985).

Resolves #1030.

Example output
Total                                                                             90,422ms 
Miscellaneous                                                                     26,895ms 
category-theory.category-of-maps-from-small-to-large-categories                    7,846ms 
everything                                                                         3,827ms 
synthetic-homotopy-theory.functoriality-sequential-colimits                        2,399ms 
trees.underlying-trees-elements-coalgebras-polynomial-endofunctors                 2,299ms 
finite-group-theory.simpson-delooping-sign-homomorphism                            1,900ms 
category-theory.slice-precategories                                                1,878ms 
synthetic-homotopy-theory.26-id-pushout                                            1,728ms 
synthetic-homotopy-theory.universal-cover-circle                                   1,570ms 
set-theory.cumulative-hierarchy                                                    1,560ms 
polytopes.abstract-polytopes                                                       1,459ms 
synthetic-homotopy-theory.hatchers-acyclic-type                                    1,446ms 
trees.equivalences-enriched-directed-trees                                         1,164ms 
trees.combinator-enriched-directed-trees                                           1,161ms 
trees.underlying-trees-of-elements-of-w-types                                      1,143ms 
synthetic-homotopy-theory.acyclic-maps                                             1,034ms 
finite-group-theory.abstract-quaternion-group                                      1,012ms 
commutative-algebra.joins-radical-ideals-commutative-rings                         1,006ms 
order-theory.galois-connections                                                      928ms 
category-theory.adjunctions-large-precategories                                      881ms 
group-theory.torsors                                                                 814ms 
group-theory.normal-submonoids                                                       794ms 
ring-theory.left-ideals-generated-by-subsets-rings                                   665ms 
commutative-algebra.euclidean-domains                                                586ms 
synthetic-homotopy-theory.sections-descent-circle                                    540ms 
trees.functoriality-combinator-directed-trees                                        535ms 
synthetic-homotopy-theory.sequential-colimits                                        522ms 
finite-group-theory.subgroups-finite-groups                                          509ms 
reflection.group-solver                                                              506ms 
order-theory.nuclei-large-locales                                                    493ms 
category-theory.natural-transformations-functors-from-small-to-large-categories      472ms 
commutative-algebra.integral-domains                                                 465ms 
category-theory.adjunctions-large-categories                                         460ms 
ring-theory.localizations-rings                                                      408ms 
group-theory.abelianization-groups                                                   399ms 
synthetic-homotopy-theory.descent-circle-equivalence-types                           380ms 
synthetic-homotopy-theory.dependent-pushout-products                                 380ms 
graph-theory.equivalences-enriched-undirected-graphs                                 369ms 
lists.universal-property-lists-wild-monoids                                          359ms 
category-theory.full-subcategories                                                   355ms 
synthetic-homotopy-theory.descent-circle-function-types                              350ms 
commutative-algebra.joins-ideals-commutative-rings                                   349ms 
category-theory.groupoids                                                            343ms 
category-theory.function-precategories                                               330ms 
commutative-algebra.zariski-locale                                                   307ms 
synthetic-homotopy-theory.interval-type                                              291ms 
trees.undirected-trees                                                               285ms 
orthogonal-factorization-systems.functoriality-higher-modalities                     280ms 
linear-algebra.vectors-on-euclidean-domains                                          280ms 
group-theory.normal-cores-subgroups                                                  280ms 
synthetic-homotopy-theory.descent-circle-subtypes                                    278ms 
category-theory.opposite-preunivalent-categories                                     274ms 
group-theory.substitution-functor-group-actions                                      269ms 
finite-group-theory.cartier-delooping-sign-homomorphism                              260ms 
structured-types.dependent-products-wild-monoids                                     254ms 
ring-theory.joins-ideals-rings                                                       253ms 
category-theory.restrictions-functors-cores-precategories                            253ms 
ring-theory.joins-left-ideals-rings                                                  243ms 
commutative-algebra.function-commutative-rings                                       240ms 
set-theory.cardinalities                                                             236ms 
commutative-algebra.integer-multiples-of-elements-commutative-rings                  233ms 
synthetic-homotopy-theory.descent-circle-dependent-pair-types                        232ms 
group-theory.normalizer-subgroups                                                    223ms 
category-theory.coproducts-in-precategories                                          219ms 
category-theory.opposite-large-precategories                                         210ms 
category-theory.opposite-categories                                                  192ms 
group-theory.saturated-congruence-relations-monoids                                  189ms 
group-theory                                                                         186ms 
ring-theory.products-left-ideals-rings                                               178ms 
lists.quicksort-lists                                                                178ms 
ring-theory.products-right-ideals-rings                                              176ms 
orthogonal-factorization-systems.extensions-lifts-families-of-elements               172ms 
category-theory                                                                      163ms 
modal-type-theory.flat-sharp-adjunction                                              159ms 
category-theory.yoneda-lemma-categories                                              154ms 
category-theory.representing-arrow-category                                          148ms 
group-theory.quotient-groups-concrete-groups                                         146ms 
synthetic-homotopy-theory.powers-of-loops                                            140ms 
linear-algebra.scalar-multiplication-vectors-on-rings                                132ms 
synthetic-homotopy-theory.coequalizers                                               130ms 
category-theory.augmented-simplex-category                                           124ms 
synthetic-homotopy-theory.1-acyclic-types                                            124ms 
ring-theory.algebras-rings                                                           123ms 
higher-group-theory.iterated-cartesian-products-higher-groups                        123ms 
group-theory.cartesian-products-abelian-groups                                       121ms 
category-theory.cores-categories                                                     121ms 
orthogonal-factorization-systems.local-maps                                          118ms 
commutative-algebra.function-commutative-semirings                                   116ms 
commutative-algebra.dependent-products-commutative-semirings                         114ms 
category-theory.representable-functors-large-precategories                           112ms 
category-theory.split-essentially-surjective-functors-precategories                  112ms 
ring-theory.function-semirings                                                       111ms 
graph-theory.trails-undirected-graphs                                                110ms 
finite-group-theory.finite-commutative-monoids                                       109ms 
commutative-algebra.ideals-commutative-semirings                                     109ms 
trees.raising-universe-levels-directed-trees                                         106ms 
category-theory.natural-numbers-object-precategories                                 104ms 
synthetic-homotopy-theory.cocartesian-morphisms-arrows                               104ms 
order-theory                                                                         103ms 
group-theory.category-of-orbits-groups                                               101ms 
category-theory.products-of-precategories                                             99ms 
category-theory.exponential-objects-precategories                                     98ms 
group-theory.category-of-group-actions                                                97ms 
organic-chemistry.alcohols                                                            96ms 
synthetic-homotopy-theory.spectra                                                     90ms 
group-theory.representations-monoids-precategories                                    88ms 
category-theory.homotopies-natural-transformations-large-precategories                88ms 
structured-types.function-wild-monoids                                                87ms 
real-numbers.dedekind-real-numbers                                                    83ms 
graph-theory.faithful-morphisms-undirected-graphs                                     83ms 
structured-types.pointed-universal-property-contractible-types                        81ms 
synthetic-homotopy-theory                                                             80ms 
ring-theory                                                                           79ms 
orthogonal-factorization-systems.factorization-operations-global-function-classes     79ms 
group-theory.function-abelian-groups                                                  77ms 
graph-theory.raising-universe-levels-directed-graphs                                  77ms 
order-theory.accessible-elements-relations                                            77ms 
order-theory.chains-preorders                                                         76ms 
category-theory.essentially-surjective-functors-precategories                         74ms 
commutative-algebra.radical-ideals-generated-by-subsets-commutative-rings             74ms 
orthogonal-factorization-systems.functoriality-pullback-hom                           72ms 
modal-type-theory.flat-dependent-pair-types                                           72ms 
synthetic-homotopy-theory.tangent-spheres                                             72ms 
group-theory.kernels-homomorphisms-concrete-groups                                    71ms 
order-theory.chains-posets                                                            68ms 
ring-theory.precategory-of-semirings                                                  65ms 
graph-theory.complete-bipartite-graphs                                                64ms 
ring-theory.quotient-rings                                                            64ms 
commutative-algebra                                                                   63ms 
group-theory.cayleys-theorem                                                          63ms 
synthetic-homotopy-theory.premanifolds                                                61ms 
category-theory.monomorphisms-in-large-precategories                                  61ms 
category-theory.initial-objects-precategories                                         60ms 
group-theory.intersections-subgroups-abelian-groups                                   58ms 
group-theory.inverse-semigroups                                                       57ms 
commutative-algebra.multiples-of-elements-commutative-rings                           53ms 
modal-type-theory.flat-discrete-types                                                 53ms 
order-theory.well-founded-relations                                                   52ms 
trees                                                                                 52ms 
group-theory.centers-monoids                                                          51ms 
category-theory.sieves-in-categories                                                  50ms 
trees.rooted-undirected-trees                                                         50ms 
organic-chemistry.methane                                                             50ms 
order-theory.maximal-chains-posets                                                    50ms 
order-theory.maximal-chains-preorders                                                 50ms 
synthetic-homotopy-theory.acyclic-types                                               50ms 
category-theory.endomorphisms-in-categories                                           49ms 
group-theory.centers-semigroups                                                       48ms 
group-theory.precategory-of-concrete-groups                                           47ms 
group-theory.monomorphisms-groups                                                     46ms 
orthogonal-factorization-systems                                                      45ms 
structured-types.finite-multiplication-magmas                                         43ms 
group-theory.function-monoids                                                         43ms 
higher-group-theory.subgroups-higher-groups                                           41ms 
orthogonal-factorization-systems.local-families-of-types                              40ms 
commutative-algebra.local-commutative-rings                                           39ms 
category-theory.representable-functors-categories                                     39ms 
synthetic-homotopy-theory.descent-circle-constant-families                            39ms 
structured-types.cyclic-types                                                         37ms 
trees.bounded-multisets                                                               36ms 
orthogonal-factorization-systems.lifting-operations                                   36ms 
group-theory.precategory-of-commutative-monoids                                       36ms 
commutative-algebra.trivial-commutative-rings                                         35ms 
order-theory.lower-types-preorders                                                    35ms 
group-theory.conjugation-concrete-groups                                              34ms 
graph-theory.paths-undirected-graphs                                                  34ms 
ring-theory.invariant-basis-property-rings                                            32ms 
order-theory.well-founded-orders                                                      31ms 
group-theory.monomorphisms-concrete-groups                                            31ms 
structured-types                                                                      31ms 
linear-algebra.diagonal-matrices-on-rings                                             30ms 
category-theory.essential-fibers-of-functors-precategories                            30ms 
graph-theory                                                                          30ms 
group-theory.function-semigroups                                                      30ms 
group-theory.transitive-group-actions                                                 29ms 
group-theory.orbit-stabilizer-theorem-concrete-groups                                 29ms 
trees.empty-multisets                                                                 28ms 
group-theory.concrete-monoids                                                         28ms 
ring-theory.radical-ideals-rings                                                      27ms 
group-theory.products-of-tuples-of-elements-commutative-monoids                       27ms 
group-theory.perfect-subgroups                                                        26ms 
graph-theory.trails-directed-graphs                                                   26ms 
finite-group-theory                                                                   25ms 
category-theory.equivalences-of-large-precategories                                   25ms 
graph-theory.vertex-covers                                                            25ms 
group-theory.elements-of-finite-order-groups                                          25ms 
order-theory.directed-complete-posets                                                 25ms 
graph-theory.eulerian-circuits-undirected-graphs                                      25ms 
group-theory.exponents-groups                                                         24ms 
graph-theory.regular-undirected-graphs                                                24ms 
order-theory.locally-finite-posets                                                    24ms 
order-theory.precategory-of-decidable-total-orders                                    24ms 
orthogonal-factorization-systems.identity-modality                                    24ms 
graph-theory.voltage-graphs                                                           23ms 
finite-group-theory.alternating-groups                                                23ms 
finite-group-theory.alternating-concrete-groups                                       23ms 
order-theory.precategory-of-finite-posets                                             23ms 
modal-type-theory.sharp-codiscrete-maps                                               23ms 
orthogonal-factorization-systems.raise-modalities                                     22ms 
group-theory.mere-equivalences-group-actions                                          22ms 
reflection.boolean-reflection                                                         21ms 
synthetic-homotopy-theory.mere-spheres                                                21ms 
ring-theory.characteristics-rings                                                     21ms 
synthetic-homotopy-theory.morphisms-descent-data-circle                               21ms 
group-theory.furstenberg-groups                                                       20ms 
structured-types.morphisms-magmas                                                     20ms 
order-theory.ideals-preorders                                                         20ms 
group-theory.principal-group-actions                                                  20ms 
trees.coalgebra-of-enriched-directed-trees                                            19ms 
order-theory.interval-subposets                                                       19ms 
group-theory.sheargroups                                                              19ms 
ring-theory.free-rings-with-one-generator                                             19ms 
trees.planar-binary-trees                                                             18ms 
group-theory.normal-subgroups-concrete-groups                                         18ms 
structured-types.fibers-of-pointed-maps                                               18ms 
modal-type-theory.crisp-identity-types                                                18ms 
group-theory.dihedral-groups                                                          17ms 
organic-chemistry.alkynes                                                             17ms 
group-theory.exponents-abelian-groups                                                 17ms 
group-theory.perfect-cores                                                            17ms 
set-theory.infinite-sets                                                              17ms 
group-theory.perfect-groups                                                           17ms 
group-theory.orbits-group-actions                                                     17ms 
orthogonal-factorization-systems.zero-modality                                        16ms 
synthetic-homotopy-theory.sequentially-compact-types                                  16ms 
group-theory.stabilizer-groups                                                        16ms 
trees.coalgebra-of-directed-trees                                                     15ms 
structured-types.contractible-pointed-types                                           15ms 
orthogonal-factorization-systems.separated-types                                      15ms 
trees.rooted-quasitrees                                                               15ms 
ring-theory.generating-elements-rings                                                 14ms 
graph-theory.hypergraphs                                                              14ms 
set-theory.cantor-space                                                               14ms 
orthogonal-factorization-systems.sigma-closed-modalities                              14ms 
commutative-algebra.boolean-rings                                                     13ms 
linear-algebra                                                                        13ms 
synthetic-homotopy-theory.join-powers-of-types                                        13ms 
lists                                                                                 13ms 
graph-theory.directed-graph-structures-on-standard-finite-sets                        12ms 
orthogonal-factorization-systems.sigma-closed-reflective-modalities                   12ms 
reflection                                                                            11ms 
trees.multiset-indexed-dependent-products-of-types                                    11ms 
graph-theory.closed-walks-undirected-graphs                                           11ms 
higher-group-theory                                                                   10ms 
synthetic-homotopy-theory.category-of-connected-set-bundles-circle                    10ms 
group-theory.isomorphisms-concrete-groups                                             10ms 
linear-algebra.scalar-multiplication-matrices                                         10ms 
graph-theory.acyclic-undirected-graphs                                                10ms 
 209,027,633,416 bytes allocated in the heap
  20,208,785,744 bytes copied during GC
   1,709,639,904 bytes maximum residency (28 sample(s))
       2,508,576 bytes maximum slop
            3121 MiB total memory in use (0 MiB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0     48930 colls,     0 par   18.386s  19.088s     0.0004s    0.0485s
  Gen  1        28 colls,     0 par    0.691s   1.009s     0.0360s    0.2568s

  TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.001s  (  0.001s elapsed)
  MUT     time   71.440s  ( 71.424s elapsed)
  GC      time   19.077s  ( 20.097s elapsed)
  EXIT    time    0.210s  (  0.002s elapsed)
  Total   time   90.727s  ( 91.525s elapsed)

  Alloc rate    2,925,929,451 bytes per MUT second

  Productivity  78.7% of total user, 78.0% of total elapsed

@VojtechStep
Copy link
Collaborator

Does typechecking with profiling take measurably longer? I think I'd rather have all CI builds with perf information.

@fredrik-bakke
Copy link
Collaborator Author

  • it uses considerably more memory
  • it's incompatible with caching in the sense that we won't get a full view of how the library typechecks if we use cache when profiling

@VojtechStep
Copy link
Collaborator

Alternatively, we now have the Ubuntu runner generate Markdown with syntax highlighting (for linkchecking), so we could use the Mac runner to compile with profiling instead

@VojtechStep
Copy link
Collaborator

Oh right, caching is a problem

@fredrik-bakke
Copy link
Collaborator Author

You don't happen to have a good solution for how to manage a graph for the profiling data?

@fredrik-bakke fredrik-bakke marked this pull request as ready for review February 17, 2024 16:57
@fredrik-bakke fredrik-bakke marked this pull request as draft February 17, 2024 16:57
@VojtechStep
Copy link
Collaborator

I've never used it, but I've seen some projects use this action https://github.com/benchmark-action/github-action-benchmark

From a quick skim of the readme, you store the historical data in the cache, give the action a JSON with current performance data, and it can generate graphs and comment on the PR. Worth looking into IMO.

@fredrik-bakke fredrik-bakke changed the title Profile typechecking Profile typechecking performance Feb 18, 2024
@fredrik-bakke
Copy link
Collaborator Author

Again, it seems to me we won't be able to test this workflow before we merge into the master branch. Would you be available to assist me a little with this tomorrow @VojtechStep?

@fredrik-bakke fredrik-bakke marked this pull request as ready for review February 21, 2024 23:43
@fredrik-bakke
Copy link
Collaborator Author

Here's an example of what the json file that is generated looks like

[
  {
    "name": "bytes_allocated_in_heap",
    "value": 25716.30834197998,
    "unit": "MiB"
  },
  {
    "name": "bytes_copied_during_GC",
    "value": 7057.416763305664,
    "unit": "MiB"
  },
  {
    "name": "maximum_residency",
    "value": 1185.245460510254,
    "unit": "MiB"
  },
  {
    "name": "bytes_maximum_slop",
    "value": 1.0803985595703125,
    "unit": "MiB"
  },
  {
    "name": "total_memory_in_use",
    "value": 2333,
    "unit": "MiB"
  },
  {
    "name": "Total",
    "value": 392223,
    "unit": "ms"
  },
  {
    "name": "Miscellaneous",
    "value": 22966,
    "unit": "ms"
  },
  {
    "name": "category-theory.category-of-functors-from-small-to-large-categories",
    "value": 10555,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.orientations-complete-undirected-graph",
    "value": 8065,
    "unit": "ms"
  },
  {
    "name": "universal-algebra.quotient-algebras",
    "value": 7738,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.orbits-permutations",
    "value": 6725,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.delooping-sign-homomorphism",
    "value": 5991,
    "unit": "ms"
  },
  {
    "name": "foundation.pullbacks",
    "value": 5699,
    "unit": "ms"
  },
  {
    "name": "category-theory.category-of-maps-from-small-to-large-categories",
    "value": 5043,
    "unit": "ms"
  },
  {
    "name": "foundation.commuting-cubes-of-maps",
    "value": 3566,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.transpositions",
    "value": 3319,
    "unit": "ms"
  },
  {
    "name": "everything",
    "value": 3250,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.universal-property-pushouts",
    "value": 2785,
    "unit": "ms"
  },
  {
    "name": "foundation-core.pullbacks",
    "value": 2674,
    "unit": "ms"
  },
  {
    "name": "foundation.commuting-prisms-of-maps",
    "value": 2393,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.bezouts-lemma-natural-numbers",
    "value": 2233,
    "unit": "ms"
  },
  {
    "name": "foundation.equivalence-relations",
    "value": 2093,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.orthogonal-maps",
    "value": 2043,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.counting-dependent-pair-types",
    "value": 2040,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.2-element-decidable-subtypes",
    "value": 2029,
    "unit": "ms"
  },
  {
    "name": "foundation.commuting-squares-of-maps",
    "value": 1987,
    "unit": "ms"
  },
  {
    "name": "type-theories.dependent-type-theories",
    "value": 1911,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.pi-finite-types",
    "value": 1821,
    "unit": "ms"
  },
  {
    "name": "foundation.functoriality-dependent-pair-types",
    "value": 1753,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.functoriality-sequential-colimits",
    "value": 1719,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.2-element-types",
    "value": 1515,
    "unit": "ms"
  },
  {
    "name": "trees.underlying-trees-elements-coalgebras-polynomial-endofunctors",
    "value": 1418,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.simpson-delooping-sign-homomorphism",
    "value": 1405,
    "unit": "ms"
  },
  {
    "name": "foundation.homotopies-morphisms-arrows",
    "value": 1395,
    "unit": "ms"
  },
  {
    "name": "type-theories.fibered-dependent-type-theories",
    "value": 1350,
    "unit": "ms"
  },
  {
    "name": "category-theory.slice-precategories",
    "value": 1330,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.flattening-lemma-pushouts",
    "value": 1314,
    "unit": "ms"
  },
  {
    "name": "foundation.retracts-of-maps",
    "value": 1299,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.binomial-types",
    "value": 1292,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.26-id-pushout",
    "value": 1226,
    "unit": "ms"
  },
  {
    "name": "polytopes.abstract-polytopes",
    "value": 1208,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.modal-subuniverse-induction",
    "value": 1198,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-set-quotients",
    "value": 1187,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.universal-cover-circle",
    "value": 1142,
    "unit": "ms"
  },
  {
    "name": "set-theory.cumulative-hierarchy",
    "value": 1131,
    "unit": "ms"
  },
  {
    "name": "foundation.functoriality-fibers-of-maps",
    "value": 1125,
    "unit": "ms"
  },
  {
    "name": "type-theories.simple-type-theories",
    "value": 1125,
    "unit": "ms"
  },
  {
    "name": "foundation.sigma-decompositions",
    "value": 1094,
    "unit": "ms"
  },
  {
    "name": "foundation.yoneda-identity-types",
    "value": 1086,
    "unit": "ms"
  },
  {
    "name": "category-theory.natural-isomorphisms-functors-categories",
    "value": 1072,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.hatchers-acyclic-type",
    "value": 1056,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.permutations-standard-finite-types",
    "value": 1036,
    "unit": "ms"
  },
  {
    "name": "structured-types.pointed-equivalences",
    "value": 1027,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.modular-arithmetic-standard-finite-types",
    "value": 1011,
    "unit": "ms"
  },
  {
    "name": "category-theory.natural-isomorphisms-functors-precategories",
    "value": 1004,
    "unit": "ms"
  },
  {
    "name": "foundation.functoriality-coproduct-types",
    "value": 972,
    "unit": "ms"
  },
  {
    "name": "foundation.surjective-maps",
    "value": 957,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.truncated-acyclic-maps",
    "value": 935,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.modular-arithmetic",
    "value": 928,
    "unit": "ms"
  },
  {
    "name": "category-theory.natural-isomorphisms-maps-precategories",
    "value": 919,
    "unit": "ms"
  },
  {
    "name": "foundation.relaxed-sigma-decompositions",
    "value": 915,
    "unit": "ms"
  },
  {
    "name": "category-theory.natural-isomorphisms-maps-categories",
    "value": 901,
    "unit": "ms"
  },
  {
    "name": "foundation.commuting-squares-of-identifications",
    "value": 885,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.products-ideals-commutative-rings",
    "value": 882,
    "unit": "ms"
  },
  {
    "name": "species.small-cauchy-composition-species-of-types-in-subuniverses",
    "value": 880,
    "unit": "ms"
  },
  {
    "name": "foundation.coproduct-decompositions",
    "value": 877,
    "unit": "ms"
  },
  {
    "name": "foundation.binary-functoriality-set-quotients",
    "value": 875,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.transpositions-standard-finite-types",
    "value": 863,
    "unit": "ms"
  },
  {
    "name": "group-theory.quotient-groups",
    "value": 836,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.groups-of-units-commutative-rings",
    "value": 822,
    "unit": "ms"
  },
  {
    "name": "category-theory.isomorphisms-in-large-precategories",
    "value": 820,
    "unit": "ms"
  },
  {
    "name": "ring-theory.isomorphisms-rings",
    "value": 817,
    "unit": "ms"
  },
  {
    "name": "foundation.telescopes",
    "value": 816,
    "unit": "ms"
  },
  {
    "name": "ring-theory.groups-of-units-rings",
    "value": 816,
    "unit": "ms"
  },
  {
    "name": "species.cauchy-composition-species-of-types-in-subuniverses",
    "value": 814,
    "unit": "ms"
  },
  {
    "name": "trees.combinator-directed-trees",
    "value": 810,
    "unit": "ms"
  },
  {
    "name": "category-theory.isomorphisms-in-precategories",
    "value": 803,
    "unit": "ms"
  },
  {
    "name": "foundation.higher-homotopies-morphisms-arrows",
    "value": 803,
    "unit": "ms"
  },
  {
    "name": "species.cauchy-products-species-of-types-in-subuniverses",
    "value": 798,
    "unit": "ms"
  },
  {
    "name": "trees.combinator-enriched-directed-trees",
    "value": 794,
    "unit": "ms"
  },
  {
    "name": "trees.equivalences-enriched-directed-trees",
    "value": 791,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.suspensions-of-types",
    "value": 786,
    "unit": "ms"
  },
  {
    "name": "foundation.path-algebra",
    "value": 785,
    "unit": "ms"
  },
  {
    "name": "foundation-core.equivalences",
    "value": 784,
    "unit": "ms"
  },
  {
    "name": "species.dirichlet-products-species-of-types-in-subuniverses",
    "value": 783,
    "unit": "ms"
  },
  {
    "name": "foundation.cartesian-products-set-quotients",
    "value": 779,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.cyclic-finite-types",
    "value": 759,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.universal-property-coequalizers",
    "value": 759,
    "unit": "ms"
  },
  {
    "name": "order-theory.finitely-graded-posets",
    "value": 756,
    "unit": "ms"
  },
  {
    "name": "trees.underlying-trees-of-elements-of-w-types",
    "value": 754,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.sigma-decompositions",
    "value": 752,
    "unit": "ms"
  },
  {
    "name": "graph-theory.walks-directed-graphs",
    "value": 751,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.26-descent",
    "value": 740,
    "unit": "ms"
  },
  {
    "name": "foundation.partitions",
    "value": 734,
    "unit": "ms"
  },
  {
    "name": "group-theory.subgroups",
    "value": 729,
    "unit": "ms"
  },
  {
    "name": "foundation.fibered-maps",
    "value": 728,
    "unit": "ms"
  },
  {
    "name": "foundation.equivalences",
    "value": 726,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.fundamental-theorem-of-arithmetic",
    "value": 719,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.sign-homomorphism",
    "value": 718,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.pushouts",
    "value": 718,
    "unit": "ms"
  },
  {
    "name": "foundation.vectors-set-quotients",
    "value": 705,
    "unit": "ms"
  },
  {
    "name": "group-theory.loop-groups-sets",
    "value": 692,
    "unit": "ms"
  },
  {
    "name": "category-theory.isomorphisms-in-categories",
    "value": 688,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.smash-products-of-pointed-types",
    "value": 678,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.abstract-quaternion-group",
    "value": 673,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.joins-radical-ideals-commutative-rings",
    "value": 669,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.acyclic-maps",
    "value": 667,
    "unit": "ms"
  },
  {
    "name": "foundation.coproduct-decompositions-subuniverse",
    "value": 666,
    "unit": "ms"
  },
  {
    "name": "graph-theory.equivalences-directed-graphs",
    "value": 663,
    "unit": "ms"
  },
  {
    "name": "ring-theory.rings",
    "value": 662,
    "unit": "ms"
  },
  {
    "name": "foundation-core.commuting-prisms-of-maps",
    "value": 661,
    "unit": "ms"
  },
  {
    "name": "group-theory.subgroups-generated-by-subsets-groups",
    "value": 659,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.dependent-universal-property-pushouts",
    "value": 659,
    "unit": "ms"
  },
  {
    "name": "foundation.truncations",
    "value": 658,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.modal-induction",
    "value": 649,
    "unit": "ms"
  },
  {
    "name": "category-theory.adjunctions-large-precategories",
    "value": 647,
    "unit": "ms"
  },
  {
    "name": "foundation.computational-identity-types",
    "value": 638,
    "unit": "ms"
  },
  {
    "name": "category-theory.subprecategories",
    "value": 638,
    "unit": "ms"
  },
  {
    "name": "category-theory.isomorphisms-in-large-categories",
    "value": 632,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.distributivity-of-set-truncation-over-finite-products",
    "value": 630,
    "unit": "ms"
  },
  {
    "name": "group-theory.abelian-groups",
    "value": 628,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.dependent-coforks",
    "value": 627,
    "unit": "ms"
  },
  {
    "name": "group-theory.normal-subgroups",
    "value": 627,
    "unit": "ms"
  },
  {
    "name": "group-theory.homomorphisms-generated-subgroups",
    "value": 625,
    "unit": "ms"
  },
  {
    "name": "order-theory.galois-connections",
    "value": 624,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.lifting-structures-on-squares",
    "value": 624,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.dependent-pullback-property-pushouts",
    "value": 622,
    "unit": "ms"
  },
  {
    "name": "foundation.fibered-equivalences",
    "value": 622,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.suspension-structures",
    "value": 622,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.divisibility-integers",
    "value": 622,
    "unit": "ms"
  },
  {
    "name": "category-theory.subcategories",
    "value": 611,
    "unit": "ms"
  },
  {
    "name": "group-theory.generating-elements-groups",
    "value": 606,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-image",
    "value": 602,
    "unit": "ms"
  },
  {
    "name": "foundation.pi-decompositions",
    "value": 601,
    "unit": "ms"
  },
  {
    "name": "foundation.exponents-set-quotients",
    "value": 599,
    "unit": "ms"
  },
  {
    "name": "group-theory.normal-submonoids",
    "value": 598,
    "unit": "ms"
  },
  {
    "name": "species.cauchy-composition-species-of-types",
    "value": 598,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.cocones-under-spans",
    "value": 595,
    "unit": "ms"
  },
  {
    "name": "foundation.set-quotients",
    "value": 592,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-pullbacks",
    "value": 590,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.multiplication-integers",
    "value": 589,
    "unit": "ms"
  },
  {
    "name": "foundation-core.commuting-squares-of-maps",
    "value": 588,
    "unit": "ms"
  },
  {
    "name": "group-theory.torsors",
    "value": 587,
    "unit": "ms"
  },
  {
    "name": "group-theory.subgroups-abelian-groups",
    "value": 585,
    "unit": "ms"
  },
  {
    "name": "trees.directed-trees",
    "value": 583,
    "unit": "ms"
  },
  {
    "name": "foundation.uniqueness-image",
    "value": 582,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.finite-types",
    "value": 580,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.rational-numbers",
    "value": 578,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.pullback-hom",
    "value": 578,
    "unit": "ms"
  },
  {
    "name": "species.cauchy-exponentials-species-of-types-in-subuniverses",
    "value": 567,
    "unit": "ms"
  },
  {
    "name": "foundation.descent-coproduct-types",
    "value": 567,
    "unit": "ms"
  },
  {
    "name": "foundation.embeddings",
    "value": 565,
    "unit": "ms"
  },
  {
    "name": "trees.equivalences-directed-trees",
    "value": 562,
    "unit": "ms"
  },
  {
    "name": "foundation.unordered-pairs",
    "value": 554,
    "unit": "ms"
  },
  {
    "name": "trees.w-types",
    "value": 551,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.eisenstein-integers",
    "value": 548,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.bezouts-lemma-integers",
    "value": 534,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.dependent-cocones-under-sequential-diagrams",
    "value": 532,
    "unit": "ms"
  },
  {
    "name": "foundation.equivalences-maybe",
    "value": 532,
    "unit": "ms"
  },
  {
    "name": "category-theory.functors-precategories",
    "value": 530,
    "unit": "ms"
  },
  {
    "name": "foundation.product-decompositions-subuniverse",
    "value": 526,
    "unit": "ms"
  },
  {
    "name": "species.dirichlet-exponentials-species-of-types-in-subuniverses",
    "value": 523,
    "unit": "ms"
  },
  {
    "name": "foundation.truncation-equivalences",
    "value": 521,
    "unit": "ms"
  },
  {
    "name": "group-theory.groups",
    "value": 520,
    "unit": "ms"
  },
  {
    "name": "category-theory.precategory-of-functors",
    "value": 519,
    "unit": "ms"
  },
  {
    "name": "finite-algebra.finite-rings",
    "value": 518,
    "unit": "ms"
  },
  {
    "name": "ring-theory.binomial-theorem-semirings",
    "value": 515,
    "unit": "ms"
  },
  {
    "name": "foundation",
    "value": 514,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.extensions-of-maps",
    "value": 514,
    "unit": "ms"
  },
  {
    "name": "category-theory.fully-faithful-functors-precategories",
    "value": 511,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.functoriality-suspensions",
    "value": 510,
    "unit": "ms"
  },
  {
    "name": "group-theory.integer-powers-of-elements-groups",
    "value": 509,
    "unit": "ms"
  },
  {
    "name": "category-theory.precategory-of-maps-precategories",
    "value": 503,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.circle",
    "value": 503,
    "unit": "ms"
  },
  {
    "name": "ring-theory.ideals-rings",
    "value": 502,
    "unit": "ms"
  },
  {
    "name": "foundation.decidable-equivalence-relations",
    "value": 500,
    "unit": "ms"
  },
  {
    "name": "category-theory.wide-subcategories",
    "value": 498,
    "unit": "ms"
  },
  {
    "name": "foundation.set-truncations",
    "value": 498,
    "unit": "ms"
  },
  {
    "name": "category-theory.dependent-products-of-categories",
    "value": 498,
    "unit": "ms"
  },
  {
    "name": "foundation.invertible-maps",
    "value": 496,
    "unit": "ms"
  },
  {
    "name": "category-theory.structure-equivalences-set-magmoids",
    "value": 494,
    "unit": "ms"
  },
  {
    "name": "group-theory.normal-submonoids-commutative-monoids",
    "value": 490,
    "unit": "ms"
  },
  {
    "name": "ring-theory.right-ideals-generated-by-subsets-rings",
    "value": 489,
    "unit": "ms"
  },
  {
    "name": "ring-theory.ideals-generated-by-subsets-rings",
    "value": 487,
    "unit": "ms"
  },
  {
    "name": "order-theory.galois-connections-large-posets",
    "value": 484,
    "unit": "ms"
  },
  {
    "name": "reflection.precategory-solver",
    "value": 482,
    "unit": "ms"
  },
  {
    "name": "foundation.strictly-involutive-identity-types",
    "value": 480,
    "unit": "ms"
  },
  {
    "name": "foundation.functoriality-set-quotients",
    "value": 479,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.main-classes-of-latin-hypercubes",
    "value": 479,
    "unit": "ms"
  },
  {
    "name": "set-theory.countable-sets",
    "value": 477,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.flattening-lemma-coequalizers",
    "value": 477,
    "unit": "ms"
  },
  {
    "name": "foundation.functoriality-set-truncation",
    "value": 474,
    "unit": "ms"
  },
  {
    "name": "foundation-core.functoriality-dependent-pair-types",
    "value": 473,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.standard-finite-types",
    "value": 472,
    "unit": "ms"
  },
  {
    "name": "category-theory.natural-transformations-maps-from-small-to-large-precategories",
    "value": 470,
    "unit": "ms"
  },
  {
    "name": "ring-theory.left-ideals-generated-by-subsets-rings",
    "value": 468,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.coforks",
    "value": 463,
    "unit": "ms"
  },
  {
    "name": "category-theory.natural-transformations-functors-from-small-to-large-precategories",
    "value": 461,
    "unit": "ms"
  },
  {
    "name": "foundation.arithmetic-law-product-and-pi-decompositions",
    "value": 461,
    "unit": "ms"
  },
  {
    "name": "category-theory.natural-transformations-functors-precategories",
    "value": 461,
    "unit": "ms"
  },
  {
    "name": "category-theory.replete-subprecategories",
    "value": 460,
    "unit": "ms"
  },
  {
    "name": "foundation.connected-maps",
    "value": 457,
    "unit": "ms"
  },
  {
    "name": "linear-algebra.vectors",
    "value": 457,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.function-classes",
    "value": 454,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.permutations",
    "value": 452,
    "unit": "ms"
  },
  {
    "name": "graph-theory.walks-undirected-graphs",
    "value": 452,
    "unit": "ms"
  },
  {
    "name": "foundation.arithmetic-law-coproduct-and-sigma-decompositions",
    "value": 451,
    "unit": "ms"
  },
  {
    "name": "foundation.slice",
    "value": 449,
    "unit": "ms"
  },
  {
    "name": "ring-theory.cyclic-rings",
    "value": 443,
    "unit": "ms"
  },
  {
    "name": "structured-types.pointed-homotopies",
    "value": 439,
    "unit": "ms"
  },
  {
    "name": "group-theory.cores-monoids",
    "value": 439,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.flattening-lemma-sequential-colimits",
    "value": 434,
    "unit": "ms"
  },
  {
    "name": "finite-algebra.commutative-finite-rings",
    "value": 430,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.euclidean-domains",
    "value": 429,
    "unit": "ms"
  },
  {
    "name": "foundation.homotopies",
    "value": 426,
    "unit": "ms"
  },
  {
    "name": "trees.morphisms-enriched-directed-trees",
    "value": 424,
    "unit": "ms"
  },
  {
    "name": "foundation.cones-over-cospan-diagrams",
    "value": 423,
    "unit": "ms"
  },
  {
    "name": "group-theory.equivalences-group-actions",
    "value": 421,
    "unit": "ms"
  },
  {
    "name": "foundation.functoriality-dependent-function-types",
    "value": 421,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.addition-integers",
    "value": 418,
    "unit": "ms"
  },
  {
    "name": "category-theory.wide-subprecategories",
    "value": 413,
    "unit": "ms"
  },
  {
    "name": "foundation.type-arithmetic-dependent-pair-types",
    "value": 413,
    "unit": "ms"
  },
  {
    "name": "category-theory.category-of-functors",
    "value": 413,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.eckmann-hilton-argument",
    "value": 412,
    "unit": "ms"
  },
  {
    "name": "trees.bases-directed-trees",
    "value": 404,
    "unit": "ms"
  },
  {
    "name": "foundation.composition-algebra",
    "value": 403,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.commutative-rings",
    "value": 400,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.higher-modalities",
    "value": 398,
    "unit": "ms"
  },
  {
    "name": "foundation.epimorphisms-with-respect-to-truncated-types",
    "value": 398,
    "unit": "ms"
  },
  {
    "name": "category-theory.category-of-maps-categories",
    "value": 396,
    "unit": "ms"
  },
  {
    "name": "category-theory.function-categories",
    "value": 395,
    "unit": "ms"
  },
  {
    "name": "organic-chemistry.ethane",
    "value": 392,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.dependent-cocones-under-spans",
    "value": 391,
    "unit": "ms"
  },
  {
    "name": "ring-theory.integer-multiples-of-elements-rings",
    "value": 388,
    "unit": "ms"
  },
  {
    "name": "category-theory.functors-set-magmoids",
    "value": 388,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.joins-of-types",
    "value": 384,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.dependent-suspension-structures",
    "value": 382,
    "unit": "ms"
  },
  {
    "name": "trees.extensional-w-types",
    "value": 380,
    "unit": "ms"
  },
  {
    "name": "structured-types.morphisms-h-spaces",
    "value": 378,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.sections-descent-circle",
    "value": 376,
    "unit": "ms"
  },
  {
    "name": "foundation.decidable-embeddings",
    "value": 376,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.subgroups-finite-groups",
    "value": 371,
    "unit": "ms"
  },
  {
    "name": "group-theory.conjugation",
    "value": 370,
    "unit": "ms"
  },
  {
    "name": "trees.functoriality-combinator-directed-trees",
    "value": 369,
    "unit": "ms"
  },
  {
    "name": "finite-algebra.finite-fields",
    "value": 368,
    "unit": "ms"
  },
  {
    "name": "foundation.equivalence-classes",
    "value": 367,
    "unit": "ms"
  },
  {
    "name": "group-theory.invertible-elements-monoids",
    "value": 366,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.sequential-colimits",
    "value": 366,
    "unit": "ms"
  },
  {
    "name": "category-theory.natural-transformations-maps-precategories",
    "value": 365,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-family-of-fibers-of-maps",
    "value": 364,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.pisano-periods",
    "value": 363,
    "unit": "ms"
  },
  {
    "name": "foundation.identity-types",
    "value": 361,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.finite-groups",
    "value": 361,
    "unit": "ms"
  },
  {
    "name": "reflection.group-solver",
    "value": 361,
    "unit": "ms"
  },
  {
    "name": "trees.ranks-of-elements-w-types",
    "value": 361,
    "unit": "ms"
  },
  {
    "name": "ring-theory.homomorphisms-rings",
    "value": 357,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.divisibility-natural-numbers",
    "value": 357,
    "unit": "ms"
  },
  {
    "name": "foundation.type-duality",
    "value": 356,
    "unit": "ms"
  },
  {
    "name": "foundation.equivalences-span-diagrams",
    "value": 352,
    "unit": "ms"
  },
  {
    "name": "foundation.symmetric-operations",
    "value": 351,
    "unit": "ms"
  },
  {
    "name": "trees.functoriality-w-types",
    "value": 350,
    "unit": "ms"
  },
  {
    "name": "foundation-core.fibers-of-maps",
    "value": 350,
    "unit": "ms"
  },
  {
    "name": "ring-theory.modules-rings",
    "value": 346,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.universal-property-integers",
    "value": 346,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.integral-domains",
    "value": 345,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.greatest-common-divisor-natural-numbers",
    "value": 343,
    "unit": "ms"
  },
  {
    "name": "group-theory.symmetric-groups",
    "value": 342,
    "unit": "ms"
  },
  {
    "name": "order-theory.nuclei-large-locales",
    "value": 342,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-propositional-truncation",
    "value": 341,
    "unit": "ms"
  },
  {
    "name": "order-theory.meet-semilattices",
    "value": 336,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.lifts-of-maps",
    "value": 335,
    "unit": "ms"
  },
  {
    "name": "category-theory.natural-transformations-functors-from-small-to-large-categories",
    "value": 335,
    "unit": "ms"
  },
  {
    "name": "order-theory.closure-operators-large-locales",
    "value": 334,
    "unit": "ms"
  },
  {
    "name": "category-theory.categories",
    "value": 332,
    "unit": "ms"
  },
  {
    "name": "foundation.equality-coproduct-types",
    "value": 330,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.local-types",
    "value": 330,
    "unit": "ms"
  },
  {
    "name": "type-theories.precategories-with-attributes",
    "value": 328,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.well-ordering-principle-standard-finite-types",
    "value": 327,
    "unit": "ms"
  },
  {
    "name": "lists.permutation-vectors",
    "value": 325,
    "unit": "ms"
  },
  {
    "name": "group-theory.abelianization-groups",
    "value": 324,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.products-radical-ideals-commutative-rings",
    "value": 323,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.set-quotients-of-index-two",
    "value": 323,
    "unit": "ms"
  },
  {
    "name": "order-theory.join-semilattices",
    "value": 322,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.dependent-universal-property-sequential-colimits",
    "value": 321,
    "unit": "ms"
  },
  {
    "name": "foundation.exclusive-disjunction",
    "value": 321,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.universal-property-sequential-colimits",
    "value": 321,
    "unit": "ms"
  },
  {
    "name": "category-theory.dependent-products-of-large-categories",
    "value": 320,
    "unit": "ms"
  },
  {
    "name": "category-theory.dependent-products-of-precategories",
    "value": 318,
    "unit": "ms"
  },
  {
    "name": "foundation.functoriality-cartesian-product-types",
    "value": 315,
    "unit": "ms"
  },
  {
    "name": "category-theory.pseudomonic-functors-precategories",
    "value": 315,
    "unit": "ms"
  },
  {
    "name": "category-theory.dependent-products-of-large-precategories",
    "value": 314,
    "unit": "ms"
  },
  {
    "name": "category-theory.adjunctions-large-categories",
    "value": 313,
    "unit": "ms"
  },
  {
    "name": "lists.lists",
    "value": 313,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.reduced-integer-fractions",
    "value": 311,
    "unit": "ms"
  },
  {
    "name": "category-theory.monads-on-precategories",
    "value": 307,
    "unit": "ms"
  },
  {
    "name": "group-theory.decidable-subgroups",
    "value": 306,
    "unit": "ms"
  },
  {
    "name": "foundation-core.homotopies",
    "value": 305,
    "unit": "ms"
  },
  {
    "name": "foundation.transport-along-higher-identifications",
    "value": 304,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.partitions",
    "value": 303,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.gaussian-integers",
    "value": 302,
    "unit": "ms"
  },
  {
    "name": "foundation.isolated-elements",
    "value": 301,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.factorizations-of-maps",
    "value": 300,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.cocones-under-sequential-diagrams",
    "value": 299,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.precomposition-lifts-families-of-elements",
    "value": 299,
    "unit": "ms"
  },
  {
    "name": "group-theory.quotients-abelian-groups",
    "value": 298,
    "unit": "ms"
  },
  {
    "name": "ring-theory.localizations-rings",
    "value": 298,
    "unit": "ms"
  },
  {
    "name": "category-theory.functors-categories",
    "value": 298,
    "unit": "ms"
  },
  {
    "name": "foundation.faithful-maps",
    "value": 297,
    "unit": "ms"
  },
  {
    "name": "trees.morphisms-coalgebras-polynomial-endofunctors",
    "value": 296,
    "unit": "ms"
  },
  {
    "name": "foundation.uniqueness-set-quotients",
    "value": 295,
    "unit": "ms"
  },
  {
    "name": "lists.sort-by-insertion-vectors",
    "value": 293,
    "unit": "ms"
  },
  {
    "name": "trees.morphisms-algebras-polynomial-endofunctors",
    "value": 292,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.greatest-common-divisor-integers",
    "value": 292,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.dependent-universal-property-coequalizers",
    "value": 290,
    "unit": "ms"
  },
  {
    "name": "foundation-core.truncated-types",
    "value": 290,
    "unit": "ms"
  },
  {
    "name": "group-theory.homomorphisms-groups",
    "value": 287,
    "unit": "ms"
  },
  {
    "name": "trees.small-multisets",
    "value": 286,
    "unit": "ms"
  },
  {
    "name": "group-theory.isomorphisms-group-actions",
    "value": 286,
    "unit": "ms"
  },
  {
    "name": "group-theory.images-of-group-homomorphisms",
    "value": 284,
    "unit": "ms"
  },
  {
    "name": "foundation-core.subtypes",
    "value": 283,
    "unit": "ms"
  },
  {
    "name": "category-theory.precategory-of-functors-from-small-to-large-precategories",
    "value": 281,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.type-duality",
    "value": 279,
    "unit": "ms"
  },
  {
    "name": "category-theory.precategory-of-maps-from-small-to-large-precategories",
    "value": 279,
    "unit": "ms"
  },
  {
    "name": "foundation.equality-dependent-pair-types",
    "value": 278,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.dependent-pushout-products",
    "value": 275,
    "unit": "ms"
  },
  {
    "name": "graph-theory.equivalences-undirected-graphs",
    "value": 275,
    "unit": "ms"
  },
  {
    "name": "group-theory.homomorphisms-group-actions",
    "value": 273,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.homomorphisms-commutative-rings",
    "value": 273,
    "unit": "ms"
  },
  {
    "name": "category-theory.monads-on-categories",
    "value": 273,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.isomorphisms-commutative-rings",
    "value": 272,
    "unit": "ms"
  },
  {
    "name": "foundation.equivalences-arrows",
    "value": 272,
    "unit": "ms"
  },
  {
    "name": "category-theory.copresheaf-categories",
    "value": 272,
    "unit": "ms"
  },
  {
    "name": "trees.fibers-enriched-directed-trees",
    "value": 270,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.integers",
    "value": 268,
    "unit": "ms"
  },
  {
    "name": "finite-algebra.homomorphisms-commutative-finite-rings",
    "value": 266,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.dependent-descent-circle",
    "value": 265,
    "unit": "ms"
  },
  {
    "name": "graph-theory.equivalences-enriched-undirected-graphs",
    "value": 264,
    "unit": "ms"
  },
  {
    "name": "foundation.postcomposition-functions",
    "value": 263,
    "unit": "ms"
  },
  {
    "name": "category-theory.isomorphisms-in-subprecategories",
    "value": 263,
    "unit": "ms"
  },
  {
    "name": "group-theory.subgroups-generated-by-families-of-elements-groups",
    "value": 263,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.decidable-equivalence-relations",
    "value": 262,
    "unit": "ms"
  },
  {
    "name": "group-theory.subgroups-generated-by-elements-groups",
    "value": 262,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.pigeonhole-principle",
    "value": 262,
    "unit": "ms"
  },
  {
    "name": "category-theory.presheaf-categories",
    "value": 262,
    "unit": "ms"
  },
  {
    "name": "foundation.type-arithmetic-coproduct-types",
    "value": 262,
    "unit": "ms"
  },
  {
    "name": "structured-types.equivalences-types-equipped-with-endomorphisms",
    "value": 261,
    "unit": "ms"
  },
  {
    "name": "lists.universal-property-lists-wild-monoids",
    "value": 261,
    "unit": "ms"
  },
  {
    "name": "species.cauchy-exponentials-species-of-types",
    "value": 260,
    "unit": "ms"
  },
  {
    "name": "foundation.perfect-images",
    "value": 259,
    "unit": "ms"
  },
  {
    "name": "group-theory.isomorphisms-semigroups",
    "value": 258,
    "unit": "ms"
  },
  {
    "name": "trees.morphisms-directed-trees",
    "value": 258,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.descent-circle-equivalence-types",
    "value": 257,
    "unit": "ms"
  },
  {
    "name": "species.products-dirichlet-series-species-of-types-in-subuniverses",
    "value": 256,
    "unit": "ms"
  },
  {
    "name": "category-theory.natural-transformations-functors-categories",
    "value": 256,
    "unit": "ms"
  },
  {
    "name": "foundation.dependent-binomial-theorem",
    "value": 256,
    "unit": "ms"
  },
  {
    "name": "order-theory.order-preserving-maps-posets",
    "value": 255,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.equivalences-sequential-diagrams",
    "value": 253,
    "unit": "ms"
  },
  {
    "name": "foundation.sections",
    "value": 252,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.intersections-radical-ideals-commutative-rings",
    "value": 250,
    "unit": "ms"
  },
  {
    "name": "ring-theory.homomorphisms-semirings",
    "value": 249,
    "unit": "ms"
  },
  {
    "name": "type-theories.unityped-type-theories",
    "value": 249,
    "unit": "ms"
  },
  {
    "name": "structured-types.initial-pointed-type-equipped-with-automorphism",
    "value": 249,
    "unit": "ms"
  },
  {
    "name": "foundation.commuting-squares-of-homotopies",
    "value": 248,
    "unit": "ms"
  },
  {
    "name": "category-theory.full-subcategories",
    "value": 247,
    "unit": "ms"
  },
  {
    "name": "foundation-core.small-types",
    "value": 247,
    "unit": "ms"
  },
  {
    "name": "foundation.commuting-triangles-of-identifications",
    "value": 246,
    "unit": "ms"
  },
  {
    "name": "category-theory.groupoids",
    "value": 246,
    "unit": "ms"
  },
  {
    "name": "lists.permutation-lists",
    "value": 246,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.codiagonals-of-maps",
    "value": 245,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.based-strong-induction-natural-numbers",
    "value": 245,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.inequality-natural-numbers",
    "value": 243,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.distance-natural-numbers",
    "value": 243,
    "unit": "ms"
  },
  {
    "name": "foundation.decidable-equality",
    "value": 241,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.joins-ideals-commutative-rings",
    "value": 241,
    "unit": "ms"
  },
  {
    "name": "ring-theory.products-subsets-rings",
    "value": 240,
    "unit": "ms"
  },
  {
    "name": "category-theory.large-function-categories",
    "value": 240,
    "unit": "ms"
  },
  {
    "name": "trees.rooted-morphisms-directed-trees",
    "value": 239,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.coproduct-types",
    "value": 239,
    "unit": "ms"
  },
  {
    "name": "category-theory.natural-transformations-maps-categories",
    "value": 239,
    "unit": "ms"
  },
  {
    "name": "category-theory.full-subprecategories",
    "value": 238,
    "unit": "ms"
  },
  {
    "name": "species.dirichlet-exponentials-species-of-types",
    "value": 238,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.factorizations-of-maps-function-classes",
    "value": 238,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-fiber-products",
    "value": 235,
    "unit": "ms"
  },
  {
    "name": "foundation.propositional-truncations",
    "value": 235,
    "unit": "ms"
  },
  {
    "name": "finite-algebra.homomorphisms-finite-rings",
    "value": 235,
    "unit": "ms"
  },
  {
    "name": "foundation.dependent-identifications",
    "value": 234,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.ferrers-diagrams",
    "value": 233,
    "unit": "ms"
  },
  {
    "name": "ring-theory.transporting-ring-structure-along-isomorphisms-abelian-groups",
    "value": 233,
    "unit": "ms"
  },
  {
    "name": "foundation.images-subtypes",
    "value": 231,
    "unit": "ms"
  },
  {
    "name": "category-theory.large-function-precategories",
    "value": 231,
    "unit": "ms"
  },
  {
    "name": "category-theory.functors-from-small-to-large-precategories",
    "value": 230,
    "unit": "ms"
  },
  {
    "name": "category-theory.function-precategories",
    "value": 230,
    "unit": "ms"
  },
  {
    "name": "foundation.type-arithmetic-empty-type",
    "value": 229,
    "unit": "ms"
  },
  {
    "name": "foundation-core.universal-property-pullbacks",
    "value": 228,
    "unit": "ms"
  },
  {
    "name": "category-theory.maps-precategories",
    "value": 228,
    "unit": "ms"
  },
  {
    "name": "category-theory.composition-operations-on-binary-families-of-sets",
    "value": 228,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.universal-property-circle",
    "value": 227,
    "unit": "ms"
  },
  {
    "name": "order-theory.order-preserving-maps-preorders",
    "value": 226,
    "unit": "ms"
  },
  {
    "name": "category-theory.functors-from-small-to-large-categories",
    "value": 226,
    "unit": "ms"
  },
  {
    "name": "foundation.transposition-identifications-along-equivalences",
    "value": 226,
    "unit": "ms"
  },
  {
    "name": "foundation.binary-relations",
    "value": 225,
    "unit": "ms"
  },
  {
    "name": "type-theories.precategories-with-families",
    "value": 224,
    "unit": "ms"
  },
  {
    "name": "lists.functoriality-lists",
    "value": 224,
    "unit": "ms"
  },
  {
    "name": "foundation-core.truncated-maps",
    "value": 223,
    "unit": "ms"
  },
  {
    "name": "foundation.binary-type-duality",
    "value": 223,
    "unit": "ms"
  },
  {
    "name": "foundation.iterating-automorphisms",
    "value": 222,
    "unit": "ms"
  },
  {
    "name": "group-theory.normal-cores-subgroups",
    "value": 221,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.descent-circle-function-types",
    "value": 221,
    "unit": "ms"
  },
  {
    "name": "foundation.univalence",
    "value": 221,
    "unit": "ms"
  },
  {
    "name": "order-theory.large-subframes",
    "value": 220,
    "unit": "ms"
  },
  {
    "name": "category-theory.terminal-category",
    "value": 220,
    "unit": "ms"
  },
  {
    "name": "foundation.decidable-propositions",
    "value": 220,
    "unit": "ms"
  },
  {
    "name": "foundation.whiskering-homotopies-composition",
    "value": 218,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.counting-decidable-subtypes",
    "value": 218,
    "unit": "ms"
  },
  {
    "name": "category-theory.functors-nonunital-precategories",
    "value": 217,
    "unit": "ms"
  },
  {
    "name": "group-theory.powers-of-elements-monoids",
    "value": 216,
    "unit": "ms"
  },
  {
    "name": "foundation.repetitions-of-values",
    "value": 215,
    "unit": "ms"
  },
  {
    "name": "foundation.whiskering-identifications-concatenation",
    "value": 214,
    "unit": "ms"
  },
  {
    "name": "group-theory.normal-closures-subgroups",
    "value": 214,
    "unit": "ms"
  },
  {
    "name": "category-theory.fully-faithful-maps-precategories",
    "value": 214,
    "unit": "ms"
  },
  {
    "name": "group-theory.subsemigroups",
    "value": 214,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.zariski-locale",
    "value": 213,
    "unit": "ms"
  },
  {
    "name": "group-theory.homomorphisms-monoids",
    "value": 212,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.infinite-cyclic-types",
    "value": 211,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.cartesian-product-types",
    "value": 211,
    "unit": "ms"
  },
  {
    "name": "category-theory.precategory-of-elements-of-a-presheaf",
    "value": 211,
    "unit": "ms"
  },
  {
    "name": "group-theory.functoriality-quotient-groups",
    "value": 210,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-set-truncation",
    "value": 210,
    "unit": "ms"
  },
  {
    "name": "ring-theory.semirings",
    "value": 210,
    "unit": "ms"
  },
  {
    "name": "foundation.morphisms-arrows",
    "value": 206,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.functoriality-higher-modalities",
    "value": 206,
    "unit": "ms"
  },
  {
    "name": "foundation.transport-along-equivalences",
    "value": 205,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-sequential-limits",
    "value": 205,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.descent-circle",
    "value": 205,
    "unit": "ms"
  },
  {
    "name": "category-theory.faithful-maps-precategories",
    "value": 204,
    "unit": "ms"
  },
  {
    "name": "foundation.logical-equivalences",
    "value": 203,
    "unit": "ms"
  },
  {
    "name": "category-theory.anafunctors-precategories",
    "value": 203,
    "unit": "ms"
  },
  {
    "name": "trees.undirected-trees",
    "value": 203,
    "unit": "ms"
  },
  {
    "name": "foundation.morphisms-cospan-diagrams",
    "value": 201,
    "unit": "ms"
  },
  {
    "name": "structured-types.involutive-type-of-h-space-structures",
    "value": 200,
    "unit": "ms"
  },
  {
    "name": "type-theories.sections-dependent-type-theories",
    "value": 200,
    "unit": "ms"
  },
  {
    "name": "group-theory.transitive-concrete-group-actions",
    "value": 200,
    "unit": "ms"
  },
  {
    "name": "foundation.subtypes",
    "value": 200,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.ring-of-integers",
    "value": 199,
    "unit": "ms"
  },
  {
    "name": "group-theory.substitution-functor-group-actions",
    "value": 199,
    "unit": "ms"
  },
  {
    "name": "foundation.symmetric-identity-types",
    "value": 199,
    "unit": "ms"
  },
  {
    "name": "ring-theory.congruence-relations-rings",
    "value": 199,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.homomorphisms-commutative-semirings",
    "value": 199,
    "unit": "ms"
  },
  {
    "name": "foundation.function-extensionality",
    "value": 199,
    "unit": "ms"
  },
  {
    "name": "group-theory.isomorphisms-groups",
    "value": 198,
    "unit": "ms"
  },
  {
    "name": "linear-algebra.vectors-on-euclidean-domains",
    "value": 198,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.pushout-products",
    "value": 198,
    "unit": "ms"
  },
  {
    "name": "foundation.preunivalent-type-families",
    "value": 198,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.dependent-pair-types",
    "value": 197,
    "unit": "ms"
  },
  {
    "name": "category-theory.pullbacks-in-precategories",
    "value": 197,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.extensions-double-lifts-families-of-elements",
    "value": 197,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.cartier-delooping-sign-homomorphism",
    "value": 197,
    "unit": "ms"
  },
  {
    "name": "foundation-core.propositions",
    "value": 197,
    "unit": "ms"
  },
  {
    "name": "trees.bases-enriched-directed-trees",
    "value": 197,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.descent-circle-subtypes",
    "value": 197,
    "unit": "ms"
  },
  {
    "name": "group-theory.isomorphisms-abelian-groups",
    "value": 196,
    "unit": "ms"
  },
  {
    "name": "lists.arrays",
    "value": 196,
    "unit": "ms"
  },
  {
    "name": "group-theory.congruence-relations-groups",
    "value": 195,
    "unit": "ms"
  },
  {
    "name": "group-theory.subgroups-concrete-groups",
    "value": 195,
    "unit": "ms"
  },
  {
    "name": "category-theory.gaunt-categories",
    "value": 194,
    "unit": "ms"
  },
  {
    "name": "group-theory",
    "value": 193,
    "unit": "ms"
  },
  {
    "name": "ring-theory.invertible-elements-rings",
    "value": 193,
    "unit": "ms"
  },
  {
    "name": "species.small-cauchy-composition-species-of-finite-inhabited-types",
    "value": 193,
    "unit": "ms"
  },
  {
    "name": "category-theory.restrictions-functors-cores-precategories",
    "value": 192,
    "unit": "ms"
  },
  {
    "name": "lists.sorted-vectors",
    "value": 192,
    "unit": "ms"
  },
  {
    "name": "linear-algebra.vectors-on-rings",
    "value": 192,
    "unit": "ms"
  },
  {
    "name": "trees.enriched-directed-trees",
    "value": 189,
    "unit": "ms"
  },
  {
    "name": "foundation.function-types",
    "value": 189,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-identity-types",
    "value": 189,
    "unit": "ms"
  },
  {
    "name": "category-theory.opposite-preunivalent-categories",
    "value": 188,
    "unit": "ms"
  },
  {
    "name": "category-theory.maps-set-magmoids",
    "value": 187,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.interval-type",
    "value": 186,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.radicals-of-ideals-commutative-rings",
    "value": 186,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.pushouts-of-pointed-types",
    "value": 186,
    "unit": "ms"
  },
  {
    "name": "set-theory.cardinalities",
    "value": 185,
    "unit": "ms"
  },
  {
    "name": "foundation-core.contractible-types",
    "value": 185,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.factorization-operations-function-classes",
    "value": 184,
    "unit": "ms"
  },
  {
    "name": "ring-theory.joins-right-ideals-rings",
    "value": 183,
    "unit": "ms"
  },
  {
    "name": "ring-theory.sums-semirings",
    "value": 182,
    "unit": "ms"
  },
  {
    "name": "order-theory.greatest-lower-bounds-posets",
    "value": 182,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.finite-semigroups",
    "value": 182,
    "unit": "ms"
  },
  {
    "name": "foundation.regensburg-extension-fundamental-theorem-of-identity-types",
    "value": 182,
    "unit": "ms"
  },
  {
    "name": "order-theory.least-upper-bounds-posets",
    "value": 182,
    "unit": "ms"
  },
  {
    "name": "order-theory.finite-preorders",
    "value": 180,
    "unit": "ms"
  },
  {
    "name": "species.composition-cauchy-series-species-of-types",
    "value": 180,
    "unit": "ms"
  },
  {
    "name": "category-theory.indiscrete-precategories",
    "value": 180,
    "unit": "ms"
  },
  {
    "name": "foundation.multivariable-homotopies",
    "value": 179,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-truncation",
    "value": 178,
    "unit": "ms"
  },
  {
    "name": "foundation.symmetric-difference",
    "value": 177,
    "unit": "ms"
  },
  {
    "name": "foundation.impredicative-encodings",
    "value": 177,
    "unit": "ms"
  },
  {
    "name": "foundation.unordered-tuples",
    "value": 177,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.morphisms-sequential-diagrams",
    "value": 177,
    "unit": "ms"
  },
  {
    "name": "foundation.equality-cartesian-product-types",
    "value": 177,
    "unit": "ms"
  },
  {
    "name": "finite-algebra.dependent-products-finite-rings",
    "value": 176,
    "unit": "ms"
  },
  {
    "name": "category-theory.cores-precategories",
    "value": 175,
    "unit": "ms"
  },
  {
    "name": "category-theory.large-categories",
    "value": 175,
    "unit": "ms"
  },
  {
    "name": "ring-theory.joins-ideals-rings",
    "value": 175,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.standard-cyclic-rings",
    "value": 175,
    "unit": "ms"
  },
  {
    "name": "graph-theory.morphisms-undirected-graphs",
    "value": 174,
    "unit": "ms"
  },
  {
    "name": "foundation.sequential-limits",
    "value": 174,
    "unit": "ms"
  },
  {
    "name": "graph-theory.fibers-directed-graphs",
    "value": 174,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.strict-inequality-natural-numbers",
    "value": 174,
    "unit": "ms"
  },
  {
    "name": "group-theory.images-of-semigroup-homomorphisms",
    "value": 174,
    "unit": "ms"
  },
  {
    "name": "ring-theory.joins-left-ideals-rings",
    "value": 173,
    "unit": "ms"
  },
  {
    "name": "ring-theory.homomorphisms-cyclic-rings",
    "value": 173,
    "unit": "ms"
  },
  {
    "name": "foundation.epimorphisms",
    "value": 173,
    "unit": "ms"
  },
  {
    "name": "group-theory.iterated-cartesian-products-concrete-groups",
    "value": 172,
    "unit": "ms"
  },
  {
    "name": "group-theory.addition-homomorphisms-abelian-groups",
    "value": 172,
    "unit": "ms"
  },
  {
    "name": "graph-theory.morphisms-directed-graphs",
    "value": 172,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.type-arithmetic-natural-numbers",
    "value": 172,
    "unit": "ms"
  },
  {
    "name": "foundation.locally-small-types",
    "value": 171,
    "unit": "ms"
  },
  {
    "name": "foundation.decidable-subtypes",
    "value": 171,
    "unit": "ms"
  },
  {
    "name": "foundation.precomposition-functions",
    "value": 170,
    "unit": "ms"
  },
  {
    "name": "category-theory.faithful-functors-precategories",
    "value": 170,
    "unit": "ms"
  },
  {
    "name": "finite-algebra.dependent-products-commutative-finite-rings",
    "value": 170,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.joins-of-maps",
    "value": 170,
    "unit": "ms"
  },
  {
    "name": "foundation.functoriality-truncation",
    "value": 170,
    "unit": "ms"
  },
  {
    "name": "foundation-core.universal-property-truncation",
    "value": 170,
    "unit": "ms"
  },
  {
    "name": "group-theory.homomorphisms-semigroups",
    "value": 169,
    "unit": "ms"
  },
  {
    "name": "group-theory.isomorphisms-monoids",
    "value": 169,
    "unit": "ms"
  },
  {
    "name": "foundation.equality-fibers-of-maps",
    "value": 169,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.powers-of-two",
    "value": 168,
    "unit": "ms"
  },
  {
    "name": "category-theory.full-large-subprecategories",
    "value": 168,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.functoriality-loop-spaces",
    "value": 167,
    "unit": "ms"
  },
  {
    "name": "foundation.cantor-schroder-bernstein-escardo",
    "value": 167,
    "unit": "ms"
  },
  {
    "name": "foundation.images",
    "value": 167,
    "unit": "ms"
  },
  {
    "name": "group-theory.integer-multiples-of-elements-abelian-groups",
    "value": 167,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.transporting-commutative-ring-structure-isomorphisms-abelian-groups",
    "value": 166,
    "unit": "ms"
  },
  {
    "name": "category-theory.preunivalent-categories",
    "value": 166,
    "unit": "ms"
  },
  {
    "name": "group-theory.orbits-monoid-actions",
    "value": 166,
    "unit": "ms"
  },
  {
    "name": "foundation.0-connected-types",
    "value": 165,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.finite-monoids",
    "value": 165,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.integer-multiples-of-elements-commutative-rings",
    "value": 165,
    "unit": "ms"
  },
  {
    "name": "group-theory.normalizer-subgroups",
    "value": 165,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.fibers-of-maps",
    "value": 164,
    "unit": "ms"
  },
  {
    "name": "foundation.equivalences-spans",
    "value": 164,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.descent-circle-dependent-pair-types",
    "value": 164,
    "unit": "ms"
  },
  {
    "name": "foundation.sets",
    "value": 163,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.ideals-commutative-rings",
    "value": 162,
    "unit": "ms"
  },
  {
    "name": "ring-theory.dependent-products-rings",
    "value": 162,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.2-element-subtypes",
    "value": 162,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.triple-loop-spaces",
    "value": 161,
    "unit": "ms"
  },
  {
    "name": "trees.functoriality-fiber-directed-tree",
    "value": 161,
    "unit": "ms"
  },
  {
    "name": "foundation.constant-maps",
    "value": 161,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.counting",
    "value": 161,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.finite-abelian-groups",
    "value": 159,
    "unit": "ms"
  },
  {
    "name": "group-theory.homomorphisms-groups-equipped-with-normal-subgroups",
    "value": 158,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.factorizations-of-maps-global-function-classes",
    "value": 158,
    "unit": "ms"
  },
  {
    "name": "foundation.descent-dependent-pair-types",
    "value": 158,
    "unit": "ms"
  },
  {
    "name": "foundation.subuniverses",
    "value": 158,
    "unit": "ms"
  },
  {
    "name": "structured-types.dependent-products-wild-monoids",
    "value": 157,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.addition-integer-fractions",
    "value": 157,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.finite-type-groups",
    "value": 157,
    "unit": "ms"
  },
  {
    "name": "ring-theory.congruence-relations-semirings",
    "value": 157,
    "unit": "ms"
  },
  {
    "name": "foundation.singleton-subtypes",
    "value": 157,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.orthogonal-factorization-systems",
    "value": 156,
    "unit": "ms"
  },
  {
    "name": "foundation-core.functoriality-dependent-function-types",
    "value": 156,
    "unit": "ms"
  },
  {
    "name": "group-theory.cartesian-products-concrete-groups",
    "value": 156,
    "unit": "ms"
  },
  {
    "name": "category-theory.full-large-subcategories",
    "value": 156,
    "unit": "ms"
  },
  {
    "name": "structured-types.pointed-types-equipped-with-automorphisms",
    "value": 156,
    "unit": "ms"
  },
  {
    "name": "foundation.fiber-inclusions",
    "value": 155,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.strong-induction-natural-numbers",
    "value": 155,
    "unit": "ms"
  },
  {
    "name": "category-theory.strict-categories",
    "value": 155,
    "unit": "ms"
  },
  {
    "name": "order-theory.large-frames",
    "value": 155,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.function-commutative-rings",
    "value": 155,
    "unit": "ms"
  },
  {
    "name": "foundation.descent-equivalences",
    "value": 155,
    "unit": "ms"
  },
  {
    "name": "foundation.decidable-types",
    "value": 154,
    "unit": "ms"
  },
  {
    "name": "group-theory.homomorphisms-abelian-groups",
    "value": 154,
    "unit": "ms"
  },
  {
    "name": "group-theory.congruence-relations-abelian-groups",
    "value": 153,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.sequences-finite-types",
    "value": 153,
    "unit": "ms"
  },
  {
    "name": "structured-types.equivalences-types-equipped-with-automorphisms",
    "value": 152,
    "unit": "ms"
  },
  {
    "name": "ring-theory.products-rings",
    "value": 152,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.multiplication-natural-numbers",
    "value": 151,
    "unit": "ms"
  },
  {
    "name": "foundation.connected-types",
    "value": 151,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.finitary-natural-numbers",
    "value": 151,
    "unit": "ms"
  },
  {
    "name": "species.products-dirichlet-series-species-of-types",
    "value": 151,
    "unit": "ms"
  },
  {
    "name": "category-theory.products-in-precategories",
    "value": 150,
    "unit": "ms"
  },
  {
    "name": "category-theory.coproducts-in-precategories",
    "value": 150,
    "unit": "ms"
  },
  {
    "name": "foundation.diagonals-of-maps",
    "value": 150,
    "unit": "ms"
  },
  {
    "name": "foundation.action-on-higher-identifications-functions",
    "value": 149,
    "unit": "ms"
  },
  {
    "name": "foundation-core.equality-dependent-pair-types",
    "value": 148,
    "unit": "ms"
  },
  {
    "name": "foundation.morphisms-spans-families-of-types",
    "value": 148,
    "unit": "ms"
  },
  {
    "name": "order-theory.frames",
    "value": 147,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.equality-standard-finite-types",
    "value": 147,
    "unit": "ms"
  },
  {
    "name": "foundation.iterated-cartesian-product-types",
    "value": 147,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.free-loops",
    "value": 146,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.decidable-subtypes",
    "value": 146,
    "unit": "ms"
  },
  {
    "name": "foundation-core.coherently-invertible-maps",
    "value": 145,
    "unit": "ms"
  },
  {
    "name": "foundation.retractions",
    "value": 145,
    "unit": "ms"
  },
  {
    "name": "category-theory",
    "value": 145,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-propositional-truncation-into-sets",
    "value": 145,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.universal-property-natural-numbers",
    "value": 143,
    "unit": "ms"
  },
  {
    "name": "group-theory.saturated-congruence-relations-monoids",
    "value": 143,
    "unit": "ms"
  },
  {
    "name": "group-theory.nullifying-group-homomorphisms",
    "value": 143,
    "unit": "ms"
  },
  {
    "name": "foundation-core.injective-maps",
    "value": 143,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.universal-property-suspensions-of-pointed-types",
    "value": 142,
    "unit": "ms"
  },
  {
    "name": "foundation.coherently-invertible-maps",
    "value": 142,
    "unit": "ms"
  },
  {
    "name": "category-theory.large-precategories",
    "value": 142,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.congruence-natural-numbers",
    "value": 141,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.dependent-products-commutative-rings",
    "value": 141,
    "unit": "ms"
  },
  {
    "name": "trees.fibers-directed-trees",
    "value": 141,
    "unit": "ms"
  },
  {
    "name": "finite-algebra.products-commutative-finite-rings",
    "value": 140,
    "unit": "ms"
  },
  {
    "name": "species.products-cauchy-series-species-of-types",
    "value": 140,
    "unit": "ms"
  },
  {
    "name": "foundation.functional-correspondences",
    "value": 139,
    "unit": "ms"
  },
  {
    "name": "foundation.commuting-triangles-of-maps",
    "value": 139,
    "unit": "ms"
  },
  {
    "name": "foundation.equivalence-extensionality",
    "value": 139,
    "unit": "ms"
  },
  {
    "name": "foundation.action-on-equivalences-type-families",
    "value": 139,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.open-modalities",
    "value": 139,
    "unit": "ms"
  },
  {
    "name": "universal-algebra.terms-over-signatures",
    "value": 139,
    "unit": "ms"
  },
  {
    "name": "category-theory.opposite-large-precategories",
    "value": 138,
    "unit": "ms"
  },
  {
    "name": "group-theory.saturated-congruence-relations-commutative-monoids",
    "value": 138,
    "unit": "ms"
  },
  {
    "name": "foundation.global-subuniverses",
    "value": 138,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.congruence-integers",
    "value": 138,
    "unit": "ms"
  },
  {
    "name": "category-theory.natural-transformations-functors-large-precategories",
    "value": 138,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.cycle-prime-decomposition-natural-numbers",
    "value": 137,
    "unit": "ms"
  },
  {
    "name": "order-theory.large-locales",
    "value": 137,
    "unit": "ms"
  },
  {
    "name": "category-theory.opposite-categories",
    "value": 137,
    "unit": "ms"
  },
  {
    "name": "foundation.univalent-type-families",
    "value": 137,
    "unit": "ms"
  },
  {
    "name": "trees.induction-w-types",
    "value": 136,
    "unit": "ms"
  },
  {
    "name": "group-theory.pullbacks-subgroups",
    "value": 136,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.uniquely-eliminating-modalities",
    "value": 136,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.equivalences-cubes",
    "value": 136,
    "unit": "ms"
  },
  {
    "name": "group-theory.submonoids",
    "value": 135,
    "unit": "ms"
  },
  {
    "name": "foundation.coproduct-types",
    "value": 135,
    "unit": "ms"
  },
  {
    "name": "foundation.type-theoretic-principle-of-choice",
    "value": 135,
    "unit": "ms"
  },
  {
    "name": "group-theory.dihedral-group-construction",
    "value": 135,
    "unit": "ms"
  },
  {
    "name": "universal-algebra.algebraic-theory-of-groups",
    "value": 134,
    "unit": "ms"
  },
  {
    "name": "category-theory.opposite-precategories",
    "value": 134,
    "unit": "ms"
  },
  {
    "name": "order-theory.large-quotient-locales",
    "value": 134,
    "unit": "ms"
  },
  {
    "name": "finite-algebra.products-finite-rings",
    "value": 133,
    "unit": "ms"
  },
  {
    "name": "foundation.morphisms-inverse-sequential-diagrams",
    "value": 132,
    "unit": "ms"
  },
  {
    "name": "foundation.truncation-images-of-maps",
    "value": 132,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.embeddings-standard-finite-types",
    "value": 132,
    "unit": "ms"
  },
  {
    "name": "species.morphisms-finite-species",
    "value": 131,
    "unit": "ms"
  },
  {
    "name": "higher-group-theory.transitive-higher-group-actions",
    "value": 131,
    "unit": "ms"
  },
  {
    "name": "foundation.involutions",
    "value": 130,
    "unit": "ms"
  },
  {
    "name": "category-theory.precategories",
    "value": 129,
    "unit": "ms"
  },
  {
    "name": "foundation.monomorphisms",
    "value": 129,
    "unit": "ms"
  },
  {
    "name": "order-theory.order-preserving-maps-large-posets",
    "value": 129,
    "unit": "ms"
  },
  {
    "name": "category-theory.yoneda-lemma-precategories",
    "value": 129,
    "unit": "ms"
  },
  {
    "name": "group-theory.submonoids-commutative-monoids",
    "value": 129,
    "unit": "ms"
  },
  {
    "name": "trees.rooted-morphisms-enriched-directed-trees",
    "value": 129,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.absolute-value-integers",
    "value": 128,
    "unit": "ms"
  },
  {
    "name": "ring-theory.products-left-ideals-rings",
    "value": 128,
    "unit": "ms"
  },
  {
    "name": "foundation.raising-universe-levels",
    "value": 128,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.finite-choice",
    "value": 127,
    "unit": "ms"
  },
  {
    "name": "ring-theory.ideals-semirings",
    "value": 127,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.prime-numbers",
    "value": 127,
    "unit": "ms"
  },
  {
    "name": "structured-types.h-spaces",
    "value": 127,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-dependent-pair-types",
    "value": 127,
    "unit": "ms"
  },
  {
    "name": "lists.quicksort-lists",
    "value": 126,
    "unit": "ms"
  },
  {
    "name": "category-theory.functors-large-precategories",
    "value": 126,
    "unit": "ms"
  },
  {
    "name": "order-theory.order-preserving-maps-large-preorders",
    "value": 126,
    "unit": "ms"
  },
  {
    "name": "foundation.families-of-maps",
    "value": 126,
    "unit": "ms"
  },
  {
    "name": "group-theory.homomorphisms-concrete-groups",
    "value": 126,
    "unit": "ms"
  },
  {
    "name": "foundation-core.sections",
    "value": 126,
    "unit": "ms"
  },
  {
    "name": "group-theory.equivalences-concrete-group-actions",
    "value": 126,
    "unit": "ms"
  },
  {
    "name": "foundation.category-of-families-of-sets",
    "value": 125,
    "unit": "ms"
  },
  {
    "name": "ring-theory.products-right-ideals-rings",
    "value": 125,
    "unit": "ms"
  },
  {
    "name": "ring-theory.products-ideals-rings",
    "value": 125,
    "unit": "ms"
  },
  {
    "name": "foundation.apartness-relations",
    "value": 124,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.global-function-classes",
    "value": 124,
    "unit": "ms"
  },
  {
    "name": "linear-algebra.vectors-on-semirings",
    "value": 124,
    "unit": "ms"
  },
  {
    "name": "order-theory.large-suplattices",
    "value": 123,
    "unit": "ms"
  },
  {
    "name": "foundation.fibered-involutions",
    "value": 123,
    "unit": "ms"
  },
  {
    "name": "category-theory.conservative-functors-precategories",
    "value": 123,
    "unit": "ms"
  },
  {
    "name": "order-theory.posets",
    "value": 122,
    "unit": "ms"
  },
  {
    "name": "modal-type-theory.flat-sharp-adjunction",
    "value": 122,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.extensions-lifts-families-of-elements",
    "value": 122,
    "unit": "ms"
  },
  {
    "name": "group-theory.full-subgroups",
    "value": 122,
    "unit": "ms"
  },
  {
    "name": "reflection.type-checking-monad",
    "value": 122,
    "unit": "ms"
  },
  {
    "name": "structured-types.dependent-types-equipped-with-automorphisms",
    "value": 122,
    "unit": "ms"
  },
  {
    "name": "foundation.pairs-of-distinct-elements",
    "value": 121,
    "unit": "ms"
  },
  {
    "name": "category-theory.pregroupoids",
    "value": 121,
    "unit": "ms"
  },
  {
    "name": "foundation.structure-identity-principle",
    "value": 121,
    "unit": "ms"
  },
  {
    "name": "foundation.russells-paradox",
    "value": 120,
    "unit": "ms"
  },
  {
    "name": "order-theory.large-meet-subsemilattices",
    "value": 120,
    "unit": "ms"
  },
  {
    "name": "ring-theory.additive-orders-of-elements-rings",
    "value": 120,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.inequality-standard-finite-types",
    "value": 119,
    "unit": "ms"
  },
  {
    "name": "foundation-core.retractions",
    "value": 119,
    "unit": "ms"
  },
  {
    "name": "foundation.binary-reflecting-maps-equivalence-relations",
    "value": 119,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.ideals-generated-by-subsets-commutative-rings",
    "value": 119,
    "unit": "ms"
  },
  {
    "name": "group-theory.homomorphisms-commutative-monoids",
    "value": 118,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.radical-ideals-commutative-rings",
    "value": 118,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.reflective-subuniverses",
    "value": 118,
    "unit": "ms"
  },
  {
    "name": "foundation.equivalence-induction",
    "value": 118,
    "unit": "ms"
  },
  {
    "name": "category-theory.nonunital-precategories",
    "value": 118,
    "unit": "ms"
  },
  {
    "name": "structured-types.morphisms-types-equipped-with-endomorphisms",
    "value": 118,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.inhabited-finite-types",
    "value": 118,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.invertible-elements-commutative-rings",
    "value": 117,
    "unit": "ms"
  },
  {
    "name": "order-theory.large-posets",
    "value": 117,
    "unit": "ms"
  },
  {
    "name": "species.coproducts-species-of-types-in-subuniverses",
    "value": 117,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.commutative-semirings",
    "value": 117,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.products-commutative-rings",
    "value": 117,
    "unit": "ms"
  },
  {
    "name": "foundation-core.equivalence-relations",
    "value": 117,
    "unit": "ms"
  },
  {
    "name": "group-theory.congruence-relations-semigroups",
    "value": 116,
    "unit": "ms"
  },
  {
    "name": "foundation.propositional-extensionality",
    "value": 115,
    "unit": "ms"
  },
  {
    "name": "trees.polynomial-endofunctors",
    "value": 115,
    "unit": "ms"
  },
  {
    "name": "group-theory.nontrivial-groups",
    "value": 115,
    "unit": "ms"
  },
  {
    "name": "ring-theory.powers-of-elements-rings",
    "value": 115,
    "unit": "ms"
  },
  {
    "name": "foundation.1-types",
    "value": 114,
    "unit": "ms"
  },
  {
    "name": "foundation.cones-over-inverse-sequential-diagrams",
    "value": 114,
    "unit": "ms"
  },
  {
    "name": "foundation.trivial-sigma-decompositions",
    "value": 114,
    "unit": "ms"
  },
  {
    "name": "group-theory.automorphism-groups",
    "value": 113,
    "unit": "ms"
  },
  {
    "name": "foundation.discrete-sigma-decompositions",
    "value": 113,
    "unit": "ms"
  },
  {
    "name": "order-theory.dependent-products-large-frames",
    "value": 112,
    "unit": "ms"
  },
  {
    "name": "foundation.epimorphisms-with-respect-to-sets",
    "value": 112,
    "unit": "ms"
  },
  {
    "name": "type-theories.pi-types-precategories-with-attributes",
    "value": 112,
    "unit": "ms"
  },
  {
    "name": "foundation.contractible-types",
    "value": 112,
    "unit": "ms"
  },
  {
    "name": "foundation.action-on-identifications-binary-functions",
    "value": 112,
    "unit": "ms"
  },
  {
    "name": "group-theory.congruence-relations-commutative-monoids",
    "value": 111,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.surjective-maps",
    "value": 110,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.decidable-types",
    "value": 110,
    "unit": "ms"
  },
  {
    "name": "type-theories.pi-types-precategories-with-families",
    "value": 110,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.retracts-of-sequential-diagrams",
    "value": 109,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.powers-of-loops",
    "value": 109,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.symmetric-difference",
    "value": 109,
    "unit": "ms"
  },
  {
    "name": "group-theory.quotient-groups-concrete-groups",
    "value": 109,
    "unit": "ms"
  },
  {
    "name": "group-theory.congruence-relations-monoids",
    "value": 109,
    "unit": "ms"
  },
  {
    "name": "foundation.transport-split-type-families",
    "value": 109,
    "unit": "ms"
  },
  {
    "name": "lists.concatenation-lists",
    "value": 109,
    "unit": "ms"
  },
  {
    "name": "foundation.inhabited-types",
    "value": 109,
    "unit": "ms"
  },
  {
    "name": "ring-theory.poset-of-right-ideals-rings",
    "value": 109,
    "unit": "ms"
  },
  {
    "name": "ring-theory.right-ideals-rings",
    "value": 109,
    "unit": "ms"
  },
  {
    "name": "foundation.choice-of-representatives-equivalence-relation",
    "value": 108,
    "unit": "ms"
  },
  {
    "name": "group-theory.concrete-groups",
    "value": 108,
    "unit": "ms"
  },
  {
    "name": "foundation.connected-components-universes",
    "value": 108,
    "unit": "ms"
  },
  {
    "name": "foundation.iterating-functions",
    "value": 108,
    "unit": "ms"
  },
  {
    "name": "group-theory.kernels-homomorphisms-groups",
    "value": 107,
    "unit": "ms"
  },
  {
    "name": "foundation-core.type-theoretic-principle-of-choice",
    "value": 107,
    "unit": "ms"
  },
  {
    "name": "ring-theory.left-ideals-rings",
    "value": 107,
    "unit": "ms"
  },
  {
    "name": "category-theory.representable-functors-precategories",
    "value": 107,
    "unit": "ms"
  },
  {
    "name": "ring-theory.dependent-products-semirings",
    "value": 106,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.equality-integers",
    "value": 106,
    "unit": "ms"
  },
  {
    "name": "group-theory.commutator-subgroups",
    "value": 106,
    "unit": "ms"
  },
  {
    "name": "order-theory.large-meet-semilattices",
    "value": 106,
    "unit": "ms"
  },
  {
    "name": "foundation.discrete-relaxed-sigma-decompositions",
    "value": 106,
    "unit": "ms"
  },
  {
    "name": "category-theory.yoneda-lemma-categories",
    "value": 106,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.sums-commutative-rings",
    "value": 105,
    "unit": "ms"
  },
  {
    "name": "foundation.pointed-torsorial-type-families",
    "value": 105,
    "unit": "ms"
  },
  {
    "name": "higher-group-theory.homomorphisms-higher-groups",
    "value": 105,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.equality-natural-numbers",
    "value": 105,
    "unit": "ms"
  },
  {
    "name": "foundation.isomorphisms-of-sets",
    "value": 105,
    "unit": "ms"
  },
  {
    "name": "structured-types.pointed-maps",
    "value": 105,
    "unit": "ms"
  },
  {
    "name": "order-theory.commuting-squares-of-galois-connections-large-posets",
    "value": 105,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-dependent-function-types",
    "value": 104,
    "unit": "ms"
  },
  {
    "name": "ring-theory.poset-of-left-ideals-rings",
    "value": 104,
    "unit": "ms"
  },
  {
    "name": "foundation.fundamental-theorem-of-identity-types",
    "value": 104,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.infinitude-of-primes",
    "value": 103,
    "unit": "ms"
  },
  {
    "name": "foundation.homotopy-induction",
    "value": 103,
    "unit": "ms"
  },
  {
    "name": "group-theory.monoids",
    "value": 103,
    "unit": "ms"
  },
  {
    "name": "category-theory.representing-arrow-category",
    "value": 103,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.well-ordering-principle-natural-numbers",
    "value": 103,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.cocones-under-spans-of-pointed-types",
    "value": 103,
    "unit": "ms"
  },
  {
    "name": "foundation.0-maps",
    "value": 102,
    "unit": "ms"
  },
  {
    "name": "order-theory.decidable-total-orders",
    "value": 102,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.closed-modalities",
    "value": 101,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.poset-of-radical-ideals-commutative-rings",
    "value": 101,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-cartesian-product-types",
    "value": 101,
    "unit": "ms"
  },
  {
    "name": "foundation.functoriality-function-types",
    "value": 101,
    "unit": "ms"
  },
  {
    "name": "foundation.propositional-maps",
    "value": 100,
    "unit": "ms"
  },
  {
    "name": "foundation.cartesian-morphisms-arrows",
    "value": 100,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.inequality-integers",
    "value": 100,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.finitely-cyclic-maps",
    "value": 99,
    "unit": "ms"
  },
  {
    "name": "foundation.precomposition-functions-into-subuniverses",
    "value": 99,
    "unit": "ms"
  },
  {
    "name": "category-theory.maps-categories",
    "value": 98,
    "unit": "ms"
  },
  {
    "name": "higher-group-theory.iterated-cartesian-products-higher-groups",
    "value": 98,
    "unit": "ms"
  },
  {
    "name": "foundation.symmetric-binary-relations",
    "value": 98,
    "unit": "ms"
  },
  {
    "name": "graph-theory.enriched-undirected-graphs",
    "value": 98,
    "unit": "ms"
  },
  {
    "name": "category-theory.maps-from-small-to-large-categories",
    "value": 98,
    "unit": "ms"
  },
  {
    "name": "foundation.existential-quantification",
    "value": 98,
    "unit": "ms"
  },
  {
    "name": "order-theory.homomorphisms-meet-semilattices",
    "value": 98,
    "unit": "ms"
  },
  {
    "name": "foundation.maybe",
    "value": 98,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.prime-ideals-commutative-rings",
    "value": 97,
    "unit": "ms"
  },
  {
    "name": "ring-theory.poset-of-ideals-rings",
    "value": 97,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.integer-fractions",
    "value": 97,
    "unit": "ms"
  },
  {
    "name": "foundation.equivalences-spans-families-of-types",
    "value": 97,
    "unit": "ms"
  },
  {
    "name": "universal-algebra.kernels",
    "value": 96,
    "unit": "ms"
  },
  {
    "name": "foundation.dependent-universal-property-equivalences",
    "value": 96,
    "unit": "ms"
  },
  {
    "name": "category-theory.set-magmoids",
    "value": 96,
    "unit": "ms"
  },
  {
    "name": "foundation.iterated-dependent-product-types",
    "value": 96,
    "unit": "ms"
  },
  {
    "name": "foundation.booleans",
    "value": 96,
    "unit": "ms"
  },
  {
    "name": "foundation.uniqueness-set-truncations",
    "value": 96,
    "unit": "ms"
  },
  {
    "name": "group-theory.homomorphisms-concrete-group-actions",
    "value": 96,
    "unit": "ms"
  },
  {
    "name": "ring-theory.algebras-rings",
    "value": 95,
    "unit": "ms"
  },
  {
    "name": "foundation.weak-function-extensionality",
    "value": 95,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.dependent-function-types",
    "value": 95,
    "unit": "ms"
  },
  {
    "name": "foundation.binary-transport",
    "value": 95,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.1-acyclic-types",
    "value": 95,
    "unit": "ms"
  },
  {
    "name": "group-theory.torsion-free-groups",
    "value": 95,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.induction-principle-pushouts",
    "value": 95,
    "unit": "ms"
  },
  {
    "name": "order-theory.similarity-of-elements-large-posets",
    "value": 95,
    "unit": "ms"
  },
  {
    "name": "species.morphisms-species-of-types",
    "value": 95,
    "unit": "ms"
  },
  {
    "name": "group-theory.full-subsemigroups",
    "value": 94,
    "unit": "ms"
  },
  {
    "name": "higher-group-theory.free-higher-group-actions",
    "value": 94,
    "unit": "ms"
  },
  {
    "name": "order-theory.preorders",
    "value": 94,
    "unit": "ms"
  },
  {
    "name": "foundation.type-arithmetic-cartesian-product-types",
    "value": 94,
    "unit": "ms"
  },
  {
    "name": "group-theory.free-groups-with-one-generator",
    "value": 94,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.loop-spaces",
    "value": 94,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.full-ideals-commutative-rings",
    "value": 94,
    "unit": "ms"
  },
  {
    "name": "lists.sorted-lists",
    "value": 93,
    "unit": "ms"
  },
  {
    "name": "order-theory.closure-operators-large-posets",
    "value": 93,
    "unit": "ms"
  },
  {
    "name": "order-theory.dependent-products-large-locales",
    "value": 93,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.maximum-natural-numbers",
    "value": 93,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.coequalizers",
    "value": 93,
    "unit": "ms"
  },
  {
    "name": "foundation.fibers-of-maps",
    "value": 93,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.groups-of-order-2",
    "value": 92,
    "unit": "ms"
  },
  {
    "name": "foundation.whiskering-homotopies-concatenation",
    "value": 92,
    "unit": "ms"
  },
  {
    "name": "ring-theory.full-ideals-rings",
    "value": 92,
    "unit": "ms"
  },
  {
    "name": "group-theory.intersections-subgroups-groups",
    "value": 92,
    "unit": "ms"
  },
  {
    "name": "linear-algebra.scalar-multiplication-vectors-on-rings",
    "value": 91,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.universal-property-standard-finite-types",
    "value": 91,
    "unit": "ms"
  },
  {
    "name": "ring-theory.subsets-rings",
    "value": 91,
    "unit": "ms"
  },
  {
    "name": "species.composition-cauchy-series-species-of-types-in-subuniverses",
    "value": 91,
    "unit": "ms"
  },
  {
    "name": "species.products-cauchy-series-species-of-types-in-subuniverses",
    "value": 91,
    "unit": "ms"
  },
  {
    "name": "foundation.structured-type-duality",
    "value": 91,
    "unit": "ms"
  },
  {
    "name": "order-theory",
    "value": 91,
    "unit": "ms"
  },
  {
    "name": "foundation.reflecting-maps-equivalence-relations",
    "value": 91,
    "unit": "ms"
  },
  {
    "name": "ring-theory.function-semirings",
    "value": 91,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.wedges-of-pointed-types",
    "value": 91,
    "unit": "ms"
  },
  {
    "name": "foundation.type-arithmetic-unit-type",
    "value": 90,
    "unit": "ms"
  },
  {
    "name": "lists.reversing-lists",
    "value": 90,
    "unit": "ms"
  },
  {
    "name": "order-theory.powers-of-large-locales",
    "value": 90,
    "unit": "ms"
  },
  {
    "name": "ring-theory.sums-rings",
    "value": 90,
    "unit": "ms"
  },
  {
    "name": "category-theory.simplex-category",
    "value": 89,
    "unit": "ms"
  },
  {
    "name": "foundation.inhabited-subtypes",
    "value": 89,
    "unit": "ms"
  },
  {
    "name": "foundation.subtype-identity-principle",
    "value": 88,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics",
    "value": 88,
    "unit": "ms"
  },
  {
    "name": "foundation.equivalence-injective-type-families",
    "value": 87,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.sums-commutative-semirings",
    "value": 87,
    "unit": "ms"
  },
  {
    "name": "ring-theory.category-of-cyclic-rings",
    "value": 87,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.minimum-natural-numbers",
    "value": 87,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.local-maps",
    "value": 86,
    "unit": "ms"
  },
  {
    "name": "group-theory.equivalences-semigroups",
    "value": 86,
    "unit": "ms"
  },
  {
    "name": "category-theory.initial-category",
    "value": 86,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.necklaces",
    "value": 86,
    "unit": "ms"
  },
  {
    "name": "category-theory.full-maps-precategories",
    "value": 86,
    "unit": "ms"
  },
  {
    "name": "ring-theory.function-rings",
    "value": 85,
    "unit": "ms"
  },
  {
    "name": "category-theory.cores-categories",
    "value": 85,
    "unit": "ms"
  },
  {
    "name": "foundation.coslice",
    "value": 85,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.fibonacci-sequence",
    "value": 85,
    "unit": "ms"
  },
  {
    "name": "order-theory.subposets",
    "value": 85,
    "unit": "ms"
  },
  {
    "name": "ring-theory.commuting-elements-rings",
    "value": 85,
    "unit": "ms"
  },
  {
    "name": "category-theory.isomorphism-induction-categories",
    "value": 85,
    "unit": "ms"
  },
  {
    "name": "group-theory.cartesian-products-abelian-groups",
    "value": 85,
    "unit": "ms"
  },
  {
    "name": "modal-type-theory.flat-modality",
    "value": 85,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-coproduct-types",
    "value": 84,
    "unit": "ms"
  },
  {
    "name": "foundation.commuting-triangles-of-homotopies",
    "value": 84,
    "unit": "ms"
  },
  {
    "name": "foundation.functoriality-propositional-truncation",
    "value": 84,
    "unit": "ms"
  },
  {
    "name": "order-theory.distributive-lattices",
    "value": 84,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory",
    "value": 84,
    "unit": "ms"
  },
  {
    "name": "modal-type-theory.sharp-modality",
    "value": 84,
    "unit": "ms"
  },
  {
    "name": "foundation.large-locale-of-subtypes",
    "value": 84,
    "unit": "ms"
  },
  {
    "name": "foundation.category-of-sets",
    "value": 84,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.finitely-presented-types",
    "value": 84,
    "unit": "ms"
  },
  {
    "name": "group-theory.group-actions",
    "value": 84,
    "unit": "ms"
  },
  {
    "name": "foundation.precomposition-dependent-functions",
    "value": 83,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.double-loop-spaces",
    "value": 83,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.modal-operators",
    "value": 82,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.subsets-commutative-rings",
    "value": 82,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.dependent-products-commutative-semirings",
    "value": 82,
    "unit": "ms"
  },
  {
    "name": "species.cauchy-series-species-of-types-in-subuniverses",
    "value": 82,
    "unit": "ms"
  },
  {
    "name": "foundation.disjunction",
    "value": 82,
    "unit": "ms"
  },
  {
    "name": "group-theory.dependent-products-abelian-groups",
    "value": 82,
    "unit": "ms"
  },
  {
    "name": "foundation-core.sets",
    "value": 81,
    "unit": "ms"
  },
  {
    "name": "category-theory.split-essentially-surjective-functors-precategories",
    "value": 81,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.concrete-quaternion-group",
    "value": 81,
    "unit": "ms"
  },
  {
    "name": "order-theory.least-upper-bounds-large-posets",
    "value": 81,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.complements-isolated-elements",
    "value": 80,
    "unit": "ms"
  },
  {
    "name": "linear-algebra.vectors-on-commutative-rings",
    "value": 80,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.function-commutative-semirings",
    "value": 80,
    "unit": "ms"
  },
  {
    "name": "foundation.repetitions-sequences",
    "value": 80,
    "unit": "ms"
  },
  {
    "name": "foundation.functoriality-pullbacks",
    "value": 80,
    "unit": "ms"
  },
  {
    "name": "foundation.contractible-maps",
    "value": 80,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.addition-natural-numbers",
    "value": 80,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.ideals-commutative-semirings",
    "value": 80,
    "unit": "ms"
  },
  {
    "name": "foundation.sigma-decomposition-subuniverse",
    "value": 80,
    "unit": "ms"
  },
  {
    "name": "foundation.trivial-relaxed-sigma-decompositions",
    "value": 80,
    "unit": "ms"
  },
  {
    "name": "foundation.pi-decompositions-subuniverse",
    "value": 80,
    "unit": "ms"
  },
  {
    "name": "species.exponentials-cauchy-series-of-types-in-subuniverses",
    "value": 79,
    "unit": "ms"
  },
  {
    "name": "graph-theory.trails-undirected-graphs",
    "value": 79,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.tetrahedra-in-3-space",
    "value": 79,
    "unit": "ms"
  },
  {
    "name": "foundation.morphisms-span-diagrams",
    "value": 79,
    "unit": "ms"
  },
  {
    "name": "foundation.path-split-maps",
    "value": 79,
    "unit": "ms"
  },
  {
    "name": "foundation-core.contractible-maps",
    "value": 79,
    "unit": "ms"
  },
  {
    "name": "ring-theory",
    "value": 79,
    "unit": "ms"
  },
  {
    "name": "order-theory.subpreorders",
    "value": 78,
    "unit": "ms"
  },
  {
    "name": "ring-theory.nilpotent-elements-semirings",
    "value": 78,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory",
    "value": 78,
    "unit": "ms"
  },
  {
    "name": "trees.raising-universe-levels-directed-trees",
    "value": 78,
    "unit": "ms"
  },
  {
    "name": "foundation.axiom-of-choice",
    "value": 78,
    "unit": "ms"
  },
  {
    "name": "linear-algebra.functoriality-vectors",
    "value": 78,
    "unit": "ms"
  },
  {
    "name": "foundation.equivalences-cospans",
    "value": 78,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.binomial-theorem-commutative-rings",
    "value": 78,
    "unit": "ms"
  },
  {
    "name": "foundation.truncated-types",
    "value": 77,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.cocartesian-morphisms-arrows",
    "value": 77,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.difference-integers",
    "value": 77,
    "unit": "ms"
  },
  {
    "name": "species.species-of-types-in-subuniverses",
    "value": 77,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.finite-commutative-monoids",
    "value": 77,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.products-subsets-commutative-rings",
    "value": 76,
    "unit": "ms"
  },
  {
    "name": "ring-theory.binomial-theorem-rings",
    "value": 76,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.lifts-families-of-elements",
    "value": 76,
    "unit": "ms"
  },
  {
    "name": "foundation.unit-type",
    "value": 76,
    "unit": "ms"
  },
  {
    "name": "category-theory.representable-functors-large-precategories",
    "value": 76,
    "unit": "ms"
  },
  {
    "name": "category-theory.augmented-simplex-category",
    "value": 75,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.unit-similarity-standard-finite-types",
    "value": 75,
    "unit": "ms"
  },
  {
    "name": "foundation.binary-embeddings",
    "value": 75,
    "unit": "ms"
  },
  {
    "name": "foundation.diagonal-maps-of-types",
    "value": 75,
    "unit": "ms"
  },
  {
    "name": "foundation.equivalences-span-diagrams-families-of-types",
    "value": 74,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.squares-natural-numbers",
    "value": 74,
    "unit": "ms"
  },
  {
    "name": "order-theory.lattices",
    "value": 74,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.trivial-sigma-decompositions",
    "value": 74,
    "unit": "ms"
  },
  {
    "name": "ring-theory.intersections-ideals-rings",
    "value": 74,
    "unit": "ms"
  },
  {
    "name": "foundation-core.propositional-maps",
    "value": 73,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.binomial-theorem-commutative-semirings",
    "value": 73,
    "unit": "ms"
  },
  {
    "name": "linear-algebra.vectors-on-commutative-semirings",
    "value": 73,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.discrete-sigma-decompositions",
    "value": 73,
    "unit": "ms"
  },
  {
    "name": "category-theory.maps-from-small-to-large-precategories",
    "value": 72,
    "unit": "ms"
  },
  {
    "name": "group-theory.pullbacks-subsemigroups",
    "value": 72,
    "unit": "ms"
  },
  {
    "name": "lists.lists-discrete-types",
    "value": 72,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.relatively-prime-natural-numbers",
    "value": 72,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.inequality-types-with-counting",
    "value": 72,
    "unit": "ms"
  },
  {
    "name": "order-theory.large-preorders",
    "value": 72,
    "unit": "ms"
  },
  {
    "name": "category-theory.natural-numbers-object-precategories",
    "value": 72,
    "unit": "ms"
  },
  {
    "name": "foundation-core.operations-span-diagrams",
    "value": 72,
    "unit": "ms"
  },
  {
    "name": "linear-algebra.matrices-on-rings",
    "value": 72,
    "unit": "ms"
  },
  {
    "name": "foundation.action-on-homotopies-functions",
    "value": 72,
    "unit": "ms"
  },
  {
    "name": "ring-theory.kernels-of-ring-homomorphisms",
    "value": 72,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.connected-set-bundles-circle",
    "value": 71,
    "unit": "ms"
  },
  {
    "name": "trees.inequality-w-types",
    "value": 71,
    "unit": "ms"
  },
  {
    "name": "foundation.empty-types",
    "value": 71,
    "unit": "ms"
  },
  {
    "name": "group-theory.cyclic-groups",
    "value": 71,
    "unit": "ms"
  },
  {
    "name": "foundation-core.diagonal-maps-of-types",
    "value": 70,
    "unit": "ms"
  },
  {
    "name": "foundation.mere-equivalences",
    "value": 70,
    "unit": "ms"
  },
  {
    "name": "foundation-core.invertible-maps",
    "value": 70,
    "unit": "ms"
  },
  {
    "name": "order-theory.decidable-total-preorders",
    "value": 70,
    "unit": "ms"
  },
  {
    "name": "order-theory.large-subsuplattices",
    "value": 70,
    "unit": "ms"
  },
  {
    "name": "foundation.multivariable-operations",
    "value": 70,
    "unit": "ms"
  },
  {
    "name": "structured-types.conjugation-pointed-types",
    "value": 70,
    "unit": "ms"
  },
  {
    "name": "order-theory.locales",
    "value": 70,
    "unit": "ms"
  },
  {
    "name": "group-theory.category-of-group-actions",
    "value": 69,
    "unit": "ms"
  },
  {
    "name": "foundation-core.decidable-propositions",
    "value": 69,
    "unit": "ms"
  },
  {
    "name": "group-theory.stabilizer-groups-concrete-group-actions",
    "value": 69,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.retracts-of-finite-types",
    "value": 69,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.spectra",
    "value": 69,
    "unit": "ms"
  },
  {
    "name": "group-theory.cartesian-products-groups",
    "value": 69,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.intersections-ideals-commutative-rings",
    "value": 69,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.parity-natural-numbers",
    "value": 68,
    "unit": "ms"
  },
  {
    "name": "graph-theory.embeddings-undirected-graphs",
    "value": 68,
    "unit": "ms"
  },
  {
    "name": "order-theory.large-subposets",
    "value": 68,
    "unit": "ms"
  },
  {
    "name": "group-theory.category-of-orbits-groups",
    "value": 68,
    "unit": "ms"
  },
  {
    "name": "category-theory.one-object-precategories",
    "value": 68,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.universal-property-suspensions",
    "value": 68,
    "unit": "ms"
  },
  {
    "name": "structured-types.pointed-cartesian-product-types",
    "value": 68,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.poset-of-ideals-commutative-rings",
    "value": 68,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.null-types",
    "value": 68,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.decidable-dependent-function-types",
    "value": 68,
    "unit": "ms"
  },
  {
    "name": "order-theory.dependent-products-large-suplattices",
    "value": 68,
    "unit": "ms"
  },
  {
    "name": "group-theory.powers-of-elements-groups",
    "value": 67,
    "unit": "ms"
  },
  {
    "name": "structured-types.wild-monoids",
    "value": 67,
    "unit": "ms"
  },
  {
    "name": "foundation.unordered-tuples-of-types",
    "value": 67,
    "unit": "ms"
  },
  {
    "name": "category-theory.natural-transformations-functors-large-categories",
    "value": 66,
    "unit": "ms"
  },
  {
    "name": "foundation.split-surjective-maps",
    "value": 66,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.unit-elements-standard-finite-types",
    "value": 66,
    "unit": "ms"
  },
  {
    "name": "foundation.binary-homotopies",
    "value": 66,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.sums-of-natural-numbers",
    "value": 66,
    "unit": "ms"
  },
  {
    "name": "category-theory.products-of-precategories",
    "value": 66,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.decidable-propositions",
    "value": 66,
    "unit": "ms"
  },
  {
    "name": "order-theory.dependent-products-large-meet-semilattices",
    "value": 66,
    "unit": "ms"
  },
  {
    "name": "category-theory.exponential-objects-precategories",
    "value": 66,
    "unit": "ms"
  },
  {
    "name": "linear-algebra.transposition-matrices",
    "value": 66,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.pullback-property-pushouts",
    "value": 65,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.minimum-standard-finite-types",
    "value": 65,
    "unit": "ms"
  },
  {
    "name": "modal-type-theory.sharp-codiscrete-types",
    "value": 65,
    "unit": "ms"
  },
  {
    "name": "foundation.homotopy-algebra",
    "value": 65,
    "unit": "ms"
  },
  {
    "name": "group-theory.representations-monoids-precategories",
    "value": 65,
    "unit": "ms"
  },
  {
    "name": "foundation-core.operations-spans",
    "value": 64,
    "unit": "ms"
  },
  {
    "name": "foundation.truncated-maps",
    "value": 64,
    "unit": "ms"
  },
  {
    "name": "foundation.dependent-telescopes",
    "value": 64,
    "unit": "ms"
  },
  {
    "name": "foundation.double-powersets",
    "value": 64,
    "unit": "ms"
  },
  {
    "name": "higher-group-theory.cartesian-products-higher-groups",
    "value": 64,
    "unit": "ms"
  },
  {
    "name": "reflection.definitions",
    "value": 64,
    "unit": "ms"
  },
  {
    "name": "real-numbers.dedekind-real-numbers",
    "value": 64,
    "unit": "ms"
  },
  {
    "name": "group-theory.commutative-monoids",
    "value": 63,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.squares-integers",
    "value": 63,
    "unit": "ms"
  },
  {
    "name": "order-theory.suplattices",
    "value": 63,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.euclidean-division-natural-numbers",
    "value": 63,
    "unit": "ms"
  },
  {
    "name": "foundation.unordered-pairs-of-types",
    "value": 63,
    "unit": "ms"
  },
  {
    "name": "organic-chemistry.alcohols",
    "value": 63,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.cavallos-trick",
    "value": 62,
    "unit": "ms"
  },
  {
    "name": "order-theory.total-orders",
    "value": 62,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.cofibers",
    "value": 62,
    "unit": "ms"
  },
  {
    "name": "category-theory.pointed-endofunctors-categories",
    "value": 62,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.maximum-standard-finite-types",
    "value": 62,
    "unit": "ms"
  },
  {
    "name": "ring-theory.subsets-semirings",
    "value": 61,
    "unit": "ms"
  },
  {
    "name": "structured-types.pointed-universal-property-contractible-types",
    "value": 61,
    "unit": "ms"
  },
  {
    "name": "foundation.implicit-function-types",
    "value": 61,
    "unit": "ms"
  },
  {
    "name": "structured-types.mere-equivalences-types-equipped-with-endomorphisms",
    "value": 61,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-contractible-types",
    "value": 60,
    "unit": "ms"
  },
  {
    "name": "foundation-core.commuting-triangles-of-maps",
    "value": 60,
    "unit": "ms"
  },
  {
    "name": "category-theory.pointed-endofunctors-precategories",
    "value": 60,
    "unit": "ms"
  },
  {
    "name": "group-theory.dependent-products-groups",
    "value": 60,
    "unit": "ms"
  },
  {
    "name": "category-theory.homotopies-natural-transformations-large-precategories",
    "value": 60,
    "unit": "ms"
  },
  {
    "name": "foundation.commuting-tetrahedra-of-homotopies",
    "value": 60,
    "unit": "ms"
  },
  {
    "name": "order-theory.upper-bounds-posets",
    "value": 60,
    "unit": "ms"
  },
  {
    "name": "group-theory.function-abelian-groups",
    "value": 60,
    "unit": "ms"
  },
  {
    "name": "graph-theory.neighbors-undirected-graphs",
    "value": 60,
    "unit": "ms"
  },
  {
    "name": "group-theory.powers-of-elements-commutative-monoids",
    "value": 59,
    "unit": "ms"
  },
  {
    "name": "group-theory.semigroups",
    "value": 59,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-identity-systems",
    "value": 59,
    "unit": "ms"
  },
  {
    "name": "foundation.products-unordered-pairs-of-types",
    "value": 59,
    "unit": "ms"
  },
  {
    "name": "foundation.multivariable-functoriality-set-quotients",
    "value": 59,
    "unit": "ms"
  },
  {
    "name": "foundation.torsorial-type-families",
    "value": 58,
    "unit": "ms"
  },
  {
    "name": "category-theory.constant-functors",
    "value": 58,
    "unit": "ms"
  },
  {
    "name": "foundation.symmetric-cores-binary-relations",
    "value": 58,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.proper-divisors-natural-numbers",
    "value": 58,
    "unit": "ms"
  },
  {
    "name": "group-theory.symmetric-concrete-groups",
    "value": 58,
    "unit": "ms"
  },
  {
    "name": "order-theory.decidable-posets",
    "value": 58,
    "unit": "ms"
  },
  {
    "name": "group-theory.centers-groups",
    "value": 58,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra",
    "value": 57,
    "unit": "ms"
  },
  {
    "name": "foundation.dependent-inverse-sequential-diagrams",
    "value": 57,
    "unit": "ms"
  },
  {
    "name": "foundation.large-binary-relations",
    "value": 57,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.binomial-theorem-integers",
    "value": 57,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.multiplication-circle",
    "value": 57,
    "unit": "ms"
  },
  {
    "name": "foundation.tight-apartness-relations",
    "value": 56,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-unit-type",
    "value": 56,
    "unit": "ms"
  },
  {
    "name": "foundation.double-negation",
    "value": 56,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.embeddings",
    "value": 56,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.factorization-operations-global-function-classes",
    "value": 56,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.subsets-commutative-semirings",
    "value": 56,
    "unit": "ms"
  },
  {
    "name": "foundation.operations-span-diagrams",
    "value": 56,
    "unit": "ms"
  },
  {
    "name": "foundation.equality-dependent-function-types",
    "value": 56,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.nilradical-commutative-rings",
    "value": 56,
    "unit": "ms"
  },
  {
    "name": "structured-types.morphisms-types-equipped-with-automorphisms",
    "value": 56,
    "unit": "ms"
  },
  {
    "name": "graph-theory.polygons",
    "value": 56,
    "unit": "ms"
  },
  {
    "name": "graph-theory.faithful-morphisms-undirected-graphs",
    "value": 55,
    "unit": "ms"
  },
  {
    "name": "organic-chemistry.hydrocarbons",
    "value": 55,
    "unit": "ms"
  },
  {
    "name": "group-theory.category-of-groups",
    "value": 55,
    "unit": "ms"
  },
  {
    "name": "order-theory.accessible-elements-relations",
    "value": 55,
    "unit": "ms"
  },
  {
    "name": "order-theory.principal-lower-sets-large-posets",
    "value": 55,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.conjugation-loops",
    "value": 55,
    "unit": "ms"
  },
  {
    "name": "order-theory.homomorphisms-frames",
    "value": 55,
    "unit": "ms"
  },
  {
    "name": "structured-types.morphisms-wild-monoids",
    "value": 55,
    "unit": "ms"
  },
  {
    "name": "order-theory.lower-bounds-posets",
    "value": 55,
    "unit": "ms"
  },
  {
    "name": "foundation.action-on-equivalences-functions",
    "value": 54,
    "unit": "ms"
  },
  {
    "name": "order-theory.principal-upper-sets-large-posets",
    "value": 54,
    "unit": "ms"
  },
  {
    "name": "category-theory.subterminal-precategories",
    "value": 54,
    "unit": "ms"
  },
  {
    "name": "modal-type-theory.flat-dependent-pair-types",
    "value": 54,
    "unit": "ms"
  },
  {
    "name": "structured-types.function-wild-monoids",
    "value": 54,
    "unit": "ms"
  },
  {
    "name": "order-theory.finite-total-orders",
    "value": 54,
    "unit": "ms"
  },
  {
    "name": "foundation.singleton-induction",
    "value": 54,
    "unit": "ms"
  },
  {
    "name": "foundation.equivalences-inverse-sequential-diagrams",
    "value": 54,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.repeating-element-standard-finite-type",
    "value": 54,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.sieve-of-eratosthenes",
    "value": 54,
    "unit": "ms"
  },
  {
    "name": "higher-group-theory.homomorphisms-higher-group-actions",
    "value": 53,
    "unit": "ms"
  },
  {
    "name": "ring-theory.quotient-rings",
    "value": 53,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.cofibonacci",
    "value": 53,
    "unit": "ms"
  },
  {
    "name": "foundation.connected-components",
    "value": 53,
    "unit": "ms"
  },
  {
    "name": "graph-theory.finite-graphs",
    "value": 53,
    "unit": "ms"
  },
  {
    "name": "group-theory.centralizer-subgroups",
    "value": 53,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.classical-finite-types",
    "value": 53,
    "unit": "ms"
  },
  {
    "name": "foundation.action-on-equivalences-type-families-over-subuniverses",
    "value": 53,
    "unit": "ms"
  },
  {
    "name": "group-theory.precategory-of-group-actions",
    "value": 53,
    "unit": "ms"
  },
  {
    "name": "group-theory.commuting-elements-semigroups",
    "value": 52,
    "unit": "ms"
  },
  {
    "name": "universal-algebra.congruences",
    "value": 52,
    "unit": "ms"
  },
  {
    "name": "category-theory.essentially-surjective-functors-precategories",
    "value": 52,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.functoriality-pullback-hom",
    "value": 52,
    "unit": "ms"
  },
  {
    "name": "order-theory.homomorphisms-meet-sup-lattices",
    "value": 52,
    "unit": "ms"
  },
  {
    "name": "trees.w-type-of-natural-numbers",
    "value": 52,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.function-types",
    "value": 52,
    "unit": "ms"
  },
  {
    "name": "group-theory.kernels-homomorphisms-concrete-groups",
    "value": 52,
    "unit": "ms"
  },
  {
    "name": "graph-theory.raising-universe-levels-directed-graphs",
    "value": 52,
    "unit": "ms"
  },
  {
    "name": "foundation.preunivalence",
    "value": 52,
    "unit": "ms"
  },
  {
    "name": "foundation.full-subtypes",
    "value": 52,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.decidable-dependent-pair-types",
    "value": 52,
    "unit": "ms"
  },
  {
    "name": "group-theory.endomorphism-rings-abelian-groups",
    "value": 52,
    "unit": "ms"
  },
  {
    "name": "order-theory.homomorphisms-sup-lattices",
    "value": 52,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.repetitions-of-values",
    "value": 52,
    "unit": "ms"
  },
  {
    "name": "higher-group-theory.equivalences-higher-groups",
    "value": 51,
    "unit": "ms"
  },
  {
    "name": "ring-theory.nilpotent-elements-rings",
    "value": 51,
    "unit": "ms"
  },
  {
    "name": "foundation.products-equivalence-relations",
    "value": 51,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-maybe",
    "value": 51,
    "unit": "ms"
  },
  {
    "name": "group-theory.kernels-homomorphisms-abelian-groups",
    "value": 51,
    "unit": "ms"
  },
  {
    "name": "foundation.negated-equality",
    "value": 51,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.radical-ideals-generated-by-subsets-commutative-rings",
    "value": 51,
    "unit": "ms"
  },
  {
    "name": "group-theory.category-of-semigroups",
    "value": 51,
    "unit": "ms"
  },
  {
    "name": "category-theory.functors-large-categories",
    "value": 50,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.binomial-theorem-natural-numbers",
    "value": 50,
    "unit": "ms"
  },
  {
    "name": "foundation.postcomposition-dependent-functions",
    "value": 50,
    "unit": "ms"
  },
  {
    "name": "foundation.decidable-maps",
    "value": 50,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.multiplication-integer-fractions",
    "value": 50,
    "unit": "ms"
  },
  {
    "name": "foundation.transport-along-homotopies",
    "value": 50,
    "unit": "ms"
  },
  {
    "name": "foundation.conjunction",
    "value": 50,
    "unit": "ms"
  },
  {
    "name": "foundation.decidable-dependent-pair-types",
    "value": 50,
    "unit": "ms"
  },
  {
    "name": "graph-theory.undirected-graphs",
    "value": 50,
    "unit": "ms"
  },
  {
    "name": "ring-theory.powers-of-elements-semirings",
    "value": 50,
    "unit": "ms"
  },
  {
    "name": "group-theory.multiples-of-elements-abelian-groups",
    "value": 50,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.tangent-spheres",
    "value": 50,
    "unit": "ms"
  },
  {
    "name": "lists.sorting-algorithms-lists",
    "value": 50,
    "unit": "ms"
  },
  {
    "name": "ring-theory.precategory-of-semirings",
    "value": 50,
    "unit": "ms"
  },
  {
    "name": "foundation.iterated-dependent-pair-types",
    "value": 50,
    "unit": "ms"
  },
  {
    "name": "group-theory.function-groups",
    "value": 49,
    "unit": "ms"
  },
  {
    "name": "order-theory.meet-suplattices",
    "value": 49,
    "unit": "ms"
  },
  {
    "name": "category-theory.isomorphism-induction-precategories",
    "value": 49,
    "unit": "ms"
  },
  {
    "name": "order-theory.precategory-of-posets",
    "value": 49,
    "unit": "ms"
  },
  {
    "name": "group-theory.commutators-of-elements-groups",
    "value": 49,
    "unit": "ms"
  },
  {
    "name": "order-theory.similarity-of-order-preserving-maps-large-posets",
    "value": 49,
    "unit": "ms"
  },
  {
    "name": "foundation.identity-systems",
    "value": 49,
    "unit": "ms"
  },
  {
    "name": "lists.flattening-lists",
    "value": 49,
    "unit": "ms"
  },
  {
    "name": "order-theory.chains-preorders",
    "value": 49,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.powers-of-elements-commutative-rings",
    "value": 49,
    "unit": "ms"
  },
  {
    "name": "trees.universal-multiset",
    "value": 48,
    "unit": "ms"
  },
  {
    "name": "group-theory.subsets-semigroups",
    "value": 48,
    "unit": "ms"
  },
  {
    "name": "group-theory.central-elements-groups",
    "value": 48,
    "unit": "ms"
  },
  {
    "name": "ring-theory.multiples-of-elements-rings",
    "value": 48,
    "unit": "ms"
  },
  {
    "name": "structured-types.wild-loops",
    "value": 48,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.distance-integers",
    "value": 48,
    "unit": "ms"
  },
  {
    "name": "finite-algebra.semisimple-commutative-finite-rings",
    "value": 48,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.sums-of-natural-numbers",
    "value": 48,
    "unit": "ms"
  },
  {
    "name": "foundation-core.embeddings",
    "value": 48,
    "unit": "ms"
  },
  {
    "name": "foundation-core.empty-types",
    "value": 48,
    "unit": "ms"
  },
  {
    "name": "graph-theory.directed-graphs",
    "value": 48,
    "unit": "ms"
  },
  {
    "name": "graph-theory.complete-bipartite-graphs",
    "value": 47,
    "unit": "ms"
  },
  {
    "name": "group-theory.cayleys-theorem",
    "value": 47,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.unions-subtypes",
    "value": 47,
    "unit": "ms"
  },
  {
    "name": "category-theory.anafunctors-categories",
    "value": 47,
    "unit": "ms"
  },
  {
    "name": "foundation.subtype-duality",
    "value": 47,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.monoid-of-natural-numbers-with-maximum",
    "value": 46,
    "unit": "ms"
  },
  {
    "name": "foundation.operations-spans",
    "value": 46,
    "unit": "ms"
  },
  {
    "name": "foundation.products-unordered-tuples-of-types",
    "value": 46,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.skipping-element-standard-finite-types",
    "value": 46,
    "unit": "ms"
  },
  {
    "name": "category-theory.embeddings-precategories",
    "value": 46,
    "unit": "ms"
  },
  {
    "name": "order-theory.similarity-of-elements-large-preorders",
    "value": 46,
    "unit": "ms"
  },
  {
    "name": "trees",
    "value": 46,
    "unit": "ms"
  },
  {
    "name": "category-theory.full-functors-precategories",
    "value": 46,
    "unit": "ms"
  },
  {
    "name": "foundation.unital-binary-operations",
    "value": 45,
    "unit": "ms"
  },
  {
    "name": "order-theory.chains-posets",
    "value": 45,
    "unit": "ms"
  },
  {
    "name": "category-theory.epimorphisms-in-large-precategories",
    "value": 45,
    "unit": "ms"
  },
  {
    "name": "order-theory.large-subpreorders",
    "value": 45,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.kuratowsky-finite-sets",
    "value": 45,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.dependent-universal-property-suspensions",
    "value": 45,
    "unit": "ms"
  },
  {
    "name": "foundation.pullback-squares",
    "value": 45,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.truncated-acyclic-types",
    "value": 45,
    "unit": "ms"
  },
  {
    "name": "foundation-core",
    "value": 45,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.wide-global-function-classes",
    "value": 44,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.initial-segments-natural-numbers",
    "value": 44,
    "unit": "ms"
  },
  {
    "name": "universal-algebra.algebras-of-theories",
    "value": 44,
    "unit": "ms"
  },
  {
    "name": "structured-types.dependent-products-h-spaces",
    "value": 44,
    "unit": "ms"
  },
  {
    "name": "foundation.mere-equality",
    "value": 44,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-empty-type",
    "value": 44,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.precategory-of-commutative-semirings",
    "value": 44,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.precategory-of-commutative-rings",
    "value": 44,
    "unit": "ms"
  },
  {
    "name": "foundation.discrete-types",
    "value": 44,
    "unit": "ms"
  },
  {
    "name": "category-theory.monomorphisms-in-large-precategories",
    "value": 44,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.premanifolds",
    "value": 43,
    "unit": "ms"
  },
  {
    "name": "foundation.span-diagrams",
    "value": 43,
    "unit": "ms"
  },
  {
    "name": "linear-algebra.matrices",
    "value": 43,
    "unit": "ms"
  },
  {
    "name": "group-theory.commuting-elements-groups",
    "value": 43,
    "unit": "ms"
  },
  {
    "name": "order-theory.finite-posets",
    "value": 43,
    "unit": "ms"
  },
  {
    "name": "foundation.retracts-of-types",
    "value": 43,
    "unit": "ms"
  },
  {
    "name": "group-theory.cartesian-products-monoids",
    "value": 43,
    "unit": "ms"
  },
  {
    "name": "category-theory.initial-objects-precategories",
    "value": 43,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.divisibility-standard-finite-types",
    "value": 43,
    "unit": "ms"
  },
  {
    "name": "ring-theory.precategory-of-rings",
    "value": 43,
    "unit": "ms"
  },
  {
    "name": "trees.w-type-of-propositions",
    "value": 43,
    "unit": "ms"
  },
  {
    "name": "foundation.mere-embeddings",
    "value": 42,
    "unit": "ms"
  },
  {
    "name": "graph-theory.totally-faithful-morphisms-undirected-graphs",
    "value": 42,
    "unit": "ms"
  },
  {
    "name": "category-theory.natural-isomorphisms-functors-large-precategories",
    "value": 42,
    "unit": "ms"
  },
  {
    "name": "category-theory.large-subprecategories",
    "value": 42,
    "unit": "ms"
  },
  {
    "name": "group-theory.intersections-subgroups-abelian-groups",
    "value": 42,
    "unit": "ms"
  },
  {
    "name": "order-theory.decidable-subposets",
    "value": 42,
    "unit": "ms"
  },
  {
    "name": "group-theory.subsets-monoids",
    "value": 42,
    "unit": "ms"
  },
  {
    "name": "foundation-core.path-split-maps",
    "value": 42,
    "unit": "ms"
  },
  {
    "name": "modal-type-theory.flat-discrete-types",
    "value": 42,
    "unit": "ms"
  },
  {
    "name": "group-theory.wild-representations-monoids",
    "value": 42,
    "unit": "ms"
  },
  {
    "name": "group-theory.category-of-abelian-groups",
    "value": 42,
    "unit": "ms"
  },
  {
    "name": "foundation.decidable-relations",
    "value": 42,
    "unit": "ms"
  },
  {
    "name": "foundation.transport-along-identifications",
    "value": 42,
    "unit": "ms"
  },
  {
    "name": "group-theory.monoid-actions",
    "value": 42,
    "unit": "ms"
  },
  {
    "name": "foundation-core.1-types",
    "value": 42,
    "unit": "ms"
  },
  {
    "name": "ring-theory.central-elements-rings",
    "value": 41,
    "unit": "ms"
  },
  {
    "name": "ring-theory.intersections-ideals-semirings",
    "value": 41,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.groups-of-loops-in-1-types",
    "value": 41,
    "unit": "ms"
  },
  {
    "name": "ring-theory.nil-ideals-rings",
    "value": 41,
    "unit": "ms"
  },
  {
    "name": "order-theory.upper-bounds-large-posets",
    "value": 41,
    "unit": "ms"
  },
  {
    "name": "foundation.morphisms-spans",
    "value": 41,
    "unit": "ms"
  },
  {
    "name": "group-theory.rational-commutative-monoids",
    "value": 41,
    "unit": "ms"
  },
  {
    "name": "foundation.type-arithmetic-dependent-function-types",
    "value": 41,
    "unit": "ms"
  },
  {
    "name": "group-theory.free-concrete-group-actions",
    "value": 41,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems",
    "value": 41,
    "unit": "ms"
  },
  {
    "name": "group-theory.centers-monoids",
    "value": 41,
    "unit": "ms"
  },
  {
    "name": "order-theory.homomorphisms-large-frames",
    "value": 40,
    "unit": "ms"
  },
  {
    "name": "order-theory.decidable-subpreorders",
    "value": 40,
    "unit": "ms"
  },
  {
    "name": "group-theory.equivalences-concrete-groups",
    "value": 40,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-equivalences",
    "value": 40,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.image-of-maps",
    "value": 40,
    "unit": "ms"
  },
  {
    "name": "category-theory.essentially-injective-functors-precategories",
    "value": 40,
    "unit": "ms"
  },
  {
    "name": "order-theory.well-founded-relations",
    "value": 40,
    "unit": "ms"
  },
  {
    "name": "organic-chemistry.methane",
    "value": 40,
    "unit": "ms"
  },
  {
    "name": "foundation-core.univalence",
    "value": 40,
    "unit": "ms"
  },
  {
    "name": "order-theory.total-preorders",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "order-theory.homomorphisms-large-meet-semilattices",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "group-theory.inverse-semigroups",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "set-theory.baire-space",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "foundation.decidable-dependent-function-types",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.peano-arithmetic",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "foundation.universal-property-booleans",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "foundation.commuting-tetrahedra-of-maps",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.dependent-sequential-diagrams",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "group-theory.precategory-of-concrete-groups",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.multiples-of-elements-commutative-rings",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "foundation.subsingleton-induction",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.kolakoski-sequence",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.addition-rational-numbers",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.decidable-total-order-natural-numbers",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "group-theory.dependent-products-monoids",
    "value": 39,
    "unit": "ms"
  },
  {
    "name": "structured-types.function-h-spaces",
    "value": 38,
    "unit": "ms"
  },
  {
    "name": "order-theory.homomorphisms-large-locales",
    "value": 38,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.cubes",
    "value": 38,
    "unit": "ms"
  },
  {
    "name": "order-theory.lower-bounds-large-posets",
    "value": 38,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.equivalences",
    "value": 38,
    "unit": "ms"
  },
  {
    "name": "foundation.large-locale-of-propositions",
    "value": 38,
    "unit": "ms"
  },
  {
    "name": "ring-theory.trivial-rings",
    "value": 38,
    "unit": "ms"
  },
  {
    "name": "reflection.terms",
    "value": 38,
    "unit": "ms"
  },
  {
    "name": "structured-types.commuting-squares-of-pointed-maps",
    "value": 38,
    "unit": "ms"
  },
  {
    "name": "order-theory.decidable-preorders",
    "value": 38,
    "unit": "ms"
  },
  {
    "name": "category-theory.terminal-objects-precategories",
    "value": 38,
    "unit": "ms"
  },
  {
    "name": "group-theory.orders-of-elements-groups",
    "value": 37,
    "unit": "ms"
  },
  {
    "name": "trees.rooted-undirected-trees",
    "value": 37,
    "unit": "ms"
  },
  {
    "name": "order-theory.homomorphisms-large-suplattices",
    "value": 37,
    "unit": "ms"
  },
  {
    "name": "group-theory.torsion-elements-groups",
    "value": 37,
    "unit": "ms"
  },
  {
    "name": "foundation.unions-subtypes",
    "value": 37,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.cycle-partitions",
    "value": 37,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.poset-of-natural-numbers-ordered-by-divisibility",
    "value": 37,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.prespectra",
    "value": 37,
    "unit": "ms"
  },
  {
    "name": "group-theory.subsets-commutative-monoids",
    "value": 37,
    "unit": "ms"
  },
  {
    "name": "species.cauchy-series-species-of-types",
    "value": 37,
    "unit": "ms"
  },
  {
    "name": "graph-theory.edge-coloured-undirected-graphs",
    "value": 37,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.exponentiation-natural-numbers",
    "value": 37,
    "unit": "ms"
  },
  {
    "name": "group-theory.commuting-elements-monoids",
    "value": 37,
    "unit": "ms"
  },
  {
    "name": "order-theory.directed-families",
    "value": 37,
    "unit": "ms"
  },
  {
    "name": "foundation.type-arithmetic-booleans",
    "value": 37,
    "unit": "ms"
  },
  {
    "name": "category-theory.embedding-maps-precategories",
    "value": 36,
    "unit": "ms"
  },
  {
    "name": "group-theory.dependent-products-commutative-monoids",
    "value": 36,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.category-of-commutative-rings",
    "value": 36,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.localizations-subuniverses",
    "value": 36,
    "unit": "ms"
  },
  {
    "name": "foundation.powersets",
    "value": 36,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.bounded-sums-arithmetic-functions",
    "value": 36,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.strictly-ordered-pairs-of-natural-numbers",
    "value": 36,
    "unit": "ms"
  },
  {
    "name": "foundation.pullbacks-subtypes",
    "value": 36,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.based-induction-natural-numbers",
    "value": 36,
    "unit": "ms"
  },
  {
    "name": "higher-group-theory.higher-groups",
    "value": 35,
    "unit": "ms"
  },
  {
    "name": "category-theory.endomorphisms-in-categories",
    "value": 35,
    "unit": "ms"
  },
  {
    "name": "order-theory.dependent-products-large-posets",
    "value": 35,
    "unit": "ms"
  },
  {
    "name": "foundation.precomposition-type-families",
    "value": 35,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.equality-finite-types",
    "value": 35,
    "unit": "ms"
  },
  {
    "name": "lists.sorting-algorithms-vectors",
    "value": 35,
    "unit": "ms"
  },
  {
    "name": "graph-theory.matchings",
    "value": 35,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.injective-maps",
    "value": 35,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.localizations-maps",
    "value": 35,
    "unit": "ms"
  },
  {
    "name": "order-theory.greatest-lower-bounds-large-posets",
    "value": 34,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.acyclic-types",
    "value": 34,
    "unit": "ms"
  },
  {
    "name": "lists.sort-by-insertion-lists",
    "value": 34,
    "unit": "ms"
  },
  {
    "name": "foundation.univalence-implies-function-extensionality",
    "value": 34,
    "unit": "ms"
  },
  {
    "name": "category-theory.sieves-in-categories",
    "value": 34,
    "unit": "ms"
  },
  {
    "name": "graph-theory.complete-multipartite-graphs",
    "value": 34,
    "unit": "ms"
  },
  {
    "name": "group-theory.monomorphisms-groups",
    "value": 34,
    "unit": "ms"
  },
  {
    "name": "group-theory.centers-semigroups",
    "value": 34,
    "unit": "ms"
  },
  {
    "name": "group-theory.embeddings-groups",
    "value": 34,
    "unit": "ms"
  },
  {
    "name": "ring-theory.category-of-rings",
    "value": 34,
    "unit": "ms"
  },
  {
    "name": "foundation-core.families-of-equivalences",
    "value": 33,
    "unit": "ms"
  },
  {
    "name": "category-theory.endomorphisms-in-precategories",
    "value": 33,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.wide-function-classes",
    "value": 33,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.equivalences-standard-finite-types",
    "value": 33,
    "unit": "ms"
  },
  {
    "name": "group-theory.function-commutative-monoids",
    "value": 33,
    "unit": "ms"
  },
  {
    "name": "ring-theory.central-elements-semirings",
    "value": 33,
    "unit": "ms"
  },
  {
    "name": "structured-types.finite-multiplication-magmas",
    "value": 33,
    "unit": "ms"
  },
  {
    "name": "species.exponentials-cauchy-series-of-types",
    "value": 33,
    "unit": "ms"
  },
  {
    "name": "group-theory.surjective-group-homomorphisms",
    "value": 33,
    "unit": "ms"
  },
  {
    "name": "order-theory.maximal-chains-preorders",
    "value": 33,
    "unit": "ms"
  },
  {
    "name": "order-theory.maximal-chains-posets",
    "value": 33,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.0-acyclic-maps",
    "value": 33,
    "unit": "ms"
  },
  {
    "name": "group-theory.embeddings-abelian-groups",
    "value": 33,
    "unit": "ms"
  },
  {
    "name": "foundation.propositions",
    "value": 33,
    "unit": "ms"
  },
  {
    "name": "foundation.induction-principle-propositional-truncation",
    "value": 32,
    "unit": "ms"
  },
  {
    "name": "group-theory.function-monoids",
    "value": 32,
    "unit": "ms"
  },
  {
    "name": "graph-theory.embeddings-directed-graphs",
    "value": 32,
    "unit": "ms"
  },
  {
    "name": "group-theory.trivial-groups",
    "value": 32,
    "unit": "ms"
  },
  {
    "name": "foundation.copartial-functions",
    "value": 32,
    "unit": "ms"
  },
  {
    "name": "foundation.action-on-equivalences-functions-out-of-subuniverses",
    "value": 32,
    "unit": "ms"
  },
  {
    "name": "group-theory.epimorphisms-groups",
    "value": 32,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.local-families-of-types",
    "value": 32,
    "unit": "ms"
  },
  {
    "name": "foundation.functoriality-sequential-limits",
    "value": 32,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.factorials",
    "value": 32,
    "unit": "ms"
  },
  {
    "name": "group-theory.cartesian-products-semigroups",
    "value": 32,
    "unit": "ms"
  },
  {
    "name": "foundation.intersections-subtypes",
    "value": 31,
    "unit": "ms"
  },
  {
    "name": "order-theory.dependent-products-large-preorders",
    "value": 31,
    "unit": "ms"
  },
  {
    "name": "species.coproducts-species-of-types",
    "value": 31,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.ramsey-theory",
    "value": 31,
    "unit": "ms"
  },
  {
    "name": "universal-algebra.homomorphisms-of-algebras",
    "value": 31,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.natural-numbers",
    "value": 31,
    "unit": "ms"
  },
  {
    "name": "foundation.subterminal-types",
    "value": 31,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.divisibility-modular-arithmetic",
    "value": 31,
    "unit": "ms"
  },
  {
    "name": "order-theory.top-elements-posets",
    "value": 30,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.descent-circle-constant-families",
    "value": 30,
    "unit": "ms"
  },
  {
    "name": "group-theory.precategory-of-monoids",
    "value": 30,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.double-counting",
    "value": 30,
    "unit": "ms"
  },
  {
    "name": "graph-theory.simple-undirected-graphs",
    "value": 30,
    "unit": "ms"
  },
  {
    "name": "order-theory.finite-coverings-locales",
    "value": 30,
    "unit": "ms"
  },
  {
    "name": "foundation.constant-type-families",
    "value": 30,
    "unit": "ms"
  },
  {
    "name": "foundation.copartial-elements",
    "value": 30,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.nonzero-integers",
    "value": 30,
    "unit": "ms"
  },
  {
    "name": "ring-theory.local-rings",
    "value": 30,
    "unit": "ms"
  },
  {
    "name": "order-theory.bottom-elements-posets",
    "value": 30,
    "unit": "ms"
  },
  {
    "name": "foundation.complements-subtypes",
    "value": 30,
    "unit": "ms"
  },
  {
    "name": "group-theory.central-elements-semigroups",
    "value": 30,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.zariski-topology",
    "value": 29,
    "unit": "ms"
  },
  {
    "name": "order-theory.inhabited-finite-total-orders",
    "value": 29,
    "unit": "ms"
  },
  {
    "name": "structured-types.cyclic-types",
    "value": 29,
    "unit": "ms"
  },
  {
    "name": "foundation.truncation-levels",
    "value": 29,
    "unit": "ms"
  },
  {
    "name": "higher-group-theory.subgroups-higher-groups",
    "value": 29,
    "unit": "ms"
  },
  {
    "name": "foundation.whiskering-higher-homotopies-composition",
    "value": 29,
    "unit": "ms"
  },
  {
    "name": "group-theory.characteristic-subgroups",
    "value": 29,
    "unit": "ms"
  },
  {
    "name": "group-theory.mere-equivalences-concrete-group-actions",
    "value": 29,
    "unit": "ms"
  },
  {
    "name": "organic-chemistry.saturated-carbons",
    "value": 29,
    "unit": "ms"
  },
  {
    "name": "universal-algebra.signatures",
    "value": 29,
    "unit": "ms"
  },
  {
    "name": "foundation.structure",
    "value": 29,
    "unit": "ms"
  },
  {
    "name": "group-theory.large-semigroups",
    "value": 29,
    "unit": "ms"
  },
  {
    "name": "structured-types",
    "value": 29,
    "unit": "ms"
  },
  {
    "name": "foundation.descent-empty-types",
    "value": 29,
    "unit": "ms"
  },
  {
    "name": "foundation.endomorphisms",
    "value": 28,
    "unit": "ms"
  },
  {
    "name": "foundation.small-maps",
    "value": 28,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.legendre-symbol",
    "value": 28,
    "unit": "ms"
  },
  {
    "name": "foundation.negation",
    "value": 28,
    "unit": "ms"
  },
  {
    "name": "trees.elementhood-relation-coalgebras-polynomial-endofunctors",
    "value": 28,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.0-acyclic-types",
    "value": 28,
    "unit": "ms"
  },
  {
    "name": "graph-theory.reflecting-maps-undirected-graphs",
    "value": 28,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.mere-lifting-properties",
    "value": 28,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.local-commutative-rings",
    "value": 28,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.isotopies-latin-squares",
    "value": 28,
    "unit": "ms"
  },
  {
    "name": "group-theory.trivial-group-homomorphisms",
    "value": 28,
    "unit": "ms"
  },
  {
    "name": "foundation.morphisms-binary-relations",
    "value": 27,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.squares-modular-arithmetic",
    "value": 27,
    "unit": "ms"
  },
  {
    "name": "foundation.cantors-diagonal-argument",
    "value": 27,
    "unit": "ms"
  },
  {
    "name": "foundation.projective-types",
    "value": 27,
    "unit": "ms"
  },
  {
    "name": "group-theory.surjective-semigroup-homomorphisms",
    "value": 27,
    "unit": "ms"
  },
  {
    "name": "structured-types.magmas",
    "value": 27,
    "unit": "ms"
  },
  {
    "name": "foundation.dependent-homotopies",
    "value": 27,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.dedekind-finite-sets",
    "value": 27,
    "unit": "ms"
  },
  {
    "name": "order-theory.reflective-galois-connections-large-posets",
    "value": 27,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.lifting-operations",
    "value": 26,
    "unit": "ms"
  },
  {
    "name": "group-theory.conjugation-concrete-groups",
    "value": 26,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.standard-cyclic-groups",
    "value": 26,
    "unit": "ms"
  },
  {
    "name": "graph-theory",
    "value": 26,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.counting-maybe",
    "value": 26,
    "unit": "ms"
  },
  {
    "name": "trees.bounded-multisets",
    "value": 26,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.trivial-commutative-rings",
    "value": 26,
    "unit": "ms"
  },
  {
    "name": "category-theory.equivalences-of-precategories",
    "value": 26,
    "unit": "ms"
  },
  {
    "name": "foundation.small-types",
    "value": 26,
    "unit": "ms"
  },
  {
    "name": "foundation.inverse-sequential-diagrams",
    "value": 26,
    "unit": "ms"
  },
  {
    "name": "category-theory.representable-functors-categories",
    "value": 26,
    "unit": "ms"
  },
  {
    "name": "category-theory.rigid-objects-precategories",
    "value": 26,
    "unit": "ms"
  },
  {
    "name": "structured-types.wild-quasigroups",
    "value": 26,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.latin-squares",
    "value": 26,
    "unit": "ms"
  },
  {
    "name": "group-theory.opposite-groups",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "species.hasse-weil-species",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "group-theory.dependent-products-semigroups",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.petri-nets",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "graph-theory.paths-undirected-graphs",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "group-theory.precategory-of-commutative-monoids",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.standard-finite-trees",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "foundation.multisubsets",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "order-theory.similarity-of-order-preserving-maps-large-preorders",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "group-theory.transitive-group-actions",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "order-theory.lower-types-preorders",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "foundation.iterating-involutions",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "graph-theory.geometric-realizations-undirected-graphs",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "ring-theory.invariant-basis-property-rings",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.powers-of-elements-commutative-semirings",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.taxicab-numbers",
    "value": 25,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.multiplication-lists-of-natural-numbers",
    "value": 24,
    "unit": "ms"
  },
  {
    "name": "species.equivalences-species-of-types-in-subuniverses",
    "value": 24,
    "unit": "ms"
  },
  {
    "name": "structured-types.noncoherent-h-spaces",
    "value": 24,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.dirichlet-convolution",
    "value": 24,
    "unit": "ms"
  },
  {
    "name": "graph-theory.stereoisomerism-enriched-undirected-graphs",
    "value": 24,
    "unit": "ms"
  },
  {
    "name": "category-theory.discrete-categories",
    "value": 24,
    "unit": "ms"
  },
  {
    "name": "foundation.binary-equivalences",
    "value": 24,
    "unit": "ms"
  },
  {
    "name": "trees.elementhood-relation-w-types",
    "value": 24,
    "unit": "ms"
  },
  {
    "name": "group-theory.precategory-of-groups",
    "value": 24,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.nilradicals-commutative-semirings",
    "value": 24,
    "unit": "ms"
  },
  {
    "name": "category-theory.rigid-objects-categories",
    "value": 24,
    "unit": "ms"
  },
  {
    "name": "structured-types.faithful-pointed-maps",
    "value": 23,
    "unit": "ms"
  },
  {
    "name": "group-theory.trivial-subgroups",
    "value": 23,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory",
    "value": 23,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.suspensions-of-pointed-types",
    "value": 23,
    "unit": "ms"
  },
  {
    "name": "group-theory.products-of-tuples-of-elements-commutative-monoids",
    "value": 23,
    "unit": "ms"
  },
  {
    "name": "ring-theory.idempotent-elements-rings",
    "value": 23,
    "unit": "ms"
  },
  {
    "name": "group-theory.trivial-concrete-groups",
    "value": 23,
    "unit": "ms"
  },
  {
    "name": "foundation.partial-functions",
    "value": 23,
    "unit": "ms"
  },
  {
    "name": "foundation.lawveres-fixed-point-theorem",
    "value": 23,
    "unit": "ms"
  },
  {
    "name": "group-theory.products-of-elements-monoids",
    "value": 23,
    "unit": "ms"
  },
  {
    "name": "linear-algebra.diagonal-matrices-on-rings",
    "value": 23,
    "unit": "ms"
  },
  {
    "name": "group-theory.monomorphisms-concrete-groups",
    "value": 23,
    "unit": "ms"
  },
  {
    "name": "order-theory.well-founded-orders",
    "value": 23,
    "unit": "ms"
  },
  {
    "name": "foundation.morphisms-twisted-arrows",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "group-theory.subsets-abelian-groups",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.orientations-cubes",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "higher-group-theory.conjugation",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "ring-theory.radical-ideals-rings",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "structured-types.pointed-unit-type",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "group-theory.function-semigroups",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "foundation-core.commuting-squares-of-homotopies",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "foundation.composite-maps-in-inverse-sequential-diagrams",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.steiner-systems",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "structured-types.pointed-dependent-functions",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "foundation.cospans",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "trees.lower-types-w-types",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "species.precategory-of-finite-species",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "species.cartesian-products-species-of-types",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "group-theory.precategory-of-semigroups",
    "value": 22,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.binomial-coefficients",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "foundation.double-negation-modality",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "graph-theory.eulerian-circuits-undirected-graphs",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "group-theory.concrete-monoids",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "order-theory.coverings-locales",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "foundation.standard-apartness-relations",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.group-of-integers",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "foundation.noncontractible-types",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "graph-theory.vertex-covers",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "category-theory.essential-fibers-of-functors-precategories",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "foundation.hilberts-epsilon-operators",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.small-types",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "group-theory.subsets-groups",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "foundation.multivariable-sections",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "foundation.effective-maps-equivalence-relations",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "ring-theory.opposite-rings",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "foundation-core.endomorphisms",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "foundation.cartesian-product-types",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.quotients-finite-types",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.inequality-integer-fractions",
    "value": 21,
    "unit": "ms"
  },
  {
    "name": "universal-algebra.models-of-signatures",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "group-theory.orbit-stabilizer-theorem-concrete-groups",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "group-theory.elements-of-finite-order-groups",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.jacobi-symbol",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "foundation.dependent-binary-homotopies",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "foundation.kernel-span-diagrams-of-maps",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "group-theory.central-elements-monoids",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "higher-group-theory.trivial-higher-groups",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.spheres",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "higher-group-theory.cyclic-higher-groups",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "graph-theory.mere-equivalences-undirected-graphs",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "group-theory.shriek-concrete-group-actions",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.ordinal-induction-natural-numbers",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "order-theory.commuting-squares-of-order-preserving-maps-large-posets",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "group-theory.perfect-subgroups",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "graph-theory.trails-directed-graphs",
    "value": 20,
    "unit": "ms"
  },
  {
    "name": "structured-types.sets-equipped-with-automorphisms",
    "value": 19,
    "unit": "ms"
  },
  {
    "name": "trees.empty-multisets",
    "value": 19,
    "unit": "ms"
  },
  {
    "name": "foundation.dependent-function-types",
    "value": 19,
    "unit": "ms"
  },
  {
    "name": "foundation.morphisms-cospans",
    "value": 19,
    "unit": "ms"
  },
  {
    "name": "foundation.global-choice",
    "value": 19,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.cd-structures",
    "value": 19,
    "unit": "ms"
  },
  {
    "name": "group-theory.exponents-groups",
    "value": 19,
    "unit": "ms"
  },
  {
    "name": "foundation.separated-types",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.collatz-bijection",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "foundation.lesser-limited-principle-of-omniscience",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "order-theory.directed-complete-posets",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.maps-of-prespectra",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "group-theory.opposite-semigroups",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "species.equivalences-species-of-types",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "order-theory.lower-sets-large-posets",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "species.unlabeled-structures-species",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "foundation.automorphisms",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.involution-standard-finite-types",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "trees.submultisets",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "category-theory.equivalences-of-large-precategories",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "foundation.law-of-excluded-middle",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.main-classes-of-latin-squares",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "group-theory.commuting-squares-of-group-homomorphisms",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "graph-theory.voltage-graphs",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "species",
    "value": 18,
    "unit": "ms"
  },
  {
    "name": "order-theory.top-elements-preorders",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "reflection.boolean-reflection",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "finite-algebra",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.suspension-prespectra",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.relatively-prime-integers",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.identity-modality",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "foundation.dependent-epimorphisms-with-respect-to-truncated-types",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "structured-types.types-equipped-with-automorphisms",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "species.species-of-types",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.hardy-ramanujan-number",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.alternating-groups",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.powers-integers",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "graph-theory.regular-undirected-graphs",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "group-theory.concrete-group-actions",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "group-theory.mere-equivalences-group-actions",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "foundation.replacement",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "foundation.discrete-reflexive-relations",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "foundation.weakly-constant-maps",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "group-theory.furstenberg-groups",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "organic-chemistry.alkenes",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "order-theory.locally-finite-posets",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "higher-group-theory.higher-group-actions",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "category-theory.commuting-squares-of-morphisms-in-large-precategories",
    "value": 17,
    "unit": "ms"
  },
  {
    "name": "order-theory.top-elements-large-posets",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "foundation.dubuc-penon-compact-types",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "modal-type-theory.sharp-codiscrete-maps",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "ring-theory.free-rings-with-one-generator",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "structured-types.wild-semigroups",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.commutative-semiring-of-natural-numbers",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "foundation.product-decompositions",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.raise-modalities",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "order-theory.bottom-elements-preorders",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "order-theory.precategory-of-total-orders",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "trees.multisets",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "online-encyclopedia-of-integer-sequences.oeis",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.finite-connected-components",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "order-theory.precategory-of-decidable-total-orders",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.mere-spheres",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.inequality-rational-numbers",
    "value": 16,
    "unit": "ms"
  },
  {
    "name": "reflection.fixity",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.multiplication-rational-numbers",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "reflection.metavariables",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "structured-types.involutive-types",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "foundation.set-presented-types",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "type-theories",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "foundation.families-of-equivalences",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "foundation.sigma-closed-subuniverses",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "order-theory.precategory-of-inhabited-finite-total-orders",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "order-theory.ideals-preorders",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "finite-group-theory.alternating-concrete-groups",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "lists",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "group-theory.principal-group-actions",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "order-theory.precategory-of-finite-posets",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "ring-theory.characteristics-rings",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.catalan-numbers",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "order-theory.precategory-of-finite-total-orders",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.half-integers",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "foundation.operations-spans-families-of-types",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "structured-types.morphisms-magmas",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "foundation.limited-principle-of-omniscience",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "group-theory.e8-lattice",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "organic-chemistry.alkynes",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "group-theory.sheargroups",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.decidable-total-order-standard-finite-types",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "foundation.preidempotent-maps",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "category-theory.equivalences-of-categories",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "trees.coalgebra-of-enriched-directed-trees",
    "value": 15,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.collatz-conjecture",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.nonzero-natural-numbers",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "lists.predicates-on-lists",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "foundation.uniqueness-truncation",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "set-theory.infinite-sets",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "species.dirichlet-series-species-of-finite-inhabited-types",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.lower-bounds-natural-numbers",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "foundation.permutations-spans-families-of-types",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "group-theory.exponents-abelian-groups",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "species.dirichlet-series-species-of-types-in-subuniverses",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "foundation.weak-limited-principle-of-omniscience",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "trees.coalgebras-polynomial-endofunctors",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "graph-theory.connected-undirected-graphs",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "structured-types.fibers-of-pointed-maps",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.infinite-complex-projective-space",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "order-theory.interval-subposets",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.sequential-diagrams",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "category-theory.commuting-squares-of-morphisms-in-set-magmoids",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "foundation-core.precomposition-dependent-functions",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "foundation.identity-truncated-types",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "foundation.constant-span-diagrams",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "order-theory.upper-sets-large-posets",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.double-lifts-families-of-elements",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "foundation.principle-of-omniscience",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.morphisms-descent-data-circle",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "group-theory.normal-subgroups-concrete-groups",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "group-theory.perfect-cores",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "foundation.truncation-modalities",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.goldbach-conjecture",
    "value": 14,
    "unit": "ms"
  },
  {
    "name": "foundation.multivariable-decidable-relations",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "modal-type-theory.crisp-identity-types",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.locally-small-modal-operators",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "trees.planar-binary-trees",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "graph-theory.orientations-undirected-graphs",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "group-theory.perfect-groups",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.products-of-natural-numbers",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.eulers-totient-function",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "foundation.total-partial-functions",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "foundation.spans-families-of-types",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "set-theory.uncountable-sets",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "foundation.span-diagrams-families-of-types",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "foundation.binary-equivalences-unordered-pairs-of-types",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "group-theory.stabilizer-groups",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "foundation.partial-elements",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "foundation.bands",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.sequentially-compact-types",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "linear-algebra.functoriality-matrices",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "ring-theory.generating-elements-rings",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "foundation.dependent-epimorphisms",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "group-theory.orbits-group-actions",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "species.unit-cauchy-composition-species-of-types-in-subuniverses",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.zero-modality",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "primitives.floats",
    "value": 13,
    "unit": "ms"
  },
  {
    "name": "trees.algebras-polynomial-endofunctors",
    "value": 12,
    "unit": "ms"
  },
  {
    "name": "reflection.names",
    "value": 12,
    "unit": "ms"
  },
  {
    "name": "foundation.multivariable-relations",
    "value": 12,
    "unit": "ms"
  },
  {
    "name": "reflection.literals",
    "value": 12,
    "unit": "ms"
  },
  {
    "name": "higher-group-theory.symmetric-higher-groups",
    "value": 12,
    "unit": "ms"
  },
  {
    "name": "linear-algebra",
    "value": 12,
    "unit": "ms"
  },
  {
    "name": "structured-types.pointed-sections",
    "value": 12,
    "unit": "ms"
  },
  {
    "name": "group-theory.orbits-concrete-group-actions",
    "value": 12,
    "unit": "ms"
  },
  {
    "name": "trees.coalgebra-of-directed-trees",
    "value": 12,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.separated-types",
    "value": 12,
    "unit": "ms"
  },
  {
    "name": "foundation.products-binary-relations",
    "value": 12,
    "unit": "ms"
  },
  {
    "name": "ring-theory.division-rings",
    "value": 12,
    "unit": "ms"
  },
  {
    "name": "modal-type-theory.crisp-law-of-excluded-middle",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "trees.rooted-quasitrees",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "set-theory.cantor-space",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "structured-types.constant-maps-pointed-types",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "structured-types.cartesian-products-types-equipped-with-endomorphisms",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "modal-type-theory.flat-dependent-function-types",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "foundation.0-images-of-maps",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "group-theory.generating-sets-groups",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.upper-bounds-natural-numbers",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "species.cauchy-products-species-of-types",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.mersenne-primes",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "foundation.partial-sequences",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.monoid-of-natural-numbers-with-addition",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "structured-types.contractible-pointed-types",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "foundation-core.discrete-types",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "graph-theory.hypergraphs",
    "value": 11,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.cellular-maps",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "primitives.strings",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "foundation.transposition-span-diagrams",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "foundation.cospan-diagrams",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "reflection",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "commutative-algebra.boolean-rings",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "higher-group-theory",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "synthetic-homotopy-theory.join-powers-of-types",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "foundation.reflexive-relations",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.cubes-natural-numbers",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "univalent-combinatorics.maybe",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "category-theory.commuting-squares-of-morphisms-in-precategories",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "foundation.strongly-extensional-maps",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "group-theory.unordered-tuples-of-elements-commutative-monoids",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "structured-types.central-h-spaces",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "group-theory.dihedral-groups",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "foundation.terminal-spans-families-of-types",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "structured-types.types-equipped-with-endomorphisms",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "elementary-number-theory.multiplicative-monoid-of-natural-numbers",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "species.dirichlet-products-species-of-types",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "foundation.propositional-resizing",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "foundation.injective-maps",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "species.cycle-index-series-species-of-types",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "structured-types.iterated-pointed-cartesian-product-types",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "graph-theory.directed-graph-structures-on-standard-finite-sets",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "structured-types.symmetric-h-spaces",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "foundation.2-types",
    "value": 10,
    "unit": "ms"
  },
  {
    "name": "orthogonal-factorization-systems.sigma-closed-modalities",
    "value": 10,
    "unit": "ms"
  }
]

@VojtechStep
Copy link
Collaborator

Would you be available to assist me a little with this tomorrow @VojtechStep?

Sure 👍

Copy link
Collaborator

@VojtechStep VojtechStep left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, though the job will fail until we set the proper NETLIFY_SITE_ID and NETLIFY_AUTH_TOKEN deployment secrets

@fredrik-bakke fredrik-bakke enabled auto-merge (squash) February 22, 2024 17:01
@fredrik-bakke fredrik-bakke merged commit 071533a into UniMath:master Feb 22, 2024
4 checks passed
fredrik-bakke pushed a commit that referenced this pull request Feb 22, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Record performance statistics for type-checking
2 participants