Delete minus1Trunc.v, close #434

I didn't write this tactic, I just copied it over from minus1Trunc and
generalized it to any truncation.
On Sep 18, 2014 1:00 AM, "Bas Spitters" <notifications@github.com> wrote:

> In theories/hit/Truncations.v:
>
> > @@ -100,3 +111,23 @@ Coercion truncation_modality : trunc_index >-> Modality.
> >
> >  (** It's sometimes convenient to use "infinity" to refer to the identity modality in a similar way.  This clashes with some uses in higher topos theory, where "oo-truncated" means instead "hypercomplete", but this has not yet been a big problem. *)
> >  Notation oo := identity_modality.
> > +
> > +(** ** A few special things about the (-1)-truncation. *)
> > +
> > +Notation merely := (Trunc -1).
> > +
> > +Definition hexists {X} (P : X -> Type) : Type := merely (sigT P).
> > +
> > +Definition hor (P Q : Type) : Type := merely (P + Q).
> > +
> > +(** ** Tactic to remove truncations in hypotheses if possible. *)
> > +Ltac strip_truncations :=
> > +  (** get the type of the goal *)
>
> I may be overlooking somehting, but this looks quite crude. You just try
> to apply Trunc_rect_nondep as much as possible. I guess we could check
> first whether the goal and the hypothesis have are truncated.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/513/files#r17713814>.
>