HoTT/HoTT — pull request #353 by JasonGross (2014-03-31 00:48:18+00:00)
Title: Prove functoriality of comma category construction

At least in its category arguments.

This is the first step in showing that two formulations of (co)limits
are equivalent.

Unfortunately, it's rather slow. Ideas for speeding it up are welcome.

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