Work around bug 3854

This is https://coq.inria.fr/bugs/show_bug.cgi?id=3854, Typeclass
resolution fails where it used to succeed (change in the order of
unification in [refine] or in the order of canonical structure
resolution?)
dummy universe parameter for O_ind_internal, needed by Nullification

N.B. (Jason Gross): On the version of Coq pinned to this commit, we get

File "./theories/Modalities/Localization.v", line 267, characters 2-121:
Anomaly: expects Atom. Please report.

This will be fixed by the next commit.
Set Keyed Unification and bump Coq submodule

Bumping the submodule gives us some keyed unification and primitive
projection fixes.

This closes #531 and #557 and #593.

The comment on the [Set Keyed Unification] directive was written by Mike
Shulman.

Note that we get a host of errors if we bump the submodule without
setting keyed unification; the current version of Coq doesn't attempt to
make [rewrite] work correctly in the presence of primitive projections
without [Set Keyed Unification].

Not sure what all the N/As are

After    | File Name                                                 | Before   || Change
--------------------------------------------------------------------------------------------
2m49.80s | Total                                                     | 3m39.42s || -0m49.62s
--------------------------------------------------------------------------------------------
  N/A    | Idempotents                                               | 0m26.73s || -0m26.73s
  N/A    | hit/V                                                     | 0m20.74s || -0m20.73s
  N/A    | contrib/Freudenthal                                       | 0m11.36s || -0m11.35s
0m07.71s | categories/LaxComma/CoreLaws                              | 0m03.63s || +0m04.08s
0m06.31s | categories/Adjoint/Composition/AssociativityLaw           | 0m01.36s || +0m04.94s
0m49.00s | categories/Adjoint/Pointwise                              | 0m45.38s || +0m03.61s
0m05.37s | Factorization                                             | 0m07.83s || -0m02.46s
0m06.91s | categories/ExponentialLaws/Law3/Law                       | 0m08.56s || -0m01.65s
0m05.97s | Modalities/Modality                                       | 0m04.67s || +0m01.29s
0m02.33s | categories/Functor/Sum                                    | 0m01.20s || +0m01.13s
  N/A    | Modalities/Localization                                   | 0m01.91s || -0m01.90s
  N/A    | hit/epi                                                   | 0m01.52s || -0m01.52s
0m01.03s | categories/Adjoint/HomCoercions                           |   N/A    || +0m01.03s
  N/A    | contrib/HoTTBookExercises                                 | 0m01.03s || -0m01.03s
0m00.76s | Types/Equiv                                               | 0m01.81s || -0m01.05s
0m11.02s | categories/Adjoint/UniversalMorphisms/FunctorialLaws      | 0m10.28s || +0m00.74s
0m07.39s | categories/ExponentialLaws/Law2/Law                       | 0m08.31s || -0m00.92s
0m06.70s | categories/ExponentialLaws/Law4/Law                       | 0m07.22s || -0m00.51s
0m04.28s | categories/Comma/ProjectionFunctors                       | 0m03.92s || +0m00.36s
0m02.69s | categories/Comma/Functorial                               | 0m02.82s || -0m00.12s
0m02.50s | categories/ExponentialLaws/Law1/Law                       | 0m01.54s || +0m00.96s
0m02.13s | categories/GroupoidCategory/Morphisms                     | 0m02.03s || +0m00.10s
0m01.79s | hit/Flattening                                            | 0m02.03s || -0m00.23s
0m01.76s | categories/Grothendieck/PseudofunctorToCat                | 0m01.15s || +0m00.61s
0m01.64s | categories/Category/Morphisms                             | 0m01.20s || +0m00.43s
0m01.58s | Modalities/ReflectiveSubuniverse                          | 0m01.51s || +0m00.07s
0m01.37s | categories/Functor/Paths                                  | 0m00.97s || +0m00.40s
0m01.35s | categories/Pseudofunctor/RewriteLaws                      | 0m00.82s || +0m00.53s
0m01.29s | categories/ExponentialLaws/Law4/Functors                  | 0m01.27s || +0m00.02s
0m01.00s | categories/Category/Sigma/OnMorphisms                     | 0m00.67s || +0m00.32s
0m00.95s | categories/Adjoint/Composition/IdentityLaws               | 0m00.76s || +0m00.18s
0m00.92s | categories/Adjoint/Composition/Core                       | 0m00.54s || +0m00.38s
0m00.92s | Types/Paths                                               | 0m00.85s || +0m00.07s
0m00.89s | categories/Functor/Pointwise/Properties                   | 0m00.89s || +0m00.00s
0m00.79s | Basics/PathGroupoids                                      | 0m00.73s || +0m00.06s
0m00.78s | categories/Comma/InducedFunctors                          | 0m00.72s || +0m00.06s
0m00.73s | categories/Adjoint/UnitCounitCoercions                    | 0m00.71s || +0m00.02s
0m00.70s | categories/Pseudofunctor/Identity                         | 0m00.68s || +0m00.01s
  N/A    | hit/quotient                                              | 0m00.70s || -0m00.70s
