Work around apply/auto bug

They can't tell that eta-expanded primitive projections are the same as
non-eta-expanded ones.  See also
https://coq.inria.fr/bugs/show_bug.cgi?id=3592.
Work around [generalize] not working up to eta
Work around [rewrite idtoiso_comp] caring about η
Work around [rewrite] caring about projection eta
Make PreCategory a primitive record

We get a pretty hefty speedup in adjunction proofs, and a nice speedup
overall.

After    | File Name                                                          | Before   || Change
-----------------------------------------------------------------------------------------------------
3m25.54s | Total                                                              | 4m05.36s || -0m39.81s
-----------------------------------------------------------------------------------------------------
0m01.53s | categories/Adjoint/Dual                                            | 0m08.58s || -0m07.04s
0m00.47s | categories/Adjoint/UnitCounit                                      | 0m05.78s || -0m05.31s
0m02.15s | categories/FunctorCategory/Dual                                    | 0m06.73s || -0m04.58s
0m13.89s | categories/LaxComma/CoreLaws                                       | 0m16.45s || -0m02.55s
0m07.66s | categories/Comma/ProjectionFunctors                                | 0m09.76s || -0m02.09s
0m29.22s | categories/ExponentialLaws/Law4/Law                                | 0m31.08s || -0m01.85s
0m20.16s | categories/ExponentialLaws/Law3/Law                                | 0m21.70s || -0m01.53s
0m15.88s | categories/ExponentialLaws/Law2/Law                                | 0m17.08s || -0m01.19s
0m09.00s | categories/Comma/Functorial                                        | 0m10.96s || -0m01.96s
0m05.77s | categories/Adjoint/Composition/AssociativityLaw                    | 0m06.86s || -0m01.09s
0m00.52s | categories/Adjoint/UniversalMorphisms                              | 0m02.23s || -0m01.71s
0m07.02s | hit/V                                                              | 0m07.03s || -0m00.01s
0m03.75s | categories/Pseudofunctor/RewriteLaws                               | 0m03.82s || -0m00.06s
0m03.54s | categories/ExponentialLaws/Law4/Functors                           | 0m04.29s || -0m00.75s
0m03.49s | categories/Grothendieck/PseudofunctorToCat                         | 0m03.48s || +0m00.01s
0m03.15s | categories/GroupoidCategory/Morphisms                              | 0m02.90s || +0m00.25s
0m02.84s | hit/Flattening                                                     | 0m02.84s || +0m00.00s
0m02.21s | categories/Adjoint/HomCoercions                                    | 0m02.48s || -0m00.27s
0m01.83s | categories/Pseudofunctor/Identity                                  | 0m01.94s || -0m00.10s
0m01.82s | categories/Adjoint/Composition/IdentityLaws                        | 0m02.42s || -0m00.59s
0m01.81s | categories/LaxComma/CoreParts                                      | 0m02.04s || -0m00.23s
0m01.72s | categories/Adjoint/Composition/Core                                | 0m02.01s || -0m00.28s
0m01.72s | categories/Comma/Dual                                              | 0m02.15s || -0m00.42s
0m01.72s | categories/Category/Morphisms                                      | 0m02.41s || -0m00.69s
0m01.64s | categories/Comma/InducedFunctors                                   | 0m02.21s || -0m00.57s
0m01.62s | categories/Functor/Pointwise/Properties                            | 0m01.66s || -0m00.03s
0m01.45s | categories/Adjoint/UnitCounitCoercions                             | 0m01.50s || -0m00.05s
0m01.44s | categories/Pseudofunctor/FromFunctor                               | 0m01.80s || -0m00.36s
0m01.43s | hit/epi                                                            | 0m01.45s || -0m00.02s
0m01.36s | categories/ExponentialLaws/Law1/Law                                | 0m01.53s || -0m00.16s
0m01.21s | categories/Yoneda                                                  | 0m01.51s || -0m00.30s
0m01.09s | HProp                                                              | 0m01.06s || +0m00.03s
0m01.07s | HSet                                                               | 0m01.09s || -0m00.02s
0m01.03s | categories/UniversalProperties                                     | 0m01.16s || -0m00.12s
0m01.00s | categories/PseudonaturalTransformation/Core                        | 0m01.02s || -0m00.02s
0m00.99s | Equivalences                                                       | 0m00.99s || +0m00.00s
0m00.94s | ReflectiveSubuniverse                                              | 0m00.89s || +0m00.04s
0m00.94s | categories/Functor/Sum                                             | 0m01.25s || -0m00.31s
0m00.88s | PathGroupoids                                                      | 0m00.93s || -0m00.05s
0m00.83s | categories/Structure/IdentityPrinciple                             | 0m01.03s || -0m00.20s
0m00.80s | contrib/HoTTBook                                                   | 0m00.79s || +0m00.01s
0m00.80s | categories/Category/Sigma/OnMorphisms                              | 0m00.96s || -0m00.15s
0m00.77s | categories/ProductLaws                                             | 0m00.92s || -0m00.15s
0m00.77s | categories/LaxComma/Core                                           | 0m01.13s || -0m00.35s
0m00.74s | hit/Connectedness                                                  | 0m00.70s || +0m00.04s
0m00.74s | categories/Functor/Paths                                           | 0m00.77s || -0m00.03s
0m00.72s | categories/Functor/Prod/Universal                                  | 0m00.81s || -0m00.09s
0m00.72s | types/Sigma                                                        | 0m00.79s || -0m00.07s
0m00.71s | categories/Limits/Core                                             | 0m00.79s || -0m00.08s
0m00.71s | categories/Functor/Attributes                                      | 0m00.78s || -0m00.07s
0m00.70s | categories/Functor/Composition/Functorial/Core                     | 0m00.77s || -0m00.07s
0m00.66s | categories/Category/Sum                                            | 0m00.89s || -0m00.23s
0m00.62s | EquivalenceVarieties                                               | 0m00.54s || +0m00.07s
0m00.62s | categories/Comma/Core                                              | 0m00.71s || -0m00.08s
0m00.60s | categories/Functor/Composition/Functorial/Attributes               | 0m00.76s || -0m00.16s
0m00.58s | categories/NaturalTransformation/Isomorphisms                      | 0m00.62s || -0m00.04s
0m00.57s | categories/ExponentialLaws/Law0                                    | 0m00.55s || +0m00.01s
0m00.52s | categories/InitialTerminalCategory/Pseudofunctors                  | 0m00.60s || -0m00.07s
0m00.52s | hit/Spheres                                                        | 0m00.55s || -0m00.03s
0m00.52s | categories/DualFunctor                                             | 0m00.54s || -0m00.02s
0m00.48s | contrib/HoTTBookExercises                                          | 0m00.49s || -0m00.01s
0m00.46s | types/Paths                                                        | 0m00.54s || -0m00.08s
0m00.46s | categories/Functor/Prod/Functorial                                 | 0m00.48s || -0m00.01s
0m00.45s | hit/quotient                                                       | 0m00.42s || +0m00.03s
0m00.43s | categories/ExponentialLaws/Law2/Functors                           | 0m00.44s || -0m00.01s
0m00.42s | categories/Functor/Pointwise                                       | 0m00.49s || -0m00.07s
0m00.41s | types/Prod                                                         | 0m00.34s || +0m00.06s
0m00.41s | categories/ExponentialLaws/Law1/Functors                           | 0m00.47s || -0m00.06s
0m00.40s | categories/Adjoint/Paths                                           | 0m00.42s || -0m00.01s
0m00.40s | categories/categories                                              | 0m00.37s || +0m00.03s
0m00.39s | categories/FunctorCategory/Morphisms                               | 0m00.49s || -0m00.09s
0m00.38s | categories/SetCategory/Morphisms                                   | 0m00.50s || -0m00.12s
0m00.37s | categories/NaturalTransformation/Pointwise                         | 0m00.38s || -0m00.01s
0m00.36s | categories/Limits/Functors                                         | 0m00.36s || +0m00.00s
0m00.32s | types/Sum                                                          | 0m00.31s || +0m00.01s
0m00.32s | categories/NaturalTransformation/Prod                              | 0m00.35s || -0m00.02s
0m00.32s | categories/Pseudofunctor/Core                                      | 0m00.36s || -0m00.03s
0m00.32s | hit/Circle                                                         | 0m00.34s || -0m00.02s
0m00.31s | types/Universe                                                     | 0m00.37s || -0m00.06s
0m00.31s | categories/Functor/Prod                                            | 0m00.49s || -0m00.18s
0m00.31s | categories/Structure/Core                                          | 0m00.30s || +0m00.01s
0m00.30s | categories/Category/Sigma/Core                                     | 0m00.28s || +0m00.01s
0m00.30s | categories/NaturalTransformation/Composition/Laws                  | 0m00.32s || -0m00.02s
0m00.30s | categories/NaturalTransformation/Dual                              | 0m00.48s || -0m00.18s
0m00.29s | categories/Grothendieck/ToSet                                      | 0m00.27s || +0m00.01s
0m00.27s | categories/KanExtensions/Functors                                  | 0m00.27s || +0m00.00s
0m00.26s | categories/NaturalTransformation/Paths                             | 0m00.28s || -0m00.02s
0m00.26s | categories/InitialTerminalCategory/Functors                        | 0m00.25s || +0m00.01s
0m00.26s | categories/Comma/Projection                                        | 0m00.34s || -0m00.08s
0m00.25s | categories/HomFunctor                                              | 0m00.32s || -0m00.07s
0m00.25s | types/Forall                                                       | 0m00.27s || -0m00.02s
0m00.24s | Trunc                                                              | 0m00.26s || -0m00.02s
0m00.24s | categories/FunctorCategory/Functorial                              | 0m00.22s || +0m00.01s
0m00.24s | Tactics                                                            | 0m00.26s || -0m00.02s
0m00.24s | hit/Pushout                                                        | 0m00.19s || +0m00.04s
0m00.24s | categories/KanExtensions/Core                                      | 0m00.28s || -0m00.04s
0m00.23s | categories/Category/Sigma/OnObjects                                | 0m00.29s || -0m00.05s
0m00.23s | categories/CategoryOfSections/Core                                 | 0m00.25s || -0m00.01s
0m00.22s | categories/NaturalTransformation/Sum                               | 0m00.22s || +0m00.00s
0m00.22s | hit/Suspension                                                     | 0m00.22s || +0m00.00s
0m00.22s | Modality                                                           | 0m00.26s || -0m00.04s
0m00.22s | hit/minus1Trunc                                                    | 0m00.21s || +0m00.01s
0m00.22s | types/ObjectClassifier                                             | 0m00.25s || -0m00.03s
0m00.22s | categories/Functor/Composition/Laws                                | 0m00.22s || +0m00.00s
0m00.21s | categories/HomotopyPreCategory                                     | 0m00.18s || +0m00.03s
0m00.20s | categories/InitialTerminalCategory/NaturalTransformations          | 0m00.18s || +0m00.02s
0m00.20s | categories/IndiscreteCategory                                      | 0m00.27s || -0m00.07s
0m00.20s | categories/Utf8                                                    | 0m00.20s || +0m00.00s
0m00.20s | categories/Notations                                               | 0m00.22s || -0m00.01s
0m00.20s | categories/Functor/Functor                                         | 0m00.18s || +0m00.02s
0m00.20s | categories/Grothendieck/Grothendieck                               | 0m00.18s || +0m00.02s
0m00.19s | categories/Cat/Core                                                | 0m00.23s || -0m00.04s
0m00.19s | categories/FundamentalPreGroupoidCategory                          | 0m00.20s || -0m00.01s
0m00.19s | UnivalenceImpliesFunext                                            | 0m00.19s || +0m00.00s
0m00.19s | HoTT                                                               | 0m00.16s || +0m00.03s
0m00.19s | categories/Category/Prod                                           | 0m00.28s || -0m00.09s
0m00.19s | categories/Adjoint/Hom                                             | 0m00.21s || -0m00.01s
0m00.19s | categories/Comma/Comma                                             | 0m00.18s || +0m00.01s
0m00.19s | types/Arrow                                                        | 0m00.22s || -0m00.03s
0m00.18s | categories/ExponentialLaws/Law3/Functors                           | 0m00.25s || -0m00.07s
0m00.18s | categories/Functor/Dual                                            | 0m00.20s || -0m00.02s
0m00.18s | categories/Functor/Notations                                       | 0m00.12s || +0m00.06s
0m00.18s | categories/Adjoint/Adjoint                                         | 0m00.21s || -0m00.03s
0m00.18s | categories/LaxComma/LaxComma                                       | 0m00.16s || +0m00.01s
0m00.18s | types/Bool                                                         | 0m00.19s || -0m00.01s
0m00.17s | categories/ExponentialLaws/ExponentialLaws                         | 0m00.16s || +0m00.01s
0m00.17s | categories/LaxComma/Utf8                                           | 0m00.17s || +0m00.00s
0m00.17s | Fibrations                                                         | 0m00.20s || -0m00.03s
0m00.17s | categories/NaturalTransformation/Composition/Core                  | 0m00.23s || -0m00.06s
0m00.16s | categories/Functor/Composition/Functorial                          | 0m00.18s || -0m00.01s
0m00.16s | categories/LaxComma/Notations                                      | 0m00.17s || -0m00.01s
0m00.16s | categories/NaturalTransformation/NaturalTransformation             | 0m00.15s || +0m00.01s
0m00.16s | Functorish                                                         | 0m00.14s || +0m00.01s
0m00.16s | categories/Adjoint/Notations                                       | 0m00.11s || +0m00.05s
0m00.16s | categories/NaturalTransformation/Core                              | 0m00.16s || +0m00.00s
0m00.16s | categories/Functor/Utf8                                            | 0m00.16s || +0m00.00s
0m00.16s | categories/NaturalTransformation/Identity                          | 0m00.18s || -0m00.01s
0m00.16s | categories/Cat/Morphisms                                           | 0m00.17s || -0m00.01s
0m00.15s | categories/FunctorCategory/Utf8                                    | 0m00.15s || +0m00.00s
0m00.15s | categories/Functor/Composition/Composition                         | 0m00.24s || -0m00.09s
0m00.15s | categories/Grothendieck/ToCat                                      | 0m00.15s || +0m00.00s
0m00.15s | categories/InitialTerminalCategory/Core                            | 0m00.13s || +0m00.01s
0m00.15s | categories/FunctorCategory/FunctorCategory                         | 0m00.12s || +0m00.03s
0m00.15s | categories/NaturalTransformation/Composition/Functorial            | 0m00.19s || -0m00.04s
0m00.15s | Overture                                                           | 0m00.16s || -0m00.01s
0m00.14s | categories/Cat/Cat                                                 | 0m00.14s || +0m00.00s
0m00.14s | categories/SetCategory/Functors/Functors                           | 0m00.13s || +0m00.01s
0m00.14s | FunextVarieties                                                    | 0m00.12s || +0m00.02s
0m00.14s | Tests                                                              | 0m00.15s || -0m00.00s
0m00.14s | categories/FunctorCategory/Notations                               | 0m00.12s || +0m00.02s
0m00.13s | categories/Profunctor/Representable                                | 0m00.16s || -0m00.03s
0m00.13s | categories/DependentProduct                                        | 0m00.14s || -0m00.01s
0m00.13s | categories/Adjoint/Utf8                                            | 0m00.11s || +0m00.02s
0m00.13s | categories/Category/Utf8                                           | 0m00.10s || +0m00.03s
0m00.13s | hit/iso                                                            | 0m00.13s || +0m00.00s
0m00.13s | categories/Pseudofunctor/Pseudofunctor                             | 0m00.16s || -0m00.03s
0m00.13s | hit/unique_choice                                                  | 0m00.10s || +0m00.03s
0m00.13s | categories/GroupoidCategory/Core                                   | 0m00.14s || -0m00.01s
0m00.13s | categories/Category/Objects                                        | 0m00.16s || -0m00.03s
0m00.13s | categories/Category/Category                                       | 0m00.16s || -0m00.03s
0m00.13s | categories/InitialTerminalCategory/Notations                       | 0m00.14s || -0m00.01s
0m00.13s | types/Record                                                       | 0m00.10s || +0m00.03s
0m00.13s | categories/PseudonaturalTransformation/PseudonaturalTransformation | 0m00.14s || -0m00.01s
0m00.13s | hit/TwoSphere                                                      | 0m00.11s || +0m00.02s
0m00.13s | categories/Profunctor/Identity                                     | 0m00.13s || +0m00.00s
0m00.13s | categories/NaturalTransformation/Composition/Composition           | 0m00.09s || +0m00.04s
0m00.13s | categories/NaturalTransformation/Utf8                              | 0m00.14s || -0m00.01s
0m00.13s | categories/Adjoint/Composition/LawsTactic                          | 0m00.13s || +0m00.00s
0m00.12s | categories/Comma/Utf8                                              | 0m00.12s || +0m00.00s
0m00.12s | categories/Limits/Limits                                           | 0m00.10s || +0m00.01s
0m00.12s | Conjugation                                                        | 0m00.15s || -0m00.03s
0m00.12s | categories/Profunctor/Core                                         | 0m00.12s || +0m00.00s
0m00.12s | categories/Functor/Prod/Prod                                       | 0m00.14s || -0m00.02s
0m00.12s | categories/SetCategory/Core                                        | 0m00.10s || +0m00.01s
0m00.12s | coq/Init/Peano                                                     | 0m00.09s || +0m00.03s
0m00.12s | categories/NatCategory                                             | 0m00.18s || -0m00.06s
0m00.12s | categories/NaturalTransformation/Notations                         | 0m00.10s || +0m00.01s
0m00.12s | categories/InitialTerminalCategory/InitialTerminalCategory         | 0m00.13s || -0m00.01s
0m00.12s | Tactics/BinderApply                                                | 0m00.08s || +0m00.03s
0m00.12s | types/Unit                                                         | 0m00.13s || -0m00.01s
0m00.12s | categories/Functor/Pointwise/Pointwise                             | 0m00.09s || +0m00.03s
0m00.12s | categories/FunctorCategory/Core                                    | 0m00.14s || -0m00.02s
0m00.11s | categories/ExponentialLaws/Law3/Law3                               | 0m00.09s || +0m00.02s
0m00.11s | categories/DiscreteCategory                                        | 0m00.11s || +0m00.00s
0m00.11s | categories/KanExtensions/KanExtensions                             | 0m00.15s || -0m00.03s
0m00.11s | categories/Profunctor/Notations                                    | 0m00.12s || -0m00.00s
0m00.11s | Contractible                                                       | 0m00.12s || -0m00.00s
0m00.11s | categories/Category/Dual                                           | 0m00.12s || -0m00.00s
0m00.11s | categories/ExponentialLaws/Law4/Law4                               | 0m00.12s || -0m00.00s
0m00.11s | categories/CategoryOfGroupoids                                     | 0m00.12s || -0m00.00s
0m00.11s | TruncType                                                          | 0m00.17s || -0m00.06s
0m00.11s | categories/Adjoint/Composition/Composition                         | 0m00.12s || -0m00.00s
0m00.11s | categories/Category/Subcategory/Subcategory                        | 0m00.08s || +0m00.03s
0m00.11s | categories/Category/Core                                           | 0m00.12s || -0m00.00s
0m00.11s | categories/Category/Notations                                      | 0m00.08s || +0m00.03s
0m00.11s | categories/ExponentialLaws/Law1/Law1                               | 0m00.15s || -0m00.03s
0m00.11s | categories/Structure/Utf8                                          | 0m00.12s || -0m00.00s
0m00.10s | categories/Adjoint/Core                                            | 0m00.10s || +0m00.00s
0m00.10s | hit/Interval                                                       | 0m00.12s || -0m00.01s
0m00.10s | categories/Adjoint/Identity                                        | 0m00.14s || -0m00.04s
0m00.10s | categories/Functor/Core                                            | 0m00.11s || -0m00.00s
0m00.10s | UnivalenceAxiom                                                    | 0m00.09s || +0m00.01s
0m00.10s | categories/ExponentialLaws/Law2/Law2                               | 0m00.14s || -0m00.04s
0m00.10s | hit/Truncations                                                    | 0m00.13s || -0m00.03s
0m00.10s | categories/Category/Pi                                             | 0m00.13s || -0m00.03s
0m00.10s | FunextAxiom                                                        | 0m00.04s || +0m00.06s
0m00.10s | categories/Profunctor/Utf8                                         | 0m00.09s || +0m00.01s
0m00.10s | categories/CategoryOfSections/CategoryOfSections                   | 0m00.09s || +0m00.01s
0m00.09s | categories/Functor/Identity                                        | 0m00.06s || +0m00.03s
0m00.09s | Misc                                                               | 0m00.13s || -0m00.04s
0m00.09s | categories/Category/Univalent                                      | 0m00.12s || -0m00.03s
0m00.09s | categories/Comma/Notations                                         | 0m00.10s || -0m00.01s
0m00.09s | categories/Category/Subcategory/Wide                               | 0m00.09s || +0m00.00s
0m00.09s | Pointed                                                            | 0m00.09s || +0m00.00s
0m00.09s | categories/SetCategory/SetCategory                                 | 0m00.15s || -0m00.06s
0m00.09s | categories/Category/Subcategory/Full                               | 0m00.09s || +0m00.00s
0m00.09s | Utf8                                                               | 0m00.13s || -0m00.04s
0m00.08s | categories/GroupoidCategory/GroupoidCategory                       | 0m00.10s || -0m00.02s
0m00.08s | categories/Category/Strict                                         | 0m00.06s || +0m00.02s
0m00.08s | categories/Structure/Structure                                     | 0m00.09s || -0m00.00s
0m00.08s | categories/Structure/Notations                                     | 0m00.10s || -0m00.02s
0m00.08s | categories/Functor/Composition/Core                                | 0m00.10s || -0m00.02s
0m00.08s | categories/Category/Sigma/Sigma                                    | 0m00.10s || -0m00.02s
0m00.08s | types/Empty                                                        | 0m00.06s || +0m00.02s
0m00.07s | categories/Profunctor/Profunctor                                   | 0m00.12s || -0m00.04s
0m00.07s | types/UniverseLevel                                                | 0m00.06s || +0m00.01s
0m00.07s | coq/Init/Logic_Type                                                | 0m00.06s || +0m00.01s
0m00.06s | coq/Init/Specif                                                    | 0m00.06s || +0m00.00s
0m00.06s | coq/Program/Tactics                                                | 0m00.07s || -0m00.01s
0m00.05s | coq/Init/Datatypes                                                 | 0m00.03s || +0m00.02s
0m00.04s | coq/Unicode/Utf8                                                   | 0m00.03s || +0m00.01s
0m00.04s | coq/Init/Prelude                                                   | 0m00.05s || -0m00.01s
0m00.03s | coq/Init/Notations                                                 | 0m00.04s || -0m00.01s
0m00.03s | coq/Unicode/Utf8_core                                              | 0m00.03s || +0m00.00s
0m00.03s | coq/Init/Tactics                                                   | 0m00.03s || +0m00.00s
0m00.02s | coq/Init/Logic                                                     | 0m00.03s || -0m00.00s
0m00.02s | coq/Bool/Bool                                                      | 0m00.02s || +0m00.00s
Take advantage of eta to reduce the kinds of ᵒᵖs

