move colimit project here

cohomology/projective_space.hlean

@@ -119,7 +119,7 @@ namespace temp
     refine @(is_trunc_equiv_closed _ _) (fEinf (- 1) 0 dec_star),
     apply equiv_of_isomorphism,
     refine Einf_isomorphism fserre 0 _ _,
-    intro r H, --apply is_contr_fD2, change (- 1) - (- 1) >[ℤ] (- 0) - (r + 1),
+    intro r H, exact sorry, exact sorry --apply is_contr_fD2, change (- 1) - (- 1) >[ℤ] (- 0) - (r + 1),
 --    apply is_contr_fD, change (-0) - (r + 1) >[ℤ] 0,
 --exact sub_nat_lt 0 r,
     -- intro r H, apply is_contr_fD, change 0 + (r + 1) >[ℤ] 0,

colimit/local_ext.hlean

@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2016 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Egbert Rijke
+-/
+
+import hit.two_quotient .seq_colim
+
+open eq prod sum two_quotient sigma function relation e_closure nat seq_colim
+
+namespace localization
+section quasi_local_extension
+
+  universe variables u v w
+  parameters {A : Type.{u}} {P : A → Type.{v}} {Q : A → Type.{w}} (F : Πa, P a → Q a)
+  definition is_local [class] (Y : Type) : Type :=
+  Π(a : A), is_equiv (λg, g ∘ F a : (Q a → Y) → (P a → Y))
+
+
+
+  section
+  parameter (X : Type.{max u v w})
+  local abbreviation Y := X + Σa, (P a → X) × Q a
+
+  -- do we want to remove the contractible pairs?
+  inductive qleR : Y → Y → Type :=
+  | J : Π{a : A} (f : P a → X) (p : P a), qleR (inr ⟨a, (f, F a p)⟩) (inl (f p))
+  | k : Π{a : A} (g : Q a → X) (q : Q a), qleR (inl (g q)) (inr ⟨a, (g ∘ F a, q)⟩)
+
+  inductive qleQ : Π⦃y₁ y₂ : Y⦄, e_closure qleR y₁ y₂ → e_closure qleR y₁ y₂ → Type :=
+  | K : Π{a : A} (g : Q a → X) (p : P a), qleQ [qleR.k g (F a p)] [qleR.J (g ∘ F a) p]⁻¹ʳ
+
+  definition one_step_localization : Type := two_quotient qleR qleQ
+  definition incl : X → one_step_localization := incl0 _ _ ∘ inl
+
+  end
+  variables (X : Type.{max u v w}) {Z : Type}
+
+  definition n_step_localization : ℕ → Type :=
+  nat.rec X (λn Y, localization.one_step_localization F Y)
+
+  definition incln (n : ℕ) :
+    n_step_localization X n → n_step_localization X (succ n) :=
+  localization.incl F (n_step_localization X n)
+
+  -- localization if P and Q consist of ω-compact types
+  definition localization : Type := seq_colim (incln X)
+  definition incll : X → localization X := ι' _ 0
+
+  protected definition rec {P : localization X → Type} [Πz, is_local (P z)]
+    (H : Πx, P (incll X x)) (z : localization X) : P z :=
+  begin
+    exact sorry
+  end
+
+  definition extend {Y Z : Type} (f : Y → Z) [is_local Z] (x : one_step_localization Y) : Z :=
+  begin
+    induction x,
+    { induction a,
+      { exact f a},
+      { induction a with a v, induction v with f q, exact sorry}},
+    { exact sorry},
+    { exact sorry}
+  end
+
+  protected definition elim {Y : Type} [is_local Y]
+    (H : X → Y) (z : localization X) : Y :=
+  begin
+    induction z with n x n x,
+    { induction n with n IH,
+      { exact H x},
+      induction x,
+      { induction a,
+        { exact IH a},
+        { induction a with a v, induction v with f q, exact sorry}},
+      { exact sorry},
+      exact sorry},
+    exact sorry
+  end
+
+
+end quasi_local_extension
+end localization

colimit/omega_compact.hlean

