Initial commit of quotients starting from a file from @SkySkimmer.
Adding Quotients
Adding Global Instances
Removing dead code
Cleaning up quotients
Merge pull request #193 from spitters/master

Adding Quotients
Prove Admitted theorems in types.ObjectClassifier

They are not very pretty, but they are no longer admits.  This is
partial work on #195.
Add a theorem with issig equivalence about hProps
Fix grammar

As per
http://www.quickanddirtytips.com/education/grammar/which-versus?page=all
Use AS_IF rather than 'if', uniformize more things
Check for usr/bin/time in configure
./autogen.sh
Autobuild documentation with travis

Now that we have a `make html` target, we can make the html
automatically on travis.  If travis builds something which is the same
as origin's master, then we autocommit updated documentation and push to
the gh-pages branch, where documentation is accessible at
http://hott.github.io/HoTT/coqdoc-html/.

Generating the files was a pain.  I record the process here, so that if
we need to update the keys, there will be a reference.

First, generate the keys that will be used
```bash
$ ROOT="$(git rev-parse --show-toplevel)"
$ ssh-keygen -t rsa -C "Travis-CI-bot@travis.fake" -f "$(readlink -f "$ROOT"/etc/ci/id_rsa)"
```
When it prompts you for a passphrase, you must leave it blank.

Then add the contents of "$ROOT"/etc/ci/id_rsa.pub as a deploy key to
the HoTT repository at https://github.com/HoTT/HoTT/settings/keys.

Now, following a modified version of
http://about.travis-ci.org/docs/user/travis-pro/#How-can-I-encrypt-files-that-include-sensitive-data%3F,
encrypt the id_rsa file:
```bash
$ password=`cat /dev/urandom | head -c 10000 | openssl sha1`
$ openssl aes-256-cbc -k "$password" -in "$ROOT"/etc/ci/id_rsa -out "$ROOT"/etc/ci/id_rsa.enc -a
```
Now, the hard part (at least if you don't have sudo). Hope that you
either have ruby and gem installed, or a version of ssh-keygen which
supports the `-e -m` flag combination (check with `ssh-keygen -\?`).  If
you have ruby and gem, then you can follow
http://about.travis-ci.org/docs/user/encryption-keys/, and run
```bash
$ gem install travis
$ travis encrypt -r HoTT/HoTT "SSHKEY_PASSWORD=$password"
```
and update the `secure:` part of the `.travis.yml` file with the resulting
secret.  Otherwise, you can follow
http://about.travis-ci.org/docs/user/travis-pro/#How-can-I-encrypt-files-that-include-sensitive-data%3F
and run
```bash
$ \curl https://api.travis-ci.org/repos/HoTT/HoTT/key | perl -pe 's/^{"key"://; s/^"//; s/"}$//' | sed s'/\\n/\n/g' > id_travis.pub
$ ssh-keygen -e -m PKCS8 -f id_travis.pub > id_travis.pub.pem
$ echo "SSHKEY_PASSWORD='$password'" | openssl rsautl -encrypt -pubin -inkey id_travis.pub.pem
```
However, if `ssh-keygen` fails, complaining about `-m` being
unrecognized, then you must clone or copy
https://gist.github.com/thwarted/1024558
(https://gist.github.com/1024558.git), install the required python
dependencies (for me, pyasn1), and then run that on `id_travis.pub` to
get the `id_travis.pub.pem` file, and then run the `openssl rsautl`
commmand.  Either way, the output of that third command should be placed
in the `.travis.yml` file, replacing the existing secret.

Perhaps we should include these instructions somewhere in the
repository?
Use OAuth instead of ssh to autogen doc on travis

This is a much simpler way of doing things.

Now that we have a `make html` target, we can make the html
automatically on travis.  If travis builds something which is the same
as origin's master, then we autocommit updated documentation and push to
the gh-pages branch, where documentation is accessible at
http://hott.github.io/HoTT/coqdoc-html/.

Generating the files was much less of a pain.  I record the process
here, so that if we need to update the keys, there will be a reference.

First, generate the OAuth token that will be used, replacing
'<username>' with your username.  You must have permission to push to
HoTT/HoTT.
```bash
$ TOKEN="$(curl -u '<username>' -d '{"scopes":["repo"],"note":"For Travis-CI Bot"}' https://api.github.com/authorizations | grep -o 'token": "[^"]*' | sed s'/token": "//g')"
```
It will prompt you for your password.

Now, the hard part (at least if you don't have sudo). Hope that you
either have ruby and gem installed, or a version of ssh-keygen which
supports the `-e -m` flag combination (check with `ssh-keygen -\?`).  If
you have ruby and gem, then you can follow
http://about.travis-ci.org/docs/user/encryption-keys/, and run
```bash
$ gem install travis
$ travis encrypt -r HoTT/HoTT "OAUTH_TOKEN=$TOKEN"
```
and update the `secure:` part of the `.travis.yml` file with the resulting
secret.  Otherwise, you can follow
http://about.travis-ci.org/docs/user/travis-pro/#How-can-I-encrypt-files-that-include-sensitive-data%3F
and run
```bash
$ \curl https://api.travis-ci.org/repos/HoTT/HoTT/key | perl -pe 's/^{"key"://; s/^"//; s/"}$//' | sed s'/\\n/\n/g' > id_travis.pub
$ ssh-keygen -e -m PKCS8 -f id_travis.pub > id_travis.pub.pem
$ echo "OAUTH_TOKEN=$TOKEN" | openssl rsautl -encrypt -pubin -inkey id_travis.pub.pem
```
However, if `ssh-keygen` fails, complaining about `-m` being
unrecognized, then you must clone or copy
https://gist.github.com/thwarted/1024558
(https://gist.github.com/1024558.git), install the required python
dependencies (for me, pyasn1), and then run that on `id_travis.pub` to
get the `id_travis.pub.pem` file, and then run the `openssl rsautl`
commmand.  Either way, the output of that third command should be placed
in the `.travis.yml` file, replacing the existing secret.

Perhaps we should include these instructions somewhere in the
repository?
Auto-push autoreconf stuff

Now travis will run autoreconf -fvi for us, and push it to
master-with-autoreconf-files.
Also build without autoreconf

We don't want the build to fail on a machine without autoreconf.
Update autogen.sh to get files from git

But only if we don't have autoreconf.
Update INSTALL.txt to mention autogen.sh
Merge pull request #197 from JasonGross/hProp-theorem

Add a theorem with issig equivalence about hProps
Merge pull request #196 from JasonGross/remove-admitted-objclassifier

Prove Admitted theorems in types.ObjectClassifier