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 with bitotal


On Thu, Aug 28, 2014 at 10:41 PM, Jason Gross <notifications@github.com>
wrote:

> In theories/hit/V.v:
>
> > +Definition RPushout_comp_nd_glue {A B : Type} (R : A -> B -> hProp)
> > +  (P : Type) (i : A -> P) (j : B -> P)
> > +  (gl : forall (a : A) (b : B) (r : R a b), (i a) = (j b))
> > +  (a : A) (b : B) (r : R a b)
> > +: ap (RPushout_rect_nd R P i j gl) (glue R a b r) = gl a b r.
> > +Proof.
> > +  apply (cancelL (transport_const (glue R a b r) (i a))).
> > +  path_via (apD (RPushout_rect_nd R P i j gl) (glue R a b r)).
> > +  apply (apD_const (RPushout_rect_nd R P i j gl) (glue R a b r))^.
> > +  refine (RPushout_comp_glue (fun _ => P) _ _ _ _ _ _).
> > +Defined.
> > +
> > +
> > +(* ** Bitotal relation ** *)
> > +
> > +Definition bitot {A B : Type} (R : A -> B -> hProp) :=
>
> I'm a fan of not truncating names, so would like to cast a vote in favor
> of bitotal here. I'm not sure if others agree.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/440/files#r16866413>.
>