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).
It seems to be related to this, which I am already discussing with
@mattam82:
There is something wrong with the implementation of quotients using private
types.

---
Require Import HoTT.
Require Import quotient.

Definition Type2:=Type.
Definition Type1:=Type:Type2.

Variable A:Type1.
Variable rel :A-> A-> Type2.
Variable relset: setrel rel.

Definition Quot:Type1:= quotient relset.
(* However, this quotient should be in Type2, the maximum of the two types
*).

Perhaps the most straightforward fix would be to provide user syntax
for the max " \/ " of two universes?

Private Inductive quotient (sR:setrel R@{U V}): Type @{U \/ V} :=
  | class_of : (A:Type@{U}) -> quotient sR.


On Thu, Aug 28, 2014 at 10:50 PM, Jason Gross <notifications@github.com>
wrote:

> In theories/hit/V.v:
>
> > +  intro p; exact (transport (fun x => u ~~ x) p (reflexive_bisim u)).
> > +  generalize u v.
> > +  refine (V_rect_hprop _ _ _); intros A f H_f.
> > +  refine (V_rect_hprop _ _ _); intros B g _.
> > +  simpl; intros [H1 H2].
> > +  apply setext'. split.
> > +  - intro a. generalize (H1 a). apply minus1Trunc_map.
> > +    intros [b h]. exists b; exact (H_f a (g b) h).
> > +  - intro b. generalize (H2 b). apply minus1Trunc_map.
> > +    intros [a h]. exists a; exact (H_f a (g b) h).
> > +Defined.
> > +
> > +
> > +(* ** Canonical presentation of V-sets (Lemma 10.5.6) ** *)
> > +
> > +(* Using the regular kernel (with = instead of ~~) also works, but this seems to be a Coq bug, it should lead to a universe inconsistency in the monic_set_present lemma later. This version is the right way to do it. *)
>
> If you think it should lead to an inconsistency, please track down the
> error, or at least make a small example and submit it as a probable bug on
> the bug tracker.
>
> If you have a definition that you think should fail with a universe
> inconsistency, you can replace it with Fail Definition ..., and then call /path/to/coq-bug-finder/find-bug.py
> hit/V.v bug_univ_01.v --topname HoTT --coqc ../hoqc --coqtop ../hoqtop
> <https://github.com/JasonGross/coq-bug-finder> from the theories/
> directory.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/440/files#r16866960>.
>