0m00.69s | categories/Pseudofunctor/FromFunctor                      | 0m00.75s || -0m00.06s
0m00.69s | Types/Sigma                                               | 0m00.64s || +0m00.04s
0m00.68s | categories/Comma/Core                                     | 0m00.47s || +0m00.21s
0m00.66s | Basics/Equivalences                                       | 0m00.85s || -0m00.18s
0m00.64s | categories/Comma/Dual                                     | 0m00.42s || +0m00.22s
0m00.61s | categories/LaxComma/CoreParts                             | 0m00.46s || +0m00.14s
0m00.60s | categories/ExponentialLaws/Law0                           | 0m00.22s || +0m00.38s
0m00.55s | EquivalenceVarieties                                      | 0m00.46s || +0m00.09s
0m00.55s | categories/Category/Sum                                   | 0m00.40s || +0m00.15s
0m00.54s | categories/Functor/Composition/Laws                       | 0m01.02s || -0m00.48s
0m00.52s | categories/Adjoint/UniversalMorphisms/FunctorialParts     | 0m00.48s || +0m00.04s
0m00.49s | Extensions                                                | 0m00.46s || +0m00.02s
0m00.46s | categories/UniversalProperties                            | 0m01.14s || -0m00.68s
0m00.44s | categories/LaxComma/Core                                  | 0m00.40s || +0m00.03s
0m00.42s | hit/Spheres                                               | 0m00.36s || +0m00.06s
0m00.41s | categories/Functor/Prod/Universal                         | 0m00.37s || +0m00.03s
0m00.41s | categories/Structure/IdentityPrinciple                    | 0m00.39s || +0m00.01s
0m00.38s | categories/SetCategory/Morphisms                          |   N/A    || +0m00.38s
0m00.35s | categories/ProductLaws                                    | 0m00.38s || -0m00.03s
0m00.35s | categories/Adjoint/Paths                                  | 0m00.32s || +0m00.02s
0m00.34s | categories/InitialTerminalCategory/Pseudofunctors         | 0m00.30s || +0m00.04s
0m00.34s | categories/DualFunctor                                    | 0m00.32s || +0m00.02s
0m00.31s | categories/Category/Sigma/Core                            | 0m00.60s || -0m00.28s
0m00.31s | categories/NaturalTransformation/Isomorphisms             | 0m00.22s || +0m00.09s
0m00.30s | Types/Universe                                            | 0m00.27s || +0m00.02s
  N/A    | Modalities/Closed                                         | 0m00.30s || -0m00.30s
0m00.30s | categories/ExponentialLaws/Law1/Functors                  | 0m00.20s || +0m00.09s
0m00.28s | categories/Limits/Core                                    | 0m00.26s || +0m00.02s
0m00.28s | TruncType                                                 | 0m00.24s || +0m00.04s
0m00.28s | categories/Adjoint/UniversalMorphisms/Core                | 0m00.28s || +0m00.00s
  N/A    | categories/FundamentalPreGroupoidCategory                 | 0m00.27s || -0m00.27s
