Improve presentation of old issig tactics

I found a way to build issig tactics which are two orders of magnitude
faster than the very old ones (which did not adjointify), but which keep
all do not adjust the sections and retractions.  The key is to apply
symmetry, so that we destruct a record rather than a sigma type.
However, the adjointifying versions are still an order of magnitude or
two faster than these versions, so we use the adjointifying ones by
default.

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

This closes #46.  Unfortunately, the typeclass glue won't work very
well until we migrate to the polyproj branch of HoTT/coq, because
typeclass resolution currently doesn't take into account universe
inconsistencies, so we'd need to explicitly provide two instances of
univalence to this theorem in order to use it.
Do exercise 6.9, add some minor lemmas about pointed types

The pointed types lemmas are in preparation for some other 6 exercises.
Define Modality, prove that double negation is one
Merge pull request #336 from JasonGross/ex-6-9-pointed

Do exercise 6.9, add some minor lemmas about pointed types
Prove Theorem 7.2.2 from the book

I chose to use the first proof because I couldn't find 4.7.7 already in
the library.  I didn't use [dpath_forall] (which HoTTBook.v tells me is
2.9.6) because that requires [Funext], and this lemma doesn't need it.
Merge pull request #347 from JasonGross/thm-7-2-2

Prove Theorem 7.2.2 from the book
Add a dependent version of minus1Trunc_map
Do Exercise 7.1 from the book
Formalize the "notion of a structure"

Hopefully we'll soon be moving to polyproj, where I hope we won't have
to deal with this nonsense of defining simple record types for speed of
[destruct].

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

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

Structure identity principle
Add many variants of the [simpl rewrite] tactic

It's unfortunate that Coq doesn't give us a notation of saying "this
takes anything that rewrite can take".  But these are useful for
making tactic scripts conceptually clearer.
Add some theorems about equivalence of equiv and iso in set_cat
Use a debian repository for HoTT/coq

Edward Yang (@ezyang) helpfully packaged HoTT/coq a while back.  The
category theory is getting slow enough that the build that generates the
html periodically fails, and I have to kick travis.  This should buy us
another 5-10 minutes.

Also install libcoq-ocaml-dev
Add the -no-native-compiler argument to coqtop

It's required for a Coq built without that argument to not complain
about various things.
Merge pull request #351 from JasonGross/ex-7-1

Exercise 7.1
I am merging as this is a small change which does not seem very critical.
Please let me know if this is too quick.
Merge pull request #355 from JasonGross/more-rewrite

Add many variants of the [simpl rewrite] tactic

Merging, this seems like harmless notation.