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).
Agreed.


On Sun, Aug 31, 2014 at 9:44 PM, Jason Gross <notifications@github.com>
wrote:

> In theories/hit/V.v:
>
> > +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) :=
> > +     (match v with
> > +      | set A f => fun _ _ => H_set A f (fun a => F (f a))
> > +     end) H_setext H_0trunc.
> > +
> > +Axiom V_comp_setext : forall (P : V -> Type)
>
> Perhaps it would be better to define it in terms of is0trunc_V, outside
> of the module, with a comment on the inside saying that we don't need to
> axiomatize the computation rule because it's automatic, but it's defined
> outside for regularity?
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/440/files#r16936534>.
>