Now we only have one kind of functor ᵒᵖ

After    | File Name                                                          | Before   || Change
-----------------------------------------------------------------------------------------------------
3m29.77s | Total                                                              | 3m32.54s || -0m02.76s
-----------------------------------------------------------------------------------------------------
0m29.17s | categories/ExponentialLaws/Law4/Law                                | 0m30.41s || -0m01.23s
0m21.10s | categories/ExponentialLaws/Law3/Law                                | 0m20.01s || +0m01.08s
0m15.35s | categories/ExponentialLaws/Law2/Law                                | 0m16.85s || -0m01.50s
0m10.26s | categories/Comma/Functorial                                        | 0m09.04s || +0m01.22s
0m07.00s | categories/Adjoint/Composition/AssociativityLaw                    | 0m05.62s || +0m01.37s
0m13.88s | categories/LaxComma/CoreLaws                                       | 0m14.61s || -0m00.72s
0m08.76s | categories/Comma/ProjectionFunctors                                | 0m07.80s || +0m00.96s
0m07.36s | hit/V                                                              | 0m07.92s || -0m00.55s
0m03.52s | categories/Pseudofunctor/RewriteLaws                               | 0m04.05s || -0m00.52s
0m03.47s | categories/ExponentialLaws/Law4/Functors                           | 0m03.41s || +0m00.06s
0m03.37s | categories/Grothendieck/PseudofunctorToCat                         | 0m03.42s || -0m00.04s
0m03.15s | categories/GroupoidCategory/Morphisms                              | 0m03.06s || +0m00.08s
0m02.99s | categories/Adjoint/HomCoercions                                    | 0m02.20s || +0m00.79s
0m02.88s | hit/Flattening                                                     | 0m02.86s || +0m00.02s
0m02.29s | categories/Adjoint/Composition/IdentityLaws                        | 0m01.94s || +0m00.35s
0m01.79s | categories/Adjoint/Dual                                            | 0m01.78s || +0m00.01s
0m01.76s | categories/Category/Morphisms                                      | 0m01.71s || +0m00.05s
0m01.75s | categories/LaxComma/CoreParts                                      | 0m01.82s || -0m00.07s
0m01.69s | categories/Pseudofunctor/Identity                                  | 0m01.75s || -0m00.06s
0m01.69s | categories/Adjoint/Composition/Core                                | 0m02.07s || -0m00.37s
0m01.67s | categories/Functor/Pointwise/Properties                            | 0m01.65s || +0m00.02s
0m01.64s | categories/Comma/InducedFunctors                                   | 0m01.64s || +0m00.00s
0m01.54s | categories/FunctorCategory/Dual                                    | 0m02.33s || -0m00.79s
0m01.48s | hit/epi                                                            | 0m01.50s || -0m00.02s
0m01.46s | categories/ExponentialLaws/Law1/Law                                | 0m01.45s || +0m00.01s
0m01.36s | categories/Pseudofunctor/FromFunctor                               | 0m01.53s || -0m00.16s
0m01.27s | categories/Yoneda                                                  | 0m01.18s || +0m00.09s
0m01.26s | categories/Adjoint/UnitCounitCoercions                             | 0m01.52s || -0m00.26s
0m01.12s | HSet                                                               | 0m01.14s || -0m00.01s
0m01.06s | HProp                                                              | 0m01.07s || -0m00.01s
0m01.04s | Equivalences                                                       | 0m01.08s || -0m00.04s
0m00.99s | categories/Functor/Sum                                             | 0m00.99s || +0m00.00s
0m00.93s | categories/Comma/Dual                                              | 0m01.86s || -0m00.93s
0m00.92s | categories/UniversalProperties                                     | 0m00.95s || -0m00.02s
0m00.92s | PathGroupoids                                                      | 0m00.90s || +0m00.02s
0m00.90s | categories/PseudonaturalTransformation/Core                        | 0m01.07s || -0m00.17s
0m00.87s | ReflectiveSubuniverse                                              | 0m00.93s || -0m00.06s
0m00.84s | contrib/HoTTBook                                                   | 0m00.79s || +0m00.04s
0m00.80s | categories/Category/Sigma/OnMorphisms                              | 0m00.89s || -0m00.08s
0m00.78s | types/Sigma                                                        | 0m00.87s || -0m00.08s
0m00.77s | categories/Limits/Core                                             | 0m00.77s || +0m00.00s
0m00.76s | categories/Structure/IdentityPrinciple                             | 0m00.75s || +0m00.01s
0m00.74s | categories/Functor/Composition/Functorial/Core                     | 0m00.75s || -0m00.01s
0m00.72s | categories/ProductLaws                                             | 0m00.78s || -0m00.06s
0m00.72s | categories/Functor/Attributes                                      | 0m00.74s || -0m00.02s
0m00.71s | categories/Functor/Paths                                           | 0m00.70s || +0m00.01s
0m00.70s | categories/Functor/Prod/Universal                                  | 0m00.71s || -0m00.01s
0m00.68s | hit/Connectedness                                                  | 0m00.80s || -0m00.12s
0m00.66s | categories/LaxComma/Core                                           | 0m00.67s || -0m00.01s
0m00.64s | EquivalenceVarieties                                               | 0m00.58s || +0m00.06s
0m00.64s | categories/Category/Sum                                            | 0m00.67s || -0m00.03s
0m00.62s | categories/Adjoint/UniversalMorphisms                              | 0m00.45s || +0m00.17s
0m00.62s | categories/Comma/Core                                              | 0m00.70s || -0m00.07s
0m00.59s | contrib/HoTTBookExercises                                          | 0m00.59s || +0m00.00s
0m00.58s | categories/Functor/Composition/Functorial/Attributes               | 0m00.65s || -0m00.07s
0m00.54s | categories/ExponentialLaws/Law0                                    | 0m00.50s || +0m00.04s
0m00.52s | hit/Spheres                                                        | 0m00.53s || -0m00.01s
0m00.50s | categories/Functor/Prod/Functorial                                 | 0m00.48s || +0m00.02s
0m00.49s | categories/Adjoint/UnitCounit                                      | 0m00.49s || +0m00.00s
0m00.48s | categories/NaturalTransformation/Isomorphisms                      | 0m00.52s || -0m00.04s
0m00.48s | categories/ExponentialLaws/Law1/Functors                           | 0m00.44s || +0m00.03s
0m00.47s | categories/InitialTerminalCategory/Pseudofunctors                  | 0m00.46s || +0m00.00s
0m00.47s | categories/DualFunctor                                             | 0m00.49s || -0m00.02s
0m00.46s | types/Paths                                                        | 0m00.49s || -0m00.02s
0m00.45s | categories/categories                                              | 0m00.41s || +0m00.04s
0m00.44s | categories/ExponentialLaws/Law2/Functors                           | 0m00.45s || -0m00.01s
0m00.42s | categories/SetCategory/Morphisms                                   | 0m00.40s || +0m00.01s
0m00.41s | categories/NaturalTransformation/Pointwise                         | 0m00.40s || +0m00.00s
0m00.40s | categories/Adjoint/Paths                                           | 0m00.48s || -0m00.07s
0m00.40s | categories/Functor/Pointwise                                       | 0m00.42s || -0m00.01s
0m00.37s | types/Prod                                                         | 0m00.36s || +0m00.01s
0m00.37s | categories/FunctorCategory/Morphisms                               | 0m00.45s || -0m00.08s
0m00.37s | hit/quotient                                                       | 0m00.37s || +0m00.00s
0m00.36s | categories/Limits/Functors                                         | 0m00.39s || -0m00.03s
0m00.36s | categories/Functor/Prod                                            | 0m00.32s || +0m00.03s
0m00.36s | hit/Circle                                                         | 0m00.36s || +0m00.00s
0m00.36s | categories/KanExtensions/Functors                                  | 0m00.28s || +0m00.07s
0m00.33s | types/Universe                                                     | 0m00.34s || -0m00.01s
0m00.33s | categories/NaturalTransformation/Prod                              | 0m00.35s || -0m00.01s
0m00.33s | categories/NaturalTransformation/Composition/Laws                  | 0m00.30s || +0m00.03s
0m00.33s | categories/Pseudofunctor/Core                                      | 0m00.32s || +0m00.01s
0m00.33s | categories/Structure/Core                                          | 0m00.30s || +0m00.03s
0m00.33s | categories/Comma/Projection                                        | 0m00.28s || +0m00.04s
0m00.32s | categories/Grothendieck/ToSet                                      | 0m00.30s || +0m00.02s
0m00.30s | categories/NaturalTransformation/Paths                             | 0m00.30s || +0m00.00s
0m00.30s | categories/HomFunctor                                              | 0m00.29s || +0m00.01s
0m00.28s | Modality                                                           | 0m00.25s || +0m00.03s
0m00.27s | Trunc                                                              | 0m00.26s || +0m00.01s
0m00.27s | categories/NaturalTransformation/Dual                              | 0m00.42s || -0m00.14s
0m00.26s | categories/Category/Sigma/Core                                     | 0m00.28s || -0m00.02s
0m00.26s | categories/Cat/Core                                                | 0m00.23s || +0m00.03s
0m00.26s | Tactics                                                            | 0m00.28s || -0m00.02s
0m00.26s | categories/LaxComma/Utf8                                           | 0m00.17s || +0m00.09s
0m00.25s | types/ObjectClassifier                                             | 0m00.26s || -0m00.01s
0m00.25s | categories/Functor/Functor                                         | 0m00.19s || +0m00.06s
0m00.25s | categories/InitialTerminalCategory/Functors                        | 0m00.29s || -0m00.03s
0m00.24s | types/Sum                                                          | 0m00.28s || -0m00.04s
0m00.24s | categories/FundamentalPreGroupoidCategory                          | 0m00.25s || -0m00.01s
0m00.24s | categories/Adjoint/Hom                                             | 0m00.26s || -0m00.02s
0m00.24s | hit/minus1Trunc                                                    | 0m00.26s || -0m00.02s
0m00.24s | hit/Pushout                                                        | 0m00.24s || +0m00.00s
0m00.23s | categories/Category/Sigma/OnObjects                                | 0m00.22s || +0m00.01s
0m00.23s | categories/LaxComma/LaxComma                                       | 0m00.18s || +0m00.05s
0m00.22s | categories/ExponentialLaws/Law3/Functors                           | 0m00.28s || -0m00.06s
0m00.22s | categories/FunctorCategory/Functorial                              | 0m00.30s || -0m00.07s
0m00.22s | categories/Adjoint/Adjoint                                         | 0m00.19s || +0m00.03s
0m00.22s | types/Forall                                                       | 0m00.26s || -0m00.04s
0m00.21s | categories/Category/Prod                                           | 0m00.18s || +0m00.03s
0m00.21s | categories/CategoryOfSections/Core                                 | 0m00.22s || -0m00.01s
0m00.20s | categories/IndiscreteCategory                                      | 0m00.21s || -0m00.00s
0m00.20s | hit/Suspension                                                     | 0m00.22s || -0m00.01s
0m00.20s | categories/Utf8                                                    | 0m00.19s || +0m00.01s
0m00.20s | categories/Functor/Composition/Laws                                | 0m00.22s || -0m00.01s
0m00.20s | types/Bool                                                         | 0m00.17s || +0m00.03s
0m00.20s | categories/NaturalTransformation/Composition/Core                  | 0m00.22s || -0m00.01s
0m00.19s | UnivalenceImpliesFunext                                            | 0m00.18s || +0m00.01s
0m00.19s | types/Arrow                                                        | 0m00.21s || -0m00.01s
0m00.19s | Fibrations                                                         | 0m00.18s || +0m00.01s
0m00.18s | categories/ExponentialLaws/ExponentialLaws                         | 0m00.19s || -0m00.01s
0m00.18s | categories/Comma/Comma                                             | 0m00.20s || -0m00.02s
0m00.18s | categories/KanExtensions/Core                                      | 0m00.26s || -0m00.08s
0m00.17s | categories/Functor/Composition/Functorial                          | 0m00.14s || +0m00.03s
0m00.17s | categories/NaturalTransformation/Sum                               | 0m00.21s || -0m00.03s
0m00.17s | categories/NaturalTransformation/Core                              | 0m00.16s || +0m00.01s
0m00.17s | categories/FunctorCategory/Core                                    | 0m00.11s || +0m00.06s
0m00.16s | categories/NaturalTransformation/NaturalTransformation             | 0m00.17s || -0m00.01s
0m00.16s | categories/NatCategory                                             | 0m00.19s || -0m00.03s
0m00.16s | categories/Functor/Utf8                                            | 0m00.17s || -0m00.01s
0m00.16s | categories/HomotopyPreCategory                                     | 0m00.17s || -0m00.01s
0m00.16s | categories/Notations                                               | 0m00.19s || -0m00.03s
0m00.16s | categories/NaturalTransformation/Identity                          | 0m00.17s || -0m00.01s
0m00.16s | FunextVarieties                                                    | 0m00.15s || +0m00.01s
0m00.16s | categories/Grothendieck/Grothendieck                               | 0m00.15s || +0m00.01s
0m00.15s | categories/ExponentialLaws/Law3/Law3                               | 0m00.14s || +0m00.00s
0m00.15s | categories/Functor/Composition/Composition                         | 0m00.14s || +0m00.00s
0m00.15s | categories/Grothendieck/ToCat                                      | 0m00.18s || -0m00.03s
0m00.15s | categories/Adjoint/Identity                                        | 0m00.17s || -0m00.02s
0m00.15s | hit/unique_choice                                                  | 0m00.13s || +0m00.01s
0m00.15s | categories/Functor/Notations                                       | 0m00.14s || +0m00.00s
0m00.15s | categories/InitialTerminalCategory/Notations                       | 0m00.16s || -0m00.01s
0m00.15s | Overture                                                           | 0m00.18s || -0m00.03s
0m00.14s | categories/InitialTerminalCategory/NaturalTransformations          | 0m00.17s || -0m00.03s
0m00.14s | categories/DependentProduct                                        | 0m00.15s || -0m00.00s
0m00.14s | categories/LaxComma/Notations                                      | 0m00.16s || -0m00.01s
0m00.14s | categories/FunctorCategory/Utf8                                    | 0m00.18s || -0m00.03s
0m00.14s | categories/Functor/Prod/Prod                                       | 0m00.14s || +0m00.00s
0m00.14s | categories/SetCategory/Functors/Functors                           | 0m00.16s || -0m00.01s
0m00.14s | Functorish                                                         | 0m00.15s || -0m00.00s
0m00.14s | HoTT                                                               | 0m00.17s || -0m00.03s
0m00.14s | categories/Pseudofunctor/Pseudofunctor                             | 0m00.15s || -0m00.00s
0m00.14s | categories/InitialTerminalCategory/Core                            | 0m00.11s || +0m00.03s
0m00.14s | categories/CategoryOfGroupoids                                     | 0m00.16s || -0m00.01s
0m00.14s | categories/GroupoidCategory/Core                                   | 0m00.13s || +0m00.01s
0m00.14s | categories/Category/Category                                       | 0m00.14s || +0m00.00s
0m00.14s | categories/Cat/Morphisms                                           | 0m00.17s || -0m00.03s
0m00.14s | categories/NaturalTransformation/Notations                         | 0m00.13s || +0m00.01s
0m00.14s | categories/InitialTerminalCategory/InitialTerminalCategory         | 0m00.12s || +0m00.02s
0m00.14s | Tests                                                              | 0m00.18s || -0m00.03s
0m00.14s | categories/NaturalTransformation/Composition/Functorial            | 0m00.19s || -0m00.04s
0m00.14s | categories/ExponentialLaws/Law1/Law1                               | 0m00.12s || +0m00.02s
0m00.14s | categories/NaturalTransformation/Utf8                              | 0m00.14s || +0m00.00s
0m00.14s | categories/Category/Pi                                             | 0m00.15s || -0m00.00s
0m00.13s | categories/Profunctor/Core                                         | 0m00.14s || -0m00.01s
0m00.13s | Misc                                                               | 0m00.12s || +0m00.01s
0m00.13s | TruncType                                                          | 0m00.12s || +0m00.01s
0m00.13s | categories/PseudonaturalTransformation/PseudonaturalTransformation | 0m00.14s || -0m00.01s
0m00.13s | types/Unit                                                         | 0m00.10s || +0m00.03s
0m00.13s | Utf8                                                               | 0m00.11s || +0m00.02s
0m00.12s | categories/Profunctor/Representable                                | 0m00.15s || -0m00.03s
0m00.12s | categories/Comma/Utf8                                              | 0m00.14s || -0m00.02s
0m00.12s | categories/Limits/Limits                                           | 0m00.12s || +0m00.00s
0m00.12s | Conjugation                                                        | 0m00.13s || -0m00.01s
0m00.12s | categories/KanExtensions/KanExtensions                             | 0m00.12s || +0m00.00s
0m00.12s | categories/Cat/Cat                                                 | 0m00.11s || +0m00.00s
0m00.12s | categories/Functor/Dual                                            | 0m00.20s || -0m00.08s
0m00.12s | hit/iso                                                            | 0m00.13s || -0m00.01s
0m00.12s | categories/FunctorCategory/FunctorCategory                         | 0m00.15s || -0m00.03s
0m00.12s | categories/Adjoint/Notations                                       | 0m00.14s || -0m00.02s
0m00.12s | categories/Category/Univalent                                      | 0m00.11s || +0m00.00s
0m00.12s | categories/Comma/Notations                                         | 0m00.11s || +0m00.00s
0m00.12s | categories/Category/Subcategory/Wide                               | 0m00.11s || +0m00.00s
0m00.12s | categories/Category/Objects                                        | 0m00.11s || +0m00.00s
0m00.12s | types/Record                                                       | 0m00.13s || -0m00.01s
0m00.12s | categories/Adjoint/Composition/Composition                         | 0m00.12s || +0m00.00s
0m00.12s | categories/Profunctor/Identity                                     | 0m00.17s || -0m00.05s
0m00.12s | categories/SetCategory/Core                                        | 0m00.12s || +0m00.00s
0m00.12s | categories/ExponentialLaws/Law2/Law2                               | 0m00.12s || +0m00.00s
0m00.11s | categories/Adjoint/Core                                            | 0m00.10s || +0m00.00s
0m00.11s | coq/Init/Peano                                                     | 0m00.10s || +0m00.00s
0m00.11s | types/UniverseLevel                                                | 0m00.06s || +0m00.05s
0m00.11s | categories/Profunctor/Utf8                                         | 0m00.11s || +0m00.00s
0m00.11s | categories/CategoryOfSections/CategoryOfSections                   | 0m00.13s || -0m00.02s
0m00.10s | categories/DiscreteCategory                                        | 0m00.08s || +0m00.02s
0m00.10s | categories/GroupoidCategory/GroupoidCategory                       | 0m00.09s || +0m00.01s
0m00.10s | categories/Adjoint/Utf8                                            | 0m00.10s || +0m00.00s
0m00.10s | categories/Profunctor/Notations                                    | 0m00.09s || +0m00.01s
0m00.10s | Contractible                                                       | 0m00.10s || +0m00.00s
0m00.10s | hit/Interval                                                       | 0m00.14s || -0m00.04s
0m00.10s | categories/Category/Dual                                           | 0m00.12s || -0m00.01s
0m00.10s | categories/ExponentialLaws/Law4/Law4                               | 0m00.10s || +0m00.00s
0m00.10s | categories/Profunctor/Profunctor                                   | 0m00.15s || -0m00.04s
0m00.10s | categories/Structure/Notations                                     | 0m00.10s || +0m00.00s
0m00.10s | categories/Category/Subcategory/Subcategory                        | 0m00.10s || +0m00.00s
0m00.10s | categories/Category/Core                                           | 0m00.11s || -0m00.00s
0m00.10s | hit/TwoSphere                                                      | 0m00.12s || -0m00.01s
0m00.10s | categories/SetCategory/SetCategory                                 | 0m00.11s || -0m00.00s
0m00.10s | Tactics/BinderApply                                                | 0m00.12s || -0m00.01s
0m00.10s | UnivalenceAxiom                                                    | 0m00.11s || -0m00.00s
0m00.10s | categories/FunctorCategory/Notations                               | 0m00.12s || -0m00.01s
0m00.09s | categories/Functor/Identity                                        | 0m00.06s || +0m00.03s
0m00.09s | categories/Structure/Structure                                     | 0m00.13s || -0m00.04s
0m00.09s | categories/Functor/Composition/Core                                | 0m00.10s || -0m00.01s
0m00.09s | categories/Category/Notations                                      | 0m00.12s || -0m00.03s
0m00.09s | categories/Category/Subcategory/Full                               | 0m00.10s || -0m00.01s
0m00.09s | categories/Functor/Pointwise/Pointwise                             | 0m00.10s || -0m00.01s
0m00.09s | hit/Truncations                                                    | 0m00.12s || -0m00.03s
0m00.09s | categories/Adjoint/Composition/LawsTactic                          | 0m00.11s || -0m00.02s
0m00.08s | categories/Category/Utf8                                           | 0m00.10s || -0m00.02s
0m00.08s | categories/Category/Strict                                         | 0m00.07s || +0m00.00s
0m00.08s | categories/Functor/Core                                            | 0m00.10s || -0m00.02s
0m00.08s | Pointed                                                            | 0m00.08s || +0m00.00s
0m00.08s | categories/NaturalTransformation/Composition/Composition           | 0m00.12s || -0m00.03s
0m00.08s | categories/Category/Sigma/Sigma                                    | 0m00.09s || -0m00.00s
0m00.08s | types/Empty                                                        | 0m00.09s || -0m00.00s
0m00.06s | coq/Init/Datatypes                                                 | 0m00.05s || +0m00.00s
0m00.06s | coq/Init/Specif                                                    | 0m00.06s || +0m00.00s
0m00.06s | coq/Init/Logic_Type                                                | 0m00.06s || +0m00.00s
0m00.06s | coq/Program/Tactics                                                | 0m00.04s || +0m00.01s
0m00.06s | categories/Structure/Utf8                                          | 0m00.11s || -0m00.05s
0m00.06s | FunextAxiom                                                        | 0m00.05s || +0m00.00s
0m00.04s | coq/Init/Notations                                                 | 0m00.04s || +0m00.00s
0m00.04s | coq/Unicode/Utf8_core                                              | 0m00.04s || +0m00.00s
0m00.04s | coq/Init/Prelude                                                   | 0m00.03s || +0m00.01s
0m00.03s | coq/Unicode/Utf8                                                   | 0m00.05s || -0m00.02s
0m00.03s | coq/Init/Logic                                                     | 0m00.04s || -0m00.01s
0m00.03s | coq/Init/Tactics                                                   | 0m00.04s || -0m00.01s
0m00.02s | coq/Bool/Bool                                                      | 0m00.02s || +0m00.00s
Add quick and vi2vo targets

It doesn't seem to help much at the moment, but maybe we'll grow some
very slow Qed'ed proofs and want to use this target.

c.f.
https://github.com/coq/coq/blob/trunk/doc/refman/AsyncProofs.tex#L98 for
documentation.

```bash
$ make clean
...
$ time make -j10
real    2m51.868s
user    4m7.179s
sys     8m45.765s

$ make clean
...
$ time make quick -j10

real    2m54.031s
user    4m15.360s
sys     8m52.969s

$ time make vi2vo J=10

real    0m21.458s
user    0m9.161s
sys     0m17.161s

```

This closes #471.
remove notation `!`; use `const (center _)` or `const tt`
Merge pull request #482 from mikeshulman/const

remove notation `!`; use `const (center _)` or `const tt`
Merge pull request #480 from mikeshulman/move

Move ObjectClassifier and UniverseLevel out of types/
uniformize reflective subuniverses and modalities
truncation is a modality
Clean up Pushout.v a bit
join
open and closed modalities
better naming for equivalence move functions
explicit Existing Instance *and* Coercion after typeclasses, for clarity
coqdoc comment
remove unnecessary imports
clarify comment about generalizing binders