small changes in colimit

colimit/pointed.hlean

@@ -11,6 +11,9 @@ namespace seq_colim
   definition pseq_colim [constructor] {X : ℕ → Type*} (f : pseq_diagram X) : Type* :=
   pointed.MK (seq_colim f) (@sι _ _ 0 pt)
 
+  variables {A A' : ℕ → Type*} {f : pseq_diagram A} {f' : pseq_diagram A'}
+    {τ : Πn, A n →* A' n} {H : Πn, τ (n+1) ∘* f n ~* f' n ∘* τ n}
+
   definition inclusion_pt {X : ℕ → Type*} (f : pseq_diagram X) (n : ℕ)
     : inclusion f (Point (X n)) = Point (pseq_colim f) :=
   begin
@@ -162,47 +165,45 @@ namespace seq_colim
   theorem prep0_succ_lemma {A : ℕ → Type*} (f : pseq_diagram A) (n : ℕ)
     (p : rep0 (λn x, f n x) n pt = rep0 (λn x, f n x) n pt)
     (q : prep0 f n (Point (A 0)) = Point (A n))
-
     : loop_equiv_eq_closed (ap (@f n) q ⬝ respect_pt (@f n))
     (ap (@f n) p) = Ω→(@f n) (loop_equiv_eq_closed q p) :=
   by rewrite [▸*, con_inv, ↑ap1_gen, +ap_con, ap_inv, +con.assoc]
 
-  variables {A : ℕ → Type} (f : seq_diagram A)
-  definition succ_add_tr_rep {n : ℕ} (k : ℕ) (x : A n)
-    : transport A (succ_add n k) (rep f k (f x)) = rep f (succ k) x :=
-  begin
-    induction k with k p,
-      reflexivity,
-      exact tr_ap A succ (succ_add n k) _ ⬝ (fn_tr_eq_tr_fn (succ_add n k) f _)⁻¹ ⬝ ap (@f _) p,
-  end
-
-  definition succ_add_tr_rep_succ {n : ℕ} (k : ℕ) (x : A n)
-    : succ_add_tr_rep f (succ k) x = tr_ap A succ (succ_add n k) _ ⬝
-        (fn_tr_eq_tr_fn (succ_add n k) f _)⁻¹ ⬝ ap (@f _) (succ_add_tr_rep f k x) :=
-  by reflexivity
-
-  definition code_glue_equiv [constructor] {n : ℕ} (k : ℕ) (x y : A n)
-    : rep f k (f x) = rep f k (f y) ≃ rep f (succ k) x = rep f (succ k) y :=
-  begin
-    refine eq_equiv_fn_eq_of_equiv (equiv_ap A (succ_add n k)) _ _ ⬝e _,
-    apply eq_equiv_eq_closed,
-      exact succ_add_tr_rep f k x,
-      exact succ_add_tr_rep f k y
-  end
-
-  theorem code_glue_equiv_ap {n : ℕ} {k : ℕ} {x y : A n} (p : rep f k (f x) = rep f k (f y))
-    : code_glue_equiv f (succ k) x y (ap (@f _) p) = ap (@f _) (code_glue_equiv f k x y p) :=
-  begin
-    rewrite [▸*, +ap_con, ap_inv, +succ_add_tr_rep_succ, con_inv, inv_con_inv_right, +con.assoc],
-    apply whisker_left,
-    rewrite [- +con.assoc], apply whisker_right, rewrite [- +ap_compose'],
-    note s := (eq_top_of_square (natural_square_tr
-      (λx, fn_tr_eq_tr_fn (succ_add n k) f x ⬝ (tr_ap A succ (succ_add n k) (f x))⁻¹) p))⁻¹ᵖ,
-    rewrite [inv_con_inv_right at s, -con.assoc at s], exact s
-  end
+  -- definition succ_add_tr_rep {A : ℕ → Type} (f : seq_diagram A) {n : ℕ} (k : ℕ) (x : A n)
+  --   : transport A (succ_add n k) (rep f k (f x)) = rep f (succ k) x :=
+  -- begin
+  --   induction k with k p,
+  --     reflexivity,
+  --     exact tr_ap A succ (succ_add n k) _ ⬝ (fn_tr_eq_tr_fn (succ_add n k) f _)⁻¹ ⬝ ap (@f _) p,
+  -- end
+
+  -- definition succ_add_tr_rep_succ {A : ℕ → Type} (f : seq_diagram A) {n : ℕ} (k : ℕ) (x : A n)
+  --   : succ_add_tr_rep f (succ k) x = tr_ap A succ (succ_add n k) _ ⬝
+  --       (fn_tr_eq_tr_fn (succ_add n k) f _)⁻¹ ⬝ ap (@f _) (succ_add_tr_rep f k x) :=
+  -- by reflexivity
+
+  -- definition code_glue_equiv [constructor] {A : ℕ → Type} (f : seq_diagram A) {n : ℕ} (k : ℕ) (x y : A n)
+  --   : rep f k (f x) = rep f k (f y) ≃ rep f (succ k) x = rep f (succ k) y :=
+  -- begin
+  --   refine eq_equiv_fn_eq_of_equiv (equiv_ap A (succ_add n k)) _ _ ⬝e _,
+  --   apply eq_equiv_eq_closed,
+  --     exact succ_add_tr_rep f k x,
+  --     exact succ_add_tr_rep f k y
+  -- end
+
+  -- theorem code_glue_equiv_ap {n : ℕ} {k : ℕ} {x y : A n} (p : rep f k (f x) = rep f k (f y))
+  --   : code_glue_equiv f (succ k) x y (ap (@f _) p) = ap (@f _) (code_glue_equiv f k x y p) :=
+  -- begin
+  --   rewrite [▸*, +ap_con, ap_inv, +succ_add_tr_rep_succ, con_inv, inv_con_inv_right, +con.assoc],
+  --   apply whisker_left,
+  --   rewrite [- +con.assoc], apply whisker_right, rewrite [- +ap_compose'],
+  --   note s := (eq_top_of_square (natural_square_tr
+  --     (λx, fn_tr_eq_tr_fn (succ_add n k) f x ⬝ (tr_ap A succ (succ_add n k) (f x))⁻¹) p))⁻¹ᵖ,
+  --   rewrite [inv_con_inv_right at s, -con.assoc at s], exact s
+  -- end
 
   definition pseq_colim_loop {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) :
-    Ω (pseq_colim f) ≃* pseq_colim (λn, Ω→(f n)) :=
+    Ω (pseq_colim f) ≃* pseq_colim (λn, Ω→ (f n)) :=
   begin
     fapply pequiv_of_equiv,
     { refine !seq_colim_eq_equiv0 ⬝e _,
@@ -216,6 +217,10 @@ namespace seq_colim
     pseq_colim_loop f ∘* Ω→ (pinclusion f n) ~* pinclusion (λn, Ω→(f n)) n :=
   sorry
 
+  definition pseq_colim_loop_natural (n : ℕ) : psquare (pseq_colim_loop f) (pseq_colim_loop f')
+    (Ω→ (pseq_colim_functor τ H)) (pseq_colim_functor (λn, Ω→ (τ n)) (λn, ap1_psquare (H n))) :=
+  sorry
+
   definition pseq_diagram_pfiber {A A' : ℕ → Type*} {f : pseq_diagram A} {f' : pseq_diagram A'}
     (g : Πn, A n →* A' n) (p : Πn, g (succ n) ∘* f n ~* f' n ∘* g n) :
     pseq_diagram (λk, pfiber (g k)) :=

colimit/seq_colim.hlean

@@ -602,6 +602,7 @@ begin
       exact (g_star_path_right_step g e w k x @(g_star_path_right g e w k)).2 }}
 end
 
+
 /- We now define the map back, and show using this induction principle that the composites are the identity -/
 variable {P}
 
@@ -742,6 +743,13 @@ begin
     intro n p, refine whisker_right _ (!lrep_irrel2⁻² ⬝ !ap_inv⁻¹) ⬝ !ap_con⁻¹ }
 end
 
+-- definition seq_colim_eq_equiv0'_natural {a₀ a₁ : A 0} {a₀' a₁' : A' 0} (p₀ : τ a₀ = a₀')
+--   (p₁ : τ a₁ = a₁') :
+--   hsquare (seq_colim_eq_equiv0' f a₀ a₁) (seq_colim_eq_equiv0' f' a₀' a₁')
+--     (pointed.ap1_gen (seq_colim_functor τ p) (ap (ι' f' 0) p₀) (ap (ι' f' 0) p₁))
+--     (seq_colim_functor (λn, pointed.ap1_gen (@τ _)) _) :=
+-- _
+
 definition seq_colim_eq_equiv0 (a₀ a₁ : A 0) : ι f a₀ = ι f a₁ ≃ seq_colim (id0_seq_diagram f a₀ a₁) :=
 seq_colim_eq_equiv0' f a₀ a₁ ⬝e seq_colim_id_equiv_seq_colim_id0 f a₀ a₁
 

colimit/sequence.hlean

@@ -152,7 +152,7 @@ namespace seq_colim
     { apply pathover_ap, exact apo f IH}
   end
 
-  variable {f}
+  variables {f f'}
   definition is_trunc_fun_lrep (k : ℕ₋₂) (H : n ≤ m) (H2 : Πn, is_trunc_fun k (@f n)) :
     is_trunc_fun k (lrep f H) :=
   begin induction H with m H IH, apply is_trunc_fun_id, exact is_trunc_fun_compose k (H2 m) IH end
@@ -161,7 +161,21 @@ namespace seq_colim
     is_conn_fun k (lrep f H) :=
   begin induction H with m H IH, apply is_conn_fun_id, exact is_conn_fun_compose k (H2 m) IH end
 
-  variable (f)
+  definition lrep_natural (τ : Π⦃n⦄, A n → A' n) (p : Π⦃n⦄ (a : A n), τ (f a) = f' (τ a))
+    {n m : ℕ} (H : n ≤ m) (a : A n) : τ (lrep f H a) = lrep f' H (τ a) :=
+  begin
+    induction H with m H IH, reflexivity, exact p (lrep f H a) ⬝ ap (@f' m) IH
+  end
+
+  definition rep_natural (τ : Π⦃n⦄, A n → A' n) (p : Π⦃n⦄ (a : A n), τ (f a) = f' (τ a))
+    {n : ℕ} (k : ℕ) (a : A n) : τ (rep f k a) = rep f' k (τ a) :=
+  lrep_natural τ p _ a
+
+  definition rep0_natural (τ : Π⦃n⦄, A n → A' n) (p : Π⦃n⦄ (a : A n), τ (f a) = f' (τ a))
+    (k : ℕ) (a : A 0) : τ (rep0 f k a) = rep0 f' k (τ a) :=
+  lrep_natural τ p _ a
+
+  variables (f f')
 
   end generalized_lrep
 

move_to_lib.hlean

@@ -732,6 +732,33 @@ by induction q'; reflexivity
   -- end
 --rexact @(ap pathover_pr1) _ idpo _,
 
+  definition sigma_functor_compose {A A' A'' : Type} {B : A → Type} {B' : A' → Type}
+    {B'' : A'' → Type} {f' : A' → A''} {f : A → A'} (g' : Πa, B' a → B'' (f' a))
+    (g : Πa, B a → B' (f a)) (x : Σa, B a) :
+    sigma_functor f' g' (sigma_functor f g x) = sigma_functor (f' ∘ f) (λa, g' (f a) ∘ g a) x :=
+  begin
+    reflexivity
+  end
+
+  definition sigma_functor_homotopy {A A' : Type} {B : A → Type} {B' : A' → Type}
+    {f f' : A → A'} {g : Πa, B a → B' (f a)} {g' : Πa, B a → B' (f' a)} (h : f ~ f')
+    (k : Πa b, g a b =[h a] g' a b) (x : Σa, B a) : sigma_functor f g x = sigma_functor f' g' x :=
+  sigma_eq (h x.1) (k x.1 x.2)
+
+  variables {A₀₀ A₂₀ A₀₂ A₂₂ : Type}
+            {B₀₀ : A₀₀ → Type} {B₂₀ : A₂₀ → Type} {B₀₂ : A₀₂ → Type} {B₂₂ : A₂₂ → Type}
+            {f₁₀ : A₀₀ → A₂₀} {f₁₂ : A₀₂ → A₂₂} {f₀₁ : A₀₀ → A₀₂} {f₂₁ : A₂₀ → A₂₂}
+            {g₁₀ : Πa, B₀₀ a → B₂₀ (f₁₀ a)} {g₁₂ : Πa, B₀₂ a → B₂₂ (f₁₂ a)}
+            {g₀₁ : Πa, B₀₀ a → B₀₂ (f₀₁ a)} {g₂₁ : Πa, B₂₀ a → B₂₂ (f₂₁ a)}
+
+  definition sigma_functor_hsquare (h : hsquare f₁₀ f₁₂ f₀₁ f₂₁)
+    (k : Πa (b : B₀₀ a), g₂₁ _ (g₁₀ _ b) =[h a] g₁₂ _ (g₀₁ _ b)) :
+    hsquare (sigma_functor f₁₀ g₁₀) (sigma_functor f₁₂ g₁₂)
+            (sigma_functor f₀₁ g₀₁) (sigma_functor f₂₁ g₂₁) :=
+  λx, sigma_functor_compose g₂₁ g₁₀ x ⬝
+      sigma_functor_homotopy h k x ⬝
+      (sigma_functor_compose g₁₂ g₀₁ x)⁻¹
+
 end sigma open sigma
 
 namespace group