blob: 2dc50c17d0c8f19e764adbcc7cdd3f89fbac7b54 (
plain)
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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
Require Import TestSuite.admit.
(* File reduced by coq-bug-finder from original input, then from 2674 lines to 136 lines, then from 115 lines to 61 lines *)
(* coqc version trunk (October 2014) compiled on Oct 28 2014 14:33:38 with OCaml 4.01.0
coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-trunk,(no branch) (53bfe9cf58a3c40e6eb7120d25c1633a9cea3126) *)
Class IsEquiv {A B : Type} (f : A -> B) := {}.
Record Equiv A B := { equiv_fun : A -> B ; equiv_isequiv : IsEquiv equiv_fun }.
Arguments equiv_fun {A B} _ _.
Record PreCategory := { object :> Type ; morphism : object -> object -> Type }.
Set Printing Coercions.
Set Printing Implicit.
Module NonPrim.
Unset Primitive Projections.
Record TruncType (n : nat) := { trunctype_type :> Type }.
Canonical Structure default_TruncType := fun n T => (@Build_TruncType n T).
Goal (forall (s d : TruncType 0) (m : trunctype_type 0 s -> trunctype_type 0 d),
@IsEquiv (trunctype_type 0 s) (trunctype_type 0 d) m -> Type) ->
forall (T T0 : Type) (m : T0 -> T), @IsEquiv T0 T m -> True.
intros isiso_isequiv' mc md e e'.
(pose (@isiso_isequiv'
_ _
(e
: (Build_TruncType 0 md) ->
(Build_TruncType 0 mc))
e') as i || fail "too early"); clear i.
pose (@isiso_isequiv'
_ _ _
e').
admit.
Defined.
End NonPrim.
Module Prim.
Set Primitive Projections.
Record TruncType (n : nat) := { trunctype_type :> Type }.
Canonical Structure default_TruncType := fun n T => (@Build_TruncType n T).
Goal (forall (s d : TruncType 0) (m : trunctype_type 0 s -> trunctype_type 0 d),
@IsEquiv (trunctype_type 0 s) (trunctype_type 0 d) m -> Type) ->
forall (T T0 : Type) (m : T0 -> T), @IsEquiv T0 T m -> True.
intros isiso_isequiv' mc md e e'.
(pose (@isiso_isequiv'
_ _
(e
: (Build_TruncType 0 md) ->
(Build_TruncType 0 mc))
e') as i || fail "too early"); clear i.
Set Printing Existential Instances.
Set Debug Unification.
pose (@isiso_isequiv'
_ _ _
e'). (* Toplevel input, characters 48-50:
Error:
In environment
isiso_isequiv' : forall (s d : TruncType 0)
(m : trunctype_type 0 s -> trunctype_type 0 d),
@IsEquiv (trunctype_type 0 s) (trunctype_type 0 d) m -> Type
mc : Type
md : Type
e : md -> mc
e' : @IsEquiv md mc e
The term "e'" has type "@IsEquiv md mc e" while it is expected to have type
"@IsEquiv (trunctype_type 0 ?t) (trunctype_type 0 ?t0) ?t1".
*)
admit.
Defined.
End Prim.
|