0m00.26s | categories/NaturalTransformation/Paths                    | 0m00.22s || +0m00.04s
0m00.26s | categories/Functor/Composition/Functorial/Core            | 0m00.25s || +0m00.01s
0m00.26s | Types/Prod                                                | 0m00.24s || +0m00.02s
  N/A    | hit/Join                                                  | 0m00.26s || -0m00.26s
  N/A    | hit/Connectedness                                         | 0m00.26s || -0m00.26s
0m00.25s | categories/Functor/Pointwise/Core                         | 0m00.20s || +0m00.04s
0m00.23s | Types/Sum                                                 | 0m00.22s || +0m00.01s
0m00.23s | Modalities/Accessible                                     | 0m00.22s || +0m00.01s
  N/A    | HoTT                                                      | 0m00.22s || -0m00.22s
0m00.22s | categories/Functor/Prod/Functorial                        | 0m00.18s || +0m00.04s
0m00.22s | hit/Circle                                                | 0m00.21s || +0m00.01s
0m00.22s | Fibrations                                                | 0m00.23s || -0m00.01s
0m00.22s | categories/Functor/Prod/Core                              | 0m00.20s || +0m00.01s
  N/A    | Modalities/Open                                           | 0m00.21s || -0m00.21s
0m00.21s | categories/NaturalTransformation/Pointwise                | 0m00.13s || +0m00.07s
0m00.21s | categories/FunctorCategory/Morphisms                      | 0m00.18s || +0m00.03s
0m00.21s | ObjectClassifier                                          | 0m00.20s || +0m00.00s
  N/A    | categories/HomotopyPreCategory                            | 0m00.21s || -0m00.21s
0m00.21s | categories/InitialTerminalCategory/Functors               | 0m00.16s || +0m00.04s
0m00.21s | categories/Grothendieck/ToSet                             |   N/A    || +0m00.21s
  N/A    | Tests                                                     | 0m00.21s || -0m00.21s
0m00.20s | categories/ExponentialLaws/Law2/Functors                  | 0m00.20s || +0m00.00s
0m00.20s | categories/HomFunctor                                     |   N/A    || +0m00.20s
0m00.18s | categories/NaturalTransformation/Prod                     | 0m00.18s || +0m00.00s
0m00.18s | Types/Forall                                              | 0m00.18s || +0m00.00s
0m00.18s | categories/FunctorCategory/Dual                           | 0m00.16s || +0m00.01s
  N/A    | hit/Truncations                                           | 0m00.18s || -0m00.18s
  N/A    | hit/iso                                                   | 0m00.17s || -0m00.17s
0m00.17s | categories/NaturalTransformation/Composition/Laws         | 0m00.20s || -0m00.03s
0m00.17s | categories/Pseudofunctor/Core                             | 0m00.16s || +0m00.01s
0m00.17s | categories/Structure/Core                                 | 0m00.18s || -0m00.00s
  N/A    | Modalities/Nullification                                  | 0m00.16s || -0m00.16s
  N/A    | hit/Pushout                                               | 0m00.16s || -0m00.16s