@@ -0,0 +1,162 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Egbert Rijke
+-/
+
+import .seq_colim types.unit
+
+open eq nat is_equiv equiv is_trunc pi unit function prod unit sigma sigma.ops sum prod trunc fin
+     algebra
+
+namespace seq_colim
+
+  universe variable u
+  variables {A : ℕ → Type.{u}} (f : seq_diagram A)
+  variables {n : ℕ} (a : A n)
+
+  definition arrow_colim_of_colim_arrow [unfold 4] {X : Type}
+    (g : seq_colim (seq_diagram_arrow_left f X)) (x : X) : seq_colim f :=
+  begin induction g with n g n g, exact ι f (g x), exact glue f (g x) end
+
+  definition omega_compact [class] (X : Type) : Type :=
+  Π⦃A : ℕ → Type⦄ (f : seq_diagram A),
+  is_equiv (arrow_colim_of_colim_arrow f :
+             seq_colim (seq_diagram_arrow_left f X) → (X → seq_colim f))
+
+  definition equiv_of_omega_compact [unfold 4] (X : Type) [H : omega_compact X]
+    {A : ℕ → Type} (f : seq_diagram A) :
+    seq_colim (seq_diagram_arrow_left f X) ≃ (X → seq_colim f) :=
+  equiv.mk _ (H f)
+
+  definition omega_compact_of_equiv [unfold 4] (X : Type)
+    (H : Π⦃A : ℕ → Type⦄ (f : seq_diagram A),
+      seq_colim (seq_diagram_arrow_left f X) ≃ (X → seq_colim f))
+    (p : Π⦃A : ℕ → Type⦄ (f : seq_diagram A) {n : ℕ} (g : X → A n) (x : X),
+      H f (ι _ g) x = ι _ (g x))
+    (q : Π⦃A : ℕ → Type⦄ (f : seq_diagram A) {n : ℕ} (g : X → A n) (x : X),
+      square (p f (@f n ∘ g) x) (p f g x) (ap (λg, H f g x)
+             (glue (seq_diagram_arrow_left f X) g)) (glue f (g x)))
+    : omega_compact X :=
+  λA f, is_equiv_of_equiv_of_homotopy (H f)
+  begin
+    intro g, apply eq_of_homotopy, intro x,
+    induction g with n g n g,
+    { exact p f g x },
+    { apply eq_pathover, refine _ ⬝hp !elim_glue⁻¹, exact q f g x }
+  end
+
+  local attribute is_contr_seq_colim [instance]
+  definition is_contr_empty_arrow [instance] (X : Type) : is_contr (empty → X) :=
+  by apply is_trunc_pi; contradiction
+
+  definition omega_compact_empty [instance] [constructor] : omega_compact empty :=
+  begin
+    intro A f,
+    fapply adjointify,
+    { intro g, exact ι' _ 0 empty.elim},
+    { intro g, apply eq_of_homotopy, contradiction},
+    { intro h, apply is_prop.elim}
+  end
+
+  definition omega_compact_unit' [instance] [constructor] : omega_compact unit :=
+  begin
+    intro A f,
+    fapply adjointify,
+    { intro g, induction g ⋆,
+      { exact ι _ (λx, a)},
+      { apply glue}},
+    { intro g, apply eq_of_homotopy, intro u, induction u,
+      induction g ⋆,
+      { reflexivity},
+      { esimp, apply eq_pathover_id_right, apply hdeg_square,
+        refine ap_compose (λx, arrow_colim_of_colim_arrow f x ⋆) _ _ ⬝ _,
+        refine ap02 _ !elim_glue ⬝ _, apply elim_glue}},
+    { intro h, induction h with n h n h,
+      { esimp, apply ap (ι' _ n), apply unit_arrow_eq},
+      { esimp, apply eq_pathover_id_right,
+        refine ap_compose' (seq_colim.elim _ _ _) _ _ ⬝ph _,
+        refine ap02 _ !elim_glue ⬝ph _,
+        refine !elim_glue ⬝ph _,
+        refine _ ⬝pv natural_square_tr (@glue _ (seq_diagram_arrow_left f unit) n) (unit_arrow_eq h),
+        refine _ ⬝ (ap_compose (ι' _ _) _ _)⁻¹,
+        apply ap02, unfold [seq_diagram_arrow_left],
+        apply unit_arrow_eq_compose}}
+  end
+
+  -- The following is a start of a different proof that unit is omega-compact,
+  -- which proves first that the types are equivalent
+  definition omega_compact_unit [instance] [constructor] : omega_compact unit :=
+  begin
+    fapply omega_compact_of_equiv,
+    { intro A f, refine _ ⬝e !arrow_unit_left⁻¹ᵉ, fapply seq_colim_equiv,
+      { intro n, apply arrow_unit_left },
+      intro n f, reflexivity },
+    { intros, induction x, reflexivity },
+    { intros, induction x, esimp, apply hdeg_square, exact !elim_glue ⬝ !idp_con },
+  end
+
+  local attribute equiv_of_omega_compact [constructor]
+  definition omega_compact_prod [instance] [constructor] {X Y : Type} [omega_compact.{_ u} X]
+    [omega_compact.{u u} Y] : omega_compact.{_ u} (X × Y) :=
+  begin
+    fapply omega_compact_of_equiv,
+    { intro A f,
+      exact calc
+        seq_colim (seq_diagram_arrow_left f (X × Y))
+              ≃ seq_colim (seq_diagram_arrow_left (seq_diagram_arrow_left f Y) X) :
+                  begin
+                    apply seq_colim_equiv (λn, !imp_imp_equiv_prod_imp⁻¹ᵉ),
+                    intro n f, reflexivity
+                  end
+          ... ≃ (X → seq_colim (seq_diagram_arrow_left f Y))  : !equiv_of_omega_compact
+          ... ≃ (X → Y → seq_colim f) : arrow_equiv_arrow_right _ !equiv_of_omega_compact
+          ... ≃ (X × Y → seq_colim f) : imp_imp_equiv_prod_imp },
+    { intros, induction x with x y, reflexivity },
+    { intros, induction x with x y, apply hdeg_square,
+      refine ap_compose (λz, arrow_colim_of_colim_arrow f z y) _ _ ⬝ _,
+      refine ap02 _ (ap_compose (λz, arrow_colim_of_colim_arrow _ z x) _ _) ⬝ _,
+      refine ap02 _ (ap02 _ !elim_glue) ⬝ _, refine ap02 _ (ap02 _ !idp_con) ⬝ _, esimp,
+      refine ap02 _ !elim_glue ⬝ _, apply elim_glue }
+  end
+
+definition not_omega_compact_nat : ¬(omega_compact.{0 0} ℕ) :=
+assume H,
+let e := equiv_of_omega_compact ℕ seq_diagram_fin ⬝e
+         arrow_equiv_arrow_right _ seq_colim_fin_equiv in
+begin
+--  check_expr e,
+  have Πx, ∥ Σn, Πm, e x m < n ∥,
+  begin
+    intro f, induction f using seq_colim.rec_prop with n f,
+    refine tr ⟨n, _⟩, intro m, exact is_lt (f m)
+  end,
+  induction this (e⁻¹ᵉ id) with x, induction x with n H2,
+  apply lt.irrefl n,
+  refine lt_of_le_of_lt (le_of_eq _) (H2 n),
+  exact ap10 (right_inv e id)⁻¹ n
+end
+
+exit
+  print seq_diagram_over
+  definition seq_colim_over_equiv {X : Type} {A : X → ℕ → Type} (g : Π⦃x n⦄, A x n → A x (succ n))
+    (x : X)
+    : @seq_colim_over _ (constant_seq X) _ _ ≃ seq_colim (@g x) :=
+  begin
+
+  end
+
+  definition seq_colim_pi_equiv {X : Type} {A : X → ℕ → Type} (g : Π⦃x n⦄, A x n → A x (succ n))
+    [omega_compact X] : (Πx, seq_colim (@g x)) ≃ seq_colim (seq_diagram_pi g) :=
+  -- calc
+--    (Πx, seq_colim (@g x)) ≃ Πx, seq_colim (@g x)
+  begin
+    refine !pi_equiv_arrow_sigma ⬝e _,
+    refine sigma_equiv_sigma_left (arrow_equiv_arrow_right X (sigma_equiv_sigma_left (seq_colim_constant_seq X)⁻¹ᵉ)) ⬝e _,
+    exact sigma_equiv_sigma_left (arrow_equiv_arrow_right X _) ⬝e _,
+  end
+
+  set_option pp.universes true
+  print seq_diagram_arrow_left
+
+end seq_colim

colimit/omega_compact_sum.hlean

@@ -0,0 +1,158 @@
+import .omega_compact ..homotopy.fwedge
+
+open eq nat seq_colim is_trunc equiv is_equiv trunc sigma sum pi function algebra sigma.ops
+
+variables {A A' : ℕ → Type} (f : seq_diagram A) (f' : seq_diagram A') {n : ℕ} (a : A n)
+universe variable u
+
+definition kshift_up (k : ℕ) (x : seq_colim f) : seq_colim (kshift_diag f k) :=
+begin
+  induction x with n a n a,
+  { apply ι' (kshift_diag f k) n, exact lrep f (le_add_left n k) a },
+  { exact ap (ι _) (lrep_f f _ a ⬝ lrep_irrel f _ _ a ⬝ !f_lrep⁻¹) ⬝ !glue }
+end
+
+definition kshift_down [unfold 4] (k : ℕ) (x : seq_colim (kshift_diag f k)) : seq_colim f :=
+begin
+  induction x with n a n a,
+  { exact ι' f (k + n) a },
+  { exact glue f a }
+end
+
+definition kshift_equiv_eq_kshift_up (k : ℕ) (a : A n) : kshift_equiv f k (ι f a) = kshift_up f k (ι f a) :=
+begin
+  induction k with k p,
+  { exact ap (ι _) !lrep_eq_transport⁻¹ },
+  { exact sorry }
+end
+
+definition kshift_equiv2 [constructor] (k : ℕ) : seq_colim f ≃ seq_colim (kshift_diag f k) :=
+begin
+  refine equiv_change_fun (kshift_equiv f k) _,
+    exact kshift_up f k,
+  intro x, induction x with n a n a,
+  { exact kshift_equiv_eq_kshift_up f k a },
+  { exact sorry }
+end
+
+definition kshift_equiv_inv_eq_kshift_down (k : ℕ) (a : A (k + n)) :
+  kshift_equiv_inv f k (ι' (kshift_diag f k) n a) = kshift_down f k (ι' (kshift_diag f k) n a) :=
+begin
+  induction k with k p,
+  { exact apd011 (ι' _) _ !pathover_tr⁻¹ᵒ },
+  { exact sorry }
+end
+
+definition kshift_equiv_inv2 [constructor] (k : ℕ) : seq_colim (kshift_diag f k) ≃ seq_colim f :=
+begin
+  refine equiv_change_fun (equiv_change_inv (kshift_equiv_inv f k) _) _,
+  { exact kshift_up f k },
+  { intro x, induction x with n a n a,
+    { exact kshift_equiv_eq_kshift_up f k a },
+    { exact sorry }},
+  { exact kshift_down f k },
+  { intro x, induction x with n a n a,
+    { exact !kshift_equiv_inv_eq_kshift_down },
+    { exact sorry }}
+end
+
+definition seq_colim_over_weakened_sequence [unfold 5] (x : seq_colim f) :
+  seq_colim_over (weakened_sequence f f') x ≃ seq_colim f' :=
+begin
+  induction x with n a n a,
+  { exact kshift_equiv_inv2 f' n },
+  { apply equiv_pathover_inv, apply arrow_pathover_constant_left, intro x,
+    apply pathover_of_tr_eq, refine !seq_colim_over_glue ⬝ _, exact sorry }
+end
+
+definition seq_colim_prod' [constructor] : seq_colim (seq_diagram_prod f f') ≃ seq_colim f × seq_colim f' :=
+calc
+  seq_colim (seq_diagram_prod f f') ≃ seq_colim (seq_diagram_sigma (weakened_sequence f f')) :
+        by exact seq_colim_equiv (λn, !sigma.equiv_prod⁻¹ᵉ) (λn a, idp)
+  ... ≃ Σ(x : seq_colim f), seq_colim_over (weakened_sequence f f') x :
+        by exact (sigma_seq_colim_over_equiv _ (weakened_sequence f f'))⁻¹ᵉ
+  ... ≃ Σ(x : seq_colim f), seq_colim f' :
+        by exact sigma_equiv_sigma_right (seq_colim_over_weakened_sequence f f')
+  ... ≃ seq_colim f × seq_colim f' :
+        by exact sigma.equiv_prod (seq_colim f) (seq_colim f')
+
+open prod prod.ops
+example {a' : A' n} : seq_colim_prod' f f' (ι _ (a, a')) = (ι f a, ι f' a') := idp
+
+definition seq_colim_prod_inv {a' : A' n} : (seq_colim_prod' f f')⁻¹ᵉ (ι f a, ι f' a') = (ι _ (a, a')) :=
+begin
+  exact sorry
+end
+
+definition prod_seq_colim_of_seq_colim_prod (x : seq_colim (seq_diagram_prod f f')) :
+  seq_colim f × seq_colim f' :=
+begin
+  induction x with n x n x,
+  { exact (ι f x.1, ι f' x.2) },
+  { exact prod_eq (glue f x.1) (glue f' x.2) }
+end
+
+definition seq_colim_prod [constructor] :
+  seq_colim (seq_diagram_prod f f') ≃ seq_colim f × seq_colim f' :=
+begin
+  refine equiv_change_fun (seq_colim_prod' f f') _,
+    exact prod_seq_colim_of_seq_colim_prod f f',
+  intro x, induction x with n x n x,
+  { reflexivity },
+  { induction x with a a', apply eq_pathover, apply hdeg_square, esimp,
+    refine _ ⬝ !elim_glue⁻¹,
+    refine ap_compose ((sigma.equiv_prod (seq_colim f) (seq_colim f') ∘
+                       sigma_equiv_sigma_right (seq_colim_over_weakened_sequence f f')) ∘
+                       sigma_colim_of_colim_sigma (weakened_sequence f f')) _ _ ⬝ _,
+    refine ap02 _ (!elim_glue ⬝ !idp_con) ⬝ _,
+    refine !ap_compose ⬝ _, refine ap02 _ !elim_glue ⬝ _,
+    refine !ap_compose ⬝ _, esimp, refine ap02 _ !ap_sigma_functor_id_sigma_eq ⬝ _,
+    apply eq_of_fn_eq_fn (prod_eq_equiv _ _), apply pair_eq,
+    { exact !ap_compose'⁻¹ ⬝ !sigma_eq_pr1 ⬝ !prod_eq_pr1⁻¹ },
+    { refine !ap_compose'⁻¹ ⬝ _ ⬝ !prod_eq_pr2⁻¹, esimp,
+      refine !sigma_eq_pr2_constant ⬝ _,
+      refine !eq_of_pathover_apo ⬝ _, exact sorry }}
+end
+
+  local attribute equiv_of_omega_compact [constructor]
+
+  definition omega_compact_sum [instance] [constructor] {X Y : Type} [omega_compact.{_ u} X]
+    [omega_compact.{u u} Y] : omega_compact.{_ u} (X ⊎ Y) :=
+  begin
+    fapply omega_compact_of_equiv,
+    { intro A f,
+      exact calc
+      seq_colim (seq_diagram_arrow_left f (X ⊎ Y))
+          ≃ seq_colim (seq_diagram_prod (seq_diagram_arrow_left f X) (seq_diagram_arrow_left f Y)) :
+            by exact seq_colim_equiv (λn, !imp_prod_imp_equiv_sum_imp⁻¹ᵉ) (λn f, idp)
+      ... ≃ seq_colim (seq_diagram_arrow_left f X) × seq_colim (seq_diagram_arrow_left f Y) :
+            by apply seq_colim_prod
+      ... ≃ (X → seq_colim f) × (Y → seq_colim f) :
+            by exact prod_equiv_prod (equiv_of_omega_compact X f) (equiv_of_omega_compact Y f)
+      ... ≃ ((X ⊎ Y) → seq_colim f) :
+            by exact !imp_prod_imp_equiv_sum_imp },
+    { intros, induction x with x y: reflexivity },
+    { intros, induction x with x y: apply hdeg_square,
+      { refine ap_compose (((λz, arrow_colim_of_colim_arrow f z _) ∘ pr1) ∘
+          seq_colim_prod _ _) _ _ ⬝ _, refine ap02 _ (!elim_glue ⬝ !idp_con) ⬝ _,
+        refine !ap_compose ⬝ _, refine ap02 _ !elim_glue ⬝ _,
+        refine !ap_compose ⬝ _, refine ap02 _ !prod_eq_pr1 ⬝ !elim_glue },
+      { refine ap_compose (((λz, arrow_colim_of_colim_arrow f z _) ∘ pr2) ∘
+          seq_colim_prod _ _) _ _ ⬝ _, refine ap02 _ (!elim_glue ⬝ !idp_con) ⬝ _,
+        refine !ap_compose ⬝ _, refine ap02 _ !elim_glue ⬝ _,
+        refine !ap_compose ⬝ _, refine ap02 _ !prod_eq_pr2 ⬝ !elim_glue }},
+  end
+
+open wedge pointed circle
+
+/- needs fwedge! -/
+definition seq_diagram_fwedge (X : Type*) : seq_diagram (λn, @fwedge (A n) (λa, X)) :=
+sorry f
+
+definition seq_colim_fwedge_equiv (X : Type*) [is_trunc 1 X] :
+  seq_colim (seq_diagram_fwedge f X) ≃ @fwedge (seq_colim f) (λn, X) :=
+sorry
+
+definition not_omega_compact_fwedge_nat_circle : ¬(omega_compact.{0 0} (@fwedge ℕ (λn, S¹*))) :=
+assume H,
+sorry

colimit/pointed.hlean

@@ -0,0 +1,257 @@
+/- pointed sequential colimits -/
+
+-- authors: Floris van Doorn, Egbert Rijke, Stefano Piceghello
+
+import .seq_colim types.fin homotopy.chain_complex types.pointed2
+open seq_colim pointed algebra eq is_trunc nat is_equiv equiv sigma sigma.ops chain_complex fiber
+
+namespace seq_colim
+
+  definition pseq_diagram [reducible] (A : ℕ → Type*) : Type := Πn, A n →* A (succ n)
+  definition pseq_colim [constructor] {X : ℕ → Type*} (f : pseq_diagram X) : Type* :=
+  pointed.MK (seq_colim f) (@sι _ _ 0 pt)
+
+  definition inclusion_pt {X : ℕ → Type*} (f : pseq_diagram X) (n : ℕ)
+    : inclusion f (Point (X n)) = Point (pseq_colim f) :=
+  begin
+    induction n with n p,
+      reflexivity,
+      exact (ap (sι f) (respect_pt _))⁻¹ᵖ ⬝ (!glue ⬝ p)
+  end
+
+  definition pinclusion [constructor] {X : ℕ → Type*} (f : pseq_diagram X) (n : ℕ)
+    : X n →* pseq_colim f :=
+  pmap.mk (inclusion f) (inclusion_pt f n)
+
+  definition pshift_equiv [constructor] {A : ℕ → Type*} (f : Πn, A n →* A (succ n)) :
+    pseq_colim f ≃* pseq_colim (λn, f (n+1)) :=
+  begin
+    fapply pequiv_of_equiv,
+    { apply shift_equiv },
+    { exact ap (ι _) (respect_pt (f 0)) }
+  end
+
+  definition pshift_equiv_pinclusion {A : ℕ → Type*} (f : Πn, A n →* A (succ n)) (n : ℕ) :
+    psquare (pinclusion f n) (pinclusion (λn, f (n+1)) n) (f n) (pshift_equiv f)  :=
+  phomotopy.mk homotopy.rfl begin
+    refine !idp_con ⬝ _, esimp,
+    induction n with n IH,
+    { esimp[inclusion_pt], esimp[shift_diag], exact !idp_con⁻¹ },
+    { esimp[inclusion_pt], refine !con_inv_cancel_left ⬝ _,
+      rewrite ap_con, rewrite ap_con,
+      refine _ ⬝ whisker_right _ !con.assoc,
+      refine _ ⬝ (con.assoc (_ ⬝ _) _ _)⁻¹,
+      xrewrite [-IH],
+      esimp[shift_up], rewrite [elim_glue,  ap_inv, -ap_compose'], esimp,
+      rewrite [-+con.assoc], apply whisker_right,
+      rewrite con.assoc, apply !eq_inv_con_of_con_eq,
+      symmetry, exact eq_of_square !natural_square
+  }
+  end
+
+  definition pseq_colim_functor [constructor] {A A' : ℕ → Type*} {f : pseq_diagram A}
+    {f' : pseq_diagram A'} (g : Πn, A n →* A' n)
+    (p : Π⦃n⦄, g (n+1) ∘* f n ~ f' n ∘* g n) : pseq_colim f →* pseq_colim f' :=
+  pmap.mk (seq_colim_functor g p) (ap (ι _) (respect_pt (g _)))
+
+  definition pseq_colim_pequiv' [constructor] {A A' : ℕ → Type*} {f : pseq_diagram A}
+    {f' : pseq_diagram A'} (g : Πn, A n ≃* A' n)
+    (p : Π⦃n⦄, g (n+1) ∘* f n ~ f' n ∘* g n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pequiv_of_equiv (seq_colim_equiv g p) (ap (ι _) (respect_pt (g _)))
+
+  definition pseq_colim_pequiv [constructor] {A A' : ℕ → Type*} {f : pseq_diagram A}
+    {f' : pseq_diagram A'} (g : Πn, A n ≃* A' n)
+    (p : Πn, g (n+1) ∘* f n ~* f' n ∘* g n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pseq_colim_pequiv' g (λn, @p n)
+
+  -- definition seq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : pseq_diagram A}
+  --   (p : Π⦃n⦄ (a : A n), f n a = f' n a) : seq_colim f ≃ seq_colim f' :=
+  -- seq_colim_equiv (λn, erfl) p
+
+  definition pseq_colim_equiv_constant' [constructor] {A : ℕ → Type*} {f f' : pseq_diagram A}
+    (p : Π⦃n⦄, f n ~ f' n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pseq_colim_pequiv' (λn, pequiv.rfl) p
+
+  definition pseq_colim_equiv_constant [constructor] {A : ℕ → Type*} {f f' : pseq_diagram A}
+    (p : Πn, f n ~* f' n) : pseq_colim @f ≃* pseq_colim @f' :=
+  pseq_colim_pequiv (λn, pequiv.rfl) (λn, !pid_pcompose ⬝* p n ⬝* !pcompose_pid⁻¹*)
+
+  definition pseq_colim_pequiv_pinclusion {A A' : ℕ → Type*} {f : Πn, A n →* A (n+1)}
+    {f' : Πn, A' n →* A' (n+1)} (g : Πn, A n ≃* A' n)
+    (p : Π⦃n⦄, g (n+1) ∘* f n ~* f' n ∘* g n) (n : ℕ) :
+    psquare (pinclusion f n) (pinclusion f' n) (g n) (pseq_colim_pequiv g p) :=
+  phomotopy.mk homotopy.rfl begin
+    esimp, refine !idp_con ⬝ _,
+    induction n with n IH,
+    { esimp[inclusion_pt], exact !idp_con⁻¹ },
+    { esimp[inclusion_pt], rewrite [+ap_con, -+ap_inv, +con.assoc, +seq_colim_functor_glue],
+      xrewrite[-IH],
+      rewrite[-+ap_compose', -+con.assoc],
+      apply whisker_right, esimp,
+      rewrite[(eq_con_inv_of_con_eq (to_homotopy_pt (@p _)))],
+      rewrite[ap_con], esimp,
+      rewrite[-+con.assoc, ap_con, -ap_compose', +ap_inv],
+      rewrite[-+con.assoc],
+      refine _ ⬝ whisker_right _ (whisker_right _ (whisker_right _ (whisker_right _ !con.left_inv⁻¹))),
+      rewrite[idp_con, +con.assoc], apply whisker_left,
+      rewrite[ap_con, -ap_compose', con_inv, +con.assoc], apply whisker_left,
+      refine eq_inv_con_of_con_eq _,
+      symmetry, exact eq_of_square !natural_square
+    }
+  end
+
+  definition seq_colim_equiv_constant_pinclusion {A : ℕ → Type*} {f f' : pseq_diagram A}
+    (p : Πn, f n ~* f' n) (n : ℕ) :
+    pseq_colim_equiv_constant p ∘* pinclusion f n ~* pinclusion f' n  :=
+  begin
+    transitivity pinclusion f' n ∘* !pid,
+    refine phomotopy_of_psquare !pseq_colim_pequiv_pinclusion,
+    exact !pcompose_pid
+  end
+
+  definition pseq_colim.elim' [constructor] {A : ℕ → Type*} {B : Type*} {f : pseq_diagram A}
+    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f n ~ g n) : pseq_colim f →* B :=
+  begin
+    fapply pmap.mk,
+    { intro x, induction x with n a n a,
+      { exact g n a },
+      { exact p n a }},
+    { esimp, apply respect_pt }
+  end
+
+  definition pseq_colim.elim [constructor] {A : ℕ → Type*} {B : Type*} {f : pseq_diagram A}
+    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f n ~* g n) : pseq_colim @f →* B :=
+  pseq_colim.elim' g p
+
+  definition pseq_colim.elim_pinclusion {A : ℕ → Type*} {B : Type*} {f : pseq_diagram A}
+    (g : Πn, A n →* B) (p : Πn, g (n+1) ∘* f n ~* g n) (n : ℕ) :
+  pseq_colim.elim g p ∘* pinclusion f n ~* g n :=
+  begin
+    refine phomotopy.mk phomotopy.rfl _,
+    refine !idp_con ⬝ _,
+    esimp,
+    induction n with n IH,
+    { esimp, esimp[inclusion_pt], exact !idp_con⁻¹ },
+    { esimp, esimp[inclusion_pt],
+      rewrite ap_con, rewrite ap_con,
+      rewrite elim_glue,
+      rewrite [-ap_inv],
+      rewrite [-ap_compose'], esimp,
+      rewrite [(eq_con_inv_of_con_eq (!to_homotopy_pt))],
+      rewrite [IH],
+      rewrite [con_inv],
+      rewrite [-+con.assoc],
+      refine _ ⬝ whisker_right _ !con.assoc⁻¹,
+      rewrite [con.left_inv], esimp,
+      refine _ ⬝ !con.assoc⁻¹,
+      rewrite [con.left_inv], esimp,
+      rewrite [ap_inv],
+      rewrite [-con.assoc],
+      refine !idp_con⁻¹ ⬝ whisker_right _ !con.left_inv⁻¹,
+    }
+  end
+
+  definition prep0 [constructor] {A : ℕ → Type*} (f : pseq_diagram A) (k : ℕ) : A 0 →* A k :=
+  pmap.mk (rep0 (λn x, f n x) k)
+          begin induction k with k p, reflexivity, exact ap (@f k) p ⬝ !respect_pt end
+
+  definition respect_pt_prep0_succ {A : ℕ → Type*} (f : pseq_diagram A) (k : ℕ)
+    : respect_pt (prep0 f (succ k)) = ap (@f k) (respect_pt (prep0 f k)) ⬝ respect_pt (f k) :=
+  by reflexivity
+
+  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 pseq_colim_loop {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) :
+    Ω (pseq_colim f) ≃* pseq_colim (λn, Ω→(f n)) :=
+  begin
+    fapply pequiv_of_equiv,
+    { refine !seq_colim_eq_equiv0 ⬝e _,
+      fapply seq_colim_equiv,
+      { intro n, exact loop_equiv_eq_closed (respect_pt (prep0 f n)) },
+      { intro n p, apply prep0_succ_lemma }},
+    { reflexivity }
+  end
+
+  definition pseq_colim_loop_pinclusion {X : ℕ → Type*} (f : Πn, X n →* X (n+1)) (n : ℕ) :
+    pseq_colim_loop f ∘* Ω→ (pinclusion f n) ~* pinclusion (λn, Ω→(f n)) 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)) :=
+  λk, pfiber_functor (f k) (f' k) (p k)
+
+/- Two issues when going to the pointed version:
+  - seq_diagram_fiber τ p a for a : A n at position k lives over (A (n + k)), so for a : A 0 you get A (0 + k), but we need A k
+  - in seq_diagram_fiber the fibers are taken in rep f ..., but in the pointed version over the basepoint of A n
+-/
+definition pfiber_pseq_colim_functor {A A' : ℕ → Type*} {f : pseq_diagram A}
+  {f' : pseq_diagram A'} (τ : Πn, A n →* A' n)
+  (p : Π⦃n⦄, τ (n+1) ∘* f n ~* f' n ∘* τ n) : pfiber (pseq_colim_functor τ p) ≃*
+    pseq_colim (pseq_diagram_pfiber τ p) :=
+begin
+  fapply pequiv_of_equiv,
+  { refine fiber_seq_colim_functor0 τ p pt ⬝e _, fapply seq_colim_equiv, intro n, esimp,
+    repeat exact sorry }, exact sorry
+end
+
+
+  -- open succ_str
+  -- definition pseq_colim_succ_str_change_index' {N : succ_str} {B : N → Type*} (n : N) (m : ℕ)
+  --   (h : Πn, B n →* B (S n)) :
+  --   pseq_colim (λk, h (n +' (m + succ k))) ≃* pseq_colim (λk, h (S n +' (m + k))) :=
+  -- sorry
+
+  -- definition pseq_colim_succ_str_change_index {N : succ_str} {B : ℕ → N → Type*} (n : N)
+  --   (h : Π(k : ℕ) n, B k n →* B k (S n)) :
+  --   pseq_colim (λk, h k (n +' succ k)) ≃* pseq_colim (λk, h k (S n +' k)) :=
+  -- sorry
+
+  -- definition pseq_colim_index_eq_general {N : succ_str} (B : N → Type*) (f g : ℕ → N) (p : f ~ g)
+  --   (pf : Πn, S (f n) = f (n+1)) (pg : Πn, S (g n) = g (n+1)) (h : Πn, B n →* B (S n)) :
+  --   @pseq_colim (λn, B (f n)) (λn, ptransport B (pf n) ∘* h (f n)) ≃*
+  --   @pseq_colim (λn, B (g n)) (λn, ptransport B (pg n) ∘* h (g n)) :=
+  -- sorry
+
+
+end seq_colim

colimit/pushout.hlean

@@ -0,0 +1,216 @@
+/-
+  Suppose we have three sequences A = (Aₙ, fₙ)ₙ, B = (Bₙ, gₙ)ₙ, C = (Cₙ, hₙ)ₙ with natural
+  transformations like this: B ← A → C. We can take pushouts pointwise and then take the colimit,
+  or we can take the colimit of each and then pushout. By the 3x3 lemma these are equivalent.
+
+  Authors: Floris van Doorn
+-/
+
+import .seq_colim ..homotopy.pushout ..homotopy.three_by_three
+open eq nat seq_colim is_trunc equiv is_equiv trunc sigma sum pi function algebra sigma.ops
+
+section
+variables {A B : ℕ → Type} {f : seq_diagram A} {g : seq_diagram B} (i : Π⦃n⦄, A n → B n)
+  (p : Π⦃n⦄ (a : A n), i (f a) = g (i a)) (a a' : Σn, A n)
+
+
+definition total_seq_rel [constructor] (f : seq_diagram A) :
+  (Σ(a a' : Σn, A n), seq_rel f a a') ≃ Σn, A n :=
+begin
+  fapply equiv.MK,
+  { intro x, exact x.2.1 },
+  { intro x, induction x with n a, exact ⟨⟨n+1, f a⟩, ⟨n, a⟩, seq_rel.Rmk f a⟩ },
+  { intro x, induction x with n a, reflexivity },
+  { intro x, induction x with a x, induction x with a' r, induction r with n a, reflexivity }
+end
+
+definition pr1_total_seq_rel_inv (x : Σn, A n) :
+  ((total_seq_rel f)⁻¹ᵉ x).1 = sigma_functor succ f x :=
+begin induction x with n a, reflexivity end
+
+definition pr2_total_seq_rel_inv (x : Σn, A n) : ((total_seq_rel f)⁻¹ᵉ x).2.1 = x :=
+to_right_inv (total_seq_rel f) x
+
+include p
+definition seq_rel_functor [unfold 9] : seq_rel f a a' → seq_rel g (total i a) (total i a') :=
+begin
+  intro r, induction r with n a,
+  exact transport (λx, seq_rel g ⟨_, x⟩ _) (p a)⁻¹ (seq_rel.Rmk g (i a))
+end
+
+open pushout
+
+definition total_seq_rel_natural [unfold 7] :
+  hsquare (sigma_functor2 (total i) (seq_rel_functor i p)) (total i)
+          (total_seq_rel f) (total_seq_rel g) :=
+homotopy.rfl
+
+end
+
+
+section
+open pushout sigma.ops quotient
+
+parameters {A B C : ℕ → Type} {f : seq_diagram A} {g : seq_diagram B} {h : seq_diagram C}
+  (i : Π⦃n⦄, A n → B n) (j : Π⦃n⦄, A n → C n)
+  (p : Π⦃n⦄ (a : A n), i (f a) = g (i a)) (q : Π⦃n⦄ (a : A n), j (f a) = h (j a))
+
+
+definition seq_diagram_pushout : seq_diagram (λn, pushout (@i n) (@j n)) :=
+λn, pushout.functor (@f n) (@g n) (@h n) (@p n)⁻¹ʰᵗʸ (@q n)⁻¹ʰᵗʸ
+
+local abbreviation sA := Σn, A n
+local abbreviation sB := Σn, B n
+local abbreviation sC := Σn, C n
+local abbreviation si : sA → sB := total i
+local abbreviation sj : sA → sC := total j
+local abbreviation rA := Σ(x y : sA), seq_rel f x y
+local abbreviation rB := Σ(x y : sB), seq_rel g x y
+local abbreviation rC := Σ(x y : sC), seq_rel h x y
+set_option pp.abbreviations false
+local abbreviation ri : rA → rB := sigma_functor2 (total i) (seq_rel_functor i p)
+local abbreviation rj : rA → rC := sigma_functor2 (total j) (seq_rel_functor j q)
+
+definition pushout_seq_colim_span [constructor] : three_by_three_span :=
+@three_by_three_span.mk
+  sB (rB ⊎ rB) rB sA (rA ⊎ rA) rA sC (rC ⊎ rC) rC
+  (sum.rec pr1 (λx, x.2.1)) (sum.rec id id)
+  (sum.rec pr1 (λx, x.2.1)) (sum.rec id id)
+  (sum.rec pr1 (λx, x.2.1)) (sum.rec id id)
+  (total i) (total j) (ri +→ ri) (rj +→ rj) ri rj
+  begin intro x, induction x: reflexivity end
+  begin intro x, induction x: reflexivity end
+  begin intro x, induction x: reflexivity end
+  begin intro x, induction x: reflexivity end
+
+definition ua_equiv_ap {A : Type} (P : A → Type) {a b : A} (p : a = b) :
+  ua (equiv_ap P p) = ap P p :=
+begin induction p, apply ua_refl end
+
+definition pushout_elim_type_eta {TL BL TR : Type} {f : TL → BL} {g : TL → TR}
+  (P : pushout f g → Type) (x : pushout f g) :
+  P x ≃ pushout.elim_type (P ∘ inl) (P ∘ inr) (λa, equiv_ap P (glue a)) x :=
+begin
+  induction x,
+  { reflexivity },
+  { reflexivity },
+  { apply equiv_pathover_inv, apply arrow_pathover_left, intro y,
+    apply pathover_of_tr_eq, symmetry, exact ap10 !elim_type_glue y }
+end
+
+definition pushout_flattening' {TL BL TR : Type} {f : TL → BL} {g : TL → TR}
+  (P : pushout f g → Type) : sigma P ≃
+  @pushout (sigma (P ∘ inl ∘ f)) (sigma (P ∘ inl)) (sigma (P ∘ inr))
+    (sigma_functor f (λa, id)) (sigma_functor g (λa, transport P (glue a))) :=
+sigma_equiv_sigma_right (pushout_elim_type_eta P) ⬝e
+pushout.flattening _ _ (P ∘ inl) (P ∘ inr) (λa, equiv_ap P (glue a))
+
+definition equiv_ap011 {A B : Type} (P : A → B → Type) {a a' : A} {b b' : B}
+  (p : a = a') (q : b = b') : P a b ≃ P a' b' :=
+equiv_ap (P a) q ⬝e equiv_ap (λa, P a b') p
+
+definition tr_tr_eq_tr_tr [unfold 8 9] {A B : Type} (P : A → B → Type) {a a' : A} {b b' : B}
+  (p : a = a') (q : b = b') (x : P a b) :
+  transport (P a') q (transport (λa, P a b) p x) = transport (λa, P a b') p (transport (P a) q x) :=
+by induction p; induction q; reflexivity
+
+definition pushout_total_seq_rel :
+  pushout (sigma_functor2 (total i) (seq_rel_functor i p))
+          (sigma_functor2 (total j) (seq_rel_functor j q)) ≃
+  Σ(x : Σ ⦃n : ℕ⦄, pushout (@i n) (@j n)), sigma (seq_rel seq_diagram_pushout x) :=
+pushout.equiv _ _ _ _ (total_seq_rel f) (total_seq_rel g) (total_seq_rel h)
+  homotopy.rfl homotopy.rfl ⬝e
+pushout_sigma_equiv_sigma_pushout i j ⬝e
+(total_seq_rel seq_diagram_pushout)⁻¹ᵉ
+
+definition pr1_pushout_total_seq_rel :
+  hsquare pushout_total_seq_rel (pushout_sigma_equiv_sigma_pushout i j)
+          (pushout.functor pr1 pr1 pr1 homotopy.rfl homotopy.rfl) pr1 :=
+begin
+  intro x, refine !pr1_total_seq_rel_inv ⬝ _, esimp,
+  refine !pushout_sigma_equiv_sigma_pushout_natural⁻¹ ⬝ _,
+  apply ap sigma_pushout_of_pushout_sigma,
+  refine !pushout_functor_compose⁻¹ ⬝ _,
+  fapply pushout_functor_homotopy,
+  { intro v, induction v with a v, induction v with a' r, induction r, reflexivity },
+  { intro v, induction v with a v, induction v with a' r, induction r, reflexivity },
+  { intro v, induction v with a v, induction v with a' r, induction r, reflexivity },
+  { intro v, induction v with a v, induction v with a' r, induction r, esimp, generalize p a,
+    generalize i (f a), intro x r, cases r, reflexivity },
+  { intro v, induction v with a v, induction v with a' r, induction r, esimp, generalize q a,
+    generalize j (f a), intro x r, cases r, reflexivity },
+end
+
+definition pr2_pushout_total_seq_rel :
+  hsquare pushout_total_seq_rel (pushout_sigma_equiv_sigma_pushout i j)
+          (pushout.functor (λx, x.2.1) (λx, x.2.1) (λx, x.2.1) homotopy.rfl homotopy.rfl)
+          (λx, x.2.1) :=
+begin
+  intro x, apply pr2_total_seq_rel_inv,
+end
+
+/- this result depends on the 3x3 lemma, which is currently not formalized in Lean -/
+definition pushout_seq_colim_equiv [constructor] :
+  pushout (seq_colim_functor i p) (seq_colim_functor j q) ≃ seq_colim seq_diagram_pushout :=
+have e1 :
+  pushout (seq_colim_functor i p) (seq_colim_functor j q) ≃ pushout2hv pushout_seq_colim_span, from
+pushout.equiv _ _ _ _ !quotient_equiv_pushout !quotient_equiv_pushout !quotient_equiv_pushout
+  begin
+    refine _ ⬝hty quotient_equiv_pushout_natural (total i) (seq_rel_functor i p),
+    intro x, apply ap pushout_quotient_of_quotient,
+    induction x,
+    { induction a with n a, reflexivity },
+    { induction H, apply eq_pathover, apply hdeg_square,
+      refine !elim_glue ⬝ _ ⬝ !elim_eq_of_rel⁻¹,
+      unfold [seq_colim.glue, seq_rel_functor],
+      symmetry,
+      refine fn_tr_eq_tr_fn (p a)⁻¹ _ _ ⬝ eq_transport_Fl (p a)⁻¹ _ ⬝ _,
+      apply whisker_right, exact !ap_inv⁻² ⬝ !inv_inv }
+  end
+  begin
+    refine _ ⬝hty quotient_equiv_pushout_natural (total j) (seq_rel_functor j q),
+    intro x, apply ap pushout_quotient_of_quotient,
+    induction x,
+    { induction a with n a, reflexivity },
+    { induction H, apply eq_pathover, apply hdeg_square,
+      refine !elim_glue ⬝ _ ⬝ !elim_eq_of_rel⁻¹,
+      unfold [seq_colim.glue, seq_rel_functor],
+      symmetry,
+      refine fn_tr_eq_tr_fn (q a)⁻¹ _ _ ⬝ eq_transport_Fl (q a)⁻¹ _ ⬝ _,
+      apply whisker_right, exact !ap_inv⁻² ⬝ !inv_inv }
+  end,
+have e2 : pushout2vh pushout_seq_colim_span ≃ pushout_quotient (seq_rel seq_diagram_pushout), from
+pushout.equiv _ _ _ _
+  (!pushout_sum_equiv_sum_pushout ⬝e sum_equiv_sum pushout_total_seq_rel pushout_total_seq_rel)
+  (pushout_sigma_equiv_sigma_pushout i j)
+  pushout_total_seq_rel
+  begin
+    intro x, symmetry,
+    refine sum_rec_hsquare pr1_pushout_total_seq_rel pr2_pushout_total_seq_rel
+      (!pushout_sum_equiv_sum_pushout x) ⬝ ap (pushout_sigma_equiv_sigma_pushout i j) _,
+    refine sum_rec_pushout_sum_equiv_sum_pushout _ _ _ _ x ⬝ _,
+    apply pushout_functor_homotopy_constant: intro x; induction x: reflexivity
+  end
+  begin
+    intro x, symmetry,
+    refine !sum_rec_sum_functor ⬝ _,
+    refine sum_rec_same_compose
+      ((total_seq_rel seq_diagram_pushout)⁻¹ᵉ ∘ pushout_sigma_equiv_sigma_pushout i j) _ _ ⬝ _,
+    apply ap (to_fun (total_seq_rel seq_diagram_pushout)⁻¹ᵉ ∘ to_fun
+      (pushout_sigma_equiv_sigma_pushout i j)),
+    refine !sum_rec_pushout_sum_equiv_sum_pushout ⬝ _,
+    refine _ ⬝ !pushout_functor_compose,
+    fapply pushout_functor_homotopy,
+    { intro x, induction x: reflexivity },
+    { intro x, induction x: reflexivity },
+    { intro x, induction x: reflexivity },
+    { intro x, induction x: exact (!idp_con ⬝ !ap_id ⬝ !inv_inv)⁻¹ },
+    { intro x, induction x: exact (!idp_con ⬝ !ap_id ⬝ !inv_inv)⁻¹ }
+  end,
+e1 ⬝e three_by_three pushout_seq_colim_span ⬝e e2 ⬝e (quotient_equiv_pushout _)⁻¹ᵉ
+
+definition seq_colim_pushout_equiv [constructor] : seq_colim seq_diagram_pushout ≃
+  pushout (seq_colim_functor i p) (seq_colim_functor j q) :=
+pushout_seq_colim_equiv⁻¹ᵉ
+
+end

colimit/seq_colim.hlean

@@ -0,0 +1,900 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Egbert Rijke
+-/
+import hit.colimit .sequence cubical.squareover types.arrow types.equiv
+       cubical.pathover2
+
+open eq nat sigma sigma.ops quotient equiv pi is_trunc is_equiv fiber function trunc
+
+namespace seq_colim
+
+-- note: this clashes with the abbreviation defined in namespace "colimit"
+abbreviation ι  [constructor] := @inclusion
+abbreviation ι' [constructor] [parsing_only] {A} (f n) := @inclusion A f n
+
+variables {A A' A'' : ℕ → Type} (f : seq_diagram A) (f' : seq_diagram A') (f'' : seq_diagram A'')
+
+definition lrep_glue {n m : ℕ} (H : n ≤ m) (a : A n) : ι f (lrep f H a) = ι f a :=
+begin
+  induction H with m H p,
+  { reflexivity },
+  { exact glue f (lrep f H a) ⬝ p }
+end
+
+-- probably not needed
+-- definition rep0_back_glue [is_equiseq f] (k : ℕ) (a : A k) : ι f (rep0_back f k a) = ι f a :=
+-- begin
+--   exact sorry
+-- end
+
+definition colim_back [unfold 4] [H : is_equiseq f] : seq_colim f → A 0 :=
+begin
+  intro x,
+  induction x with k a k a,
+  { exact lrep_back f (zero_le k) a},
+  rexact ap (lrep_back f (zero_le k)) (left_inv (@f k) a),
+end
+
+set_option pp.binder_types true
+
+section
+local attribute is_equiv_lrep [instance] --[priority 500]
+definition is_equiv_ι (H : is_equiseq f) : is_equiv (ι' f 0) :=
+begin
+  fapply adjointify,
+  { exact colim_back f},
+  { intro x, induction x with k a k a,
+    { esimp,
+      refine (lrep_glue f (zero_le k) (lrep_back f (zero_le k) a))⁻¹ ⬝ _,
+      exact ap (ι f) (right_inv (lrep f (zero_le k)) a)},
+    apply eq_pathover_id_right,
+    refine (ap_compose (ι f) (colim_back f) _) ⬝ph _,
+    refine ap02 _ _ ⬝ph _, rotate 1,
+    { rexact elim_glue f _ _ a},
+    refine _ ⬝pv ((natural_square (lrep_glue f (zero_le k))
+                                  (ap (lrep_back f (zero_le k)) (left_inv (@f k) a)))⁻¹ʰ ⬝h _),
+    { exact (glue f (lrep f (zero_le k) (lrep_back f (zero_le (succ k)) (f a))))⁻¹ ⬝
+            ap (ι f) (right_inv (lrep f (zero_le (succ k))) (f a))},
+    { rewrite [-con.assoc, -con_inv]},
+    refine !ap_compose⁻¹ ⬝ ap_compose (ι f) _ _ ⬝ph _,
+    refine dconcat (aps (ι' f k) (natural_square (right_inv (lrep f (zero_le k)))
+                                                 (left_inv (@f _) a))) _,
+    apply move_top_of_left, apply move_left_of_bot,
+    refine ap02 _ (whisker_left _ (adj (@f _) a)) ⬝pv _,
+    rewrite [-+ap_con, -ap_compose', ap_id],
+    apply natural_square_tr},
+  intro a,
+  reflexivity,
+end
+end
+
+section
+variables {n : ℕ} (a : A n)
+
+definition rep_glue (k : ℕ) (a : A n) : ι f (rep f k a) = ι f a :=
+begin
+  induction k with k IH,
+  { reflexivity},
+  { exact glue f (rep f k a) ⬝ IH}
+end
+
+/- functorial action and equivalences -/
+section functor
+variables {f f' f''}
+variables (τ τ₂ : Π⦃n⦄, A n → A' n) (p : Π⦃n⦄ (a : A n), τ (f a) = f' (τ a))
+          (p₂ : Π⦃n⦄ (a : A n), τ₂ (f a) = f' (τ₂ a))
+          (τ' : Π⦃n⦄, A' n → A'' n) (p' : Π⦃n⦄ (a' : A' n), τ' (f' a') = f'' (τ' a'))
+include p
+definition seq_colim_functor [unfold 7] : seq_colim f → seq_colim f' :=
+begin
+  intro x, induction x with n a n a,
+  { exact ι f' (τ a)},
+  { exact ap (ι f') (p a) ⬝ glue f' (τ a)}
+end
+omit p
+
+theorem seq_colim_functor_glue {n : ℕ} (a : A n)
+  : ap (seq_colim_functor τ p) (glue f a) = ap (ι f') (p a) ⬝ glue f' (τ a) :=
+!elim_glue
+
+definition seq_colim_functor_compose [constructor] (x : seq_colim f) :
+  seq_colim_functor (λn x, τ' (τ x)) (λn, hvconcat (@p n) (@p' n)) x =
+  seq_colim_functor τ' p' (seq_colim_functor τ p x)  :=
+begin
+  induction x, reflexivity,
+  apply eq_pathover, apply hdeg_square,
+  refine !seq_colim_functor_glue ⬝ _ ⬝ (ap_compose (seq_colim_functor _ _) _ _)⁻¹,
+  refine _ ⬝ (ap02 _ proof !seq_colim_functor_glue qed ⬝ !ap_con)⁻¹,
+  refine _ ⬝ (proof !ap_compose'⁻¹ ⬝ ap_compose (ι f'') _ _ qed ◾ proof !seq_colim_functor_glue qed)⁻¹,
+  exact whisker_right _ !ap_con ⬝ !con.assoc
+end
+
+variable (f)
+definition seq_colim_functor_id [constructor] (x : seq_colim f) :
+  seq_colim_functor (λn, id) (λn, homotopy.rfl) x =
+  x :=
+begin
+  induction x, reflexivity,
+  apply eq_pathover, apply hdeg_square,
+  exact !seq_colim_functor_glue ⬝ !idp_con ⬝ !ap_id⁻¹,
+end
+variables {f τ τ₂ p p₂}
+
+definition seq_colim_functor_homotopy [constructor] (q : τ ~2 τ₂)
+  (r : Π⦃n⦄ (a : A n), square (q (n+1) (f a)) (ap (@f' n) (q n a)) (p a) (p₂ a))
+  (x : seq_colim f) :
+  seq_colim_functor τ p x = seq_colim_functor τ₂ p₂ x  :=
+begin
+  induction x,
+    exact ap (ι f') (q n a),
+  apply eq_pathover,
+  refine !seq_colim_functor_glue ⬝ph _ ⬝hp !seq_colim_functor_glue⁻¹,
+  refine aps (ι f') (r a) ⬝v !ap_compose⁻¹ ⬝pv natural_square_tr (glue f') (q n a),
+end
+variables (τ τ₂ p p₂)
+
+definition is_equiv_seq_colim_functor [constructor] [H : Πn, is_equiv (@τ n)]
+   : is_equiv (seq_colim_functor @τ p) :=
+adjointify _ (seq_colim_functor (λn, (@τ _)⁻¹) (λn a, inv_commute' τ f f' p a))
+           abstract begin
+             intro x,
+             refine !seq_colim_functor_compose⁻¹ ⬝ seq_colim_functor_homotopy _ _ x ⬝ !seq_colim_functor_id,
+             { intro n a, exact right_inv (@τ n) a },
+             { intro n a,
+               refine whisker_right _ !ap_inv_commute' ⬝ !inv_con_cancel_right ⬝ whisker_left _ !ap_inv ⬝ph _,
+               apply whisker_bl, apply whisker_tl, exact ids }
+           end end
+           abstract begin
+             intro x,
+             refine !seq_colim_functor_compose⁻¹ ⬝ seq_colim_functor_homotopy _ _ x ⬝ !seq_colim_functor_id,
+             { intro n a, exact left_inv (@τ n) a },
+             { intro n a,
+               esimp [hvconcat],
+               refine whisker_left _ (!inv_commute'_fn ⬝ !con.assoc) ⬝ !con_inv_cancel_left ⬝ph _,
+               apply whisker_bl, apply whisker_tl, exact ids }
+           end end
+
+definition seq_colim_equiv [constructor] (τ : Π{n}, A n ≃ A' n)
+  (p : Π⦃n⦄ (a : A n), τ (f a) = f' (τ a)) : seq_colim f ≃ seq_colim f' :=
+equiv.mk _ (is_equiv_seq_colim_functor @τ p)
+
+definition seq_colim_rec_unc [unfold 4] {P : seq_colim f → Type}
+  (v : Σ(Pincl : Π ⦃n : ℕ⦄ (a : A n), P (ι f a)),
+                 Π ⦃n : ℕ⦄ (a : A n), Pincl (f a) =[glue f a] Pincl a)
+  : Π(x : seq_colim f), P x :=
+by induction v with Pincl Pglue; exact seq_colim.rec f Pincl Pglue
+
+definition is_equiv_seq_colim_rec (P : seq_colim f → Type) :
+  is_equiv (seq_colim_rec_unc :
+    (Σ(Pincl : Π ⦃n : ℕ⦄ (a : A n), P (ι f a)),
+      Π ⦃n : ℕ⦄ (a : A n), Pincl (f a) =[glue f a] Pincl a)
+        → (Π (aa : seq_colim f), P aa)) :=
+begin
+  fapply adjointify,
+  { intro s, exact ⟨λn a, s (ι f a), λn a, apd s (glue f a)⟩},
+  { intro s, apply eq_of_homotopy, intro x, induction x,
+    { reflexivity},
+    { apply eq_pathover_dep, esimp, apply hdeg_squareover, apply rec_glue}},
+  { intro v, induction v with Pincl Pglue, fapply ap (sigma.mk _),
+    apply eq_of_homotopy2, intros n a, apply rec_glue},
+end
+
+/- universal property -/
+definition equiv_seq_colim_rec (P : seq_colim f → Type) :
+  (Σ(Pincl : Π ⦃n : ℕ⦄ (a : A n), P (ι f a)),
+     Π ⦃n : ℕ⦄ (a : A n), Pincl (f a) =[glue f a] Pincl a) ≃ (Π (aa : seq_colim f), P aa) :=
+equiv.mk _ !is_equiv_seq_colim_rec
+
+end functor
+
+definition shift_up [unfold 3] (x : seq_colim f) : seq_colim (shift_diag f) :=
+begin
+  induction x,
+  { exact ι' (shift_diag f) n (f a)},
+  { exact glue (shift_diag f) (f a)}
+end
+
+definition shift_down [unfold 3] (x : seq_colim (shift_diag f)) : seq_colim f :=
+begin
+  induction x,
+  { exact ι' f (n+1) a},
+  { exact glue f a}
+end
+
+-- definition kshift_up' (k : ℕ) (x : seq_colim f) : seq_colim (kshift_diag' f k) :=
+-- begin
+--   induction x,
+--   { apply ι' _ n, exact rep f k a},
+--   { exact sorry}
+-- end
+
+-- definition kshift_down' (k : ℕ) (x : seq_colim (kshift_diag' f k)) : seq_colim f :=
+-- begin
+--   induction x,
+--   { exact ι f a},
+--   { esimp, exact sorry}
+-- end
+
+end
+
+definition shift_equiv [constructor] : seq_colim f ≃ seq_colim (shift_diag f) :=
+equiv.MK (shift_up f)
+         (shift_down f)
+         abstract begin
+           intro x, induction x,
+           { exact glue _ a },
+           { apply eq_pathover,
+             rewrite [▸*, ap_id, ap_compose (shift_up f) (shift_down f), ↑shift_down,
+                      elim_glue],
+             apply square_of_eq, apply whisker_right, exact !elim_glue⁻¹ }
+         end end
+         abstract begin
+           intro x, induction x,
+           { exact glue _ a },
+           { apply eq_pathover,
+             rewrite [▸*, ap_id, ap_compose (shift_down f) (shift_up f), ↑shift_up,
+                      elim_glue],
+             apply square_of_eq, apply whisker_right, exact !elim_glue⁻¹ }
+         end end
+
+-- definition kshift_equiv [constructor] (k : ℕ)
+--   : seq_colim A ≃ @seq_colim (λn, A (k + n)) (kshift_diag A k) :=
+-- equiv.MK (kshift_up k)
+--          (kshift_down k)
+--          abstract begin
+--            intro a, exact sorry,
+--            -- induction a,
+--            -- { esimp, exact glue a},
+--            -- { apply eq_pathover,
+--            --   rewrite [▸*, ap_id, ap_compose shift_up shift_down, ↑shift_down,
+--            --            @elim_glue (λk, A (succ k)) _, ↑shift_up],
+--            --   apply square_of_eq, apply whisker_right, exact !elim_glue⁻¹}
+--          end end
+--          abstract begin
+--            intro a, exact sorry
+--            -- induction a,
+--            -- { exact glue a},
+--            -- { apply eq_pathover,
+--            --   rewrite [▸*, ap_id, ap_compose shift_down shift_up, ↑shift_up,
+--            --            @elim_glue A _, ↑shift_down],
+--            --   apply square_of_eq, apply whisker_right, exact !elim_glue⁻¹}
+--          end end
+
+-- definition kshift_equiv' [constructor] (k : ℕ) : seq_colim f ≃ seq_colim (kshift_diag' f k) :=
+-- equiv.MK (kshift_up' f k)
+--          (kshift_down' f k)
+--          abstract begin
+--            intro a, exact sorry,
+--            -- induction a,
+--            -- { esimp, exact glue a},
+--            -- { apply eq_pathover,
+--            --   rewrite [▸*, ap_id, ap_compose shift_up shift_down, ↑shift_down,
+--            --            @elim_glue (λk, A (succ k)) _, ↑shift_up],
+--            --   apply square_of_eq, apply whisker_right, exact !elim_glue⁻¹}
+--          end end
+--          abstract begin
+--            intro a, exact sorry
+--            -- induction a,
+--            -- { exact glue a},
+--            -- { apply eq_pathover,
+--            --   rewrite [▸*, ap_id, ap_compose shift_down shift_up, ↑shift_up,
+--            --            @elim_glue A _, ↑shift_down],
+--            --   apply square_of_eq, apply whisker_right, exact !elim_glue⁻¹}
+--          end end
+
+/- todo: define functions back and forth explicitly -/
+
+definition kshift'_equiv (k : ℕ) : seq_colim f ≃ seq_colim (kshift_diag' f k) :=
+begin
+  induction k with k IH,
+  { reflexivity },
+  { exact IH ⬝e shift_equiv (kshift_diag' f k) ⬝e
+      seq_colim_equiv (λn, equiv_ap A (succ_add n k))
+                      (λn a, proof !tr_inv_tr ⬝ !transport_lemma⁻¹ qed) }
+end
+
+definition kshift_equiv_inv (k : ℕ) : seq_colim (kshift_diag f k) ≃ seq_colim f :=
+begin
+  induction k with k IH,
+  { exact seq_colim_equiv (λn, equiv_ap A (nat.zero_add n)) (λn a, !transport_lemma2) },
+  { exact seq_colim_equiv (λn, equiv_ap A (succ_add k n))
+                          (λn a, transport_lemma2 (succ_add k n) f a) ⬝e
+          (shift_equiv (kshift_diag f k))⁻¹ᵉ ⬝e IH }
+end
+
+definition kshift_equiv [constructor] (k : ℕ) : seq_colim f ≃ seq_colim (kshift_diag f k) :=
+(kshift_equiv_inv f k)⁻¹ᵉ
+
+-- definition kshift_equiv2 [constructor] (k : ℕ) : seq_colim f ≃ seq_colim (kshift_diag f k) :=
+-- begin
+--   refine equiv_change_fun (kshift_equiv f k) _,
+
+-- end
+
+variable {f}
+definition equiv_of_is_equiseq [constructor] (H : is_equiseq f) : seq_colim f ≃ A 0 :=
+(equiv.mk _ (is_equiv_ι _ H))⁻¹ᵉ
+
+definition seq_colim_constant_seq [constructor] (X : Type) : seq_colim (constant_seq X) ≃ X :=
+equiv_of_is_equiseq (λn, !is_equiv_id)
+
+variable (f)
+definition is_contr_seq_colim {A : ℕ → Type} (f : seq_diagram A)
+  [Πk, is_contr (A k)] : is_contr (seq_colim f) :=
+begin
+  apply @is_trunc_is_equiv_closed (A 0),
+  apply is_equiv_ι, intro n, apply is_equiv_of_is_contr
+end
+
+/- colimits of dependent sequences, sigma's commute with colimits -/
+
+section over
+
+universe variable v
+variables {P : Π⦃n⦄, A n → Type.{v}} (g : seq_diagram_over f P) {n : ℕ} {a : A n}
+variable {f}
+
+definition rep_f_equiv_natural {k : ℕ} (p : P (rep f k (f a))) :
+  transporto P (rep_f f (succ k) a) (g p) = g (transporto P (rep_f f k a) p) :=
+(fn_tro_eq_tro_fn2 (rep_f f k a) g p)⁻¹
+
+variable (a)
+definition over_f_equiv [constructor] :
+  seq_colim (seq_diagram_of_over g (f a)) ≃ seq_colim (shift_diag (seq_diagram_of_over g a)) :=
+seq_colim_equiv (rep_f_equiv f P a) (λk p, rep_f_equiv_natural g p)
+
+definition seq_colim_over_equiv :
+  seq_colim (seq_diagram_of_over g (f a)) ≃ seq_colim (seq_diagram_of_over g a) :=
+over_f_equiv g a ⬝e (shift_equiv (seq_diagram_of_over g a))⁻¹ᵉ
+
+definition seq_colim_over_equiv_glue {k : ℕ} (x : P (rep f k (f a))) :
+  ap (seq_colim_over_equiv g a) (glue (seq_diagram_of_over g (f a)) x) =
+  ap (ι' (seq_diagram_of_over g a) (k+2)) (rep_f_equiv_natural g x) ⬝
+  glue (seq_diagram_of_over g a) (rep_f f k a ▸o x) :=
+begin
+  refine ap_compose (shift_down (seq_diagram_of_over g a)) _ _ ⬝ _,
+  exact ap02 _ !elim_glue ⬝ !ap_con ⬝ !ap_compose'⁻¹ ◾ !elim_glue
+end
+
+variable {a}
+
+include g
+definition seq_colim_over [unfold 5] (x : seq_colim f) : Type.{v} :=
+begin
+  refine seq_colim.elim_type f _ _ x,
+  { intro n a, exact seq_colim (seq_diagram_of_over g a)},
+  { intro n a, exact seq_colim_over_equiv g a }
+end
+omit g
+
+definition ιo [constructor] (p : P a) : seq_colim_over g (ι f a) :=
+ι' _ 0 p
+
+-- Warning: the order of addition has changed in rep_rep
+-- definition rep_equiv_rep_rep (l : ℕ)
+--   : @seq_colim (λk, P (rep (k + l) a)) (kshift_diag' _ _) ≃
+--   @seq_colim (λk, P (rep k (rep l a))) (seq_diagram_of_over P (rep l a)) :=
+-- seq_colim_equiv (λk, rep_rep_equiv P a k l) abstract (λk p,
+--   begin
+--     esimp,
+--     rewrite [+cast_apd011],
+--     refine _ ⬝ (fn_tro_eq_tro_fn (rep_f k a)⁻¹ᵒ g p)⁻¹ᵖ,
+--     rewrite [↑rep_f,↓rep_f k a],
+--     refine !pathover_ap_invo_tro ⬝ _,
+--     rewrite [apo_invo,apo_tro]
+--   end) end
+
+variable {P}
+theorem seq_colim_over_glue /- r -/ (x : seq_colim_over g (ι f (f a)))
+  : transport (seq_colim_over g) (glue f a) x = shift_down _ (over_f_equiv g a x) :=
+ap10 (elim_type_glue _ _ _ a) x
+
+theorem seq_colim_over_glue_inv (x : seq_colim_over g (ι f a))
+  : transport (seq_colim_over g) (glue f a)⁻¹ x = to_inv (over_f_equiv g a) (shift_up _ x) :=
+ap10 (elim_type_glue_inv _ _ _ a) x
+
+definition glue_over (p : P (f a)) : pathover (seq_colim_over g) (ιo g p) (glue f a) (ι' _ 1 p) :=
+pathover_of_tr_eq !seq_colim_over_glue
+
+-- we can define a function from the colimit of total spaces to the total space of the colimit.
+
+/- TO DO: define glue' in the same way as glue' -/
+definition glue' (p : P a) : ⟨ι f (f a), ιo g (g p)⟩ = ⟨ι f a, ιo g p⟩ :=
+sigma_eq (glue f a) (glue_over g (g p) ⬝op glue (seq_diagram_of_over g a) p)
+
+definition glue_star (k : ℕ) (x : P (rep f k (f a))) :
+  ⟨ι f (f a), ι (seq_diagram_of_over g (f a)) x⟩ =
+  ⟨ι f a, ι (seq_diagram_of_over g a) (to_fun (rep_f_equiv f P a k) x)⟩
+  :> sigma (seq_colim_over g) :=
+begin
+  apply dpair_eq_dpair (glue f a),
+  apply pathover_of_tr_eq,
+  refine seq_colim_over_glue g (ι (seq_diagram_of_over g (f a)) x)
+end
+
+definition sigma_colim_of_colim_sigma [unfold 5] (a : seq_colim (seq_diagram_sigma g)) :
+  Σ(x : seq_colim f), seq_colim_over g x :=
+begin
+induction a with n v n v,
+{ induction v with a p, exact ⟨ι f a, ιo g p⟩},
+{ induction v with a p, exact glue' g p }
+end
+
+definition colim_sigma_triangle [unfold 5] (a : seq_colim (seq_diagram_sigma g)) :
+  (sigma_colim_of_colim_sigma g a).1 = seq_colim_functor (λn, sigma.pr1) (λn, homotopy.rfl) a :=
+begin
+induction a with n v n v,
+{ induction v with a p, reflexivity },
+{ induction v with a p, apply eq_pathover, apply hdeg_square,
+  refine ap_compose sigma.pr1 _ _ ⬝ ap02 _ !elim_glue ⬝ _ ⬝ !elim_glue⁻¹,
+  exact !sigma_eq_pr1 ⬝ !idp_con⁻¹ }
+end
+
+-- we now want to show that this function is an equivalence.
+
+/-
+  Kristina's proof of the induction principle of colim-sigma for sigma-colim.
+  It's a double induction, so we have 4 cases: point-point, point-path, path-point and path-path.
+  The main idea of the proof is that for the path-path case you need to fill a square, but we can
+  define the point-path case as a filler for this square.
+-/
+
+open sigma
+
+/-
+  dictionary:
+  Kristina | Lean
+  VARIABLE NAMES (A, P, k, n, e, w are the same)
+  x : A_n                     | a : A n
+  a : A_n → A_{n+1}           | f : A n → A (n+1)
+  y : P(n, x)                 | x : P a (maybe other variables)
+  f : P(n, x) → P(n+1, a_n x) | g : P a → P (f a)
+  DEFINITION NAMES
+  κ   | glue
+  U   | rep_f_equiv : P (n+1+k, rep f k (f x)) ≃ P (n+k+1, rep f (k+1) x)
+  δ   | rep_f_equiv_natural
+  F   | over_f_equiv g a ⬝e (shift_equiv (λk, P (rep f k a)) (seq_diagram_of_over g a))⁻¹ᵉ
+  g_* | g_star
+  g   | sigma_colim_rec_point
+-/
+
+definition glue_star_eq (k : ℕ) (x : P (rep f k (f a))) :
+  glue_star g k x =
+  dpair_eq_dpair (glue f a) (pathover_tr (glue f a) (ι (seq_diagram_of_over g (f a)) x)) ⬝
+  ap (dpair (ι f a)) (seq_colim_over_glue g (ι (seq_diagram_of_over g (f a)) x)) :=
+ap (sigma_eq _) !pathover_of_tr_eq_eq_concato ⬝ !sigma_eq_con ⬝ whisker_left _ !ap_dpair⁻¹
+
+definition g_star_step {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type}
+  (e : Πn (a : A n) (x : P a), E ⟨ι f a, ιo g x⟩) {k : ℕ}
+  (IH : Π{n} {a : A n} (x : P (rep f k a)), E ⟨ι f a, ι (seq_diagram_of_over g a) x⟩) :
+  Σ(gs : Π⦃n : ℕ⦄ {a : A n} (x : P (rep f (k+1) a)), E ⟨ι f a, ι (seq_diagram_of_over g a) x⟩),
+  Π⦃n : ℕ⦄ {a : A n} (x : P (rep f k (f a))),
+    pathover E (IH x) (glue_star g k x) (gs (transporto P (rep_f f k a) x)) :=
+begin
+  fconstructor,
+  { intro n a,
+    refine equiv_rect (rep_f_equiv f P a k) _ _,
+    intro z, refine transport E _ (IH z),
+    exact glue_star g k z },
+  { intro n a x, exact !pathover_tr ⬝op !equiv_rect_comp⁻¹ }
+end
+
+definition g_star /- g_* -/ {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type}
+  (e : Πn (a : A n) (x : P a), E ⟨ι f a, ιo g x⟩) {k : ℕ} :
+  Π {n : ℕ} {a : A n} (x : P (rep f k a)), E ⟨ι f a, ι (seq_diagram_of_over g a) x⟩ :=
+begin
+  induction k with k IH: intro n a x,
+  { exact e n a x },
+  { apply (g_star_step g e @IH).1 }
+end
+
+definition g_star_path_left {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type}
+  (e : Π⦃n⦄ ⦃a : A n⦄ (x : P a), E ⟨ι f a, ιo g x⟩)
+  (w : Π⦃n⦄ ⦃a : A n⦄ (x : P a), pathover E (e (g x)) (glue' g x) (e x))
+  {k : ℕ} {n : ℕ} {a : A n} (x : P (rep f k (f a))) :
+  pathover E (g_star g e x) (glue_star g k x)
+             (g_star g e (transporto P (rep_f f k a) x)) :=
+by apply (g_star_step g e (@(g_star g e) k)).2
+
+/- this is the bottom of the square we have to fill in the end -/
+definition bottom_square {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type}
+  (e : Π⦃n⦄ ⦃a : A n⦄ (x : P a), E ⟨ι f a, ιo g x⟩)
+  (w : Π⦃n⦄ ⦃a : A n⦄ (x : P a), pathover E (e (g x)) (glue' g x) (e x))
+  (k : ℕ) {n : ℕ} {a : A n} (x : P (rep f k (f a))) :=
+move_top_of_right (natural_square
+    (λ b, dpair_eq_dpair (glue f a) (pathover_tr (glue f a) b) ⬝
+      ap (dpair (ι f a)) (seq_colim_over_glue g b))
+    (glue (seq_diagram_of_over g (f a)) x) ⬝hp
+  ap_compose (dpair (ι f a)) (to_fun (seq_colim_over_equiv g a))
+    (glue (seq_diagram_of_over g (f a)) x) ⬝hp
+  (ap02 (dpair (ι f a)) (seq_colim_over_equiv_glue g a x)⁻¹)⁻¹ ⬝hp
+  ap_con (dpair (ι f a))
+    (ap (λx, shift_down (seq_diagram_of_over g a) (ι (shift_diag (seq_diagram_of_over g a)) x))
+      (rep_f_equiv_natural g x))
+    (glue (seq_diagram_of_over g a) (to_fun (rep_f_equiv f P a k) x)))
+
+/- this is the composition + filler -/
+definition g_star_path_right_step {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type}
+  (e : Π⦃n⦄ ⦃a : A n⦄ (x : P a), E ⟨ι f a, ιo g x⟩)
+  (w : Π⦃n⦄ ⦃a : A n⦄ (x : P a), pathover E (e (g x)) (glue' g x) (e x))
+  (k : ℕ) {n : ℕ} {a : A n} (x : P (rep f k (f a)))
+  (IH : Π(n : ℕ) (a : A n) (x : P (rep f k a)),
+  pathover E (g_star g e (seq_diagram_of_over g a x))
+           (ap (dpair (ι f a)) (glue (seq_diagram_of_over g a) x))
+           (g_star g e x)) :=
+squareover_fill_r
+  (bottom_square g e w k x)
+  (change_path (glue_star_eq g (succ k) (g x)) (g_star_path_left g e w (g x)) ⬝o
+    pathover_ap E (dpair (ι f a))
+      (pathover_ap (λ (b : seq_colim (seq_diagram_of_over g a)), E ⟨ι f a, b⟩)
+        (ι (seq_diagram_of_over g a)) (apd (g_star g e) (rep_f_equiv_natural g x))))
+  (change_path (glue_star_eq g k x) (g_star_path_left g e w x))
+  (IH (n+1) (f a) x)
+
+/- this is just the composition -/
+definition g_star_path_right_step1 {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type}
+  (e : Π⦃n⦄ ⦃a : A n⦄ (x : P a), E ⟨ι f a, ιo g x⟩)
+  (w : Π⦃n⦄ ⦃a : A n⦄ (x : P a), pathover E (e (g x)) (glue' g x) (e x))
+  (k : ℕ) {n : ℕ} {a : A n} (x : P (rep f k (f a)))
+  (IH : Π(n : ℕ) (a : A n) (x : P (rep f k a)),
+  pathover E (g_star g e (seq_diagram_of_over g a x))
+           (ap (dpair (ι f a)) (glue (seq_diagram_of_over g a) x))
+           (g_star g e x)) :=
+(g_star_path_right_step g e w k x IH).1
+
+definition g_star_path_right {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type}
+  (e : Π⦃n⦄ ⦃a : A n⦄ (x : P a), E ⟨ι f a, ιo g x⟩)
+  (w : Π⦃n⦄ ⦃a : A n⦄ (x : P a), pathover E (e (g x)) (glue' g x) (e x))
+  (k : ℕ) {n : ℕ} {a : A n} (x : P (rep f k a)) :
+  pathover E (g_star g e (seq_diagram_of_over g a x))
+           (ap (dpair (ι f a)) (glue (seq_diagram_of_over g a) x))
+           (g_star g e x) :=
+begin
+  revert n a x, induction k with k IH: intro n a x,
+  { exact abstract begin refine pathover_cancel_left !pathover_tr⁻¹ᵒ (change_path _ (w x)),
+    apply sigma_eq_concato_eq end end },
+  { revert x, refine equiv_rect (rep_f_equiv f P a k) _ _, intro x,
+    exact g_star_path_right_step1 g e w k x IH }
+end
+
+definition sigma_colim_rec_point [unfold 10] /- g -/ {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type}
+  (e : Π⦃n⦄ ⦃a : A n⦄ (x : P a), E ⟨ι f a, ιo g x⟩)
+  (w : Π⦃n⦄ ⦃a : A n⦄ (x : P a), pathover E (e (g x)) (glue' g x) (e x))
+  {n : ℕ} {a : A n} (x : seq_colim_over g (ι f a)) : E ⟨ι f a, x⟩ :=
+begin
+  induction x with k x k x,
+  { exact g_star g e x },
+  { apply pathover_of_pathover_ap E (dpair (ι f a)),
+    exact g_star_path_right g e w k x }
+end
+
+definition sigma_colim_rec {E : (Σ(x : seq_colim f), seq_colim_over g x) → Type}
+  (e : Π⦃n⦄ ⦃a : A n⦄ (x : P a), E ⟨ι f a, ιo g x⟩)
+  (w : Π⦃n⦄ ⦃a : A n⦄ (x : P a), pathover E (e (g x)) (glue' g x) (e x))
+  (v : Σ(x : seq_colim f), seq_colim_over g x) : E v :=
+begin
+  induction v with x y,
+  induction x with n a n a,
+  { exact sigma_colim_rec_point g e w y },
+  { apply pi_pathover_left', intro x,
+    refine change_path (whisker_left _ !ap_inv ⬝ !con_inv_cancel_right)
+      (_ ⬝o pathover_ap E (dpair _) (apd (sigma_colim_rec_point g e w) !seq_colim_over_glue⁻¹)),
+    /- we can simplify the squareover we need to fill a bit if we apply this rule here -/
+    -- refine change_path (ap (sigma_eq (glue f a)) !pathover_of_tr_eq_eq_concato ⬝ !sigma_eq_con ⬝ whisker_left _ !ap_dpair⁻¹) _,
+    induction x with k x k x,
+    { exact change_path !glue_star_eq (g_star_path_left g e w x) },
+    -- { exact g_star_path_left g e w x },
+    { apply pathover_pathover, esimp,
+      refine _ ⬝hop (ap (pathover_ap E _) (apd_compose2 (sigma_colim_rec_point g e w) _ _) ⬝
+        pathover_ap_pathover_of_pathover_ap E (dpair (ι f a)) (seq_colim_over_equiv g a) _)⁻¹,
+      apply squareover_change_path_right',
+      refine _ ⬝hop !pathover_ap_change_path⁻¹ ⬝ ap (pathover_ap E _)
+        (apd02 _ !seq_colim_over_equiv_glue⁻¹),
+      apply squareover_change_path_right,
+      refine _ ⬝hop (ap (pathover_ap E _) (!apd_con ⬝ (!apd_ap ◾o idp)) ⬝ !pathover_ap_cono)⁻¹,
+      apply squareover_change_path_right',
+      apply move_right_of_top_over,
+      refine _ ⬝hop (ap (pathover_ap E _) !rec_glue ⬝ to_right_inv !pathover_compose _)⁻¹,
+      refine ap (pathover_ap E _) !rec_glue ⬝ to_right_inv !pathover_compose _ ⬝pho _,
+      refine _ ⬝hop !equiv_rect_comp⁻¹,
+      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}
+
+definition colim_sigma_of_sigma_colim_constructor [unfold 7] (p : seq_colim_over g (ι f a))
+  : seq_colim (seq_diagram_sigma g) :=
+begin
+  induction p with k p k p,
+  { exact ι _ ⟨rep f k a, p⟩},
+  { apply glue}
+end
+
+definition colim_sigma_of_sigma_colim_path1 /- μ -/ {k : ℕ} (p : P (rep f k (f a))) :
+  ι (seq_diagram_sigma g) ⟨rep f k (f a), p⟩ =
+  ι (seq_diagram_sigma g) ⟨rep f (succ k) a, transporto P (rep_f f k a) p⟩ :=
+begin
+  apply apd0111 (λn a p, ι' (seq_diagram_sigma g) n ⟨a, p⟩) (succ_add n k) (rep_f f k a),
+  apply pathover_tro
+end
+
+definition colim_sigma_of_sigma_colim_path2 {k : ℕ} (p : P (rep f k (f a))) :
+square (colim_sigma_of_sigma_colim_path1 g (g p)) (colim_sigma_of_sigma_colim_path1 g p)
+  (ap (colim_sigma_of_sigma_colim_constructor g) (glue (seq_diagram_of_over g (f a)) p))
+  (ap (λx, colim_sigma_of_sigma_colim_constructor g (shift_down (seq_diagram_of_over g a)
+        (seq_colim_functor (λk, transporto P (rep_f f k a)) (λk p, rep_f_equiv_natural g p) x)))
+    (glue (seq_diagram_of_over g (f a)) p)) :=
+begin
+  refine !elim_glue ⬝ph _,
+  refine _ ⬝hp (ap_compose' (colim_sigma_of_sigma_colim_constructor g) _ _)⁻¹,
+  refine _ ⬝hp ap02 _ !seq_colim_over_equiv_glue⁻¹,
+  refine _ ⬝hp !ap_con⁻¹,
+  refine _ ⬝hp !ap_compose' ◾ !elim_glue⁻¹,
+  refine _ ⬝pv whisker_rt _ (natural_square0111 P (pathover_tro (rep_f f k a) p) g
+                                                  (λn a p, glue (seq_diagram_sigma g) ⟨a, p⟩)),
+  refine _ ⬝ whisker_left _ (ap02 _ !inv_inv⁻¹ ⬝ !ap_inv),
+  symmetry, apply apd0111_precompose
+end
+
+definition colim_sigma_of_sigma_colim [unfold 5] (v : Σ(x : seq_colim f), seq_colim_over g x)
+  : seq_colim (seq_diagram_sigma g) :=
+begin
+  induction v with x p,
+  induction x with n a n a,
+  { exact colim_sigma_of_sigma_colim_constructor g p },
+  apply arrow_pathover_constant_right, intro x, esimp at x,
+  refine _ ⬝ ap (colim_sigma_of_sigma_colim_constructor g) !seq_colim_over_glue⁻¹,
+  induction x with k p k p,
+  { exact colim_sigma_of_sigma_colim_path1 g p },
+  apply eq_pathover, apply colim_sigma_of_sigma_colim_path2
+end
+
+/- TODO: prove and merge these theorems -/
+definition colim_sigma_of_sigma_colim_glue' [unfold 5] (p : P a)
+  : ap (colim_sigma_of_sigma_colim g) (glue' g p) = glue (seq_diagram_sigma g) ⟨a, p⟩ :=
+begin
+  refine !ap_dpair_eq_dpair ⬝ _,
+  refine !apd011_eq_apo11_apd ⬝ _,
+  refine ap (λx, apo11_constant_right x _) !rec_glue ⬝ _,
+  refine !apo11_arrow_pathover_constant_right ⬝ _, esimp,
+  refine whisker_right _ !idp_con ⬝ _,
+  rewrite [▸*, tr_eq_of_pathover_concato_eq, ap_con, ↑glue_over,
+           to_right_inv !pathover_equiv_tr_eq, ap_inv, inv_con_cancel_left],
+  apply elim_glue
+end
+
+theorem colim_sigma_of_sigma_colim_of_colim_sigma (a : seq_colim (seq_diagram_sigma g)) :
+  colim_sigma_of_sigma_colim g (sigma_colim_of_colim_sigma g a) = a :=
+begin
+induction a with n v n v,
+{ induction v with a p, reflexivity },
+{ induction v with a p, esimp, apply eq_pathover_id_right, apply hdeg_square,
+  refine ap_compose (colim_sigma_of_sigma_colim g) _ _ ⬝ _,
+  refine ap02 _ !elim_glue ⬝ _, exact colim_sigma_of_sigma_colim_glue' g p }
+end
+
+theorem sigma_colim_of_colim_sigma_of_sigma_colim (v : Σ(x : seq_colim f), seq_colim_over g x)
+  : sigma_colim_of_colim_sigma g (colim_sigma_of_sigma_colim g v) = v :=
+begin
+  revert v, refine sigma_colim_rec _ _ _,
+  { intro n a x, reflexivity },
+  { intro n a x, apply eq_pathover_id_right, apply hdeg_square,
+    refine ap_compose (sigma_colim_of_colim_sigma g) _ _ ⬝ _,
+    refine ap02 _ (colim_sigma_of_sigma_colim_glue' g x) ⬝ _,
+    apply elim_glue }
+end
+
+variable (P)
+definition sigma_seq_colim_over_equiv [constructor]
+  : (Σ(x : seq_colim f), seq_colim_over g x) ≃ seq_colim (seq_diagram_sigma g) :=
+equiv.MK (colim_sigma_of_sigma_colim g)
+         (sigma_colim_of_colim_sigma g)
+         (colim_sigma_of_sigma_colim_of_colim_sigma g)
+         (sigma_colim_of_colim_sigma_of_sigma_colim g)
+
+end over
+
+definition seq_colim_id_equiv_seq_colim_id0 (x y : A 0) :
+  seq_colim (id_seq_diagram f 0 x y) ≃ seq_colim (id0_seq_diagram f x y) :=
+seq_colim_equiv
+  (λn, !lrep_eq_lrep_irrel (nat.zero_add n))
+  (λn p, !lrep_eq_lrep_irrel_natural)
+
+definition kshift_equiv_inv_incl_kshift_diag {n k : ℕ} (x : A (n + k)) :
+  kshift_equiv_inv f n (ι' (kshift_diag f n) k x) = ι f x :=
+begin
+  revert A f k x, induction n with n IH: intro A f k x,
+  { exact apd011 (ι' f) !nat.zero_add⁻¹ !pathover_tr⁻¹ᵒ },
+  { exact !IH ⬝ apd011 (ι' f) !succ_add⁻¹ !pathover_tr⁻¹ᵒ }
+end
+
+definition incl_kshift_diag {n k : ℕ} (x : A (n + k)) :
+  ι' (kshift_diag f n) k x = kshift_equiv f n (ι f x) :=
+eq_inv_of_eq (kshift_equiv_inv_incl_kshift_diag f x)
+
+definition incl_kshift_diag0 {n : ℕ} (x : A n) :
+  ι' (kshift_diag f n) 0 x = kshift_equiv f n (ι f x) :=
+incl_kshift_diag f x
+
+definition seq_colim_eq_equiv0' (a₀ a₁ : A 0) : ι f a₀ = ι f a₁ ≃ seq_colim (id_seq_diagram f 0 a₀ a₁) :=
+begin
+  refine total_space_method2 (ι f a₀) (seq_colim_over (id0_seq_diagram_over f a₀)) _ _ (ι f a₁) ⬝e _,
+  { apply @(is_trunc_equiv_closed_rev _
+      (sigma_seq_colim_over_equiv _ _)), apply is_contr_seq_colim },
+  { exact ιo _ idp },
+  /-
+    In the next equivalence we have to show that
+      seq_colim_over (id0_seq_diagram_over f a₀) (ι f a₁) ≃ seq_colim (id_seq_diagram f 0 a₀ a₁).
+    This looks trivial, because both of them reduce to
+      seq_colim (f^{0 ≤ 0+k}(a₀) = f^{0 ≤ 0+k}(a₁), ap_f).
+    However, not all proofs of these inequalities are definitionally equal. 3 of them are proven by
+      zero_le : 0 ≤ n,
+    but one of them (the RHS of seq_colim_over (id0_seq_diagram_over f a₀) (ι f a₁)) uses
+      le_add_right : n ≤ n+k
+    Alternatively, we could redefine le_add_right so that for n=0, it reduces to `zero_le (0+k)`.
+  -/
+  { refine seq_colim_equiv (λn, eq_equiv_eq_closed !lrep_irrel idp) _,
+    intro n p, refine whisker_right _ (!lrep_irrel2⁻² ⬝ !ap_inv⁻¹) ⬝ !ap_con⁻¹ }
+end
+
+definition seq_colim_eq_equiv0 (x y : A 0) : ι f x = ι f y ≃ seq_colim (id0_seq_diagram f x y) :=
+seq_colim_eq_equiv0' f x y ⬝e seq_colim_id_equiv_seq_colim_id0 f x y
+
+definition seq_colim_eq_equiv {n : ℕ} (x y : A n) :
+  ι f x = ι f y ≃ seq_colim (id_seq_diagram f n x y) :=
+eq_equiv_fn_eq_of_equiv (kshift_equiv f n) (ι f x) (ι f y) ⬝e
+eq_equiv_eq_closed (incl_kshift_diag0 f x)⁻¹ (incl_kshift_diag0 f y)⁻¹ ⬝e
+seq_colim_eq_equiv0' (kshift_diag f n) x y ⬝e
+@seq_colim_equiv _ _ _ (λk, ap (@f _))
+  (λm, eq_equiv_eq_closed !lrep_kshift_diag !lrep_kshift_diag)
+  (λm p, whisker_right _ (whisker_right _ !ap_inv⁻¹ ⬝ !ap_con⁻¹) ⬝ !ap_con⁻¹) ⬝e
+seq_colim_equiv
+  (λm, !lrep_eq_lrep_irrel (ap (add n) (nat.zero_add m)))
+  begin
+    intro m q,
+    refine _ ⬝ lrep_eq_lrep_irrel_natural f (le_add_right n m) (ap (add n) (nat.zero_add m)) q,
+    exact ap (λx, lrep_eq_lrep_irrel f _ _ _ _ x _) !is_prop.elim
+  end
+
+open algebra
+theorem is_trunc_seq_colim [instance] (k : ℕ₋₂) [H : Πn, is_trunc k (A n)] :
+  is_trunc k (seq_colim f) :=
+begin
+  revert A f H, induction k with k IH: intro A f H,
+  { apply is_contr_seq_colim },
+  { apply is_trunc_succ_intro, intro x y,
+    induction x using seq_colim.rec_prop with n a,
+    induction y using seq_colim.rec_prop with m a',
+    apply is_trunc_equiv_closed,
+      exact eq_equiv_eq_closed (lrep_glue _ (le_max_left n m) _) (lrep_glue _ (le_max_right n m) _),
+    apply is_trunc_equiv_closed_rev,
+      apply seq_colim_eq_equiv,
+    apply IH, intro l, apply is_trunc_eq }
+end
+
+definition seq_colim_trunc_of_trunc_seq_colim [unfold 4] (k : ℕ₋₂) (x : trunc k (seq_colim f)) :
+  seq_colim (trunc_diagram k f) :=
+begin induction x with x, exact seq_colim_functor (λn, tr) (λn y, idp) x end
+
+definition trunc_seq_colim_of_seq_colim_trunc [unfold 4] (k : ℕ₋₂)
+  (x : seq_colim (trunc_diagram k f)) : trunc k (seq_colim f) :=
+begin
+  induction x with n x n x,
+  { induction x with a, exact tr (ι f a) },
+  { induction x with a, exact ap tr (glue f a) }
+end
+
+definition trunc_seq_colim_equiv [constructor] (k : ℕ₋₂) :
+  trunc k (seq_colim f) ≃ seq_colim (trunc_diagram k f) :=
+equiv.MK (seq_colim_trunc_of_trunc_seq_colim f k) (trunc_seq_colim_of_seq_colim_trunc f k)
+  abstract begin
+    intro x, induction x with n x n x,
+    { induction x with a, reflexivity },
+    { induction x with a, apply eq_pathover_id_right, apply hdeg_square,
+      refine ap_compose (seq_colim_trunc_of_trunc_seq_colim f k) _ _ ⬝ ap02 _ !elim_glue ⬝ _,
+      refine !ap_compose'⁻¹ ⬝ !elim_glue ⬝ _, exact !idp_con }
+  end end
+  abstract begin
+    intro x, induction x with x, induction x with n a n a,
+    { reflexivity },
+    { apply eq_pathover, apply hdeg_square,
+      refine ap_compose (trunc_seq_colim_of_seq_colim_trunc f k) _ _ ⬝ ap02 _ !elim_glue ⬝ _,
+      refine !ap_compose'⁻¹ ⬝ !elim_glue }
+  end end
+
+/- the colimit of a sequence of fibers is the fiber of the functorial action of the colimit -/
+definition domain_seq_colim_functor {A A' : ℕ → Type} {f : seq_diagram A}
+  {f' : seq_diagram A'} (τ : Πn, A' n → A n)
+  (p : Π⦃n⦄, τ (n+1) ∘ @f' n ~ @f n ∘ @τ n) :
+    (Σ(x : seq_colim f), seq_colim_over (seq_diagram_over_fiber τ p) x) ≃ seq_colim f' :=
+begin
+  transitivity seq_colim (seq_diagram_sigma (seq_diagram_over_fiber τ p)),
+    exact sigma_seq_colim_over_equiv _ (seq_diagram_over_fiber τ p),
+    exact seq_colim_equiv (λn, sigma_fiber_equiv (τ n)) (λn x, idp)
+end
+
+definition fiber_seq_colim_functor {A A' : ℕ → Type} {f : seq_diagram A}
+  {f' : seq_diagram A'} (τ : Πn, A' n → A n)
+  (p : Π⦃n⦄, τ (n+1) ∘ @f' n ~ @f n ∘ @τ n) {n : ℕ} (a : A n) :
+    fiber (seq_colim_functor τ p) (ι f a) ≃ seq_colim (seq_diagram_fiber τ p a) :=
+begin
+  refine _ ⬝e fiber_pr1 (seq_colim_over (seq_diagram_over_fiber τ p)) (ι f a),
+  apply fiber_equiv_of_triangle (domain_seq_colim_functor τ p)⁻¹ᵉ,
+  refine _ ⬝hty λx, (colim_sigma_triangle _ _)⁻¹,
+  apply homotopy_inv_of_homotopy_pre (seq_colim_equiv _ _) (seq_colim_functor _ _) (seq_colim_functor _ _),
+  refine (λx, !seq_colim_functor_compose⁻¹) ⬝hty _,
+  refine seq_colim_functor_homotopy _ _,
+  intro n x, exact point_eq x.2,
+  intro n x, induction x with x y, induction y with y q, induction q,
+  apply square_of_eq, refine !idp_con⁻¹
+end
+
+definition fiber_seq_colim_functor0 {A A' : ℕ → Type} {f : seq_diagram A}
+  {f' : seq_diagram A'} (τ : Πn, A' n → A n)
+  (p : Π⦃n⦄, τ (n+1) ∘ @f' n ~ @f n ∘ @τ n) (a : A 0) :
+    fiber (seq_colim_functor τ p) (ι f a) ≃ seq_colim (seq_diagram_fiber0 τ p a) :=
+sorry
+
+
+/- the sequential colimit of standard finite types is ℕ -/
+open fin
+definition nat_of_seq_colim_fin [unfold 1] (x : seq_colim seq_diagram_fin) : ℕ :=
+begin
+  induction x with n x n x,
+  { exact x },
+  { reflexivity }
+end
+
+definition seq_colim_fin_of_nat (n : ℕ) : seq_colim seq_diagram_fin :=
+ι' _ (n+1) (fin.mk n (self_lt_succ n))
+
+definition lrep_seq_diagram_fin {n : ℕ} (x : fin n) :
+  lrep seq_diagram_fin (is_lt x) (fin.mk x (self_lt_succ x)) = x :=
+begin
+  induction x with k H, esimp, induction H with n H p,
+    reflexivity,
+  exact ap (@lift_succ2 _) p
+end
+
+definition lrep_seq_diagram_fin_lift_succ {n : ℕ} (x : fin n) :
+  lrep_seq_diagram_fin (lift_succ2 x) = ap (@lift_succ2 _) (lrep_seq_diagram_fin x) :=
+begin
+  induction x with k H, reflexivity
+end
+
+definition seq_colim_fin_equiv [constructor] : seq_colim seq_diagram_fin ≃ ℕ :=
+equiv.MK nat_of_seq_colim_fin seq_colim_fin_of_nat
+  abstract begin
+    intro n, reflexivity
+  end end
+  abstract begin
+    intro x, induction x with n x n x,
+    { esimp, refine (lrep_glue _ (is_lt x) _)⁻¹ ⬝ ap (ι _) (lrep_seq_diagram_fin x), },
+    { apply eq_pathover_id_right,
+      refine ap_compose seq_colim_fin_of_nat _ _ ⬝ ap02 _ !elim_glue ⬝ph _,
+      esimp, refine (square_of_eq !con_idp)⁻¹ʰ ⬝h _,
+      refine _ ⬝pv natural_square_tr (@glue _ (seq_diagram_fin) n) (lrep_seq_diagram_fin x),
+      refine ap02 _ !lrep_seq_diagram_fin_lift_succ ⬝ !ap_compose⁻¹ }
+  end end
+
+/- the sequential colimit of embeddings is an embedding -/
+
+definition seq_colim_eq_equiv0'_inv_refl (a₀ : A 0) :
+  (seq_colim_eq_equiv0' f a₀ a₀)⁻¹ᵉ (ι' (id_seq_diagram f 0 a₀ a₀) 0 proof (refl a₀) qed) = refl (ι f a₀) :=
+begin
+  apply inv_eq_of_eq,
+  reflexivity,
+end
+
+definition is_embedding_ι (H : Πn, is_embedding (@f n)) : is_embedding (ι' f 0) :=
+begin
+  intro x y, fapply is_equiv_of_equiv_of_homotopy,
+  { symmetry, refine seq_colim_eq_equiv0' f x y ⬝e _,
+    apply equiv_of_is_equiseq, intro n, apply H },
+  { intro p, induction p, apply seq_colim_eq_equiv0'_inv_refl }
+end
+
+end seq_colim

colimit/sequence.hlean

@@ -0,0 +1,263 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Egbert Rijke
+-/
+
+import ..move_to_lib types.fin types.trunc
+
+open nat eq equiv sigma sigma.ops is_equiv is_trunc trunc prod fiber
+
+namespace seq_colim
+
+  definition seq_diagram [reducible] (A : ℕ → Type) : Type := Π⦃n⦄, A n → A (succ n)
+
+  structure Seq_diagram : Type :=
+    (carrier : ℕ → Type)
+    (struct : seq_diagram carrier)
+
+  definition is_equiseq [reducible] {A : ℕ → Type} (f : seq_diagram A) : Type :=
+  forall (n : ℕ), is_equiv (@f n)
+
+  structure Equi_seq : Type :=
+    (carrier : ℕ → Type)
+    (maps : seq_diagram carrier)
+    (prop : is_equiseq maps)
+
+  protected abbreviation Mk [constructor] := Seq_diagram.mk
+  attribute Seq_diagram.carrier [coercion]
+  attribute Seq_diagram.struct [coercion]
+
+  variables {A A' : ℕ → Type} (f : seq_diagram A) (f' : seq_diagram A')
+  include f
+
+  definition lrep {n m : ℕ} (H : n ≤ m) (a : A n) : A m :=
+  begin
+    induction H with m H y,
+    { exact a },
+    { exact f y }
+  end
+
+  definition lrep_irrel_pathover {n m m' : ℕ} (H₁ : n ≤ m) (H₂ : n ≤ m') (p : m = m') (a : A n) :
+    lrep f H₁ a =[p] lrep f H₂ a :=
+  apo (λm H, lrep f H a) !is_prop.elimo
+
+  definition lrep_irrel {n m : ℕ} (H₁ H₂ : n ≤ m) (a : A n) : lrep f H₁ a = lrep f H₂ a :=
+  ap (λH, lrep f H a) !is_prop.elim
+
+  definition lrep_eq_transport {n m : ℕ} (H : n ≤ m) (p : n = m) (a : A n) : lrep f H a = transport A p a :=
+  begin induction p, exact lrep_irrel f H (nat.le_refl n) a end
+
+  definition lrep_irrel2 {n m : ℕ} (H₁ H₂ : n ≤ m) (a : A n) :
+    lrep_irrel f (le.step H₁) (le.step H₂) a = ap (@f m) (lrep_irrel f H₁ H₂ a) :=
+  begin
+    have H₁ = H₂, from !is_prop.elim, induction this,
+    refine ap02 _ !is_prop_elim_self ⬝ _ ⬝ ap02 _(ap02 _ !is_prop_elim_self⁻¹),
+    reflexivity
+  end
+
+  definition lrep_eq_lrep_irrel {n m m' : ℕ} (H₁ : n ≤ m) (H₂ : n ≤ m') (a₁ a₂ : A n) (p : m = m') :
+    (lrep f H₁ a₁ = lrep f H₁ a₂) ≃ (lrep f H₂ a₁ = lrep f H₂ a₂) :=
+  equiv_apd011 (λm H, lrep f H a₁ = lrep f H a₂) (is_prop.elimo p H₁ H₂)
+
+  definition lrep_eq_lrep_irrel_natural {n m m' : ℕ} {H₁ : n ≤ m} (H₂ : n ≤ m') {a₁ a₂ : A n}
+    (p : m = m') (q : lrep f H₁ a₁ = lrep f H₁ a₂) :
+    lrep_eq_lrep_irrel f (le.step H₁) (le.step H₂) a₁ a₂ (ap succ p) (ap (@f m) q) =
+    ap (@f m') (lrep_eq_lrep_irrel f H₁ H₂ a₁ a₂ p q) :=
+  begin
+    esimp [lrep_eq_lrep_irrel],
+    symmetry,
+    refine fn_tro_eq_tro_fn2 _ (λa₁ a₂, ap (@f _)) q ⬝ _,
+    refine ap (λx, x ▸o _) (@is_prop.elim _ _ _ _),
+    apply is_trunc_pathover
+  end
+
+  definition is_equiv_lrep [constructor] [Hf : is_equiseq f] {n m : ℕ} (H : n ≤ m) :
+    is_equiv (lrep f H) :=
+  begin
+    induction H with m H Hlrepf,
+    { apply is_equiv_id },
+    { exact is_equiv_compose (@f _) (lrep f H) },
+  end
+
+  local attribute is_equiv_lrep [instance]
+  definition lrep_back [reducible] [Hf : is_equiseq f] {n m : ℕ} (H : n ≤ m) : A m → A n :=
+  (lrep f H)⁻¹ᶠ
+
+  section generalized_lrep
+  variable {n : ℕ}
+
+  -- definition lrep_pathover_lrep0 [reducible] (k : ℕ) (a : A 0) : lrep f k a =[nat.zero_add k] lrep0 f k a :=
+  -- begin induction k with k p, constructor, exact pathover_ap A succ (apo f p) end
+
+  /- lreplace le_of_succ_le with this -/
+
+  definition lrep_f {n m : ℕ} (H : succ n ≤ m) (a : A n) :
+    lrep f H (f a) = lrep f (le_step_left H) a :=
+  begin
+    induction H with m H p,
+    { reflexivity },
+    { exact ap (@f m) p }
+  end
+
+  definition lrep_lrep {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) (a : A n) :
+    lrep f H2 (lrep f H1 a) = lrep f (nat.le_trans H1 H2) a :=
+  begin
+    induction H2 with k H2 p,
+    { reflexivity },
+    { exact ap (@f k) p }
+  end
+
+  -- -- this should be a squareover
+  -- definition lrep_lrep_succ (k l : ℕ) (a : A n) :
+  --   lrep_lrep f k (succ l) a = change_path (idontwanttoprovethis n l k)
+  --   (lrep_f f k (lrep f l a) ⬝o
+  --    lrep_lrep f (succ k) l a ⬝o
+  --    pathover_ap _ (λz, n + z) (apd (λz, lrep f z a) (succ_add l k)⁻¹ᵖ)) :=
+  -- begin
+  --   induction k with k IH,
+  --   { constructor},
+  --   { exact sorry}
+  -- end
+
+  definition f_lrep {n m : ℕ} (H : n ≤ m) (a : A n) : f (lrep f H a) = lrep f (le.step H) a := idp
+
+  definition rep (m : ℕ) (a : A n) : A (n + m) :=
+  lrep f (le_add_right n m) a
+
+  definition rep0 (m : ℕ) (a : A 0) : A m :=
+  lrep f (zero_le m) a
+
+  -- definition old_rep (m : ℕ) (a : A n) : A (n + m) :=
+  -- by induction m with m y; exact a; exact f y
+
+  -- definition rep_eq_old_rep (m : ℕ) (a : A n) : rep f m a = old_rep f m a :=
+  -- by induction m with m p; reflexivity; exact ap (@f _) p
+
+  definition rep_f (k : ℕ) (a : A n) :
+    pathover A (rep f k (f a)) (succ_add n k) (rep f (succ k) a) :=
+  begin
+    induction k with k IH,
+    { constructor },
+    { unfold [succ_add], apply pathover_ap, exact apo f IH}
+  end
+
+  definition rep_rep (k l : ℕ) (a : A n) :
+    pathover A (rep f k (rep f l a)) (nat.add_assoc n l k) (rep f (l + k) a) :=
+  begin
+    induction k with k IH,
+    { constructor},
+    { apply pathover_ap, exact apo f IH}
+  end
+
+  end generalized_lrep
+
+  section shift
+
+  definition shift_diag [unfold_full] : seq_diagram (λn, A (succ n)) :=
+  λn a, f a
+
+  definition kshift_diag [unfold_full] (k : ℕ) : seq_diagram (λn, A (k + n)) :=
+  λn a, f a
+
+  definition kshift_diag' [unfold_full] (k : ℕ) : seq_diagram (λn, A (n + k)) :=
+  λn a, transport A (succ_add n k)⁻¹ (f a)
+
+  definition lrep_kshift_diag {n m k : ℕ} (H : m ≤ k) (a : A (n + m)) :
+    lrep (kshift_diag f n) H a = lrep f (nat.add_le_add_left2 H n) a :=
+  by induction H with k H p; reflexivity; exact ap (@f _) p
+
+  end shift
+
+  section constructions
+
+    omit f
+
+    definition constant_seq (X : Type) : seq_diagram (λ n, X) :=
+    λ n x, x
+
+    definition seq_diagram_arrow_left [unfold_full] (X : Type) : seq_diagram (λn, X → A n) :=
+    λn g x, f (g x)
+
+    definition seq_diagram_prod [unfold_full] : seq_diagram (λn, A n × A' n) :=
+    λn, prod_functor (@f n) (@f' n)
+
+    open fin
+    definition seq_diagram_fin [unfold_full] : seq_diagram fin :=
+    lift_succ2
+
+    definition id0_seq [unfold_full] (a₁ a₂ : A 0) : ℕ → Type :=
+    λ k, rep0 f k a₁ = lrep f (zero_le k) a₂
+
+    definition id0_seq_diagram [unfold_full] (a₁ a₂ : A 0) : seq_diagram (id0_seq f a₁ a₂) :=
+    λ (k : ℕ) (p : rep0 f k a₁ = rep0 f k a₂), ap (@f k) p
+
+    definition id_seq [unfold_full] (n : ℕ) (a₁ a₂ : A n) : ℕ → Type :=
+    λ k, rep f k a₁ = rep f k a₂
+
+    definition id_seq_diagram [unfold_full] (n : ℕ) (a₁ a₂ : A n) : seq_diagram (id_seq f n a₁ a₂) :=
+    λ (k : ℕ) (p : rep f k a₁ = rep f k a₂), ap (@f (n + k)) p
+
+    definition trunc_diagram [unfold_full] (k : ℕ₋₂) (f : seq_diagram A) :
+      seq_diagram (λn, trunc k (A n)) :=
+    λn, trunc_functor k (@f n)
+
+  end constructions
+
+  section over
+
+  variable {A}
+  variable (P : Π⦃n⦄, A n → Type)
+
+  definition seq_diagram_over : Type := Π⦃n⦄ {a : A n}, P a → P (f a)
+
+  definition weakened_sequence [unfold_full] : seq_diagram_over f (λn a, A' n) :=
+  λn a a', f' a'
+
+  definition id0_seq_diagram_over [unfold_full] (a₀ : A 0) :
+    seq_diagram_over f (λn a, lrep f (zero_le n) a₀ = a) :=
+  λn a p, ap (@f n) p
+
+  variable (g : seq_diagram_over f P)
+  variables {f P}
+
+  definition seq_diagram_of_over [unfold_full] {n : ℕ} (a : A n) :
+    seq_diagram (λk, P (rep f k a)) :=
+  λk p, g p
+
+  definition seq_diagram_sigma [unfold 6] : seq_diagram (λn, Σ(x : A n), P x) :=
+  λn v, ⟨f v.1, g v.2⟩
+
+  variables {n : ℕ} (f P)
+
+  theorem rep_f_equiv [constructor] (a : A n) (k : ℕ) :
+    P (lrep f (le_add_right (succ n) k) (f a)) ≃ P (lrep f (le_add_right n (succ k)) a) :=
+  equiv_apd011 P (rep_f f k a)
+
+  theorem rep_rep_equiv [constructor] (a : A n) (k l : ℕ) :
+    P (rep f (l + k) a) ≃ P (rep f k (rep f l a)) :=
+  (equiv_apd011 P (rep_rep f k l a))⁻¹ᵉ
+
+  end over
+
+  omit f
+  -- do we need to generalize this to the case where the bottom sequence consists of equivalences?
+  definition seq_diagram_pi {X : Type} {A : X → ℕ → Type} (g : Π⦃x n⦄, A x n → A x (succ n)) :
+    seq_diagram (λn, Πx, A x n) :=
+  λn f x, g (f x)
+
+  variables {f f'}
+  definition seq_diagram_over_fiber (g : Π⦃n⦄, A n → A' n)
+    (p : Π⦃n⦄ (a : A n), g (f a) = f' (g a)) : seq_diagram_over f' (λn, fiber (@g n)) :=
+  λk a, fiber_functor (@f k) (@f' k) (@p k) idp
+
+  definition seq_diagram_fiber (g : Π⦃n⦄, A n → A' n) (p : Π⦃n⦄ (a : A n), g (f a) = f' (g a))
+    {n : ℕ} (a : A' n) : seq_diagram (λk, fiber (@g (n + k)) (rep f' k a)) :=
+  seq_diagram_of_over (seq_diagram_over_fiber g p) a
+
+  definition seq_diagram_fiber0 (g : Π⦃n⦄, A n → A' n) (p : Π⦃n⦄ (a : A n), g (f a) = f' (g a))
+    (a : A' 0) : seq_diagram (λk, fiber (@g k) (rep0 f' k a)) :=
+  λk, fiber_functor (@f k) (@f' k) (@p k) idp
+
+
+end seq_colim

move_to_lib.hlean

@@ -8,9 +8,12 @@ open eq nat int susp pointed sigma is_equiv equiv fiber algebra trunc pi group
 attribute pType.sigma_char sigma_pi_equiv_pi_sigma sigma.coind_unc [constructor]
 attribute ap1_gen [unfold 8 9 10]
 attribute ap010 [unfold 7]
+attribute tro_invo_tro [unfold 9] -- TODO: move
   -- TODO: homotopy_of_eq and apd10 should be the same
   -- TODO: there is also apd10_eq_of_homotopy in both pi and eq(?)
 
+
+
 namespace algebra
 
 variables {A : Type} [add_ab_inf_group A]
@@ -21,6 +24,10 @@ end algebra
 
 namespace eq
 
+definition homotopy.symm_symm {A : Type} {P : A → Type} {f g : Πx, P x} (H : f ~ g) :
+  H⁻¹ʰᵗʸ⁻¹ʰᵗʸ = H :=
+begin apply eq_of_homotopy, intro x, apply inv_inv end
+
   definition apd10_prepostcompose_nondep {A B C D : Type} (h : C → D) {g g' : B → C} (p : g = g')
     (f : A → B) (a : A) : apd10 (ap (λg a, h (g (f a))) p) a = ap h (apd10 p (f a)) :=
   begin induction p, reflexivity end
@@ -123,6 +130,162 @@ namespace eq
   homotopy_group_isomorphism_of_pequiv n f ⬝g
   ghomotopy_group_ptrunc_of_le H B
 
+definition equiv_pathover2 {A : Type} {a a' : A} (p : a = a')
+  {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a')
+  (r : to_fun f =[p] to_fun g) : f =[p] g :=
+begin
+  fapply pathover_of_fn_pathover_fn,
+  { intro a, apply equiv.sigma_char },
+  { apply sigma_pathover _ _ _ r, apply is_prop.elimo }
+end
+
+definition equiv_pathover_inv {A : Type} {a a' : A} (p : a = a')
+  {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a')
+  (r : to_inv f =[p] to_inv g) : f =[p] g :=
+begin
+  /- this proof is a bit weird, but it works -/
+  apply equiv_pathover2,
+  change f⁻¹ᶠ⁻¹ᶠ =[p] g⁻¹ᶠ⁻¹ᶠ,
+  apply apo (λ(a: A) (h : C a ≃ B a), h⁻¹ᶠ),
+  apply equiv_pathover2,
+  exact r
+end
+
+definition transport_lemma {A : Type} {C : A → Type} {g₁ : A → A}
+  {x y : A} (p : x = y) (f : Π⦃x⦄, C x → C (g₁ x)) (z : C x) :
+  transport C (ap g₁ p)⁻¹ (f (transport C p z)) = f z :=
+by induction p; reflexivity
+
+definition transport_lemma2 {A : Type} {C : A → Type} {g₁ : A → A}
+  {x y : A} (p : x = y) (f : Π⦃x⦄, C x → C (g₁ x)) (z : C x) :
+  transport C (ap g₁ p) (f z) = f (transport C p z) :=
+by induction p; reflexivity
+
+definition eq_of_pathover_apo {A C : Type} {B : A → Type} {a a' : A} {b : B a} {b' : B a'}
+  {p : a = a'} (g : Πa, B a → C) (q : b =[p] b') :
+  eq_of_pathover (apo g q) = apd011 g p q :=
+by induction q; reflexivity
+
+  definition apd02 [unfold 8] {A : Type} {B : A → Type} (f : Πa, B a) {a a' : A} {p q : a = a'}
+    (r : p = q) : change_path r (apd f p) = apd f q :=
+  by induction r; reflexivity
+
+  definition pathover_ap_cono {A A' : Type} {a₁ a₂ a₃ : A}
+    {p₁ : a₁ = a₂} {p₂ : a₂ = a₃} (B' : A' → Type) (f : A → A')
+    {b₁ : B' (f a₁)} {b₂ : B' (f a₂)} {b₃ : B' (f a₃)}
+    (q₁ : b₁ =[p₁] b₂) (q₂ : b₂ =[p₂] b₃) :
+    pathover_ap B' f (q₁ ⬝o q₂) =
+    change_path !ap_con⁻¹ (pathover_ap B' f q₁ ⬝o pathover_ap B' f q₂) :=
+  by induction q₁; induction q₂; reflexivity
+
+  definition concato_eq_eq {A : Type} {B : A → Type} {a₁ a₂ : A} {p₁ : a₁ = a₂}
+    {b₁ : B a₁} {b₂ b₂' : B a₂} (r : b₁ =[p₁] b₂) (q : b₂ = b₂') :
+    r ⬝op q = r ⬝o pathover_idp_of_eq q :=
+  by induction q; reflexivity
+
+definition ap_apd0111 {A₁ A₂ A₃ : Type} {B : A₁ → Type} {C : Π⦃a⦄, B a → Type} {a a₂ : A₁}
+  {b : B a} {b₂ : B a₂} {c : C b} {c₂ : C b₂}
+  (g : A₂ → A₃) (f : Πa b, C b → A₂) (Ha : a = a₂) (Hb : b =[Ha] b₂)
+    (Hc : c =[apd011 C Ha Hb] c₂) :
+  ap g (apd0111 f Ha Hb Hc) = apd0111 (λa b c, (g (f a b c))) Ha Hb Hc :=
+by induction Hb; induction Hc using idp_rec_on; reflexivity
+
+section squareover
+
+  variables {A A' : Type} {B : A → Type}
+            {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ : A}
+            /-a₀₀-/ {p₁₀ : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/
+       {p₀₁ : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂}
+            /-a₀₂-/ {p₁₂ : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/
+       {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄}
+            /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/
+            {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} {s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁}
+            {s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃} {s₃₃ : square p₃₂ p₃₄ p₂₃ p₄₃}
+
+            {b : B a}
+            {b₀₀ : B a₀₀} {b₂₀ : B a₂₀} {b₄₀ : B a₄₀}
+            {b₀₂ : B a₀₂} {b₂₂ : B a₂₂} {b₄₂ : B a₄₂}
+            {b₀₄ : B a₀₄} {b₂₄ : B a₂₄} {b₄₄ : B a₄₄}
+            /-b₀₀-/ {q₁₀ : b₀₀ =[p₁₀] b₂₀} /-b₂₀-/ {q₃₀ : b₂₀ =[p₃₀] b₄₀} /-b₄₀-/
+            /-b₀₂-/ {q₁₂ : b₀₂ =[p₁₂] b₂₂} /-b₂₂-/ {q₃₂ : b₂₂ =[p₃₂] b₄₂} /-b₄₂-/
+            /-b₀₄-/ {q₁₄ : b₀₄ =[p₁₄] b₂₄} /-b₂₄-/ {q₃₄ : b₂₄ =[p₃₄] b₄₄} /-b₄₄-/
+   {q₀₁ : b₀₀ =[p₀₁] b₀₂} /-t₁₁-/ {q₂₁ : b₂₀ =[p₂₁] b₂₂} /-t₃₁-/ {q₄₁ : b₄₀ =[p₄₁] b₄₂}
+   {q₀₃ : b₀₂ =[p₀₃] b₀₄} /-t₁₃-/ {q₂₃ : b₂₂ =[p₂₃] b₂₄} /-t₃₃-/ {q₄₃ : b₄₂ =[p₄₃] b₄₄}
+
+  definition move_right_of_top_over {p : a₀₀ = a} {p' : a = a₂₀}
+    {s : square p p₁₂ p₀₁ (p' ⬝ p₂₁)} {q : b₀₀ =[p] b} {q' : b =[p'] b₂₀}
+    (t : squareover B (move_top_of_right s) (q ⬝o q') q₁₂ q₀₁ q₂₁) :
+    squareover B s q q₁₂ q₀₁ (q' ⬝o q₂₁) :=
+  begin induction q', induction q, induction q₂₁, exact t end
+
+  /- TODO: replace the version in the library by this -/
+  definition hconcato_pathover' {p : a₂₀ = a₂₂} {sp : p = p₂₁} {s : square p₁₀ p₁₂ p₀₁ p}
+    {q : b₂₀ =[p] b₂₂} (t₁₁ : squareover B (s ⬝hp sp) q₁₀ q₁₂ q₀₁ q₂₁)
+    (r : change_path sp q = q₂₁) : squareover B s q₁₀ q₁₂ q₀₁ q :=
+  by induction sp; induction r; exact t₁₁
+
+  variables (s₁₁ q₀₁ q₁₀ q₂₁ q₁₂)
+  definition squareover_fill_t : Σ (q : b₀₀ =[p₁₀] b₂₀), squareover B s₁₁ q q₁₂ q₀₁ q₂₁ :=
+  begin
+    induction s₁₁, induction q₀₁ using idp_rec_on, induction q₂₁ using idp_rec_on,
+    induction q₁₂ using idp_rec_on, exact ⟨idpo, idso⟩
+  end
+
+  definition squareover_fill_b : Σ (q : b₀₂ =[p₁₂] b₂₂), squareover B s₁₁ q₁₀ q q₀₁ q₂₁ :=
+  begin
+    induction s₁₁, induction q₀₁ using idp_rec_on, induction q₂₁ using idp_rec_on,
+    induction q₁₀ using idp_rec_on, exact ⟨idpo, idso⟩
+  end
+
+  definition squareover_fill_l : Σ (q : b₀₀ =[p₀₁] b₀₂), squareover B s₁₁ q₁₀ q₁₂ q q₂₁ :=
+  begin
+    induction s₁₁, induction q₁₀ using idp_rec_on, induction q₂₁ using idp_rec_on,
+    induction q₁₂ using idp_rec_on, exact ⟨idpo, idso⟩
+  end
+
+  definition squareover_fill_r : Σ (q : b₂₀ =[p₂₁] b₂₂) , squareover B s₁₁ q₁₀ q₁₂ q₀₁ q :=
+  begin
+    induction s₁₁, induction q₀₁ using idp_rec_on, induction q₁₀ using idp_rec_on,
+    induction q₁₂ using idp_rec_on, exact ⟨idpo, idso⟩
+  end
+
+
+end squareover
+
+/- move this to types.eq, and replace the proof there -/
+  section
+    parameters {A : Type} (a₀ : A) (code : A → Type) (H : is_contr (Σa, code a))
+      (c₀ : code a₀)
+    include H c₀
+    protected definition encode2 {a : A} (q : a₀ = a) : code a :=
+    transport code q c₀
+
+    protected definition decode2' {a : A} (c : code a) : a₀ = a :=
+    have ⟨a₀, c₀⟩ = ⟨a, c⟩ :> Σa, code a, from !is_prop.elim,
+    this..1
+
+    protected definition decode2 {a : A} (c : code a) : a₀ = a :=
+    (decode2' c₀)⁻¹ ⬝ decode2' c
+
+    open sigma.ops
+    definition total_space_method2 (a : A) : (a₀ = a) ≃ code a :=
+    begin
+      fapply equiv.MK,
+      { exact encode2 },
+      { exact decode2 },
+      { intro c, unfold [encode2, decode2, decode2'],
+        rewrite [is_prop_elim_self, ▸*, idp_con],
+        apply tr_eq_of_pathover, apply eq_pr2 },
+      { intro q, induction q, esimp, apply con.left_inv, },
+    end
+  end
+
+definition total_space_method2_refl {A : Type} (a₀ : A) (code : A → Type) (H : is_contr (Σa, code a))
+  (c₀ : code a₀) : total_space_method2 a₀ code H c₀ a₀ idp = c₀ :=
+begin
+  reflexivity
+end
+
   section hsquare
   variables {A₀₀ A₂₀ A₄₀ A₀₂ A₂₂ A₄₂ A₀₄ A₂₄ A₄₄ : Type}
             {f₁₀ : A₀₀ → A₂₀} {f₃₀ : A₂₀ → A₄₀}
@@ -209,6 +372,21 @@ namespace nat
       exact q ⬝htyh p
   end
 
+definition iterate_equiv2 {A : Type} {C : A → Type} (f : A → A) (h : Πa, C a ≃ C (f a))
+  (k : ℕ) (a : A) : C a ≃ C (f^[k] a) :=
+begin induction k with k IH, reflexivity, exact IH ⬝e h (f^[k] a) end
+
+
+
+  /- replace proof of le_of_succ_le by this -/
+  definition le_step_left {n m : ℕ} (H : succ n ≤ m) : n ≤ m :=
+  by induction H with H m H'; exact le_succ n; exact le.step H'
+
+  /- TODO: make proof of le_succ_of_le simpler -/
+
+  definition nat.add_le_add_left2 {n m : ℕ} (H : n ≤ m) (k : ℕ) : k + n ≤ k + m :=
+  by induction H with m H H₂; reflexivity; exact le.step H₂
+
 end nat
 
 
@@ -511,6 +689,29 @@ namespace sigma
     change_path (ap_sigma_pr1 f g p)⁻¹ (pathover_ap C f (apd g p)) :=
   by induction p; reflexivity
 
+definition ap_sigma_functor_sigma_eq {A A' : Type} {B : A → Type} {B' : A' → Type}
+  {a a' : A} {b : B a} {b' : B a'} (f : A → A') (g : Πa, B a → B' (f a)) (p : a = a') (q : b =[p] b') :
+  ap (sigma_functor f g) (sigma_eq p q) = sigma_eq (ap f p) (pathover_ap B' f (apo g q)) :=
+by induction q; reflexivity
+
+definition ap_sigma_functor_id_sigma_eq {A : Type} {B B' : A → Type}
+  {a a' : A} {b : B a} {b' : B a'} (g : Πa, B a → B' a) (p : a = a') (q : b =[p] b') :
+  ap (sigma_functor id g) (sigma_eq p q) = sigma_eq p (apo g q) :=
+by induction q; reflexivity
+
+definition sigma_eq_pr2_constant {A B : Type} {a a' : A} {b b' : B} (p : a = a')
+  (q : b =[p] b') : ap pr2 (sigma_eq p q) = (eq_of_pathover q) :=
+by induction q; reflexivity
+
+definition sigma_eq_pr2_constant2 {A B : Type} {a a' : A} {b b' : B} (p : a = a')
+  (q : b = b') : ap pr2 (sigma_eq p (pathover_of_eq p q)) = q :=
+by induction p; induction q; reflexivity
+
+definition sigma_eq_concato_eq {A : Type} {B : A → Type} {a a' : A} {b : B a} {b₁ b₂ : B a'}
+  (p : a = a') (q : b =[p] b₁) (q' : b₁ = b₂) : sigma_eq p (q ⬝op q') = sigma_eq p q ⬝ ap (dpair a') q' :=
+by induction q'; reflexivity
+
+
   -- open sigma.ops
   -- definition eq.rec_sigma {A : Type} {B : A → Type} {a₀ : A} {b₀ : B a₀}
   --   {P : Π(a : A) (b : B a), ⟨a₀, b₀⟩ = ⟨a, b⟩ → Type} (H : P a₀ b₀ idp) {a : A} {b : B a}
@@ -592,8 +793,48 @@ namespace fiber
   definition is_contr_pfiber_pid (A : Type*) : is_contr (pfiber (pid A)) :=
   is_contr.mk pt begin intro x, induction x with a p, esimp at p, cases p, reflexivity end
 
+definition fiber_functor [constructor] {A A' B B' : Type} {f : A → B} {f' : A' → B'} {b : B} {b' : B'}
+  (g : A → A') (h : B → B') (H : hsquare g h f f') (p : h b = b') (x : fiber f b) : fiber f' b' :=
+fiber.mk (g (point x)) (H (point x) ⬝ ap h (point_eq x) ⬝ p)
+
+definition pfiber_functor [constructor] {A A' B B' : Type*} {f : A →* B} {f' : A' →* B'}
+  (g : A →* A') (h : B →* B') (H : psquare g h f f') : pfiber f →* pfiber f' :=
+pmap.mk (fiber_functor g h H (respect_pt h))
+  begin
+    fapply fiber_eq,
+      exact respect_pt g,
+      exact !con.assoc ⬝ to_homotopy_pt H
+  end
+
+-- TODO: use this in pfiber_pequiv_of_phomotopy
+definition fiber_equiv_of_homotopy {A B : Type} {f g : A → B} (h : f ~ g) (b : B)
+  : fiber f b ≃ fiber g b :=
+begin
+  refine (fiber.sigma_char f b ⬝e _ ⬝e (fiber.sigma_char g b)⁻¹ᵉ),
+  apply sigma_equiv_sigma_right, intros a,
+  apply equiv_eq_closed_left, apply h
+end
+
+definition fiber_equiv_of_square {A B C D : Type} {b : B} {d : D} {f : A → B} {g : C → D} (h : A ≃ C)
+  (k : B ≃ D) (s : k ∘ f ~ g ∘ h) (p : k b = d) : fiber f b ≃ fiber g d :=
+  calc fiber f b ≃ fiber (k ∘ f) (k b) : fiber.equiv_postcompose
+            ... ≃ fiber (k ∘ f) d : transport_fiber_equiv (k ∘ f) p
+            ... ≃ fiber (g ∘ h) d : fiber_equiv_of_homotopy s d
+            ... ≃ fiber g d : fiber.equiv_precompose
+
+definition fiber_equiv_of_triangle {A B C : Type} {b : B} {f : A → B} {g : C → B} (h : A ≃ C)
+  (s : f ~ g ∘ h) : fiber f b ≃ fiber g b :=
+fiber_equiv_of_square h erfl s idp
+
 end fiber
 
+namespace fin
+
+definition lift_succ2 [constructor] ⦃n : ℕ⦄ (x : fin n) : fin (nat.succ n) :=
+fin.mk x (le.step (is_lt x))
+
+end fin
+
 namespace function
   variables {A B : Type} {f f' : A → B}
   open is_conn sigma.ops