Fix the universes of some HITs; add a check file

Susp X is now in the same universe as X.

This is verified in the Tests.v file.

This closes #369.

It's possible we should fix the universes of quotients, but this will be
trickier.  In trunk-polyproj, we can do it like this:

```coq
Section Domain.
Let U := Type.
(** We need a universe level that is not lower than [U], but doesn't
need to be the same. *)
Let U' : Type.
Proof.
  let U' := constr:(Type) in
  let U_le_U' := constr:(fun x : U => (x : U')) in
  exact U'.
Defined.
Context {A : Type} {R:A -> A -> U} {sR:setrel R}.

Inductive quotient (sR:setrel R): U' :=
 | class_of : A -> quotient sR.
```

But in HoTT/coq, this gives "Error: No such section variable or
assumption: U'." at `End Domain.` (see
https://github.com/HoTT/coq/issues/116).
Merge pull request #370 from JasonGross/fix-universes

Fix the universes of some HITs; add a check file
Remove a natural language tactic

Discussion on
https://github.com/JasonGross/HoTT/commit/7f6d4cfe2c0213e83cd3486286ca1ff1e7e4b1dd:

spitters added a note 7 hours ago
Why this pun ?

JasonGross added a note 2 hours ago
I figured that anyone wanting to mirror proofs in the book ~verbatim
might appreciate this tactic, (or maybe it should be Tactic Notation
"Since" "the" "goal" "is" "a" "mere" "proposition," "we" "may" "strip"
"truncations"). I could probably get it even closer, if there's actually
an interest here, so that you could write Since our goal is a mere
proposition, we may assume given a : A and H : P a. and have it find a
truncated thing of type { a : A | P a} and give you back a hypothesis a
: A and a hypothesis H : P a.

Bas Spitters
But why experiment with natural language only in an isolated place ?
Don't you think that one experiment (HoTT) is enough ?

JasonGross added a note 16 minutes ago
I think I was actually originally going to call it the longer name, and
later shortened it, but figured I'd leave in the longer one as well.

HoTT might be enough of an experiment, though I tend to like
experimenting with everything I can. Shall I go remove the pun? (It
doesn't matter much either way to me.)

spitters added a note 15 minutes ago
I prefer somewhat controlled experiments :-)
Merge pull request #379 from JasonGross/remove-natural-language-pun

Remove a natural language tactic
Updating timing scripts to explicitly show changes
Add [forall]/pi categories (indexed product categories)

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

Fix documentation of NaturalTransformation.v
Define pseudonatural transformations

This is based on an email from Mike Shulman.

Compared with the pain of pseduofunctors, this one is (comparatively)
lacking in pain.

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

Pseudonatural transformation
Document eta-expansion workaround for Empty : Set

I thought I had pushed this before (see
https://github.com/HoTT/HoTT/pull/371#issuecomment-41201465).  But I
guess no.
Make lift and lower transparent

The reason to make them opaque was purely for typeclasses.  They will
need to be transparent when we move to trunk-polyproj, to get an
alternate version of Funext_downward_closed to work correctly.
Give a better error message on a tactic
Merge pull request #386 from JasonGross/transparent-lift-lower

Make lift and lower transparent
Add an instance about [idtoiso] and [components_of]
Add some typeclass resolution hints for apply being stupid

[apply] doesn't know that, e.g., the identity functor applied to x is
x, nor vice-versa.  And because it infers arguments in the "wrong"
order, it errors before it has a chance to pick up that information.
So we need to help it along a little.
Fix timing files to deal with negative times
Add some lemmas and tactics for removing isos

This is the main tactic used to prove that lax comma categories are
precategories.  Unfortunately, it's sometimes rather slow.  It could
probably benefit from reflective automation.

This closes #383
Vastly simplify the helper-tactics in Category/Morphisms.v

We don't actually need all of those; I was being stupid with
associativity.
Add some helper lemmas about [commutes]