forked from cmu-phil/Spectral
-
Notifications
You must be signed in to change notification settings - Fork 0
/
pointed_pi.hlean
240 lines (198 loc) · 8.81 KB
/
pointed_pi.hlean
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
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
/-
Copyright (c) 2016 Ulrik Buchholtz. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Ulrik Buchholtz
-/
import .move_to_lib
open eq pointed equiv sigma is_equiv
/-
The goal of this file is to give the truncation level
of the type of pointed maps, giving the connectivity of
the domain and the truncation level of the codomain.
This is is_trunc_pmap_of_is_conn at the end.
First we define the type of dependent pointed maps
as a tool, because these appear in the more general
statement is_trunc_ppi (the generality needed for induction).
-/
namespace pointed
abbreviation ppi_resp_pt [unfold 3] := @ppi.resp_pt
definition ppi_const [constructor] {A : Type*} (P : A → Type*) : Π*(a : A), P a :=
ppi.mk (λa, pt) idp
definition pointed_ppi [instance] [constructor] {A : Type*}
(P : A → Type*) : pointed (ppi A P) :=
pointed.mk (ppi_const P)
definition pppi [constructor] {A : Type*} (P : A → Type*) : Type* :=
pointed.mk' (ppi A P)
notation `Π*` binders `, ` r:(scoped P, pppi P) := r
structure ppi_homotopy {A : Type*} {P : A → Type*} (f g : Π*(a : A), P a) :=
(homotopy : f ~ g)
(homotopy_pt : homotopy pt ⬝ ppi_resp_pt g = ppi_resp_pt f)
variables {A : Type*} {P Q R : A → Type*} {f g h : Π*(a : A), P a}
infix ` ~~* `:50 := ppi_homotopy
abbreviation ppi_to_homotopy_pt [unfold 5] := @ppi_homotopy.homotopy_pt
abbreviation ppi_to_homotopy [coercion] [unfold 5] (p : f ~~* g) : Πa, f a = g a :=
ppi_homotopy.homotopy p
variable (f)
protected definition ppi_homotopy.refl : f ~~* f :=
sorry
variable {f}
protected definition ppi_homotopy.rfl [refl] : f ~~* f :=
ppi_homotopy.refl f
protected definition ppi_homotopy.symm [symm] (p : f ~~* g) : g ~~* f :=
sorry
protected definition ppi_homotopy.trans [trans] (p : f ~~* g) (q : g ~~* h) : f ~~* h :=
sorry
infix ` ⬝*' `:75 := ppi_homotopy.trans
postfix `⁻¹*'`:(max+1) := ppi_homotopy.symm
definition ppi_equiv_pmap (A B : Type*) : (Π*(a : A), B) ≃ (A →* B) :=
begin
fapply equiv.MK,
{ intro f, induction f with f p, exact pmap.mk f p },
{ intro f, induction f with f p, exact ppi.mk f p },
{ intro f, induction f with f p, reflexivity },
{ intro f, induction f with f p, reflexivity }
end
definition ppi.sigma_char [constructor] {A : Type*} (P : A → Type*)
: (Π*(a : A), P a) ≃ Σ(f : (Π (a : A), P a)), f pt = pt :=
begin
fapply equiv.MK : intros f,
{ exact ⟨ f , ppi_resp_pt f ⟩ },
all_goals cases f with f p,
{ exact ppi.mk f p },
all_goals reflexivity
end
-- the same as pmap_eq
definition ppi_eq (h : f ~ g) : ppi_resp_pt f = h pt ⬝ ppi_resp_pt g → f = g :=
begin
cases f with f p, cases g with g q, intro r,
esimp at *,
fapply apd011 ppi.mk,
{ apply eq_of_homotopy h },
{ esimp, apply concato_eq, apply eq_pathover_Fl, apply inv_con_eq_of_eq_con,
rewrite [ap_eq_apd10, apd10_eq_of_homotopy], exact r }
end
variables (f g)
definition ppi_homotopy.sigma_char [constructor]
: (f ~~* g) ≃ Σ(p : f ~ g), p pt ⬝ ppi_resp_pt g = ppi_resp_pt f :=
begin
fapply equiv.MK : intros h,
{ exact ⟨h , ppi_to_homotopy_pt h⟩ },
all_goals cases h with h p,
{ exact ppi_homotopy.mk h p },
all_goals reflexivity
end
-- the same as pmap_eq_equiv
definition ppi_eq_equiv : (f = g) ≃ (f ~~* g) :=
calc (f = g) ≃ ppi.sigma_char P f = ppi.sigma_char P g
: eq_equiv_fn_eq (ppi.sigma_char P) f g
... ≃ Σ(p : f = g),
pathover (λh, h pt = pt) (ppi_resp_pt f) p (ppi_resp_pt g)
: sigma_eq_equiv _ _
... ≃ Σ(p : f = g),
ppi_resp_pt f = ap (λh, h pt) p ⬝ ppi_resp_pt g
: sigma_equiv_sigma_right
(λp, eq_pathover_equiv_Fl p (ppi_resp_pt f) (ppi_resp_pt g))
... ≃ Σ(p : f = g),
ppi_resp_pt f = apd10 p pt ⬝ ppi_resp_pt g
: sigma_equiv_sigma_right
(λp, equiv_eq_closed_right _ (whisker_right _ (ap_eq_apd10 p _)))
... ≃ Σ(p : f ~ g), ppi_resp_pt f = p pt ⬝ ppi_resp_pt g
: sigma_equiv_sigma_left' eq_equiv_homotopy
... ≃ Σ(p : f ~ g), p pt ⬝ ppi_resp_pt g = ppi_resp_pt f
: sigma_equiv_sigma_right (λp, eq_equiv_eq_symm _ _)
... ≃ (f ~~* g) : ppi_homotopy.sigma_char f g
definition ppi_loop_equiv_lemma (p : f ~ f)
: (p pt ⬝ ppi_resp_pt f = ppi_resp_pt f) ≃ (p pt = idp) :=
calc (p pt ⬝ ppi_resp_pt f = ppi_resp_pt f)
≃ (p pt ⬝ ppi_resp_pt f = idp ⬝ ppi_resp_pt f)
: equiv_eq_closed_right (p pt ⬝ ppi_resp_pt f) (inverse (idp_con (ppi_resp_pt f)))
... ≃ (p pt = idp)
: eq_equiv_con_eq_con_right
definition ppi_loop_equiv : (f = f) ≃ Π*(a : A), Ω (pType.mk (P a) (f a)) :=
calc (f = f) ≃ (f ~~* f)
: ppi_eq_equiv
... ≃ Σ(p : f ~ f), p pt ⬝ ppi_resp_pt f = ppi_resp_pt f
: ppi_homotopy.sigma_char f f
... ≃ Σ(p : f ~ f), p pt = idp
: sigma_equiv_sigma_right
(λ p, ppi_loop_equiv_lemma f p)
... ≃ Π*(a : A), pType.mk (f a = f a) idp
: ppi.sigma_char
... ≃ Π*(a : A), Ω (pType.mk (P a) (f a))
: erfl
variables {f g}
definition eq_of_ppi_homotopy (h : f ~~* g) : f = g :=
(ppi_eq_equiv f g)⁻¹ᵉ h
definition ppi_loop_pequiv : Ω (Π*(a : A), P a) ≃* Π*(a : A), Ω (P a) :=
pequiv_of_equiv (ppi_loop_equiv pt) idp
definition pmap_compose_ppi [constructor] (g : Π(a : A), ppmap (P a) (Q a))
(f : Π*(a : A), P a) : Π*(a : A), Q a :=
proof ppi.mk (λa, g a (f a)) (ap (g pt) (ppi.resp_pt f) ⬝ respect_pt (g pt)) qed
definition pmap_compose_ppi_const_right (g : Π(a : A), ppmap (P a) (Q a)) :
pmap_compose_ppi g (ppi_const P) ~~* ppi_const Q :=
proof ppi_homotopy.mk (λa, respect_pt (g a)) !idp_con⁻¹ qed
definition pmap_compose_ppi_const_left (f : Π*(a : A), P a) :
pmap_compose_ppi (λa, pconst (P a) (Q a)) f ~~* ppi_const Q :=
sorry
definition ppi_compose_left [constructor] (g : Π(a : A), ppmap (P a) (Q a)) :
(Π*(a : A), P a) →* Π*(a : A), Q a :=
pmap.mk (pmap_compose_ppi g) (eq_of_ppi_homotopy (pmap_compose_ppi_const_right g))
definition pmap_compose_ppi_phomotopy_left [constructor] {g g' : Π(a : A), ppmap (P a) (Q a)}
(f : Π*(a : A), P a) (p : Πa, g a ~* g' a) : pmap_compose_ppi g f ~~* pmap_compose_ppi g' f :=
sorry
definition pmap_compose_ppi_pid_left [constructor]
(f : Π*(a : A), P a) : pmap_compose_ppi (λa, pid (P a)) f ~~* f :=
sorry
definition pmap_compose_pmap_compose_ppi [constructor] (h : Π(a : A), ppmap (Q a) (R a))
(g : Π(a : A), ppmap (P a) (Q a)) :
pmap_compose_ppi h (pmap_compose_ppi g f) ~~* pmap_compose_ppi (λa, h a ∘* g a) f :=
sorry
definition ppi_pequiv_right [constructor] (g : Π(a : A), P a ≃* Q a) :
(Π*(a : A), P a) ≃* Π*(a : A), Q a :=
begin
apply pequiv_of_pmap (ppi_compose_left g),
apply adjointify _ (ppi_compose_left (λa, (g a)⁻¹ᵉ*)),
{ intro f, apply eq_of_ppi_homotopy,
refine !pmap_compose_pmap_compose_ppi ⬝*' _,
refine pmap_compose_ppi_phomotopy_left _ (λa, !pright_inv) ⬝*' _,
apply pmap_compose_ppi_pid_left },
{ intro f, apply eq_of_ppi_homotopy,
refine !pmap_compose_pmap_compose_ppi ⬝*' _,
refine pmap_compose_ppi_phomotopy_left _ (λa, !pleft_inv) ⬝*' _,
apply pmap_compose_ppi_pid_left }
end
end pointed open pointed
open is_trunc is_conn
section
variables (A : Type*) (n : ℕ₋₂) [H : is_conn (n.+1) A]
include H
definition is_contr_ppi_match (P : A → (n.+1)-Type*)
: is_contr (Π*(a : A), P a) :=
begin
apply is_contr.mk pt,
intro f, induction f with f p,
fapply ppi_eq,
{ apply is_conn.elim n, esimp, exact p⁻¹ },
{ krewrite (is_conn.elim_β n), apply inverse, apply con.left_inv }
end
definition is_trunc_ppi (k : ℕ₋₂) (P : A → (n.+1+2+k)-Type*)
: is_trunc k.+1 (Π*(a : A), P a) :=
begin
induction k with k IH,
{ apply is_prop_of_imp_is_contr, intro f,
apply is_contr_ppi_match },
{ apply is_trunc_succ_of_is_trunc_loop
(trunc_index.succ_le_succ (trunc_index.minus_two_le k)),
intro f,
apply @is_trunc_equiv_closed_rev _ _ k.+1
(ppi_loop_equiv f),
apply IH, intro a,
apply ptrunctype.mk (Ω (pType.mk (P a) (f a))),
{ apply is_trunc_loop, exact is_trunc_ptrunctype (P a) },
{ exact pt } }
end
definition is_trunc_pmap_of_is_conn (k : ℕ₋₂) (B : (n.+1+2+k)-Type*)
: is_trunc k.+1 (A →* B) :=
@is_trunc_equiv_closed _ _ k.+1 (ppi_equiv_pmap A B)
(is_trunc_ppi A n k (λ a, B))
end