Define pseudonatural transformations

This is based on an email from Mike Shulman.

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

I'm not at all confident that I got it right, given that
[nCatLab](http://ncatlab.org/nlab/show/pseudonatural+transformation#definition)
mentions three laws rather than just one (respect for composition,
respect for units, and naturality).  But I guess if it gives me enough
rope to define lax comma categories, and if I can show that every
natural transformation between functors to Cat gives rise to a
pseudonatural transformation between the corresponding pseudofunctors, I
might not care?

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