From 6c6dde7e481175d62701092781a75a729f539598 Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Tue, 24 Nov 2015 14:07:06 +0000 Subject: [PATCH] feat(hott/homotopy): progress on join associativity, many coherence lemmas about square operations needed --- hott/cubical/cube.hlean | 18 ++++++++++------ hott/cubical/square.hlean | 6 +++++- hott/homotopy/join.hlean | 44 +++++++++++++++++++++++++++------------ 3 files changed, 48 insertions(+), 20 deletions(-) diff --git a/hott/cubical/cube.hlean b/hott/cubical/cube.hlean index b4f151924..ffd370af9 100644 --- a/hott/cubical/cube.hlean +++ b/hott/cubical/cube.hlean @@ -176,11 +176,11 @@ namespace eq (hdeg_square s₂₁) (hdeg_square s₁₀) (hdeg_square s₁₂) ids ids := by induction p₀₀; induction sq; apply idc - definition ids2_cube_of_square : cube ids ids + definition ids1_cube_of_square : cube ids ids (vdeg_square s₁₀) (vdeg_square s₁₂) (hdeg_square s₀₁) (hdeg_square s₂₁) := by induction p₀₀; induction sq; apply idc - definition ids1_cube_of_square : cube (vdeg_square s₁₀) (vdeg_square s₁₂) + definition ids2_cube_of_square : cube (vdeg_square s₁₀) (vdeg_square s₁₂) ids ids (vdeg_square s₀₁) (vdeg_square s₂₁) := by induction p₀₀; induction sq; apply idc @@ -200,7 +200,7 @@ namespace eq apply cube_transport101 (left_inv (vdeg_square_equiv _ _) s₁₀₁), apply cube_transport112 (left_inv (hdeg_square_equiv _ _) s₁₁₂), apply cube_transport121 (left_inv (vdeg_square_equiv _ _) s₁₂₁), - apply ids2_cube_of_square, exact fillsq.2 + apply ids1_cube_of_square, exact fillsq.2 end definition cube_fill112 : Σ lid, cube s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ lid := @@ -212,7 +212,7 @@ namespace eq apply cube_transport101 (left_inv (vdeg_square_equiv _ _) s₁₀₁), apply cube_transport110 (left_inv (hdeg_square_equiv _ _) s₁₁₀), apply cube_transport121 (left_inv (vdeg_square_equiv _ _) s₁₂₁), - apply ids2_cube_of_square, exact fillsq.2, + apply ids1_cube_of_square, exact fillsq.2, end definition cube_fill011 : Σ lid, cube lid s₂₁₁ s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂ := @@ -224,7 +224,7 @@ namespace eq apply cube_transport110 (left_inv (vdeg_square_equiv _ _) s₁₁₀), apply cube_transport211 (left_inv (vdeg_square_equiv _ _) s₂₁₁), apply cube_transport112 (left_inv (vdeg_square_equiv _ _) s₁₁₂), - apply ids1_cube_of_square, exact fillsq.2, + apply ids2_cube_of_square, exact fillsq.2, end definition cube_fill211 : Σ lid, cube s₀₁₁ lid s₁₀₁ s₁₂₁ s₁₁₀ s₁₁₂ := @@ -236,7 +236,7 @@ namespace eq apply cube_transport011 (left_inv (vdeg_square_equiv _ _) s₀₁₁), apply cube_transport110 (left_inv (vdeg_square_equiv _ _) s₁₁₀), apply cube_transport112 (left_inv (vdeg_square_equiv _ _) s₁₁₂), - apply ids1_cube_of_square, exact fillsq.2, + apply ids2_cube_of_square, exact fillsq.2, end definition cube_fill101 : Σ lid, cube s₀₁₁ s₂₁₁ lid s₁₂₁ s₁₁₀ s₁₁₂ := @@ -265,4 +265,10 @@ namespace eq end cube_fillers + include c + definition apc (f : A → B) : + cube (aps f s₀₁₁) (aps f s₂₁₁) (aps f s₁₀₁) (aps f s₁₂₁) (aps f s₁₁₀) (aps f s₁₁₂) := + by cases c; exact idc + omit c + end eq diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean index cd86bc382..d96498b31 100644 --- a/hott/cubical/square.hlean +++ b/hott/cubical/square.hlean @@ -500,10 +500,14 @@ namespace eq by induction p₁₀; induction p₁₂; exact ⟨_, !hrefl⟩ --TODO find better names - definition square_Flr_ap_idp {A B : Type} {b : B} {f : A → B} (p : Π a, f a = b) + definition square_Flr_ap_idp {A B : Type} {c : B} {f : A → B} (p : Π a, f a = c) {a b : A} (q : a = b) : square (p a) (p b) (ap f q) idp := by induction q; apply vrfl + definition square_Flr_idp_ap {A B : Type} {c : B} {f : A → B} (p : Π a, c = f a) + {a b : A} (q : a = b) : square (p a) (p b) idp (ap f q) := + by induction q; apply vrfl + definition square_ap_idp_Flr {A B : Type} {b : B} {f : A → B} (p : Π a, f a = b) {a b : A} (q : a = b) : square (ap f q) idp (p a) (p b) := by induction q; apply hrfl diff --git a/hott/homotopy/join.hlean b/hott/homotopy/join.hlean index f115ca5ba..1d64d846e 100644 --- a/hott/homotopy/join.hlean +++ b/hott/homotopy/join.hlean @@ -89,7 +89,7 @@ namespace join --This proves that the join operator is associative --The proof is more or less ported from Evan Cavallo's agda version - section switch_assoc + section join_switch private definition massage_sq {A : Type} {a₀₀ a₂₀ a₀₂ a₂₂ : A} {p₁₀ : a₀₀ = a₂₀} {p₁₂ : a₀₂ = a₂₂} {p₀₁ : a₀₀ = a₀₂} {p₂₁ : a₂₀ = a₂₂} (sq : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₁₀⁻¹ p₀₁⁻¹ (p₂₁ ⬝ p₁₂⁻¹) idp := @@ -103,15 +103,15 @@ namespace join end private definition switch_coh_fill (a : A) (b : B) (c : C) : - Σ sq : square (jglue (inl c) a)⁻¹ (ap inl (jglue c b))⁻¹ (ap switch_left (jglue a b)) idp, - cube hrfl hrfl (hdeg_square !elim_glue) ids - sq (eq_hconcat !idp_con⁻¹ (massage_sq (square_Fl_Fl_ap_idp _ _))) := + Σ sq : square (jglue (inl c) a)⁻¹ (ap inl (jglue c b)⁻¹) (ap switch_left (jglue a b)) idp, + cube (hdeg_square !elim_glue) ids sq + (!idp_con⁻¹ ⬝ph (massage_sq (square_Flr_ap_idp _ _)) ⬝vp !ap_inv⁻¹) hrfl hrfl := by esimp; apply cube_fill101 private definition switch_coh (ab : join A B) (c : C) : switch_left ab = inl (inl c) := begin induction ab with a b, apply !jglue⁻¹, apply ap inl !jglue⁻¹, induction x with a b, - apply eq_pathover, refine _ ⬝hp !ap_constant⁻¹, refine _ ⬝vp !ap_inv⁻¹, + apply eq_pathover, refine _ ⬝hp !ap_constant⁻¹, apply !switch_coh_fill.1, end @@ -164,19 +164,37 @@ namespace join section variables (a : A) (b : B) (c : C) - check cube ids (switch_inv_left_square a b) - private definition switch_inv_cube (a : A) (b : B) (c : C) : - cube ids (switch_inv_left_square a b) - (square_Fl_Fl_ap_idp _ _) (square_Fl_Fl_ap_idp _ _) - --(switch_inv_coh_left c a) (switch_inv_coh_right c b) - := + private definition switch_inv_cube_aux1 {A B C : Type} {b : B} {f : A → B} (h : B → C) + (g : Π a, f a = b) {x y : A} (p : x = y) : + cube (hdeg_square (ap_compose h f p)) ids (square_Flr_ap_idp (λ a, ap h (g a)) p) + (aps h (square_Flr_ap_idp _ _)) hrfl hrfl := begin - + cases p, esimp[square_Flr_ap_idp], apply deg2_cube, + cases (g x), reflexivity, end + private definition switch_inv_cube_aux2 {A B C : Type} {b : B} {f : A → B} + (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 := + begin + cases p, esimp at *, exact sorry + end - end switch_assoc + private definition switch_inv_cube (a : A) (b : B) (c : C) : + 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) := + begin + esimp [switch_inv_coh_left, switch_inv_coh_right, switch_inv_left_square], + apply cube_concat2, apply switch_inv_cube_aux1, + apply cube_concat2, esimp, apply cube_transport101, + apply inverse, apply ap (λ x, aps join.switch x), + apply switch_inv_cube_aux2, esimp[switch_coh, jglue], apply rec_glue, + apply apc, apply (switch_coh_fill a b c).2, + end + check ap_constant + + end join_switch exit