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
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
|
Inductive Empty : Prop := .
Inductive paths {A : Type} (a : A) : A -> Type :=
idpath : paths a a.
Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.
Arguments idpath {A a} , [A] a.
Definition idmap {A : Type} : A -> A := fun x => x.
Definition path_sum {A B : Type} (z z' : A + B)
(pq : match z, z' with
| inl z0, inl z'0 => z0 = z'0
| inr z0, inr z'0 => z0 = z'0
| _, _ => Empty
end)
: z = z'.
destruct z, z', pq; exact idpath.
Defined.
Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
:= match p with idpath => idpath end.
Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
(* Fortunately, this unifies properly *)
(pq : match (x, y) with (inl x', inl y') => x' = y' | (inr x', inr y') => x' = y' | _ => Empty end) :
let f z := match z with inl z' => inl (g z') | inr z' => inr (h z') end in
ap f (path_sum x y pq) = path_sum (f x) (f y)
(* Coq appears to require *ALL* of the annotations *)
((match x as x return match (x, y) with
(inl x', inl y') => x' = y'
| (inr x', inr y') => x' = y'
| _ => Empty
end -> match (f x, f y) with
| (inl x', inl y') => x' = y'
| (inr x', inr y') => x' = y'
| _ => Empty end with
| inl x' => match y as y return match y with
inl y' => x' = y'
| _ => Empty
end -> match f y with
| inl y' => g x' = y'
| _ => Empty end with
| inl y' => ap g
| inr y' => idmap
end
| inr x' => match y as y return match y return Prop with
inr y' => x' = y'
| _ => Empty
end -> match f y return Prop with
| inr y' => h x' = y'
| _ => Empty end with
| inl y' => idmap
| inr y' => ap h
end
end) pq).
destruct x; destruct y; destruct pq; reflexivity.
Qed.
(* Toplevel input, characters 1367-1374:
Error:
In environment
A : Type
B : Type
A' : Type
B' : Type
g : A -> A'
h : B -> B'
x : A + B
y : A + B
pq :
match x with
| inl x' => match y with
| inl y' => x' = y'
| inr _ => Empty
end
| inr x' => match y with
| inl _ => Empty
| inr y' => x' = y'
end
end
f :=
fun z : A + B =>
match z with
| inl z' => inl (g z')
| inr z' => inr (h z')
end : A + B -> A' + B'
x' : B
y0 : A + B
y' : B
The term "x' = y'" has type "Type" while it is expected to have type
"Prop" (Universe inconsistency). *)
|
