Add an alternative version of functor composition

Also make a folder for functorial functor composition
Define Type0 to mean Set
Prove that pre-comp w/ an ess. surj. functor is ess. surj

Or, without abbreviations, prove that precomposition with an
essentially surjective functor is essentially surjective.

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

Define Type0 to mean Set
Merge pull request #374 from JasonGross/note-quotient-universes

Add a note about the universes of [quotient].
Merge pull request #378 from JasonGross/precomp-ess-surj

Prove that precomposition with an essentially surjective functor is essentially surjective.
Make Empty a Set

It fixes some universe issues.  If you want the [Prop], use [False].
Merge pull request #371 from JasonGross/empty-is-set

Make Empty a Set
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.