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
30
31
32
33
34
35
36
37
38
|
(* File reduced by coq-bug-finder from original input, then from 981 lines to 33 lines *)
(* coqc version 8.5beta2 (May 2015) compiled on May 5 2015 15:20:21 with OCaml 4.01.0
coqtop version 8.5beta2 (May 2015) *)
Axiom ap : forall {A B:Type} (f:A -> B) {x y:A} (p:x = y), f x = f y.
Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
forall x : A, r (s x) = x.
Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
equiv_inv : B -> A ;
eisretr : Sect equiv_inv f;
eissect : Sect f equiv_inv;
eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
}.
Definition Lift@{i j} (A : Type@{i}) : Type@{j}
:= Eval hnf in let enforce_lt := Type@{i} : Type@{j} in A.
Definition lower {A} : Lift A -> A := fun x => x.
Definition lift2 {A B} (f : forall x : A, B x) : forall x : Lift A, Lift (B (lower x))
:= f.
Global Instance lift_isequiv {A B} (f : A -> B) {H : IsEquiv f} : @ IsEquiv _ _ (lift2 f).
(* Used to be: *)
(* Toplevel input, characters 95-102:
Error:
In environment
A : Type
B : Type
f : A -> B
H : IsEquiv f
The term "lift2 f" has type "Lift A -> Lift B"
while it is expected to have type "Lift A -> ?T0" (cannot instantiate
"?T0" because "x" is not in its scope: available arguments are
"A" "B" "f" "H"). *)
Abort.
|
