Delete minus1Trunc.v, close #434

It became one line longer.  That one line is because I changed the definition of `IsSurjection` to be a special case of `IsConnMap`, so that it asserts contractibility of the truncation of the fibers rather than inhabitation.  However, on reflection, the equivalence of that with the simpler definition (in the case -1) should probably be split out into its own lemma.