1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
Require Import TestSuite.admit.
Set Universe Polymorphism.
Inductive paths {A : Type} (a : A) : A -> Type :=
idpath : paths a a.
Goal forall (A : Type) (P : forall _ : A, Type) (x0 : A)
(p : P x0) (q : @paths (@sigT A P) (@existT A P x0 p) (@existT A P x0 p)),
@paths (@paths (@sigT A P) (@existT A P x0 p) (@existT A P x0 p))
(@idpath (@sigT A P) (@existT A P x0 p))
(@idpath (@sigT A P) (@existT A P x0 p)).
intros.
induction q.
admit.
Qed.
(** Error: Illegal application:
The term "paths_rect" of type
"forall (A : Type) (a : A) (P : forall a0 : A, paths a a0 -> Type),
P a (idpath a) -> forall (y : A) (p : paths a y), P y p"
cannot be applied to the terms
"{x : _ & P x}" : "Type"
"s" : "{x : _ & P x}"
"fun (a : {x : _ & P x}) (_ : paths s a) => paths (idpath a) (idpath a)"
: "forall a : {x : _ & P x}, paths s a -> Type"
"match proof_admitted return (paths (idpath s) (idpath s)) with
end" : "paths (idpath s) (idpath s)"
"s" : "{x : _ & P x}"
"q" : "paths (existT P x0 p) (existT P x0 p)"
The 3rd term has type "forall a : {x : _ & P x}, paths s a -> Type"
which should be coercible to "forall a : {x : _ & P x}, paths s a -> Type". *)
|
