Define the proposition IsGroupoid of a precategory

Also define the precategory of strict groupoids.
Make inverse rewrite laws for pseudofunctor

These are slow, but useful for lax comma categories.

Also, split out the rewrite laws into a separate file.

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

Define the proposition IsGroupoid of a precategory
Merge pull request #387 from JasonGross/more-pseudofunctors

Make inverse rewrite laws for pseudofunctor
Add instances for pointedness of suspension
Merge pull request #390 from JasonGross/more-pointed

Add instances for pointedness of suspension
Use NaiveFunext for proving funext_downward_closed

The new version of @mattam82's universe polymorphism isn't as libral
with inductive universes.  So we use NaiveFunext to allow a simpler
transformation of universes.

This is in preparation for switching to Coq trunk, once enough bugs are
fixed.
Merge pull request #391 from JasonGross/funext-down-naive

Use NaiveFunext for proving funext_downward_closed
Stick an aborted definition in a comment

Coq trunk's coqc -time doesn't like it
(https://coq.inria.fr/bugs/show_bug.cgi?id=3332)

Also coqdoc-ify comments
Use [transport] rather than [match] in path_object

This is nicer in HoTT proofs.

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

Stick an aborted definition in a comment
Give nicer HoTT definitions for functor comp. laws

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

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

Give functor composition a more HoTT-style definition, and improving some unfolding behavior
Remove an outdated comment
Make travis test for axiom dependence

Now travis will enforce the convention that nothing in the library
should depend on FunextAxiom or UnivalenceAxiom.
Add some instances about truncation of IsTrunc
Merge pull request #398 from JasonGross/istrunc-instances

Add some instances about truncation of IsTrunc
Merge pull request #397 from JasonGross/check-no-axiom

Make travis test for axiom dependence
Less restrictive Funext_downward_closed

Funext has three universes, and we want them all to be independent; this
seems to be necessary to eliminate universe inconsistencies in the
latest version of trunk.