Mark the arguments to Equiv projections implicit

This is required for pattern matching on primitive projections to work
(which I hope we'll be moving to soon) (see
https://coq.inria.fr/bugs/show_bug.cgi?id=3503), and also seems nicer;
we generally don't need to talk about the type arguments to [equiv_fun]
and [equiv_isequiv].
Merge pull request #427 from JasonGross/implicit-equiv

Mark the arguments to Equiv projections implicit
Prove [A * (B * C) <~> (A * B) * C]

Make use of the new dependent goals feature to make the proof prettier.
Merge pull request #428 from JasonGross/prod-type-assoc

LGTM. I am merging because it is so small and it does not conflict with other stuff.

Prove [A * (B * C) <~> (A * B) * C]
Use the coq-git ppa on travis

Now that ezyang's ppa works on precise, we can use it rather than
building Coq ourselves; this is about 10 minutes faster on each build.
We keep one test running Coq, to make sure that the pinned version of
Coq can always build the relevant version of the library.
Merge pull request #431 from JasonGross/travis-ppa

Great! Thanks @ezyang!
I am assuming we now have a ppa for Coq trunk.

Use the coq-git ppa on travis
Add format specifiers to notations to remove space

Now things like [p^] will display as [p^] rather than [p ^].  This means
that confusing expressions like [p ^ @ ! x] will be rendered as the less
confusing [p^ @ !x].
Merge pull request #432 from JasonGross/format-notations

Add format specifiers to notations to remove space
How to avoid Emacs prompts about risky local variables
Merge pull request #433 from mikeshulman/lvdoc

How to avoid Emacs prompts about risky local variables
! suffices in newer emacsen
Revert "Use the coq-git ppa on travis"

This reverts commit d17f47f34bc4352d9fa83fb97fa138c99b8d9fb8.

We probably don't actually want the pull requests to show red `x`s
whenever the most recent Coq trunk happens to break some random file in
HoTT.
Merge pull request #436 from JasonGross/revert-travis-ppa

Revert "Use the coq-git ppa on travis"

In case anyone's interested, in this case, the bug is https://coq.inria.fr/bugs/show_bug.cgi?id=3545.
Add Utf8 notations in a separate file
Add notation <>, add Utf8 notations from stdlib
Replace BULLET OPERATOR (∙) with BULLET (•)

Apparently, Emacs' built-in `tex` mode can do BULLET (`\bu` in
agda-mode), but not BULLET OPERATOR (`\.` in agda-mode).
Add an error message about BULLET OPERATOR

E.g., So that people coming from HoTT-Agda are less confused when using
agda-mode input.
Add unicode instructions
Merge pull request #376 from JasonGross/utf8-notations

Utf8 notations
Add reflexive subuniverse theory