time-of-build-both.log

After    | File Name                                                                                        | Before   || Change   
-----------------------------------------------------------------------------------------------------------------------------------
3m20.88s | Total                                                                                            | 3m17.92s || +0m02.96s
-----------------------------------------------------------------------------------------------------------------------------------
0m18.30s | [notation-overridden,parsing]
theories/Spaces/BAut/Bool                                          | 0m18.39s || -0m00.08s
0m12.34s | [notation-overridden,parsing]
theories/Algebra/ooGroup                                           | 0m11.77s || +0m00.57s
0m07.99s | [notation-overridden,parsing]
theories/Modalities/ReflectiveSubuniverse                          | 0m07.75s || +0m00.24s
0m07.33s | [notation-overridden,parsing]
theories/Spaces/Finite                                             | 0m07.04s || +0m00.29s
0m06.67s | [notation-overridden,parsing]
theories/Idempotents                                               | 0m06.02s || +0m00.65s
0m06.40s | [notation-overridden,parsing]
theories/Spaces/BAut                                               | 0m06.27s || +0m00.13s
0m06.34s | [notation-overridden,parsing]
theories/Categories/Adjoint/Pointwise                              | 0m06.48s || -0m00.14s
0m05.93s | [notation-overridden,parsing]
contrib/Freudenthal                                                | 0m05.87s || +0m00.05s
0m05.91s | [notation-overridden,parsing]
theories/Categories/Category/Sigma/Univalent                       | 0m05.79s || +0m00.12s
0m05.57s | [notation-overridden,parsing]
theories/Spaces/No                                                 | 0m05.36s || +0m00.20s
0m04.65s | [notation-overridden,parsing]
theories/Categories/ExponentialLaws/Law2/Law                       | 0m04.57s || +0m00.08s
0m04.52s | [notation-overridden,parsing]
theories/Categories/Adjoint/Functorial/Laws                        | 0m04.62s || -0m00.10s
0m04.19s | [notation-overridden,parsing]
theories/Modalities/Lex                                            | 0m04.12s || +0m00.07s
0m04.00s | [notation-overridden,parsing]
theories/Categories/ExponentialLaws/Law3/Law                       | 0m03.96s || +0m00.04s
0m03.68s | [notation-overridden,parsing]
theories/Pointed                                                   | 0m03.47s || +0m00.20s
0m03.20s | [notation-overridden,parsing]
theories/HIT/V                                                     | 0m03.06s || +0m00.14s
0m03.06s | [notation-overridden,parsing]
theories/Categories/ExponentialLaws/Law4/Law                       | 0m03.29s || -0m00.23s
0m02.80s | [notation-overridden,parsing]
theories/HIT/Spheres                                               | 0m02.62s || +0m00.17s
0m02.50s | [notation-overridden,parsing]
theories/Modalities/Modality                                       | 0m02.24s || +0m00.25s
0m02.39s | [notation-overridden,parsing]
theories/Categories/LaxComma/CoreLaws                              | 0m02.48s || -0m00.08s
0m02.35s | [notation-overridden,parsing]
theories/Categories/Category/Paths                                 | 0m02.40s || -0m00.04s
0m02.17s | [notation-overridden,parsing]
theories/HIT/FreeIntQuotient                                       | 0m02.07s || +0m00.10s
0m02.10s | [notation-overridden,parsing]
theories/HIT/Coeq                                                  | 0m02.08s || +0m00.02s
0m02.02s | [notation-overridden,parsing]
theories/Spaces/BAut/Cantor                                        | 0m01.96s || +0m00.06s
0m01.90s | [notation-overridden,parsing]
theories/Categories/Comma/ProjectionFunctors                       | 0m01.91s || -0m00.01s
0m01.86s | [notation-overridden,parsing]
theories/HIT/Suspension                                            | 0m01.85s || +0m00.01s
0m01.85s | [notation-overridden,parsing]
theories/Factorization                                             | 0m01.76s || +0m00.09s
0m01.67s | [notation-overridden,parsing]
contrib/HoTTBookExercises                                          | 0m01.66s || +0m00.01s
0m01.65s | [notation-overridden,parsing]
theories/Spaces/BAut/Bool/IncoherentIdempotent                     | 0m01.64s || +0m00.01s
0m01.64s | [non-primitive-record,record]
theories/Types/Universe                                            | 0m01.53s || +0m00.10s
0m01.52s | [notation-overridden,parsing]
theories/Comodalities/CoreflectiveSubuniverse                      | 0m01.52s || +0m00.00s
0m01.51s | [notation-overridden,parsing]
theories/HIT/Connectedness                                         | 0m01.41s || +0m00.10s
0m01.42s | [notation-overridden,parsing]
theories/Categories/Comma/Functorial                               | 0m01.46s || -0m00.04s
0m01.41s | [notation-overridden,parsing]
theories/Modalities/Fracture                                       | 0m01.42s || -0m00.01s
0m01.20s | [notation-overridden,parsing]
theories/Tactics/EquivalenceInduction                              | 0m01.11s || +0m00.08s
0m01.18s | [notation-overridden,parsing]
contrib/HoTTBook                                                   | 0m01.21s || -0m00.03s
0m01.17s | [notation-overridden,parsing]
theories/HIT/Truncations                                           | 0m01.11s || +0m00.05s
0m01.16s | [notation-overridden,parsing]
theories/Types/Sigma                                               | 0m01.22s || -0m00.06s
0m01.16s | [notation-overridden,parsing]
theories/Categories/GroupoidCategory/Morphisms                     | 0m01.23s || -0m00.07s
0m01.04s | [notation-overridden,parsing]
theories/Types/Sum                                                 | 0m00.88s || +0m00.16s
0m01.01s | [notation-overridden,parsing]
theories/Categories/Category/Morphisms                             | 0m01.05s || -0m00.04s
0m01.00s | [notation-overridden,parsing]
theories/HIT/epi                                                   | 0m00.88s || +0m00.12s
0m00.97s | [notation-overridden,parsing]
theories/Categories/Grothendieck/ToSet/Morphisms                   | 0m01.04s || -0m00.07s
0m00.92s | [notation-overridden,parsing]
theories/Categories/ExponentialLaws/Law1/Law                       | 0m00.86s || +0m00.06s
0m00.90s | [notation-overridden,parsing]
theories/Algebra/Aut                                               | 0m00.86s || +0m00.04s
0m00.76s | [notation-overridden,parsing]
theories/Categories/Grothendieck/ToSet/Univalent                   | 0m00.72s || +0m00.04s
0m00.76s | [notation-overridden,parsing]
theories/Categories/Adjoint/Composition/AssociativityLaw           | 0m00.72s || +0m00.04s
0m00.75s | [notation-overridden,parsing]
theories/HIT/Flattening                                            | 0m00.74s || +0m00.01s
0m00.74s | [notation-overridden,parsing]
theories/Modalities/Localization                                   | 0m00.72s || +0m00.02s
0m00.73s | [notation-overridden,parsing]
theories/Modalities/Open                                           | 0m00.75s || -0m00.02s
0m00.72s | [notation-overridden,parsing]
theories/Modalities/Accessible                                     | 0m00.68s || +0m00.03s
0m00.72s | [notation-overridden,parsing]
theories/Modalities/Closed                                         | 0m00.66s || +0m00.05s
0m00.72s | [notation-overridden,parsing]
theories/Basics/PathGroupoids                                      | 0m00.74s || -0m00.02s
0m00.72s | [notation-overridden,parsing]
theories/Modalities/Topological                                    | 0m00.71s || +0m00.01s
0m00.71s | [notation-overridden,parsing]
theories/Categories/Functor/Composition/Functorial/Attributes      | 0m00.73s || -0m00.02s
0m00.68s | [notation-overridden,parsing]
theories/HIT/quotient                                              | 0m00.70s || -0m00.01s
0m00.67s | [notation-overridden,parsing]
theories/Categories/Grothendieck/PseudofunctorToCat                | 0m00.67s || +0m00.00s
0m00.66s | [meta-collision,ltac]
theories/Categories/Functor/Sum                                            | 0m00.67s || -0m00.01s
0m00.65s | [notation-overridden,parsing]
theories/Constant                                                  | 0m00.53s || +0m00.12s
0m00.65s | [notation-overridden,parsing]
theories/Categories/Functor/Paths                                  | 0m00.66s || -0m00.01s
0m00.64s | [notation-overridden,parsing]
theories/Categories/ExponentialLaws/Law4/Functors                  | 0m00.64s || +0m00.00s
0m00.62s | [notation-overridden,parsing]
theories/DProp                                                     | 0m00.64s || -0m00.02s
0m00.59s | [notation-overridden,parsing]
theories/Categories/Pseudofunctor/RewriteLaws                      | 0m00.57s || +0m00.02s
0m00.58s | [notation-overridden,parsing]
theories/Categories/Adjoint/HomCoercions                           | 0m00.60s || -0m00.02s
0m00.55s | [notation-overridden,parsing]
theories/Tests                                                     | 0m00.58s || -0m00.02s
0m00.53s | [notation-overridden,parsing]
theories/HIT/TwoSphere                                             | 0m00.52s || +0m00.01s
0m00.51s | [notation-overridden,parsing]
theories/HoTT                                                      | 0m00.52s || -0m00.01s
0m00.51s | [notation-overridden,parsing]
theories/EquivalenceVarieties                                      | 0m00.47s || +0m00.04s
0m00.50s | [notation-overridden,parsing]
theories/Categories/Functor/Composition/Laws                       | 0m00.54s || -0m00.04s
0m00.50s | [notation-overridden,parsing]
theories/Categories/Adjoint/Composition/IdentityLaws               | 0m00.53s || -0m00.03s
0m00.48s | [notation-overridden,parsing]
theories/Types/Paths                                               | 0m00.43s || +0m00.04s
0m00.47s | [notation-overridden,parsing]
theories/Categories/LaxComma/Core                                  | 0m00.42s || +0m00.04s
0m00.46s | [notation-overridden,parsing]
theories/Categories/Pseudofunctor/Identity                         | 0m00.44s || +0m00.02s
0m00.46s | [notation-overridden,parsing]
theories/Categories/Pseudofunctor/FromFunctor                      | 0m00.48s || -0m00.01s
0m00.44s | [notation-overridden,parsing]
theories/Categories/Yoneda                                         | 0m00.45s || -0m00.01s
0m00.44s | [notation-overridden,parsing]
theories/Categories/Comma/InducedFunctors                          | 0m00.46s || -0m00.02s
0m00.44s | [notation-overridden,parsing]
theories/TruncType                                                 | 0m00.42s || +0m00.02s
0m00.43s | [notation-overridden,parsing]
theories/Categories/Adjoint/Composition/Core                       | 0m00.38s || +0m00.04s
0m00.43s | [notation-overridden,parsing]
theories/Categories/ChainCategory                                  | 0m00.48s || -0m00.04s
0m00.42s | [notation-overridden,parsing]
theories/Categories/UniversalProperties                            | 0m00.43s || -0m00.01s
0m00.41s | [notation-overridden,parsing]
theories/Categories/Category/Sigma/OnMorphisms                     | 0m00.39s || +0m00.01s
0m00.40s | [notation-overridden,parsing]
theories/Categories/Comma/Dual                                     | 0m00.46s || -0m00.06s
0m00.40s | [notation-overridden,parsing]
theories/Types/Equiv                                               | 0m00.37s || +0m00.03s
0m00.38s | [notation-overridden,parsing]
theories/HIT/Pushout                                               | 0m00.34s || +0m00.03s
0m00.38s | [notation-overridden,parsing]
theories/Categories/Functor/Pointwise/Properties                   | 0m00.42s || -0m00.03s
0m00.37s | [notation-overridden,parsing]
theories/Basics/Equivalences                                       | 0m00.39s || -0m00.02s
0m00.36s | [notation-overridden,parsing]
theories/Modalities/Nullification                                  | 0m00.33s || +0m00.02s
0m00.36s | [notation-overridden,parsing]
theories/Types/Prod                                                | 0m00.36s || +0m00.00s
0m00.36s | [notation-overridden,parsing]
theories/Categories/Comma/Core                                     | 0m00.43s || -0m00.07s
0m00.36s | [notation-overridden,parsing]
theories/Categories                                                | 0m00.40s || -0m00.04s
0m00.35s | [notation-overridden,parsing]
theories/HIT/Circle                                                | 0m00.30s || +0m00.04s
0m00.33s | [notation-overridden,parsing]
theories/Categories/LaxComma/CoreParts                             | 0m00.37s || -0m00.03s
0m00.32s | [notation-overridden,parsing]
theories/Categories/Adjoint/UnitCounitCoercions                    | 0m00.36s || -0m00.03s
0m00.31s | [notation-overridden,parsing]
theories/Categories/Functor/Attributes                             | 0m00.28s || +0m00.02s
0m00.30s | [notation-overridden,parsing]
theories/Categories/ExponentialLaws/Law0                           | 0m00.35s || -0m00.04s
0m00.30s | [notation-overridden,parsing]
theories/Categories/Functor/Prod/Universal                         | 0m00.28s || +0m00.01s
0m00.30s | [notation-overridden,parsing]
theories/Categories/SemiSimplicialSets                             | 0m00.28s || +0m00.01s
0m00.30s | [notation-overridden,parsing]
theories/Categories/ProductLaws                                    | 0m00.29s || +0m00.01s
0m00.29s | [notation-overridden,parsing]
theories/Categories/ExponentialLaws/Law1/Functors                  | 0m00.25s || +0m00.03s
0m00.29s | [notation-overridden,parsing]
theories/Categories/Adjoint/Paths                                  | 0m00.28s || +0m00.00s
0m00.27s | [notation-overridden,parsing]
theories/Categories/Adjoint/UniversalMorphisms/Core                | 0m00.36s || -0m00.08s
0m00.26s | [notation-overridden,parsing]
theories/Categories/InitialTerminalCategory/Pseudofunctors         | 0m00.26s || +0m00.00s
0m00.26s | [notation-overridden,parsing]
theories/Extensions                                                | 0m00.30s || -0m00.03s
0m00.25s | [notation-overridden,parsing]
theories/Categories/SetCategory/Morphisms                          | 0m00.25s || +0m00.00s
0m00.25s | [notation-overridden,parsing]
theories/Modalities/Identity                                       | 0m00.24s || +0m00.01s
0m00.24s | [notation-overridden,parsing]
theories/Categories/NaturalTransformation/Isomorphisms             | 0m00.23s || +0m00.00s
0m00.24s | [notation-overridden,parsing]
theories/Categories/SimplicialSets                                 | 0m00.24s || +0m00.00s
0m00.24s | [notation-overridden,parsing]
theories/Types/Wtype                                               | 0m00.18s || +0m00.06s
0m00.24s | [notation-overridden,parsing]
theories/Categories/Category/Sum                                   | 0m00.23s || +0m00.00s
0m00.23s | [notation-overridden,parsing]
theories/Categories/Structure/IdentityPrinciple                    | 0m00.23s || +0m00.00s
0m00.22s | [notation-overridden,parsing]
theories/HIT/Join                                                  | 0m00.19s || +0m00.03s
0m00.22s | [notation-overridden,parsing]
theories/Fibrations                                                | 0m00.24s || -0m00.01s
0m00.22s | [notation-overridden,parsing]
theories/Categories/FundamentalPreGroupoidCategory                 | 0m00.24s || -0m00.01s
0m00.22s | [notation-overridden,parsing]
theories/Categories/GroupoidCategory/Dual                          | 0m00.24s || -0m00.01s
0m00.21s | [notation-overridden,parsing]
theories/Categories/Category/Sigma/Core                            | 0m00.24s || -0m00.03s
0m00.21s | [notation-overridden,parsing]
theories/Pullback                                                  | 0m00.21s || +0m00.00s
0m00.21s | [notation-overridden,parsing]
theories/Categories/Adjoint/Functorial/Core                        | 0m00.25s || -0m00.04s
0m00.20s | [notation-overridden,parsing]
theories/Categories/DualFunctor                                    | 0m00.27s || -0m00.07s
0m00.20s | [notation-overridden,parsing]
theories/Spaces/Nat                                                | 0m00.18s || +0m00.02s
0m00.20s | [notation-overridden,parsing]
theories/Categories/NaturalTransformation/Paths                    | 0m00.19s || +0m00.01s
0m00.19s | [notation-overridden,parsing]
theories/Categories/HomotopyPreCategory                            | 0m00.24s || -0m00.04s
0m00.18s | [notation-overridden,parsing]
theories/Categories/Notations                                      | 0m00.20s || -0m00.02s
0m00.18s | [notation-overridden,parsing]
theories/Categories/Limits/Core                                    | 0m00.18s || +0m00.00s
0m00.18s | [notation-overridden,parsing]
theories/Spaces/Int                                                | 0m00.15s || +0m00.03s
0m00.18s | [notation-overridden,parsing]
theories/Categories/Utf8                                           | 0m00.18s || +0m00.00s
0m00.17s | [notation-overridden,parsing]
theories/Types/Forall                                              | 0m00.18s || -0m00.00s
0m00.17s | [notation-overridden,parsing]
theories/ObjectClassifier                                          | 0m00.16s || +0m00.01s
0m00.17s | [notation-overridden,parsing]
theories/Categories/Grothendieck/ToSet/Core                        | 0m00.16s || +0m00.01s
0m00.16s | [notation-overridden,parsing]
theories/Spectra/Coinductive                                       | 0m00.16s || +0m00.00s
0m00.16s | [notation-overridden,parsing]
theories/HIT/TruncImpliesFunext                                    | 0m00.16s || +0m00.00s
0m00.16s | Categories/NaturalTransformation/Utf8                                                            | 0m00.18s || -0m00.01s
0m00.16s | [notation-overridden,parsing]
theories/Categories/Functor/Pointwise/Core                         | 0m00.13s || +0m00.03s
0m00.15s | [notation-overridden,parsing]
theories/Categories/InitialTerminalCategory/Functors               | 0m00.16s || -0m00.01s
0m00.15s | Categories/Functor/Notations                                                                     | 0m00.14s || +0m00.00s
0m00.15s | Categories/Functor/Utf8                                                                          | 0m00.14s || +0m00.00s
0m00.15s | [notation-overridden,parsing]
theories/Modalities/Notnot                                         | 0m00.13s || +0m00.01s
0m00.15s | [notation-overridden,parsing]
theories/HIT/iso                                                   | 0m00.15s || +0m00.00s
0m00.15s | Categories/Functor                                                                               | 0m00.17s || -0m00.02s
0m00.15s | [notation-overridden,parsing]
theories/HProp                                                     | 0m00.12s || +0m00.03s
0m00.14s | [notation-overridden,parsing]
theories/Spectra/Spectrum                                          | 0m00.15s || -0m00.00s
0m00.14s | [notation-overridden,parsing]
theories/Categories/NaturalTransformation/Composition/Laws         | 0m00.15s || -0m00.00s
0m00.14s | [notation-overridden,parsing]
theories/Categories/Adjoint/Functorial/Parts                       | 0m00.15s || -0m00.00s
0m00.14s | Categories/Functor/Composition/Functorial                                                        | 0m00.15s || -0m00.00s
0m00.14s | [notation-overridden,parsing]
theories/Algebra/ooAction                                          | 0m00.12s || +0m00.02s
0m00.14s | [notation-overridden,parsing]
theories/Categories/Functor/Prod/Core                              | 0m00.12s || +0m00.02s
0m00.14s | [notation-overridden,parsing]
theories/Categories/Functor/Composition/Functorial/Core            | 0m00.15s || -0m00.00s
0m00.14s | Categories/FunctorCategory/Utf8                                                                  | 0m00.17s || -0m00.03s
0m00.14s | [notation-overridden,parsing]
theories/Categories/ExponentialLaws/Law2/Functors                  | 0m00.12s || +0m00.02s
0m00.14s | [notation-overridden,parsing]
theories/Categories/NaturalTransformation/Pointwise                | 0m00.10s || +0m00.04s
0m00.13s | [notation-overridden,parsing]
theories/Categories/PseudonaturalTransformation/Core               | 0m00.14s || -0m00.01s
0m00.13s | [notation-overridden,parsing]
theories/Categories/Limits/Functors                                | 0m00.12s || +0m00.01s
0m00.13s | [notation-overridden,parsing]
theories/Categories/FunctorCategory/Morphisms                      | 0m00.15s || -0m00.01s
0m00.13s | Categories/Functor/Composition                                                                   | 0m00.15s || -0m00.01s
0m00.12s | [notation-overridden,parsing]
theories/HIT/unique_choice                                         | 0m00.13s || -0m00.01s
0m00.12s | [notation-overridden,parsing]
theories/HSet                                                      | 0m00.12s || +0m00.00s
0m00.12s | [notation-overridden,parsing]
theories/Categories/FunctorCategory/Functorial                     | 0m00.09s || +0m00.03s
0m00.12s | [notation-overridden,parsing]
theories/Types/Arrow                                               | 0m00.12s || +0m00.00s
0m00.12s | [notation-overridden,parsing]
theories/Categories/Pseudofunctor/Core                             | 0m00.18s || -0m00.06s
0m00.12s | [notation-overridden,parsing]
theories/Categories/Adjoint/Hom                                    | 0m00.08s || +0m00.03s
0m00.12s | [notation-overridden,parsing]
theories/Categories/NaturalTransformation/Prod                     | 0m00.11s || +0m00.00s
0m00.12s | [notation-overridden,parsing]
theories/Utf8                                                      | 0m00.14s || -0m00.02s
0m00.12s | [notation-overridden,parsing]
theories/Tactics/RewriteModuloAssociativity                        | 0m00.10s || +0m00.01s
0m00.11s | [notation-overridden,parsing]
theories/Categories/Category/Sigma/OnObjects                       | 0m00.12s || -0m00.00s
0m00.11s | [notation-overridden,parsing]
theories/Basics/Overture                                           | 0m00.11s || +0m00.00s
0m00.11s | [notation-overridden,parsing]
theories/UnivalenceImpliesFunext                                   | 0m00.14s || -0m00.03s
0m00.11s | [notation-overridden,parsing]
theories/Categories/Functor/Prod/Functorial                        | 0m00.14s || -0m00.03s
0m00.11s | [notation-overridden,parsing]
theories/Categories/IndiscreteCategory                             | 0m00.11s || +0m00.00s
0m00.11s | [notation-overridden,parsing]
theories/EquivGroupoids                                            | 0m00.14s || -0m00.03s
0m00.11s | [notation-overridden,parsing]
theories/Categories/Comma/Projection                               | 0m00.10s || +0m00.00s
0m00.11s | [notation-overridden,parsing]
theories/Categories/Structure/Core                                 | 0m00.12s || -0m00.00s
0m00.11s | [notation-overridden,parsing]
theories/Categories/CategoryOfSections/Core                        | 0m00.13s || -0m00.02s
0m00.10s | [notation-overridden,parsing]
theories/Basics/Decidable                                          | 0m00.08s || +0m00.02s
0m00.10s | [notation-overridden,parsing]
theories/Tactics                                                   | 0m00.09s || +0m00.01s
0m00.10s | [notation-overridden,parsing]
theories/Categories/FunctorCategory/Dual                           | 0m00.12s || -0m00.01s
0m00.10s | [notation-overridden,parsing]
theories/Types/Bool                                                | 0m00.10s || +0m00.00s
0m00.10s | [notation-overridden,parsing]
theories/Categories/HomFunctor                                     | 0m00.11s || -0m00.00s
0m00.10s | [notation-overridden,parsing]
theories/Categories/Category/Prod                                  | 0m00.09s || +0m00.01s
0m00.10s | [notation-overridden,parsing]
theories/Categories/KanExtensions/Functors                         | 0m00.12s || -0m00.01s
0m00.09s | [notation-overridden,parsing]
theories/Categories/Category/Objects                               | 0m00.07s || +0m00.01s
0m00.09s | [notation-overridden,parsing]
theories/Categories/Adjoint/UnitCounit                             | 0m00.11s || -0m00.02s
0m00.09s | [notation-overridden,parsing]
theories/Categories/ExponentialLaws/Law3/Functors                  | 0m00.08s || +0m00.00s
0m00.09s | [notation-overridden,parsing]
theories/Categories/NatCategory                                    | 0m00.10s || -0m00.01s
0m00.09s | [notation-overridden,parsing]
theories/Categories/LaxComma                                       | 0m00.10s || -0m00.01s
0m00.08s | Categories/Adjoint                                                                               | 0m00.10s || -0m00.02s
0m00.08s | [notation-overridden,parsing]
theories/Categories/LaxComma/Utf8                                  | 0m00.06s || +0m00.02s
0m00.08s | coq/Init/Peano                                                                                   | 0m00.05s || +0m00.03s
0m00.08s | [notation-overridden,parsing]
theories/Categories/NaturalTransformation/Composition/Core         | 0m00.07s || +0m00.00s
0m00.08s | [notation-overridden,parsing]
theories/Categories/NaturalTransformation/Sum                      | 0m00.08s || +0m00.00s
0m00.08s | Categories/Adjoint/Composition                                                                   | 0m00.04s || +0m00.04s
0m00.08s | [notation-overridden,parsing]
theories/Categories/Cat/Core                                       | 0m00.12s || -0m00.03s
0m00.08s | [notation-overridden,parsing]
theories/Basics/Contractible                                       | 0m00.06s || +0m00.02s
0m00.08s | [notation-overridden,parsing]
theories/Functorish                                                | 0m00.08s || +0m00.00s
0m00.08s | [notation-overridden,parsing]
theories/Categories/LaxComma/Notations                             | 0m00.07s || +0m00.00s
0m00.08s | [notation-overridden,parsing]
theories/Categories/Cat/Morphisms                                  | 0m00.07s || +0m00.00s
0m00.08s | [notation-overridden,parsing]
theories/Basics/UniverseLevel                                      | 0m00.11s || -0m00.03s
0m00.08s | [notation-overridden,parsing]
theories/Basics/Trunc                                              | 0m00.07s || +0m00.00s
0m00.07s | Categories/Cat                                                                                   | 0m00.05s || +0m00.02s
0m00.07s | [notation-overridden,parsing]
theories/Categories/NaturalTransformation/Identity                 | 0m00.07s || +0m00.00s
0m00.07s | [notation-overridden,parsing]
theories/Categories/InitialTerminalCategory/NaturalTransformations | 0m00.08s || -0m00.00s
0m00.07s | [notation-overridden,parsing]
theories/Categories/KanExtensions/Core                             | 0m00.08s || -0m00.00s
0m00.07s | Categories/Grothendieck                                                                          | 0m00.07s || +0m00.00s
0m00.07s | [notation-overridden,parsing]
theories/Categories/SetCategory/Functors/SetProp                   | 0m00.06s || +0m00.01s
0m00.07s | [notation-overridden,parsing]
theories/Types/Record                                              | 0m00.07s || +0m00.00s
0m00.07s | Categories/Pseudofunctor                                                                         | 0m00.07s || +0m00.00s
0m00.07s | [notation-overridden,parsing]
theories/Categories/Grothendieck/ToCat                             | 0m00.06s || +0m00.01s
0m00.07s | [notation-overridden,parsing]
theories/Categories/NaturalTransformation/Composition/Functorial   | 0m00.08s || -0m00.00s
0m00.07s | Categories/Limits                                                                                | 0m00.06s || +0m00.01s
0m00.06s | Categories/KanExtensions                                                                         | 0m00.07s || -0m00.01s
0m00.06s | [notation-overridden,parsing]
theories/Categories/Profunctor/Identity                            | 0m00.05s || +0m00.00s
0m00.06s | [notation-overridden,parsing]
theories/Categories/Category                                       | 0m00.08s || -0m00.02s
0m00.06s | [notation-overridden,parsing]
theories/HIT/Interval                                              | 0m00.04s || +0m00.01s
0m00.06s | [notation-overridden,parsing]
theories/Conjugation                                               | 0m00.06s || +0m00.00s
0m00.06s | Categories/Functor/Prod                                                                          | 0m00.05s || +0m00.00s
0m00.06s | [notation-overridden,parsing]
theories/Categories/Adjoint/Composition/LawsTactic                 | 0m00.07s || -0m00.01s
0m00.06s | [notation-overridden,parsing]
theories/Categories/Comma/Utf8                                     | 0m00.04s || +0m00.01s
0m00.06s | Categories/Adjoint/Notations                                                                     | 0m00.06s || +0m00.00s
0m00.06s | [notation-overridden,parsing]
theories/Categories/Category/Utf8                                  | 0m00.06s || +0m00.00s
0m00.06s | [notation-overridden,parsing]
theories/Types/Unit                                                | 0m00.06s || +0m00.00s
0m00.06s | Categories/FunctorCategory                                                                       | 0m00.05s || +0m00.00s
0m00.06s | Categories/InitialTerminalCategory/Notations                                                     | 0m00.06s || +0m00.00s
0m00.06s | [notation-overridden,parsing]
theories/Categories/Adjoint/Dual                                   | 0m00.05s || +0m00.00s
0m00.06s | [notation-overridden,parsing]
theories/Basics/FunextVarieties                                    | 0m00.06s || +0m00.00s
0m00.06s | [notation-overridden,parsing]
theories/Categories/Comma                                          | 0m00.10s || -0m00.04s
0m00.06s | Categories/Profunctor/Notations                                                                  | 0m00.05s || +0m00.00s
0m00.06s | Categories/FunctorCategory/Notations                                                             | 0m00.04s || +0m00.01s
0m00.06s | [notation-overridden,parsing]
theories/Categories/Category/Pi                                    | 0m00.06s || +0m00.00s
0m00.06s | [notation-overridden,parsing]
theories/Categories/DependentProduct                               | 0m00.07s || -0m00.01s
0m00.06s | [notation-overridden,parsing]
theories/Categories/GroupoidCategory/Core                          | 0m00.10s || -0m00.04s
0m00.06s | Categories/Adjoint/UniversalMorphisms                                                            | 0m00.06s || +0m00.00s
0m00.06s | [notation-overridden,parsing]
theories/Categories/FunctorCategory/Core                           | 0m00.06s || +0m00.00s
0m00.06s | [notation-overridden,parsing]
theories/Categories/Category/Univalent                             | 0m00.04s || +0m00.01s
0m00.06s | [notation-overridden,parsing]
theories/Categories/Profunctor/Core                                | 0m00.05s || +0m00.00s
0m00.06s | [notation-overridden,parsing]
theories/Categories/Functor/Dual                                   | 0m00.05s || +0m00.00s
0m00.05s | Categories/Adjoint/Core                                                                          | 0m00.05s || +0m00.00s
0m00.05s | [notation-overridden,parsing]
theories/Categories/NaturalTransformation/Core                     | 0m00.04s || +0m00.01s
0m00.05s | Categories/Functor/Pointwise                                                                     | 0m00.06s || -0m00.00s
0m00.05s | Categories/Category/Sigma                                                                        | 0m00.06s || -0m00.00s
0m00.05s | [notation-overridden,parsing]
theories/Categories/Category/Dual                                  | 0m00.06s || -0m00.00s
0m00.05s | Categories/Profunctor                                                                            | 0m00.08s || -0m00.03s
0m00.05s | Categories/NaturalTransformation/Composition                                                     | 0m00.04s || +0m00.01s
0m00.05s | [notation-overridden,parsing]
theories/Categories/DiscreteCategory                               | 0m00.06s || -0m00.00s
0m00.05s | Categories/Grothendieck/ToSet                                                                    | 0m00.04s || +0m00.01s
0m00.05s | Categories/Category/Notations                                                                    | 0m00.06s || -0m00.00s
0m00.05s | [notation-overridden,parsing]
theories/Categories/ExponentialLaws/Tactics                        | 0m00.08s || -0m00.03s
0m00.05s | [non-primitive-record,record]
theories/Categories/InitialTerminalCategory/Core                   | 0m00.06s || -0m00.00s
0m00.05s | [notation-overridden,parsing]
theories/Categories/Profunctor/Representable                       | 0m00.06s || -0m00.00s
0m00.05s | Categories/NaturalTransformation                                                                 | 0m00.06s || -0m00.00s
0m00.05s | Types                                                                                            | 0m00.04s || +0m00.01s
0m00.05s | Categories/ExponentialLaws                                                                       | 0m00.07s || -0m00.02s
0m00.05s | Categories/InitialTerminalCategory                                                               | 0m00.05s || +0m00.00s
0m00.05s | Categories/CategoryOfSections                                                                    | 0m00.04s || +0m00.01s
0m00.05s | Categories/GroupoidCategory                                                                      | 0m00.05s || +0m00.00s
0m00.05s | [notation-overridden,parsing]
theories/Categories/SetCategory/Core                               | 0m00.06s || -0m00.00s
0m00.05s | Categories/Category/Subcategory/Wide                                                             | 0m00.04s || +0m00.01s
0m00.05s | [notation-overridden,parsing]
theories/Spaces/Cantor                                             | 0m00.06s || -0m00.00s
0m00.05s | Categories/Structure                                                                             | 0m00.05s || +0m00.00s
0m00.05s | Categories/SetCategory                                                                           | 0m00.04s || +0m00.01s
0m00.05s | [notation-overridden,parsing]
theories/Categories/CategoryOfGroupoids                            | 0m00.10s || -0m00.05s
0m00.05s | Categories/ExponentialLaws/Law3                                                                  | 0m00.06s || -0m00.00s
0m00.05s | Categories/ExponentialLaws/Law2                                                                  | 0m00.04s || +0m00.01s
0m00.05s | Categories/SetCategory/Functors                                                                  | 0m00.03s || +0m00.02s
0m00.04s | Categories/Adjoint/Functorial                                                                    | 0m00.06s || -0m00.01s
0m00.04s | [notation-overridden,parsing]
theories/Categories/Adjoint/Identity                               | 0m00.06s || -0m00.01s
0m00.04s | Categories/PseudonaturalTransformation                                                           | 0m00.06s || -0m00.01s
0m00.04s | Categories/Adjoint/Utf8                                                                          | 0m00.05s || -0m00.01s
0m00.04s | Categories/Category/Subcategory                                                                  | 0m00.02s || +0m00.02s
0m00.04s | [notation-overridden,parsing]
theories/Types/Empty                                               | 0m00.03s || +0m00.01s
0m00.04s | Categories/Category/Subcategory/Full                                                             | 0m00.05s || -0m00.01s
0m00.04s | Categories/Structure/Utf8                                                                        | 0m00.04s || +0m00.00s
0m00.04s | [notation-overridden,parsing]
theories/Misc                                                      | 0m00.04s || +0m00.00s
0m00.04s | [notation-overridden,parsing]
theories/Tactics/EvalIn                                            | 0m00.02s || +0m00.02s
0m00.04s | [notation-overridden,parsing]
theories/Categories/Category/Core                                  | 0m00.04s || +0m00.00s
0m00.04s | [notation-overridden,parsing]
theories/Categories/NaturalTransformation/Dual                     | 0m00.05s || -0m00.01s
0m00.04s | [notation-overridden,parsing]
theories/Tactics/BinderApply                                       | 0m00.04s || +0m00.00s
0m00.04s | Categories/NaturalTransformation/Notations                                                       | 0m00.05s || -0m00.01s
0m00.04s | [notation-overridden,parsing]
theories/Categories/Comma/Notations                                | 0m00.05s || -0m00.01s
0m00.04s | coq/Init/Logic_Type                                                                              | 0m00.04s || +0m00.00s
0m00.04s | [notation-overridden,parsing]
theories/HIT/IntervalImpliesFunext                                 | 0m00.04s || +0m00.00s
0m00.04s | Categories/Profunctor/Utf8                                                                       | 0m00.06s || -0m00.01s
0m00.04s | Categories/ExponentialLaws/Law1                                                                  | 0m00.06s || -0m00.01s
0m00.04s | Categories/ExponentialLaws/Law4                                                                  | 0m00.05s || -0m00.01s
0m00.03s | UnivalenceAxiom                                                                                  | 0m00.04s || -0m00.01s
0m00.03s | Categories/Structure/Notations                                                                   | 0m00.04s || -0m00.01s
0m00.03s | [notation-overridden,parsing]
theories/NullHomotopy                                              | 0m00.05s || -0m00.02s
0m00.03s | Categories/Functor/Core                                                                          | 0m00.03s || +0m00.00s
0m00.03s | [notation-overridden,parsing]
theories/Categories/Functor/Composition/Core                       | 0m00.03s || +0m00.00s
0m00.03s | coq/Program/Tactics                                                                              | 0m00.02s || +0m00.00s
0m00.02s | coq/Init/Notations                                                                               | 0m00.01s || +0m00.01s
0m00.02s | [notation-overridden,parsing]
theories/Categories/Category/Strict                                | 0m00.03s || -0m00.00s
0m00.02s | [notation-overridden,parsing]
theories/Categories/Functor/Identity                               | 0m00.01s || +0m00.01s
0m00.02s | [notation-overridden,parsing]
theories/Basics                                                    | 0m00.03s || -0m00.00s
0m00.02s | coq/Init/Specif                                                                                  | 0m00.02s || +0m00.00s
0m00.02s | coq/Unicode/Utf8_core                                                                            | 0m00.01s || +0m00.01s
0m00.02s | coq/Init/Prelude                                                                                 | 0m00.02s || +0m00.00s
0m00.02s | Basics/Notations                                                                                 | 0m00.01s || +0m00.01s
0m00.02s | coq/Unicode/Utf8                                                                                 | 0m00.01s || +0m00.01s
0m00.01s | coq/Init/Logic                                                                                   | 0m00.00s || +0m00.01s
0m00.01s | [notation-overridden,parsing]
theories/FunextAxiom                                               | 0m00.02s || -0m00.01s
0m00.01s | coq/Init/Datatypes                                                                               | 0m00.03s || -0m00.01s
0m00.01s | coq/Bool/Bool                                                                                    | 0m00.01s || +0m00.00s
0m00.01s | coq/Init/Tactics                                                                                 | 0m00.01s || +0m00.00s