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
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
|
(* File reduced by coq-bug-finder from original input, then from 9593 lines to 104 lines, then from 187 lines to 103 lines, then from 113 lines to 90 lines *)
(* coqc version trunk (October 2014) compiled on Oct 1 2014 18:13:54 with OCaml 4.01.0
coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (68846802a7be637ec805a5e374655a426b5723a5) *)
Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y.
Inductive trunc_index := minus_two | trunc_S (_ : trunc_index).
Axiom IsTrunc : trunc_index -> Type -> Type.
Existing Class IsTrunc.
Axiom Contr : Type -> Type.
Inductive Trunc (n : trunc_index) (A :Type) : Type := tr : A -> Trunc n A.
Module NonPrim.
Unset Primitive Projections.
Set Implicit Arguments.
Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope.
Unset Implicit Arguments.
Notation "( x ; y )" := (existT _ x y) : fibration_scope.
Open Scope fibration_scope.
Notation pr1 := projT1.
Notation pr2 := projT2.
Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :> Contr (Trunc n A).
Axiom isconnected_elim : forall {n} {A} `{IsConnected n A}
(C : Type) `{IsTrunc n C} (f : A -> C),
{ c:C & forall a:A, f a = c }.
Class IsConnMap (n : trunc_index) {A B : Type} (f : A -> B)
:= isconnected_hfiber_conn_map :> forall b:B, IsConnected n (hfiber f b).
Definition conn_map_elim {n : trunc_index}
{A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
(P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
(d : forall a:A, P (f a))
: forall b:B, P b.
Proof.
intros b.
refine (pr1 (isconnected_elim _ _)).
2:exact b.
intro x.
exact (transport P x.2 (d x.1)).
Defined.
Definition conn_map_elim' {n : trunc_index}
{A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
(P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
(d : forall a:A, P (f a))
: forall b:B, P b.
Proof.
intros b.
refine (pr1 (isconnected_elim _ _)).
2:exact b.
intros [a p].
exact (transport P p (d a)).
Defined.
Definition conn_map_comp {n : trunc_index}
{A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
(P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
(d : forall a:A, P (f a))
: forall a:A, conn_map_elim f P d (f a) = d a /\ conn_map_elim' f P d (f a) = d a.
Proof.
intros a.
unfold conn_map_elim, conn_map_elim'.
Set Printing Coercions.
set (fibermap := fun a0p : hfiber f (f a)
=> let (a0, p) := a0p in transport P p (d a0)).
Set Printing Implicit.
let G := match goal with |- ?G => constr:G end in
first [ match goal with
| [ |- (@isconnected_elim n (@hfiber A B f (f a))
(@isconnected_hfiber_conn_map n A B f H (f a))
(P (f a)) (HP (f a))
(fun x : @hfiber A B f (f a) =>
@transport B P (f x.1) (f a) x.2 (d x.1))).1 =
d a /\ _ ] => idtac
end
| fail 1 "projection names should be folded, [let] should generate unfolded projections, goal:" G ];
first [ match goal with
| [ |- _ /\ (@isconnected_elim n (@hfiber A B f (f a))
(@isconnected_hfiber_conn_map n A B f H (f a))
(P (f a)) (HP (f a)) fibermap).1 = d a ] => idtac
end
| fail 1 "destruct should generate unfolded projections, as should [let], goal:" G ].
admit.
Defined.
End NonPrim.
Module Prim.
Set Primitive Projections.
Set Implicit Arguments.
Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }.
Notation "{ x : A & P }" := (sigT (fun x:A => P)) : type_scope.
Unset Implicit Arguments.
Notation "( x ; y )" := (existT _ x y) : fibration_scope.
Open Scope fibration_scope.
Notation pr1 := projT1.
Notation pr2 := projT2.
Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
Class IsConnected (n : trunc_index) (A : Type) := isconnected_contr_trunc :> Contr (Trunc n A).
Axiom isconnected_elim : forall {n} {A} `{IsConnected n A}
(C : Type) `{IsTrunc n C} (f : A -> C),
{ c:C & forall a:A, f a = c }.
Class IsConnMap (n : trunc_index) {A B : Type} (f : A -> B)
:= isconnected_hfiber_conn_map :> forall b:B, IsConnected n (hfiber f b).
Definition conn_map_elim {n : trunc_index}
{A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
(P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
(d : forall a:A, P (f a))
: forall b:B, P b.
Proof.
intros b.
refine (pr1 (isconnected_elim _ _)).
2:exact b.
intro x.
exact (transport P x.2 (d x.1)).
Defined.
Definition conn_map_elim' {n : trunc_index}
{A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
(P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
(d : forall a:A, P (f a))
: forall b:B, P b.
Proof.
intros b.
refine (pr1 (isconnected_elim _ _)).
2:exact b.
intros [a p].
exact (transport P p (d a)).
Defined.
Definition conn_map_comp {n : trunc_index}
{A B : Type} (f : A -> B) `{IsConnMap n _ _ f}
(P : B -> Type) {HP : forall b:B, IsTrunc n (P b)}
(d : forall a:A, P (f a))
: forall a:A, conn_map_elim f P d (f a) = d a /\ conn_map_elim' f P d (f a) = d a.
Proof.
intros a.
unfold conn_map_elim, conn_map_elim'.
Set Printing Coercions.
set (fibermap := fun a0p : hfiber f (f a)
=> let (a0, p) := a0p in transport P p (d a0)).
Set Printing Implicit.
let G := match goal with |- ?G => constr:G end in
first [ match goal with
| [ |- (@isconnected_elim n (@hfiber A B f (f a))
(@isconnected_hfiber_conn_map n A B f H (f a))
(P (f a)) (HP (f a))
(fun x : @hfiber A B f (f a) =>
@transport B P (f x.1) (f a) x.2 (d x.1))).1 =
d a /\ _ ] => idtac
end
| fail 1 "projection names should be folded, [let] should generate unfolded projections, goal:" G ];
first [ match goal with
| [ |- _ /\ (@isconnected_elim n (@hfiber A B f (f a))
(@isconnected_hfiber_conn_map n A B f H (f a))
(P (f a)) (HP (f a)) fibermap).1 = d a ] => idtac
end
| fail 1 "destruct should generate unfolded projections, as should [let], goal:" G ].
admit.
Defined.
End Prim.
|
