various results requested by Matthieu

    =============================================================================
    make SHARING=no
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    Time Timeout 50 exact (Eqn X T_ob T_el).
    Finished transaction in 4.645 secs (4.639u,0.004s)
    }
    exists k'.
    intros k.
    apply El.mor_equality.
    exact (Uniqueness X (pr1 T) (pr1 k) (pr1 k')
		   (fun i => (apevalsecat i (pr2 k)) @ ! (apevalsecat i (pr2 k')))).
    Defined.
    End Product.
    End Ab.
    8.95 sec, 1431388160 bytes: Categories
    =============================================================================
    -*- mode: compilation; default-directory: "~/src/HoTT/Ktheory/src/" -*-
    Comint started at Thu Jan 30 18:56:59

    make SHARING=yes
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    Time Timeout 50 exact (Eqn X T_ob T_el).
    File "./Categories.v", line 857, characters 25-65:
    Timeout!
    Command exited with non-zero status 1
    52.07 sec, 1603158016 bytes: Categories
    =============================================================================
    make SHARING=no
    "coqdep" -c -R . Ktheory "Categories.v" > "Categories.v.d" || ( RV=$?; rm -f "Categories.v.d"; exit ${RV} )
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    Time Timeout 50 exact (Eqn X T_ob T_el).
    Finished transaction in 4.659 secs (4.653u,0.004s)
    }
    admit.
    Defined.
    End Product.
    End Ab.
    8.30 sec, 1425031168 bytes: Categories
    =============================================================================
    make SHARING=no
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    Time Timeout 50 exact (Eqn X T_ob T_el).
    Finished transaction in 4.611 secs (4.606u,0.004s)
    }
    abstract (
	  exists k'; intros k;
	  apply El.mor_equality;
	  exact (Uniqueness X (pr1 T) (pr1 k) (pr1 k')
		   (fun i => (apevalsecat i (pr2 k)) @ ! (apevalsecat i (pr2 k')))) ).
    Defined.
    End Product.
    End Ab.
    9.25 sec, 1429291008 bytes: Categories
    =============================================================================
    make SHARING=no
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    simpl.
    Time Timeout 50 exact (Eqn X T_ob T_el).
    Finished transaction in 4.676 secs (4.671u,0.004s)
    }
    admit.
    Defined.
    End Product.
    End Ab.
    8.31 sec, 1422262272 bytes: Categories
    =============================================================================
    make SHARING=yes
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    simpl.
    Time Timeout 50 exact (Eqn X T_ob T_el).
    File "./Categories.v", line 857, characters 32-72:
    Timeout!
    Command exited with non-zero status 1
    52.02 sec, 1599225856 bytes: Categories
    =============================================================================
    make SHARING=yes
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    simpl.
    admit.
    }
    admit.
    Defined.
    End Product.
    End Ab.
    2.18 sec, 1383694336 bytes: Categories
    =============================================================================
    make SHARING=no
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    simpl.
    admit.
    }
    admit.
    Defined.
    End Product.
    End Ab.
    1.33 sec, 1373143040 bytes: Categories
    =============================================================================
    make SHARING=no
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    simpl.
    Time Timeout 50 abstract exact (Eqn X T_ob T_el).
    Finished transaction in 7.007 secs (6.996u,0.009s)
    }
    admit.
    Defined.
    End Product.
    End Ab.
    10.67 sec, 1443905536 bytes: Categories
    =============================================================================
    make SHARING=yes
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    simpl.
    Time Timeout 50 abstract exact (Eqn X T_ob T_el).
    File "./Categories.v", line 860, characters 8-57:
    Timeout!
    Command exited with non-zero status 1
    52.04 sec, 1599307776 bytes: Categories
    =============================================================================
    make SHARING=no
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    Time Timeout 50 abstract (simpl; exact (Eqn X T_ob T_el)).
    Finished transaction in 6.998 secs (6.991u,0.007s)
    }
    admit.
    Defined.
    End Product.
    End Ab.
    10.65 sec, 1445986304 bytes: Categories
    =============================================================================
    make SHARING=yes
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    Time Timeout 50 abstract (simpl; exact (Eqn X T_ob T_el)).
    File "./Categories.v", line 859, characters 8-66:
    Timeout!
    Command exited with non-zero status 1
    52.05 sec, 1598865408 bytes: Categories
    =============================================================================
    make SHARING=no
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    Time Timeout 50 abstract (simpl; admit).
    Finished transaction in 0.054 secs (0.053u,0.s)
    }
    admit.
    Defined.
    End Product.
    End Ab.
    1.40 sec, 1373962240 bytes: Categories
    =============================================================================
    make SHARING=yes
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    Time Timeout 50 abstract (simpl; admit).
    Finished transaction in 0.02 secs (0.02u,0.s)
    }
    admit.
    Defined.
    End Product.
    End Ab.
    2.19 sec, 1383383040 bytes: Categories
    =============================================================================
    make SHARING=no
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    Time (
		 let x := constr:(Eqn X T_ob T_el) in
		 let T := type of x in
		 let G := match goal with |- ?G => constr:(G) end in
		 idtac
	      ).
    Finished transaction in 0.004 secs (0.004u,0.s)
    admit.
    }
    admit.
    Defined.
    End Product.
    End Ab.
    1.33 sec, 1373700096 bytes: Categories
    =============================================================================
    make SHARING=no
    : compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
    ...
    {
    destruct T as [T_ob T_el].
    exists (Mor X T_ob T_el).
    simpl.
    apply funextsec.
    Time (
	       let x := constr:(Eqn X T_ob T_el) in
	       let T := type of X in
	       let G := match goal with |- ?G => constr:(G) end in
	       unify T G
	    ).
    File "./Categories.v", line 862, characters 11-20:
    Error: Tactic failure:Not unifiable.
    Command exited with non-zero status 1
    1.21 sec, 1368457216 bytes: Categories
    =============================================================================
various results requested by Jason Gross, corrected

=============================================================================
make SHARING=no
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
Time Timeout 50 exact (Eqn X T_ob T_el).
Finished transaction in 4.645 secs (4.639u,0.004s)
}
exists k'.
intros k.
apply El.mor_equality.
exact (Uniqueness X (pr1 T) (pr1 k) (pr1 k')
               (fun i => (apevalsecat i (pr2 k)) @ ! (apevalsecat i (pr2 k')))).
Defined.
End Product.
End Ab.
8.95 sec, 1431388160 bytes: Categories
=============================================================================
-*- mode: compilation; default-directory: "~/src/HoTT/Ktheory/src/" -*-
Comint started at Thu Jan 30 18:56:59

make SHARING=yes
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
Time Timeout 50 exact (Eqn X T_ob T_el).
File "./Categories.v", line 857, characters 25-65:
Timeout!
Command exited with non-zero status 1
52.07 sec, 1603158016 bytes: Categories
=============================================================================
make SHARING=no
"coqdep" -c -R . Ktheory "Categories.v" > "Categories.v.d" || ( RV=$?; rm -f "Categories.v.d"; exit ${RV} )
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
Time Timeout 50 exact (Eqn X T_ob T_el).
Finished transaction in 4.659 secs (4.653u,0.004s)
}
admit.
Defined.
End Product.
End Ab.
8.30 sec, 1425031168 bytes: Categories
=============================================================================
make SHARING=no
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
Time Timeout 50 exact (Eqn X T_ob T_el).
Finished transaction in 4.611 secs (4.606u,0.004s)
}
abstract (
      exists k'; intros k;
      apply El.mor_equality;
      exact (Uniqueness X (pr1 T) (pr1 k) (pr1 k')
               (fun i => (apevalsecat i (pr2 k)) @ ! (apevalsecat i (pr2 k')))) ).
Defined.
End Product.
End Ab.
9.25 sec, 1429291008 bytes: Categories
=============================================================================
make SHARING=no
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
simpl.
Time Timeout 50 exact (Eqn X T_ob T_el).
Finished transaction in 4.676 secs (4.671u,0.004s)
}
admit.
Defined.
End Product.
End Ab.
8.31 sec, 1422262272 bytes: Categories
=============================================================================
make SHARING=yes
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
simpl.
Time Timeout 50 exact (Eqn X T_ob T_el).
File "./Categories.v", line 857, characters 32-72:
Timeout!
Command exited with non-zero status 1
52.02 sec, 1599225856 bytes: Categories
=============================================================================
make SHARING=yes
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
simpl.
admit.
}
admit.
Defined.
End Product.
End Ab.
2.18 sec, 1383694336 bytes: Categories
=============================================================================
make SHARING=no
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
simpl.
admit.
}
admit.
Defined.
End Product.
End Ab.
1.33 sec, 1373143040 bytes: Categories
=============================================================================
make SHARING=no
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
simpl.
Time Timeout 50 abstract exact (Eqn X T_ob T_el).
Finished transaction in 7.007 secs (6.996u,0.009s)
}
admit.
Defined.
End Product.
End Ab.
10.67 sec, 1443905536 bytes: Categories
=============================================================================
make SHARING=yes
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
simpl.
Time Timeout 50 abstract exact (Eqn X T_ob T_el).
File "./Categories.v", line 860, characters 8-57:
Timeout!
Command exited with non-zero status 1
52.04 sec, 1599307776 bytes: Categories
=============================================================================
make SHARING=no
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
Time Timeout 50 abstract (simpl; exact (Eqn X T_ob T_el)).
Finished transaction in 6.998 secs (6.991u,0.007s)
}
admit.
Defined.
End Product.
End Ab.
10.65 sec, 1445986304 bytes: Categories
=============================================================================
make SHARING=yes
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
Time Timeout 50 abstract (simpl; exact (Eqn X T_ob T_el)).
File "./Categories.v", line 859, characters 8-66:
Timeout!
Command exited with non-zero status 1
52.05 sec, 1598865408 bytes: Categories
=============================================================================
make SHARING=no
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
Time Timeout 50 abstract (simpl; admit).
Finished transaction in 0.054 secs (0.053u,0.s)
}
admit.
Defined.
End Product.
End Ab.
1.40 sec, 1373962240 bytes: Categories
=============================================================================
make SHARING=yes
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
Time Timeout 50 abstract (simpl; admit).
Finished transaction in 0.02 secs (0.02u,0.s)
}
admit.
Defined.
End Product.
End Ab.
2.19 sec, 1383383040 bytes: Categories
=============================================================================
make SHARING=no
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
Time (
             let x := constr:(Eqn X T_ob T_el) in
             let T := type of x in
             let G := match goal with |- ?G => constr:(G) end in
             idtac
          ).
Finished transaction in 0.004 secs (0.004u,0.s)
admit.
}
admit.
Defined.
End Product.
End Ab.
1.33 sec, 1373700096 bytes: Categories
=============================================================================
make SHARING=no
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -no-sharing -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
Time (
           let x := constr:(Eqn X T_ob T_el) in
           let T := type of x in
           let G := match goal with |- ?G => constr:(G) end in
           unify T G
        ).
Finished transaction in 2.321 secs (2.317u,0.002s)
admit.
}
admit.
Defined.
End Product.
End Ab.
3.64 sec, 1387053056 bytes: Categories
=============================================================================
make SHARING=yes
: compiling Categories.v ; \time -f "%U sec, %M bytes: Categories" coqc  -q  -R . Ktheory -no-native-compiler -indices-matter -verbose  Categories
...
{
destruct T as [T_ob T_el].
exists (Mor X T_ob T_el).
simpl.
apply funextsec.
Time Timeout 50 (
           let x := constr:(Eqn X T_ob T_el) in
           let T := type of x in
           let G := match goal with |- ?G => constr:(G) end in
           unify T G
        ).
File "./Categories.v", line 858, characters 8-201:
Timeout!
Command exited with non-zero status 1
52.03 sec, 1599700992 bytes: Categories
=============================================================================