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 think they are equivalent. Fixpoint seems somewhat cleaner.


On Sun, Aug 31, 2014 at 9:33 PM, Mike Shulman <notifications@github.com>
wrote:

> In theories/hit/V.v:
>
> > +
> > +Axiom setext : forall {A B : Type} (R : A -> B -> hProp)
> > +  (bitot_R : bitotal R) (h : RPushout R -> V),
> > +set (h o (inL R)) = set (h o (inR R)).
> > +
> > +Axiom is0trunc_V : IsTrunc 0 V.
> > +
> > +Definition V_rect (P : V -> Type)
> > +  (H_0trunc : forall v : V, IsTrunc 0 (P v))
> > +  (H_set : forall (A : Type) (f : A -> V) (H_f : forall a : A, P (f a)), P (set f))
> > +  (H_setext : forall (A B : Type) (R : A -> B -> hProp) (bitot_R : bitotal R)
> > +    (h : RPushout R -> V) (H_h : forall x : RPushout R, P (h x)),
> > +    (setext R bitot_R h) # (H_set A (h o inL R) (H_h oD inL R))
> > +      = H_set B (h o inR R) (H_h oD inR R) )
> > +: forall v : V, P v
> > +:= fix F (v : V) :=
>
> Is there a reason to write Definition ... := fix rather than Fixpoint ...?
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/440/files#r16936480>.
>