Merge pull request #256 from andrejbauer/master

A number of changes to configuration
Merge pull request #263 from marcbezem/master

Added links for Section 2.3 in contrib/HoTTBook.v

I am going ahead without a second pair of eyes, as it only affects contrib/HoTTBook.v
Comment out a line so the HoTT book might compile

I wasn't sure whether or not it was an answer or a misplaced theorem or
what.  So I just commented it out.
Add contrib/.dir-locals.el for emacs
Fix a typo
Add a target to cover the HoTT book
Merge pull request #265 from JasonGross/add-hott-book-target

Add hott book target
Only use two threads

Hopefully this will cut down on spurious failures
Fix contrib paths
Port NaturalTransformaion/Pointwise

After    | File Name                                                | Before
------------------------------------------------------------------------------
5m30.92s | Total                                                    | 5m29.40s
------------------------------------------------------------------------------
0m33.71s | categories/Adjoint/Composition/AssociativityLaw          | 0m33.59s
0m27.12s | categories/Comma/Dual                                    | 0m27.89s
0m17.79s | categories/ExponentialLaws/Law4/Functors                 | 0m18.02s
0m16.76s | categories/Adjoint/UnitCounitCoercions                   | 0m17.15s
0m13.34s | hit/Flattening                                           | 0m13.80s
0m12.14s | categories/Adjoint/Composition/Core                      | 0m11.76s
0m11.96s | categories/Adjoint/Dual                                  | 0m12.04s
0m10.97s | categories/Comma/InducedFunctors                         | 0m10.27s
0m10.87s | categories/Adjoint/Composition/IdentityLaws              | 0m10.31s
0m09.71s | categories/Functor/Pointwise/Properties                  | 0m09.73s
0m08.49s | categories/Functor/Prod/Universal                        | 0m08.16s
0m08.47s | categories/GroupoidCategory/Morphisms                    | 0m08.07s
0m08.36s | categories/ExponentialLaws/Law1/Law                      | 0m08.13s
0m07.58s | hit/Connectedness                                        | 0m07.60s
0m06.74s | categories/UniversalProperties                           | 0m06.62s
0m06.69s | categories/Adjoint/Paths                                 | 0m06.42s
0m06.01s | categories/Functor/Paths                                 | 0m05.78s
0m05.88s | categories/Functor/Sum                                   | 0m05.78s
0m05.82s | categories/Category/Morphisms                            | 0m06.10s
0m05.74s | categories/Adjoint/UnitCounit                            | 0m05.65s
0m05.04s | EquivalenceVarieties                                     | 0m05.37s
0m04.79s | categories/ExponentialLaws/Law2/Functors                 | 0m05.12s
0m04.25s | categories/Category/Sigma/OnMorphisms                    | 0m04.21s
0m03.78s | types/ObjectClassifier                                   | 0m03.61s
0m03.58s | categories/ProductLaws                                   | 0m03.68s
0m02.98s | types/Sigma                                              | 0m02.85s
0m02.77s | categories/Adjoint/UniversalMorphisms                    | 0m02.81s
0m02.76s | categories/Functor/Prod/Functorial                       | 0m02.85s
0m02.62s | categories/FunctorCategory/Functorial                    | 0m02.61s
0m02.57s | Equivalences                                             | 0m02.52s
0m02.40s | categories/Functor/Attributes                            | 0m02.33s
0m02.34s | categories/Category/Sum                                  | 0m02.13s
0m02.18s | categories/Category/Sigma/Core                           | 0m02.21s
0m01.97s | categories/NaturalTransformation/Dual                    | 0m01.96s
0m01.86s | PathGroupoids                                            | 0m02.06s
0m01.84s | categories/HomFunctor                                    | 0m01.83s
0m01.71s | categories/FunctorCategory/Morphisms                     | 0m01.76s
0m01.68s | categories/NaturalTransformation/Composition/Laws        | 0m01.67s
0m01.67s | categories/Comma/Core                                    | 0m01.53s
0m01.61s | categories/NaturalTransformation/Paths                   | 0m01.76s
0m01.43s | categories/Category/Sigma/OnObjects                      | 0m01.38s
0m01.34s | categories/Category/Prod                                 | 0m01.33s
0m01.33s | categories/NaturalTransformation/Composition/Core        | 0m01.32s
0m01.30s | categories/NaturalTransformation/Pointwise               |   N/A
0m01.28s | types/Prod                                               | 0m01.28s
0m01.21s | categories/NaturalTransformation/Composition/Functorial  | 0m01.52s
0m01.15s | categories/Functor/Pointwise                             | 0m01.34s
0m01.07s | hit/Spheres                                              | 0m00.94s
0m01.06s | categories/Limits/Limits                                 | 0m01.11s
0m01.00s | categories/ExponentialLaws/Law  N/A                      | 0m00.97s
0m00.96s | categories/ExponentialLaws/Law1/Functors                 | 0m01.12s
0m00.95s | categories/NaturalTransformation/Prod                    | 0m01.01s
0m00.91s | categories/Functor/Prod                                  | 0m00.87s
0m00.89s | types/Paths                                              | 0m00.86s
0m00.86s | hit/epi                                                  | 0m00.93s
0m00.82s | categories/Functor/Composition/Functorial                | 0m00.82s
0m00.78s | Trunc                                                    | 0m00.82s
0m00.74s | types/Universe                                           | 0m00.64s
0m00.66s | categories/KanExtensions/KanExtensions                   | 0m00.68s
0m00.66s | categories/InitialTerminalCategory                       | 0m00.67s
0m00.62s | Functorish                                               | 0m00.48s
0m00.58s | types/Sum                                                | 0m00.60s
0m00.57s | categories/NaturalTransformation/Sum                     | 0m00.60s
0m00.56s | categories/Comma/Projection                              | 0m00.56s
0m00.55s | hit/Suspension                                           | 0m00.44s
0m00.51s | types/Record                                             | 0m00.51s
0m00.51s | hit/quotient                                             | 0m00.52s
0m00.50s | categories/ExponentialLaws/Law3/Functors                 | 0m00.44s
0m00.49s | hit/Circle                                               | 0m00.51s
0m00.46s | categories/categories                                    | 0m00.45s
0m00.45s | categories/Functor/Composition/Laws                      | 0m00.53s
0m00.44s | HSet                                                     | 0m00.38s
0m00.44s | types/Forall                                             | 0m00.45s
0m00.41s | Tactics                                                  | 0m00.40s
0m00.40s | Fibrations                                               | 0m00.36s
0m00.38s | HProp                                                    | 0m00.42s
0m00.36s | categories/Cat/Core                                      | 0m00.36s
0m00.33s | categories/Functor/Dual                                  | 0m00.32s
0m00.32s | categories/Functor/Functor                               | 0m00.37s
0m00.31s | TruncType                                                | 0m00.33s
0m00.30s | hit/minus1Trunc                                          | 0m00.33s
0m00.29s | categories/NaturalTransformation/Identity                | 0m00.29s
0m00.28s | categories/ExponentialLaws/ExponentialLaws               | 0m00.28s
0m00.28s | categories/IndiscreteCategory                            | 0m00.30s
0m00.28s | categories/Cat/Morphisms                                 | 0m00.28s
0m00.26s | categories/Category/Objects                              | 0m00.23s
0m00.26s | Misc                                                     | 0m00.31s
0m00.23s | categories/Adjoint/Adjoint                               | 0m00.19s
0m00.23s | categories/Utf8                                          | 0m00.27s
0m00.22s | Conjugation                                              | 0m00.22s
0m00.22s | categories/Functor/Composition/Core                      | 0m00.23s
0m00.22s | hit/iso                                                  | 0m00.16s
0m00.21s | categories/NatCategory                                   | 0m00.20s
0m00.21s | types/Arrow                                              | 0m00.26s
0m00.21s | categories/Notations                                     | 0m00.18s
0m00.20s | categories/Functor/Prod/Prod                             | 0m00.19s
0m00.19s | categories/NaturalTransformation/NaturalTransformation   | 0m00.19s
0m00.18s | categories/Category/Core                                 | 0m00.13s
0m00.18s | categories/SetCategory/Functors/Functors                 | 0m00.22s
0m00.17s | FunextVarieties                                          | 0m00.18s
0m00.17s | categories/NaturalTransformation/Notations               | 0m00.13s
0m00.17s | categories/FunctorCategory/FunctorCategory               | 0m00.16s
0m00.16s | categories/GroupoidCategory/Core                         | 0m00.17s
0m00.16s | categories/ExponentialLaws/Law3/Law3                     | 0m00.16s
0m00.16s | categories/Cat/Cat                                       | 0m00.16s
0m00.16s | categories/SetCategory/Core                              | 0m00.14s
0m00.16s | categories/NaturalTransformation/Composition/Composition | 0m00.12s
0m00.16s | categories/FunctorCategory/Core                          | 0m00.19s
0m00.16s | categories/NaturalTransformation/Core                    | 0m00.14s
0m00.15s | HoTT                                                     | 0m00.12s
0m00.15s | categories/Adjoint/Utf8                                  | 0m00.15s
0m00.15s | categories/Adjoint/Composition/Composition               | 0m00.15s
0m00.15s | categories/Profunctor/Core                               | 0m00.17s
0m00.15s | categories/Category/Dual                                 | 0m00.20s
0m00.15s | categories/Category/Sigma/Sigma                          | 0m00.13s
0m00.15s | Overture                                                 | 0m00.13s
0m00.15s | hit/unique_choice                                        | 0m00.18s
0m00.14s | categories/Comma/Comma                                   | 0m00.16s
0m00.14s | categories/FunctorCategory/Utf8                          | 0m00.14s
0m00.14s | categories/Functor/Utf8                                  | 0m00.17s
0m00.14s | categories/Functor/Notations                             | 0m00.14s
0m00.14s | hit/Interval                                             | 0m00.11s
0m00.14s | types/Bool                                               | 0m00.14s
0m00.14s | categories/ExponentialLaws/Law1/Law1                     | 0m00.16s
0m00.14s | categories/Functor/Composition/Composition               | 0m00.12s
0m00.13s | categories/Comma/Notations                               | 0m00.16s
0m00.13s | categories/Category/Category                             | 0m00.18s
0m00.13s | categories/Profunctor/Notations                          | 0m00.10s
0m00.13s | types/Unit                                               | 0m00.12s
0m00.13s | coq/Init/Peano                                           | 0m00.12s
0m00.13s | categories/ExponentialLaws/Law2/Law2                     | 0m00.15s
0m00.13s | categories/NaturalTransformation/Utf8                    | 0m00.13s
0m00.13s | categories/FunctorCategory/Notations                     | 0m00.14s
0m00.13s | categories/Adjoint/Notations                             | 0m00.15s
0m00.13s | categories/Category/Univalent                            | 0m00.11s
0m00.13s | categories/Profunctor/Utf8                               | 0m00.11s
0m00.12s | categories/GroupoidCategory/GroupoidCategory             | 0m00.12s
0m00.12s | categories/Category/Subcategory/Wide                     | 0m00.08s
0m00.12s | hit/Truncations                                          | 0m00.12s
0m00.12s | categories/ExponentialLaws/Law4/Law4                     | 0m00.13s
0m00.11s | categories/Comma/Utf8                                    | 0m00.13s
0m00.11s | categories/Adjoint/Identity                              | 0m00.13s
0m00.11s | categories/Functor/Pointwise/Pointwise                   | 0m00.12s
0m00.11s | categories/Adjoint/Composition/LawsTactic                | 0m00.15s
0m00.11s | categories/Profunctor/Profunctor                         | 0m00.12s
0m00.10s | categories/DiscreteCategory                              | 0m00.12s
0m00.10s | categories/Adjoint/Core                                  | 0m00.11s
0m00.10s | categories/Category/Utf8                                 | 0m00.10s
0m00.10s | Contractible                                             | 0m00.11s
0m00.10s | categories/Profunctor/Representable                      | 0m00.10s
0m00.10s | categories/Category/Notations                            | 0m00.13s
0m00.10s | categories/Profunctor/Identity                           | 0m00.12s
0m00.10s | categories/Functor/Core                                  | 0m00.09s
0m00.09s | categories/Category/Subcategory/Subcategory              | 0m00.12s
0m00.09s | Pointed                                                  | 0m00.07s
0m00.09s | categories/Category/Subcategory/Full                     | 0m00.09s
0m00.09s | types/Empty                                              | 0m00.09s
0m00.08s | categories/Category/Strict                               | 0m00.06s
0m00.07s | categories/SetCategory/SetCategory                       | 0m00.11s
0m00.07s | categories/Functor/Identity                              | 0m00.08s
0m00.07s | coq/Init/Specif                                          | 0m00.06s
0m00.07s | UnivalenceAxiom                                          | 0m00.12s
0m00.06s | coq/Init/Datatypes                                       | 0m00.06s
0m00.06s | FunextAxiom                                              | 0m00.04s
0m00.05s | coq/Init/Prelude                                         | 0m00.05s
0m00.05s | coq/Init/Logic_Type                                      | 0m00.06s
0m00.05s | coq/Init/Logic                                           | 0m00.04s
0m00.05s | coq/Program/Tactics                                      | 0m00.05s
0m00.03s | coq/Init/Notations                                       | 0m00.04s
0m00.03s | coq/Bool/Bool                                            | 0m00.04s
0m00.03s | coq/Init/Tactics                                         | 0m00.02s
Add documentation to Adjoint.Pointwise
Merge pull request #266 from JasonGross/natural-transformation-pointwise

Port NaturalTransformaion/Pointwise
Improve travis scripts

Now we will always build html, even on pull requests, and the checking
for whether or not to push is more robust.
Cut out contrib. in html paths

Proviola was picking up the wrong path for the HoTT book.
Improved contrib/HoTTBook.v and etc/Book.py, close #272

The `HoTTBook.v` file now contains coqdoc comments.
Merge pull request #273 from andrejbauer/master

Improved contrib/HoTTBook.v and etc/Book.py, close #272
unclear what I changed
Merge branch 'master' of https://github.com/HoTT/HoTT

Conflicts:
	contrib/HoTTBook.v