Formalize the cumulative hierarchy V (most of §10.5 of the book)

This is joint work with Bas Spitters.
It formalizes exercise 10.11 (the "pushout" definition of V), where we had to slightly modify the induction principle given in the book in order to make it provable (see V_rect').
Then most of section 10.5 is proven (up to theorem 10.5.8).
I agree, I found this description of bullets vs braces somewhat useful.
It should be in the ref man too, but couldn't find it immediately:
http://poleiro.info/posts/2013-06-27-structuring-proofs-with-bullets.html


On Thu, Aug 28, 2014 at 10:45 PM, Jason Gross <notifications@github.com>
wrote:

> In theories/hit/V.v:
>
> > +    (H_eqimg : (forall a : A, hexists (fun (b : B) =>
> > +                  hexists (fun (p:f a = g b) => p # (H_f a) = H_g b)))
> > +             * (forall b : B, hexists (fun (a : A) =>
> > +                  hexists (fun (p:f a = g b) => p # (H_f a) = H_g b))) ),
> > +    (setext' f g eq_img) # (H_set A f H_f) = (H_set B g H_g)
> > +  )
> > +: forall v : V, P v.
> > +Proof.
> > +  apply V_rect with H_set; try assumption.
> > +  intros A B R bitot_R h H_h.
> > +  pose (f := h o inL R : A -> V ).
> > +  pose (g := h o inR R : B -> V ).
> > +  pose (H_f := H_h o inL R : forall a : A, P (f a)).
> > +  pose (H_g := H_h o inR R : forall b : B, P (g b)).
> > +  assert (eq_img : equal_img f g). split.
> > +    intro a. generalize (fst bitot_R a). apply minus1Trunc_map.
>
> It might be nice to use structured braces ({ proof script. }) rather than
> just indentation to mark off separate goals. (This is not a requirement,
> though.)
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/440/files#r16866668>.
>