Work around bug 3424 in trunk

https://coq.inria.fr/bugs/show_bug.cgi?id=3424

Current code gives error:

Toplevel input, characters 7-13:
Error: In environment
A : Type
a : A
b : A
H' : IsHSet A
Unable to unify "Contr_internal (?194 = ?195)" with
 "forall x y : ?14,
  (fix IsTrunc_internal (n : trunc_index) (A : Type) {struct n} :
   Type :=
     match n with
     | minus_two => Contr_internal A
     | trunc_S n' => forall x0 y0 : A, IsTrunc_internal n' (x0 = y0)
     end) minus_two (x = y)".
Work around a universe problem in trunk
Work around bug 3319 in trunk

https://coq.inria.fr/bugs/show_bug.cgi?id=3319

The error with the old code is:

Toplevel input, characters 154-156:
Error:
In environment
X : PreCategory
P : NotionOfStructure X
xa : @sigT (obj X) (@structure X ?25)
yb : @sigT (obj X) (@structure X ?25)
The term "xa" has type "@sigT (obj X) (@structure X ?25)"
while it is expected to have type
 "@sigT (obj X) (fun x : obj X => @structure X P x)".
Work around bug 3425 in trunk

https://coq.inria.fr/bugs/show_bug.cgi?id=3425
Work around bug 3419 in trunk

https://coq.inria.fr/bugs/show_bug.cgi?id=3419

Current error:

Toplevel input, characters 606-612:
Error:
In environment
A : Type
P : A -> Type
u : {x : _ & P x}
v : {x : _ & P x}
pq : {p : u .1 = v .1 & transport P p u .2 = v .2}
p : u .1 = v .1
q : transport P p u .2 = v .2
x : A
y : P x
x' : A
y' : P x'
p1 : ?73 = ?74
q1 : transport ?69 p1 (x; y) .2 = (x'; y') .2
y'0 : ?96 ?73
q2 : transport ?96 idpath y = y'0
The term "idpath" has type "(x; y) = (x; y)"
while it is expected to have type "(x; y) = (?73; ?103)"
(cannot instantiate "?73" because "x" is not in its scope: available
arguments are "A" "P" "u" "v" "pq" "p" "q" "(x; y)"
"(x'; y')").
Work around bug/HO unification change 3420 in trunk

https://coq.inria.fr/bugs/show_bug.cgi?id=3420

Current error:

Toplevel input, characters 414-425:
Error:
In environment
X : Type
A : X -> Type
P : forall x : X, A x -> Type
h : {f : forall x : X, A x & forall x : X, P x (f x)}
The term "eta_sigma ?53" has type "(projT1 ?53; projT2 ?53) = ?53"
while it is expected to have type
 "(fun x : X => projT1 (sigT_corect_uncurried P h x);
  fun x : X => projT2 (sigT_corect_uncurried P h x)) = h".
Work around trunk having dependent goals

Since [instantiate (n := ...)] is deprecated in trunk, we shouldn't use
it.