From e1e86804747f3ddaa6b5423a51800531d5297004 Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Thu, 29 Oct 2015 16:57:54 +0000 Subject: [PATCH] feat(hott/homotopy): continue defining squares for join associativity --- hott/cubical/cube.hlean | 2 +- hott/cubical/square.hlean | 21 +++++---- hott/homotopy/join.hlean | 91 ++++++++++++++++++++++++++++----------- 3 files changed, 80 insertions(+), 34 deletions(-) diff --git a/hott/cubical/cube.hlean b/hott/cubical/cube.hlean index 28e1f50f4..3080f710c 100644 --- a/hott/cubical/cube.hlean +++ b/hott/cubical/cube.hlean @@ -157,7 +157,7 @@ namespace eq section cube_fillers variables (s₁₁₀ s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁) - definition cube_fil110 : Σ lid, cube lid s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ := + definition cube_fill110 : Σ lid, cube lid s₁₁₂ s₀₁₁ s₂₁₁ s₁₀₁ s₁₂₁ := begin induction s₀₁₁, induction s₂₁₁, let fillsq := square_fill_l (eq_of_vdeg_square s₁₀₁) diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean index 55c157eab..e7b443b95 100644 --- a/hott/cubical/square.hlean +++ b/hott/cubical/square.hlean @@ -76,14 +76,14 @@ namespace eq square p₁₀ p₁₂ p₀₁ p := by induction r; exact s₁₁ - infix ` ⬝h `:75 := hconcat - infix ` ⬝v `:75 := vconcat - infix ` ⬝hp `:75 := hconcat_eq - infix ` ⬝vp `:75 := vconcat_eq - infix ` ⬝ph `:75 := eq_hconcat - infix ` ⬝pv `:75 := eq_vconcat - postfix `⁻¹ʰ`:(max+1) := hinverse - postfix `⁻¹ᵛ`:(max+1) := vinverse + infix `⬝h`:75 := hconcat --type using \tr + infix `⬝v`:75 := vconcat --type using \tr + infix `⬝hp`:75 := hconcat_eq --type using \tr + infix `⬝vp`:75 := vconcat_eq --type using \tr + infix `⬝ph`:75 := eq_hconcat --type using \tr + infix `⬝pv`:75 := eq_vconcat --type using \tr + postfix `⁻¹ʰ`:(max+1) := hinverse --type using \-1h + postfix `⁻¹ᵛ`:(max+1) := vinverse --type using \-1v definition transpose [unfold 10] (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) : square p₀₁ p₂₁ p₁₀ p₁₂ := by induction s₁₁;exact ids @@ -499,4 +499,9 @@ namespace eq definition square_fill_r : Σ (p : a₂₀ = a₂₂) , square p₁₀ p₁₂ p₀₁ p := by induction p₁₀; induction p₁₂; exact ⟨_, !hrefl⟩ + --TODO find better names + definition square_Fl_Fl_ap_idp {A B : Type} {b : B} {f : A → B} (p : Π a, f a = b) + {a₀ a₁ : A} (q : a₀ = a₁) : square (p a₀) (p a₁) (ap f q) idp := + by induction q; apply vrfl + end eq diff --git a/hott/homotopy/join.hlean b/hott/homotopy/join.hlean index bab876732..f5f7146ed 100644 --- a/hott/homotopy/join.hlean +++ b/hott/homotopy/join.hlean @@ -6,17 +6,19 @@ Authors: Jakob von Raumer Declaration of a join as a special case of a pushout -/ -import hit.pushout .susp +import hit.pushout .susp cubical.cube cubical.squareover -open eq function prod equiv pushout is_trunc bool +open eq function prod equiv pushout is_trunc bool sigma.ops function namespace join + section + variables (A B C : Type) - definition join (A B : Type) : Type := @pushout (A × B) A B pr1 pr2 + definition join : Type := @pushout (A × B) A B pr1 pr2 definition jglue {A B : Type} (a : A) (b : B) := @glue (A × B) A B pr1 pr2 (a, b) - protected definition is_contr (A B : Type) [HA : is_contr A] : + protected definition is_contr [HA : is_contr A] : is_contr (join A B) := begin fapply is_contr.mk, exact inl (center A), @@ -26,7 +28,7 @@ namespace join generalize center_eq a, intro p, cases p, apply idp_con, end - protected definition bool (A : Type) : join bool A ≃ susp A := + protected definition bool : join bool A ≃ susp A := begin fapply equiv.MK, intro ba, induction ba with b a, induction b, exact susp.south, exact susp.north, exact susp.north, @@ -60,14 +62,13 @@ namespace join apply square_of_eq_top, rewrite idp_con, apply !con.right_inv⁻¹, end - protected definition swap (A B : Type) : - join A B → join B A := + protected definition swap : join A B → join B A := begin intro x, induction x with a b, exact inr a, exact inl b, apply !jglue⁻¹ end - protected definition swap_involutive (A B : Type) (x : join A B) : + protected definition swap_involutive (x : join A B) : join.swap B A (join.swap A B x) = x := begin induction x with a b, do 2 reflexivity, @@ -78,30 +79,70 @@ namespace join krewrite [elim_glue, ap_inv, elim_glue], apply inv_inv, end - protected definition symm (A B : Type) : join A B ≃ join B A := + protected definition symm : join A B ≃ join B A := begin fapply equiv.MK, do 2 apply join.swap, do 2 apply join.swap_involutive, end - protected definition switch (A B C : Type) : - join (join A B) C → join (join C B) A := - begin - intro x, induction x with ab c, - induction ab with a b, exact inr a, exact inl (inr b), - apply !jglue⁻¹, exact inl (inl c), esimp, - induction x with ab c, induction ab with a b, apply !jglue⁻¹, - apply ap inl, apply !jglue⁻¹, induction x with a b, esimp, - let H := eq_of_square (square_of_pathover (apdo (λ x, jglue x a) (jglue c b))), - rewrite [ap_constant at H, con_idp at H], apply eq_pathover, esimp, - krewrite [elim_glue, ap_constant, ap_inv], esimp, apply hinverse, - esimp at *, apply square_of_eq, krewrite [H, con.assoc, con.right_inv], - krewrite [idp_con], end - print definition join.switch - protected definition switch_involutive (A B C : Type) (x : join (join A B) C) : - join.switch C B A (join.switch A B C x) = x := sorry + --This proves that the join operator is associative + --The proof is more or less ported from Evan Cavallo's agda version + section switch_assoc + 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 := + by induction sq; exact ids + + variables {A B C : Type} + + private definition switch_left : join A B → join (join C B) A := + begin + intro x, induction x with a b, exact inr a, exact inl (inr b), apply !jglue⁻¹, + 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 _ _))) := + 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 (switch_coh_fill _ _ _).1, + end + + protected definition switch : join (join A B) C → join (join C B) A := + begin + intro x, induction x with ab c, exact switch_left ab, exact inl (inl c), + induction x with ab c, exact switch_coh ab c, + end + + private definition switch_inv_left_square (a : A) (b : B) : + square idp idp (ap (!(@join.switch C) ∘ switch_left) (jglue a b)) (ap inl (jglue a b)) := + begin + refine hdeg_square !ap_compose ⬝h _, + refine aps join.switch (hdeg_square !elim_glue) ⬝h _, esimp, + refine hdeg_square !(ap_inv join.switch) ⬝h _, + refine hrfl⁻¹ʰ⁻¹ᵛ ⬝h _, esimp[join.switch,switch_left,switch_coh], + refine (hdeg_square !elim_glue)⁻¹ᵛ ⬝h _, esimp, + refine (hdeg_square !ap_inv)⁻¹ᵛ ⬝h _, apply hdeg_square !inv_inv, + end + + private definition switch_inv_coh_left (c : C) (a : A) : + square idp idp (ap !(@join.switch C B) (switch_coh (inl a) c)) (jglue (inl a) c) := + begin + refine hrfl ⬝h _, + refine + end + + + end switch_assoc + +exit protected definition switch_equiv (A B C : Type) : join (join A B) C ≃ join (join C B) A :=