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).
This one seems small and seems tied to V, so I think it belongs here.


On Thu, Aug 28, 2014 at 10:40 PM, Jason Gross <notifications@github.com>
wrote:

> In theories/hit/V.v:
>
> > +Proof.
> > +  intros H a a' p.
> > +  specialize (H (m a')). unfold hfiber in *.
> > +  assert ((a; p) = (a'; 1) :> {x : A & m x = m a'}) by apply allpath_hprop.
> > +  apply (path_sigma_uncurried (fun x => m x = m a') (a; p) (a'; 1))^-1.
> > +  assumption.
> > +Defined.
> > +
> > +
> > +(* ** Pushout with respect to a relation ** *)
> > +
> > +(* This could be implemented using the pushouts in /hit/Pushout.v, where f and g are the (fst ∘ pr1) and (snd ∘ pr1), with domain {(a,b) : A * B & R a b}. However, these pushouts weren't implemented when I started this work, and doing it this way is closer to exercise 10.11 of the HoTT book *)
> > +
> > +Module Export RPushout.
> > +
> > +Private Inductive RPushout {A B : Type} (R : A -> B -> hProp) : Type :=
>
> What's our custom on hits? Should each hit get it's own specially named
> file, or is it ok to define them inline in other files?
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/440/files#r16866366>.
>