michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(hott/homotopy): prove missing helper lemmas up to cube massaging

Browse source
This commit is contained in:
Jakob von Raumer 2015-11-25 18:16:02 +00:00 committed by Leonardo de Moura
parent 811f3067ff
commit bd064ef9c8
2 changed files with 15 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
hott/cubical/square.hlean
View file

@ -46,6 +46,12 @@ namespace eq
definition vdeg_square [unfold 6] {p q : a = a'} (r : p = q) : square p q idp idp := definition vdeg_square [unfold 6] {p q : a = a'} (r : p = q) : square p q idp idp :=
by induction r;apply vrefl by induction r;apply vrefl
definition hdeg_square_idp (p : a = a') : hdeg_square (refl p) = hrfl :=
by cases p; reflexivity
definition vdeg_square_idp (p : a = a') : vdeg_square (refl p) = vrfl :=
by cases p; reflexivity
definition hconcat [unfold 16] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁) definition hconcat [unfold 16] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁)
: square (p₁₀ ⬝ p₃₀) (p₁₂ ⬝ p₃₂) p₀₁ p₄₁ := : square (p₁₀ ⬝ p₃₀) (p₁₂ ⬝ p₃₂) p₀₁ p₄₁ :=
by induction s₃₁; exact s₁₁ by induction s₃₁; exact s₁₁

19
hott/homotopy/join.hlean
View file

@ -128,7 +128,7 @@ namespace join
(c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) : (c : cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂) :
cube s₁₁₂⁻¹ᵛ vrfl (massage_sq s₁₀₁) (massage_sq s₁₂₁) s₁₁₀⁻¹ᵛ s₀₁₁⁻¹ᵛ := cube s₁₁₂⁻¹ᵛ vrfl (massage_sq s₁₀₁) (massage_sq s₁₂₁) s₁₁₀⁻¹ᵛ s₀₁₁⁻¹ᵛ :=
begin begin
unfold massage_sq, exact sorry exact sorry,
end end
private definition massage_massage {A : Type} {a₀₀ a₀₂ a₂₀ : A} private definition massage_massage {A : Type} {a₀₀ a₀₂ a₂₀ : A}
@ -226,11 +226,12 @@ namespace join
(g : Π a, f a = b) {x y : A} (p : x = y) {sq : square (g x) (g y) (ap f p) idp} (g : Π a, f a = b) {x y : A} (p : x = y) {sq : square (g x) (g y) (ap f p) idp}
(q : apdo g p = eq_pathover (sq ⬝hp !ap_constant⁻¹)) : square_Flr_ap_idp _ _ = sq := (q : apdo g p = eq_pathover (sq ⬝hp !ap_constant⁻¹)) : square_Flr_ap_idp _ _ = sq :=
begin begin
cases p, esimp at *, exact sorry cases p, esimp at *, apply concat, apply inverse, apply vdeg_square_idp,
apply concat, apply ap vdeg_square, exact ap eq_of_pathover_idp q,
krewrite (is_equiv.right_inv (equiv.to_fun !pathover_idp)),
exact is_equiv.left_inv (equiv.to_fun (vdeg_square_equiv _ _)) sq,
end end
--set_option pp.implicit true
private definition switch_inv_cube (a : A) (b : B) (c : C) : private definition switch_inv_cube (a : A) (b : B) (c : C) :
cube (switch_inv_left_square a b) ids (square_Flr_ap_idp _ _) cube (switch_inv_left_square a b) ids (square_Flr_ap_idp _ _)
(square_Flr_ap_idp _ _) (switch_inv_coh_left c a) (switch_inv_coh_right c b) := (square_Flr_ap_idp _ _) (switch_inv_coh_left c a) (switch_inv_coh_right c b) :=
@ -282,12 +283,10 @@ namespace join
(e : apdo p q = eq_pathover sq) : (e : apdo p q = eq_pathover sq) :
natural_square_tr p q = sq := natural_square_tr p q = sq :=
begin begin
cases q, esimp at *, cases q, esimp at *, apply concat, apply inverse, apply vdeg_square_idp,
apply concat, apply inverse, apply vdeg_square_idp, apply concat, apply ap vdeg_square, apply ap eq_of_pathover_idp e,
assert H : refl (p y) = eq_of_vdeg_square sq, krewrite (is_equiv.right_inv (equiv.to_fun !pathover_idp)),
{ exact sorry }, exact is_equiv.left_inv (equiv.to_fun (vdeg_square_equiv _ _)) sq,
apply concat, apply ap vdeg_square, exact H,
apply is_equiv.left_inv (equiv.to_fun !vdeg_square_equiv),
end end
private definition switch_inv_coh (c : C) (k : join A B) : private definition switch_inv_coh (c : C) (k : join A B) :