Reindent hit/quotient

I want to use it as an example, so I'd like to have it nicely indented
so that it's clear where the private inductive module ends.

I think this only needs one pair of eyes, because I've only changed formatting (indentation, and also in some places `Definition foo : forall a, B` into `Definition foo a : B`).  I'd like to have this merged in the next few hours, so I can use the [wiki page for quotient](http://hott.github.io/HoTT/proviola-html/HoTT.hit.quotient.html) as an example.