0m00.16s | categories/Limits/Functors                                | 0m00.15s || +0m00.01s
0m00.16s | Basics/Trunc                                              | 0m00.14s || +0m00.01s
0m00.16s | HSet                                                      | 0m00.14s || +0m00.01s
0m00.15s | categories/IndiscreteCategory                             | 0m00.14s || +0m00.00s
0m00.15s | categories/Category/Prod                                  | 0m00.12s || +0m00.03s
0m00.14s | Modalities/Notnot                                         | 0m00.12s || +0m00.02s
0m00.14s | categories/Cat/Core                                       | 0m00.11s || +0m00.03s
0m00.14s | categories/Category/Sigma/OnObjects                       | 0m00.13s || +0m00.01s
0m00.14s | HProp                                                     | 0m00.14s || +0m00.00s
0m00.14s | categories/Comma                                          | 0m00.11s || +0m00.03s
0m00.14s | categories/CategoryOfSections/Core                        | 0m00.16s || -0m00.01s
0m00.14s | categories/KanExtensions/Functors                         | 0m00.14s || +0m00.00s
0m00.14s | categories/Adjoint/UnitCounit                             | 0m00.13s || +0m00.01s
0m00.13s | Types/Arrow                                               | 0m00.11s || +0m00.02s
0m00.13s | categories/NaturalTransformation/Sum                      | 0m00.11s || +0m00.02s
0m00.13s | categories/PseudonaturalTransformation/Core               | 0m00.15s || -0m00.01s
0m00.13s | categories/Adjoint/Hom                                    |   N/A    || +0m00.13s
0m00.13s | hit/Suspension                                            | 0m00.13s || +0m00.00s
0m00.13s | categories/NatCategory                                    | 0m00.09s || +0m00.04s
0m00.13s | Tactics                                                   | 0m00.16s || -0m00.03s
0m00.13s | categories/Adjoint                                        |   N/A    || +0m00.13s
0m00.13s | categories/KanExtensions/Core                             | 0m00.11s || +0m00.02s
0m00.13s | categories/NaturalTransformation/Composition/Core         | 0m00.11s || +0m00.02s
0m00.13s | categories/Comma/Projection                               | 0m00.14s || -0m00.01s
0m00.12s | categories/LaxComma/Notations                             | 0m00.12s || +0m00.00s
0m00.12s | UnivalenceImpliesFunext                                   | 0m00.10s || +0m00.01s
0m00.12s | categories/ExponentialLaws/Law3/Functors                  | 0m00.12s || +0m00.00s
  N/A    | hit/unique_choice                                         | 0m00.12s || -0m00.12s
0m00.12s | Tactics/RewriteModuloAssociativity                        | 0m00.10s || +0m00.01s
  N/A    | Utf8                                                      | 0m00.12s || -0m00.12s
0m00.11s | categories/Grothendieck/ToCat                             | 0m00.10s || +0m00.00s
0m00.11s | categories/FunctorCategory/Functorial                     | 0m00.12s || -0m00.00s
  N/A    | Modalities/Identity                                       | 0m00.10s || -0m00.10s
