forked from cmu-phil/Spectral
-
Notifications
You must be signed in to change notification settings - Fork 0
/
coind_colim.hlean
141 lines (124 loc) · 6.22 KB
/
coind_colim.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
-- author: Floris van Doorn
import .colim
open nat seq_colim seq_colim.ops eq equiv is_equiv is_trunc function
namespace seq_colim
variables {A : ℕ → Type} {f : seq_diagram A}
definition ι0 [reducible] : A 0 → seq_colim f :=
ι f
variable (f)
definition ι0' [reducible] : A 0 → seq_colim f :=
ι f
definition glue0 (a : A 0) : shift_down f (ι0 (f a)) = ι f a :=
glue f a
definition rec_coind_point {P : Π⦃A : ℕ → Type⦄ (f : seq_diagram A), seq_colim f → Type}
(P0 : Π⦃A⦄ (f : seq_diagram A) (a : A 0), P f (ι0 a))
(Ps : Π⦃A⦄ (f : seq_diagram A) (x : seq_colim (shift_diag f)),
P (shift_diag f) x → P f (shift_down f x))
(Pe : Π⦃A⦄ (f : seq_diagram A) (a : A 0),
pathover (P f) (Ps f (ι0 (f a)) !P0) (proof glue f a qed) (P0 f a))
(n : ℕ) : Π{A : ℕ → Type} {f : seq_diagram A} (a : A n), P f (ι f a) :=
begin
induction n with n IH: intro A f a,
{ exact P0 f a },
{ exact Ps f (ι _ a) (IH a) }
end
definition rec_coind_point_succ {P : Π⦃A : ℕ → Type⦄ (f : seq_diagram A), seq_colim f → Type}
(P0 : Π⦃A⦄ (f : seq_diagram A) (a : A 0), P f (ι0 a))
(Ps : Π⦃A⦄ (f : seq_diagram A) (x : seq_colim (shift_diag f)),
P (shift_diag f) x → P f (shift_down f x))
(Pe : Π⦃A⦄ (f : seq_diagram A) (a : A 0),
pathover (P f) (Ps f (ι0 (f a)) !P0) _ (P0 f a))
(n : ℕ) {A : ℕ → Type} {f : seq_diagram A} (a : A (succ n)) :
rec_coind_point P0 Ps Pe (succ n) a = Ps f (ι _ a) (rec_coind_point P0 Ps Pe n a) :=
by reflexivity
definition rec_coind {P : Π⦃A : ℕ → Type⦄ (f : seq_diagram A), seq_colim f → Type}
(P0 : Π⦃A⦄ (f : seq_diagram A) (a : A 0), P f (ι0 a))
(Ps : Π⦃A⦄ (f : seq_diagram A) (x : seq_colim (shift_diag f)),
P (shift_diag f) x → P f (shift_down f x))
(Pe : Π⦃A⦄ (f : seq_diagram A) (a : A 0),
pathover (P f) (Ps f (ι0 (f a)) !P0) (proof glue f a qed) (P0 f a))
{A : ℕ → Type} {f : seq_diagram A} (x : seq_colim f) : P f x :=
begin
induction x,
{ exact rec_coind_point P0 Ps Pe n a },
{ revert A f a, induction n with n IH: intro A f a,
{ exact Pe f a },
{ rewrite [rec_coind_point_succ _ _ _ n, rec_coind_point_succ],
note p := IH _ (shift_diag f) a,
refine change_path _ (pathover_ap _ _ (apo (Ps f) p)),
exact !elim_glue
}},
end
definition rec_coind_pt2 {P : Π⦃A : ℕ → Type⦄ (f : seq_diagram A), seq_colim f → Type}
(P0 : Π⦃A⦄ (f : seq_diagram A) (a : A 0), P f (ι0 a))
(Ps : Π⦃A⦄ (f : seq_diagram A) (x : seq_colim (shift_diag f)),
P (shift_diag f) x → P f (shift_down f x))
(Pe : Π⦃A⦄ (f : seq_diagram A) (a : A 0),
pathover (P f) (Ps f (ι0 (f a)) !P0) _ (P0 f a))
{A : ℕ → Type} {f : seq_diagram A} (x : seq_colim (shift_diag f))
: rec_coind P0 Ps Pe (shift_down f x) = Ps f x (rec_coind P0 Ps Pe x) :=
begin
induction x,
{ reflexivity },
{ apply eq_pathover_dep,
apply hdeg_squareover, esimp,
refine apd_compose2 (rec_coind P0 Ps Pe) _ _ ⬝ _ ⬝ (apd_compose1 (Ps f) _ _)⁻¹,
exact sorry
--refine ap (λx, pathover_of_pathover_ap _ _ (x)) _ ⬝ _ ,
}
end
definition elim_coind_point {P : Π⦃A : ℕ → Type⦄ (f : seq_diagram A), Type}
(P0 : Π⦃A⦄ (f : seq_diagram A) (a : A 0), P f)
(Ps : Π⦃A⦄ (f : seq_diagram A) (x : seq_colim (shift_diag f)), P (shift_diag f) → P f)
(Pe : Π⦃A⦄ (f : seq_diagram A) (a : A 0), Ps f (ι0 (f a)) (P0 _ (f a)) = P0 f a)
(n : ℕ) : Π{A : ℕ → Type} (f : seq_diagram A) (a : A n), P f :=
begin
induction n with n IH: intro A f a,
{ exact P0 f a },
{ exact Ps f (ι _ a) (IH _ a) }
end
definition elim_coind_point_succ {P : Π⦃A : ℕ → Type⦄ (f : seq_diagram A), Type}
(P0 : Π⦃A⦄ (f : seq_diagram A) (a : A 0), P f)
(Ps : Π⦃A⦄ (f : seq_diagram A) (x : seq_colim (shift_diag f)), P (shift_diag f) → P f)
(Pe : Π⦃A⦄ (f : seq_diagram A) (a : A 0), Ps f (ι0 (f a)) (P0 _ (f a)) = P0 f a)
(n : ℕ) {A : ℕ → Type} {f : seq_diagram A} (a : A (succ n)) :
elim_coind_point P0 Ps Pe (succ n) f a =
Ps f (ι _ a) (elim_coind_point P0 Ps Pe n (shift_diag f) a) :=
by reflexivity
definition elim_coind_path {P : Π⦃A : ℕ → Type⦄ (f : seq_diagram A), Type}
(P0 : Π⦃A⦄ (f : seq_diagram A) (a : A 0), P f)
(Ps : Π⦃A⦄ (f : seq_diagram A) (x : seq_colim (shift_diag f)), P (shift_diag f) → P f)
(Pe : Π⦃A⦄ (f : seq_diagram A) (a : A 0), Ps f (ι0 (f a)) (P0 _ (f a)) = P0 f a)
(n : ℕ) : Π{A : ℕ → Type} (f : seq_diagram A) (a : A n),
elim_coind_point P0 Ps Pe (succ n) f (f a) = elim_coind_point P0 Ps Pe n f a :=
begin
induction n with n IH: intro A f a,
{ exact Pe f a },
{ rewrite [elim_coind_point_succ _ _ _ n, elim_coind_point_succ],
note p := IH (shift_diag f) a,
refine ap011 (Ps f) !glue p }
end
definition elim_coind {P : Π⦃A : ℕ → Type⦄ (f : seq_diagram A), Type}
(P0 : Π⦃A⦄ (f : seq_diagram A) (a : A 0), P f)
(Ps : Π⦃A⦄ (f : seq_diagram A) (x : seq_colim (shift_diag f)), P (shift_diag f) → P f)
(Pe : Π⦃A⦄ (f : seq_diagram A) (a : A 0), Ps f (ι0 (f a)) (P0 _ (f a)) = P0 f a)
{A : ℕ → Type} {f : seq_diagram A} (x : seq_colim f) : P f :=
begin
induction x,
{ exact elim_coind_point P0 Ps Pe n f a },
{ exact elim_coind_path P0 Ps Pe n f a },
end
definition elim_coind_pt2 {P : Π⦃A : ℕ → Type⦄ (f : seq_diagram A), Type}
(P0 : Π⦃A⦄ (f : seq_diagram A) (a : A 0), P f)
(Ps : Π⦃A⦄ (f : seq_diagram A) (x : seq_colim (shift_diag f)), P (shift_diag f) → P f)
(Pe : Π⦃A⦄ (f : seq_diagram A) (a : A 0), Ps f (ι0 (f a)) (P0 _ (f a)) = P0 f a)
{A : ℕ → Type} {f : seq_diagram A} (x : seq_colim (shift_diag f))
: elim_coind P0 Ps Pe (shift_down f x) = Ps f x (elim_coind P0 Ps Pe x) :=
begin
induction x,
{ reflexivity },
{ apply eq_pathover, apply hdeg_square,
refine ap_compose (elim_coind P0 Ps Pe) _ _ ⬝ _ ⬝ (ap_eq_ap011 (Ps f) _ _ _)⁻¹,
refine ap02 _ !elim_glue ⬝ !elim_glue ⬝ ap011 (ap011 _) !ap_id⁻¹ !elim_glue⁻¹ }
end
end seq_colim