0m00.10s | categories/Pseudofunctor                                  | 0m00.07s || +0m00.03s
0m00.10s | Types/Bool                                                | 0m00.10s || +0m00.00s
0m00.10s | categories/LaxComma/Utf8                                  | 0m00.10s || +0m00.00s
0m00.10s | Basics/FunextVarieties                                    | 0m00.10s || +0m00.00s
0m00.10s | categories/FunctorCategory                                | 0m00.07s || +0m00.03s
0m00.10s | categories/NaturalTransformation/Identity                 | 0m00.09s || +0m00.01s
0m00.10s | categories/Cat/Morphisms                                  | 0m00.10s || +0m00.00s
0m00.10s | categories/Adjoint/Composition                            | 0m00.07s || +0m00.03s
0m00.10s | categories/Limits                                         | 0m00.09s || +0m00.01s
0m00.09s | Basics/Overture                                           | 0m00.12s || -0m00.03s
0m00.09s | categories/DependentProduct                               | 0m00.09s || +0m00.00s
0m00.09s | categories/Category                                       | 0m00.08s || +0m00.00s
0m00.09s | categories/LaxComma                                       | 0m00.10s || -0m00.01s
0m00.09s | Functorish                                                | 0m00.07s || +0m00.01s
0m00.09s | categories/SetCategory/Core                               | 0m00.06s || +0m00.03s
0m00.09s | Types/Unit                                                | 0m00.04s || +0m00.05s
0m00.09s | categories/Adjoint/UniversalMorphisms                     | 0m00.09s || +0m00.00s
0m00.09s | categories/Functor/Prod                                   | 0m00.07s || +0m00.01s
0m00.09s | categories/InitialTerminalCategory/NaturalTransformations | 0m00.08s || +0m00.00s
0m00.09s | categories/KanExtensions                                  | 0m00.08s || +0m00.00s
0m00.08s | categories/Comma/Utf8                                     | 0m00.06s || +0m00.02s
0m00.08s | categories/Adjoint/Utf8                                   | 0m00.07s || +0m00.00s
0m00.08s | categories/NaturalTransformation/Notations                | 0m00.10s || -0m00.02s
0m00.08s | categories/Profunctor/Core                                |   N/A    || +0m00.08s
0m00.08s | categories/ExponentialLaws                                | 0m00.09s || -0m00.00s
0m00.08s | categories/Functor/Dual                                   | 0m00.06s || +0m00.02s
0m00.08s | categories/PseudonaturalTransformation                    | 0m00.06s || +0m00.02s
0m00.08s | categories/Category/Dual                                  | 0m00.06s || +0m00.02s
0m00.08s | categories/ExponentialLaws/Law4                           | 0m00.05s || +0m00.03s
0m00.08s | categories/Adjoint/Identity                               | 0m00.07s || +0m00.00s
0m00.08s | categories/GroupoidCategory/Core                          | 0m00.10s || -0m00.02s
0m00.08s | categories/Category/Objects                               | 0m00.09s || -0m00.00s
0m00.08s | categories/NaturalTransformation/Composition              | 0m00.04s || +0m00.04s
0m00.08s | categories/InitialTerminalCategory/Notations              | 0m00.06s || +0m00.02s
0m00.08s | categories/NaturalTransformation                          | 0m00.09s || -0m00.00s
0m00.08s | categories/SetCategory                                    |   N/A    || +0m00.08s
0m00.08s | categories/SetCategory/Functors/SetProp                   |   N/A    || +0m00.08s
0m00.08s | Types/Record                                              | 0m00.10s || -0m00.02s
0m00.08s | categories/NaturalTransformation/Composition/Functorial   | 0m00.09s || -0m00.00s
0m00.08s | categories/Profunctor/Identity                            |   N/A    || +0m00.08s
0m00.08s | categories/GroupoidCategory                               | 0m00.06s || +0m00.02s
0m00.08s | categories/Category/Pi                                    | 0m00.06s || +0m00.02s
0m00.08s | categories/FunctorCategory/Core                           | 0m00.06s || +0m00.02s
0m00.08s | categories/Profunctor/Utf8                                |   N/A    || +0m00.08s
0m00.08s | categories/NaturalTransformation/Core                     | 0m00.06s || +0m00.02s
0m00.07s | categories/Cat                                            | 0m00.06s || +0m00.01s
0m00.07s | categories/SetCategory/Functors                           |   N/A    || +0m00.07s
0m00.07s | hit/Interval                                              | 0m00.06s || +0m00.01s
0m00.07s | categories/Profunctor                                     |   N/A    || +0m00.07s
0m00.07s | categories/ExponentialLaws/Tactics                        | 0m00.06s || +0m00.01s
0m00.07s | categories/InitialTerminalCategory                        | 0m00.06s || +0m00.01s
0m00.07s | coq/Init/Peano                                            | 0m00.10s || -0m00.03s
0m00.07s | categories/Grothendieck                                   |   N/A    || +0m00.07s
0m00.07s | categories/Functor/Pointwise                              | 0m00.04s || +0m00.03s
0m00.07s | categories/Comma/Notations                                | 0m00.07s || +0m00.00s
0m00.07s | hit/TwoSphere                                             | 0m00.09s || -0m00.01s
0m00.07s | categories/Adjoint/Composition/LawsTactic                 | 0m00.07s || +0m00.00s
0m00.06s | categories/Profunctor/Representable                       |   N/A    || +0m00.06s
0m00.06s | Conjugation                                               | 0m00.09s || -0m00.03s
0m00.06s | categories/Category/Sigma                                 | 0m00.06s || +0m00.00s
0m00.06s | categories/Adjoint/Dual                                   | 0m00.09s || -0m00.03s
0m00.06s | Basics/Contractible                                       | 0m00.05s || +0m00.00s
0m00.06s | categories/ExponentialLaws/Law1                           | 0m00.06s || +0m00.00s
0m00.06s | categories/ExponentialLaws/Law3                           | 0m00.06s || +0m00.00s
0m00.06s | categories/InitialTerminalCategory/Core                   | 0m00.07s || -0m00.01s
0m00.06s | categories/CategoryOfGroupoids                            | 0m00.08s || -0m00.02s
0m00.06s | categories/Adjoint/Notations                              | 0m00.08s || -0m00.02s
0m00.06s | categories/NaturalTransformation/Dual                     | 0m00.06s || +0m00.00s
0m00.06s | categories/Category/Univalent                             | 0m00.07s || -0m00.01s
0m00.06s | categories/Structure                                      | 0m00.06s || +0m00.00s
0m00.06s | categories/Category/Notations                             | 0m00.06s || +0m00.00s
0m00.06s | categories/FunctorCategory/Notations                      | 0m00.04s || +0m00.01s
0m00.05s | categories/DiscreteCategory                               | 0m00.05s || +0m00.00s
0m00.05s | coq/Init/Specif                                           | 0m00.04s || +0m00.01s
0m00.05s | categories/Profunctor/Notations                           |   N/A    || +0m00.05s
0m00.05s | categories/ExponentialLaws/Law2                           | 0m00.06s || -0m00.00s
0m00.05s | categories/Category/Subcategory                           | 0m00.05s || +0m00.00s
0m00.05s | hit/IntervalImpliesFunext                                 | 0m00.05s || +0m00.00s
0m00.05s | Types/Empty                                               | 0m00.04s || +0m00.01s
0m00.05s | categories/Functor/Core                                   | 0m00.05s || +0m00.00s
0m00.05s | categories/CategoryOfSections                             | 0m00.04s || +0m00.01s
0m00.05s | categories/Structure/Notations                            | 0m00.05s || +0m00.00s
0m00.05s | categories/Functor/Composition/Core                       | 0m00.03s || +0m00.02s
0m00.05s | categories/Category/Core                                  | 0m00.04s || +0m00.01s
0m00.05s | Tactics/BinderApply                                       | 0m00.05s || +0m00.00s
0m00.05s | NullHomotopy                                              | 0m00.06s || -0m00.00s
0m00.05s | coq/Program/Tactics                                       | 0m00.04s || +0m00.01s
0m00.04s | categories/Adjoint/Core                                   | 0m00.04s || +0m00.00s
0m00.04s | categories/Category/Utf8                                  | 0m00.06s || -0m00.01s
0m00.04s | coq/Init/Datatypes                                        | 0m00.04s || +0m00.00s
0m00.04s | Basics/UniverseLevel                                      | 0m00.04s || +0m00.00s
0m00.04s | Misc                                                      | 0m00.05s || -0m00.01s
0m00.04s | Types                                                     | 0m00.07s || -0m00.03s
0m00.04s | Basics/Pointed                                            | 0m00.04s || +0m00.00s
0m00.04s | coq/Init/Logic_Type                                       | 0m00.04s || +0m00.00s
0m00.04s | Types/Nat                                                 | 0m00.04s || +0m00.00s
0m00.04s | categories/Category/Subcategory/Full                      | 0m00.04s || +0m00.00s
0m00.04s | categories/Structure/Utf8                                 | 0m00.05s || -0m00.01s
0m00.04s | Basics                                                    | 0m00.03s || +0m00.01s
0m00.03s | categories/Functor/Identity                               | 0m00.04s || -0m00.01s
0m00.03s | categories/Category/Subcategory/Wide                      | 0m00.07s || -0m00.04s
0m00.03s | coq/Unicode/Utf8_core                                     | 0m00.02s || +0m00.00s
0m00.03s | coq/Init/Prelude                                          | 0m00.02s || +0m00.00s
0m00.03s | UnivalenceAxiom                                           | 0m00.04s || -0m00.01s
0m00.03s | FunextAxiom                                               | 0m00.02s || +0m00.00s
0m00.02s | coq/Init/Notations                                        | 0m00.01s || +0m00.01s
0m00.02s | categories/Category/Strict                                | 0m00.02s || +0m00.00s
0m00.02s | coq/Unicode/Utf8                                          | 0m00.01s || +0m00.01s
0m00.02s | coq/Init/Logic                                            | 0m00.03s || -0m00.00s
0m00.02s | coq/Bool/Bool                                             | 0m00.02s || +0m00.00s
0m00.02s | coq/Init/Tactics                                          | 0m00.02s || +0m00.00s

NOTE: THIS TIMING DIFF IS FROM AN EARLIER VERSION OF HoTT, AND SHOULD BE
REDONE BEFORE MERGING.

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