feat(homotopy): prove the naive Seifert-Van Kampen theorem

Also define the pushout of categories and the pushout of groupoids
2016-05-18 00:33:35 -04:00 · 2016-05-18 00:33:35 -04:00 · e96e4a677d
commit e96e4a677d
parent 61848c4a2e
10 changed files with 477 additions and 56 deletions
--- a/hott/algebra/category/constructions/constructions.md
+++ b/hott/algebra/category/constructions/constructions.md
@ -10,11 +10,13 @@ Common categories and constructions on categories. The following files are in th
 * [product](product.hlean) : Product category
 * [comma](comma.hlean) : Comma category
 * [cone](cone.hlean) : Cone category
+* [pushout](pushout.hlean) : Pushout of categories, pushout of groupoids. Also more generally the category formed by a (quotient of) paths in a graph
+* [fundamental_groupoid](fundamental_groupoid.hlean) : The fundamental groupoid of a type

 Discrete, indiscrete or finite categories:

 * [finite_cats](finite_cats.hlean) : Some finite categories, which are diagrams of common limits (the diagram for the pullback or the equalizer). Also contains a general construction of categories where you give some generators for the morphisms, with the condition that you cannot compose two of thosex
-* [discrete](discrete.hlean)
+* [discrete](discrete.hlean) : Discrete category. Also the groupoid formed by a 1-type
 * [indiscrete](indiscrete.hlean)
 * [terminal](terminal.hlean)
 * [initial](initial.hlean)
--- a/hott/algebra/category/constructions/default.hlean
+++ b/hott/algebra/category/constructions/default.hlean
@ -5,3 +5,4 @@ Authors: Floris van Doorn
 -/

 import .functor .set .opposite .product .comma .sum .discrete .indiscrete .terminal .initial .order
+       .pushout .fundamental_groupoid
--- a/hott/algebra/category/constructions/discrete.hlean
+++ b/hott/algebra/category/constructions/discrete.hlean
@ -69,6 +69,4 @@ namespace category
  { intro b₁ b₂ p, induction p, induction b₁: esimp: apply id_comp_eq_comp_id},
  end

-
-
 end category
--- a/hott/algebra/category/constructions/fundamental_groupoid.hlean
+++ b/hott/algebra/category/constructions/fundamental_groupoid.hlean
@ -0,0 +1,32 @@
+/-
+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
+-/
+
+import ..groupoid ..functor.basic
+
+open eq is_trunc iso trunc functor
+
+namespace category
+
+  definition fundamental_precategory [constructor] (A : Type) : Precategory :=
+  precategory.MK A
+                 (λa a', trunc 0 (a = a'))
+                 _
+                 (λa₁ a₂ a₃ q p, tconcat p q)
+                 (λa, tidp)
+                 (λa₁ a₂ a₃ a₄ r q p, tassoc p q r)
+                 (λa₁ a₂, tcon_tidp)
+                 (λa₁ a₂, tidp_tcon)
+
+  definition fundamental_groupoid [constructor] (A : Type) : Groupoid :=
+  groupoid.MK (fundamental_precategory A)
+              (λa b p, is_iso.mk (tinverse p) (right_tinv p) (left_tinv p))
+
+  definition fundamental_groupoid_functor [constructor] {A B : Type} (f : A → B) :
+    fundamental_groupoid A ⇒ fundamental_groupoid B :=
+  functor.mk f (λa a', tap f) (λa, tap_tidp f) (λa₁ a₂ a₃ q p, tap_tcon f p q)
+
+end category
--- a/hott/algebra/category/constructions/pushout.hlean
+++ b/hott/algebra/category/constructions/pushout.hlean
@ -156,6 +156,52 @@ namespace indexed_list
    { rewrite [cons_append, +reverse_cons, append_concat, v_0]}
  end

+  definition realize (P : A → A → Type) (f : Π⦃a a'⦄, R a a' → P a a') (ρ : Πa, P a a)
+    (c : Π⦃a₁ a₂ a₃⦄, P a₁ a₂ → P a₂ a₃ → P a₁ a₃)
+    ⦃a a' : A⦄ (l : indexed_list R a a') : P a a' :=
+  begin
+    induction l,
+    { exact ρ a},
+    { exact c v_0 (f r)}
+  end
+
+  definition realize_nil (P : A → A → Type) (f : Π⦃a a'⦄, R a a' → P a a') (ρ : Πa, P a a)
+    (c : Π⦃a₁ a₂ a₃⦄, P a₁ a₂ → P a₂ a₃ → P a₁ a₃) (a : A) :
+    realize P f ρ c nil = ρ a :=
+  idp
+
+  definition realize_cons (P : A → A → Type) (f : Π⦃a a'⦄, R a a' → P a a') (ρ : Πa, P a a)
+    (c : Π⦃a₁ a₂ a₃⦄, P a₁ a₂ → P a₂ a₃ → P a₁ a₃)
+    ⦃a₁ a₂ a₃ : A⦄ (r : R a₂ a₃) (l : indexed_list R a₁ a₂) :
+    realize P f ρ c (r :: l) = c (realize P f ρ c l) (f r) :=
+  idp
+
+  theorem realize_singleton {P : A → A → Type} {f : Π⦃a a'⦄, R a a' → P a a'} {ρ : Πa, P a a}
+    {c : Π⦃a₁ a₂ a₃⦄, P a₁ a₂ → P a₂ a₃ → P a₁ a₃}
+    (id_left : Π⦃a₁ a₂⦄ (p : P a₁ a₂), c (ρ a₁) p = p)
+    ⦃a₁ a₂ : A⦄ (r : R a₁ a₂) :
+    realize P f ρ c [r] = f r :=
+  id_left (f r)
+
+  theorem realize_pair {P : A → A → Type} {f : Π⦃a a'⦄, R a a' → P a a'} {ρ : Πa, P a a}
+    {c : Π⦃a₁ a₂ a₃⦄, P a₁ a₂ → P a₂ a₃ → P a₁ a₃}
+    (id_left : Π⦃a₁ a₂⦄ (p : P a₁ a₂), c (ρ a₁) p = p)
+    ⦃a₁ a₂ a₃ : A⦄ (r₂ : R a₂ a₃) (r₁ : R a₁ a₂) :
+    realize P f ρ c [r₂, r₁] = c (f r₁) (f r₂) :=
+  ap (λx, c x (f r₂)) (realize_singleton id_left r₁)
+
+  theorem realize_append {P : A → A → Type} {f : Π⦃a a'⦄, R a a' → P a a'} {ρ : Πa, P a a}
+    {c : Π⦃a₁ a₂ a₃⦄, P a₁ a₂ → P a₂ a₃ → P a₁ a₃}
+    (assoc : Π⦃a₁ a₂ a₃ a₄⦄ (p : P a₁ a₂) (q : P a₂ a₃) (r : P a₃ a₄), c (c p q) r = c p (c q r))
+    (id_right : Π⦃a₁ a₂⦄ (p : P a₁ a₂), c p (ρ a₂) = p)
+    ⦃a₁ a₂ a₃ : A⦄ (l₂ : indexed_list R a₂ a₃) (l₁ : indexed_list R a₁ a₂) :
+    realize P f ρ c (l₂ ++ l₁) = c (realize P f ρ c l₁) (realize P f ρ c l₂) :=
+  begin
+    induction l₂,
+    { exact !id_right⁻¹},
+    { rewrite [cons_append, +realize_cons, v_0, assoc]}
+  end
+
  inductive indexed_list_rel {A : Type} {R : A → A → Type}
    (Q : Π⦃a a' : A⦄, indexed_list R a a' → indexed_list R a a' → Type)
    : Π⦃a a' : A⦄, indexed_list R a a' → indexed_list R a a' → Type :=
@ -249,6 +295,23 @@ namespace indexed_list
      exact rel_respect_append_right _ (ri r)}
  end

+  definition realize_eq {P : A → A → Type} {f : Π⦃a a'⦄, R a a' → P a a'} {ρ : Πa, P a a}
+    {c : Π⦃a₁ a₂ a₃⦄, P a₁ a₂ → P a₂ a₃ → P a₁ a₃}
+    (assoc : Π⦃a₁ a₂ a₃ a₄⦄ (p : P a₁ a₂) (q : P a₂ a₃) (r : P a₃ a₄), c (c p q) r = c p (c q r))
+    (id_right : Π⦃a₁ a₂⦄ (p : P a₁ a₂), c p (ρ a₂) = p)
+    (resp_rel : Π⦃a₁ a₂⦄ {l₁ l₂ : indexed_list R a₁ a₂}, Q l₁ l₂ →
+      realize P f ρ c l₁ = realize P f ρ c l₂)
+    ⦃a a' : A⦄ {l l' : indexed_list R a a'} (H : indexed_list_rel Q l l') :
+    realize P f ρ c l = realize P f ρ c l' :=
+  begin
+    induction H,
+    { reflexivity},
+    { rewrite [+realize_append assoc id_right], apply ap (c _), exact resp_rel q},
+    { exact ap (λx, c x (f r)) v_0},
+    { exact v_0 ⬝ v_1}
+  end
+
+
 end indexed_list
 namespace indexed_list
  section
@ -347,7 +410,6 @@ namespace indexed_list
  end


-
 end indexed_list
 open indexed_list

@ -355,10 +417,10 @@ namespace category

  inductive pushout_prehom_index {C D E : Precategory} (F : C ⇒ D) (G : C ⇒ E) :
    D + E → D + E → Type :=
-  | il : Π{d d' : D} (f : d ⟶ d'), pushout_prehom_index F G (inl d) (inl d')
-  | ir : Π{e e' : E} (g : e ⟶ e'), pushout_prehom_index F G (inr e) (inr e')
-  | lr : Π{c c' : C} (h : c ⟶ c'), pushout_prehom_index F G (inl (F c)) (inr (G c'))
-  | rl : Π{c c' : C} (h : c ⟶ c'), pushout_prehom_index F G (inr (G c)) (inl (F c'))
+  | iD : Π{d d' : D} (f : d ⟶ d'), pushout_prehom_index F G (inl d) (inl d')
+  | iE : Π{e e' : E} (g : e ⟶ e'), pushout_prehom_index F G (inr e) (inr e')
+  | DE : Π(c : C), pushout_prehom_index F G (inl (F c)) (inr (G c))
+  | ED : Π(c : C), pushout_prehom_index F G (inr (G c)) (inl (F c))

  open pushout_prehom_index

@ -368,15 +430,13 @@ namespace category
  inductive pushout_hom_rel_index {C D E : Precategory} (F : C ⇒ D) (G : C ⇒ E) :
    Π⦃x x' : D + E⦄, pushout_prehom F G x x' → pushout_prehom F G x x' → Type :=
  | DD  : Π{d₁ d₂ d₃ : D} (g : d₂ ⟶ d₃) (f : d₁ ⟶ d₂),
-      pushout_hom_rel_index F G [il F G g, il F G f] [il F G (g ∘ f)]
+      pushout_hom_rel_index F G [iD F G g, iD F G f] [iD F G (g ∘ f)]
  | EE  : Π{e₁ e₂ e₃ : E} (g : e₂ ⟶ e₃) (f : e₁ ⟶ e₂),
-      pushout_hom_rel_index F G [ir F G g, ir F G f] [ir F G (g ∘ f)]
-  | DED : Π{c₁ c₂ c₃ : C} (g : c₂ ⟶ c₃) (f : c₁ ⟶ c₂),
-      pushout_hom_rel_index F G [rl F G g, lr F G f] [il F G (to_fun_hom F (g ∘ f))]
-  | EDE : Π{c₁ c₂ c₃ : C} (g : c₂ ⟶ c₃) (f : c₁ ⟶ c₂),
-      pushout_hom_rel_index F G [lr F G g, rl F G f] [ir F G (to_fun_hom G (g ∘ f))]
-  | idD : Π(d : D), pushout_hom_rel_index F G [il F G (ID d)] nil
-  | idE : Π(e : E), pushout_hom_rel_index F G [ir F G (ID e)] nil
+      pushout_hom_rel_index F G [iE F G g, iE F G f] [iE F G (g ∘ f)]
+  | DED : Π(c : C), pushout_hom_rel_index F G [ED F G c, DE F G c] nil
+  | EDE : Π(c : C), pushout_hom_rel_index F G [DE F G c, ED F G c] nil
+  | idD : Π(d : D), pushout_hom_rel_index F G [iD F G (ID d)] nil
+  | idE : Π(e : E), pushout_hom_rel_index F G [iE F G (ID e)] nil

  open pushout_hom_rel_index
  -- section
@ -450,10 +510,10 @@ namespace category
    pushout_prehom_index F G x' x :=
  begin
    induction i,
-    { exact il F G f⁻¹},
-    { exact ir F G g⁻¹},
-    { exact rl F G h⁻¹},
-    { exact lr F G h⁻¹},
+    { exact iD F G f⁻¹},
+    { exact iE F G g⁻¹},
+    { exact ED F G c},
+    { exact DE F G c},
  end

  open indexed_list.indexed_list_rel
@ -461,14 +521,9 @@ namespace category
    (q : pushout_hom_rel_index F G l l') : indexed_list_rel (pushout_hom_rel_index F G)
      (reverse (pushout_index_inv F G) l) (reverse (pushout_index_inv F G) l') :=
  begin
-    induction q: apply indexed_list_rel_of_Q; rewrite reverse_singleton; try rewrite reverse_pair;
-    try rewrite reverse_nil; esimp,
-    { rewrite [comp_inverse], constructor},
-    { rewrite [comp_inverse], constructor},
-    { rewrite [-respect_inv, comp_inverse], constructor},
-    { rewrite [-respect_inv, comp_inverse], constructor},
-    { rewrite [id_inverse], constructor},
-    { rewrite [id_inverse], constructor}
+    induction q: apply indexed_list_rel_of_Q;
+    try rewrite reverse_singleton; try rewrite reverse_pair; try rewrite reverse_nil; esimp;
+    try rewrite [comp_inverse]; try rewrite [id_inverse]; constructor,
  end

  theorem pushout_index_li (i : pushout_prehom_index F G x x') :
@ -479,10 +534,8 @@ namespace category
      rewrite [comp.left_inverse], exact indexed_list_rel_of_Q !idD},
    { refine rtrans (indexed_list_rel_of_Q !EE) _,
      rewrite [comp.left_inverse], exact indexed_list_rel_of_Q !idE},
-    { refine rtrans (indexed_list_rel_of_Q !DED) _,
-      rewrite [comp.left_inverse, respect_id], exact indexed_list_rel_of_Q !idD},
-    { refine rtrans (indexed_list_rel_of_Q !EDE) _,
-      rewrite [comp.left_inverse, respect_id], exact indexed_list_rel_of_Q !idE}
+    { exact indexed_list_rel_of_Q !DED},
+    { exact indexed_list_rel_of_Q !EDE}
  end

  theorem pushout_index_ri (i : pushout_prehom_index F G x x') :
@ -493,10 +546,8 @@ namespace category
      rewrite [comp.right_inverse], exact indexed_list_rel_of_Q !idD},
    { refine rtrans (indexed_list_rel_of_Q !EE) _,
      rewrite [comp.right_inverse], exact indexed_list_rel_of_Q !idE},
-    { refine rtrans (indexed_list_rel_of_Q !EDE) _,
-      rewrite [comp.right_inverse, respect_id], exact indexed_list_rel_of_Q !idE},
-    { refine rtrans (indexed_list_rel_of_Q !DED) _,
-      rewrite [comp.right_inverse, respect_id], exact indexed_list_rel_of_Q !idD}
+    { exact indexed_list_rel_of_Q !EDE},
+    { exact indexed_list_rel_of_Q !DED}
  end

  definition Groupoid_pushout [constructor] : Groupoid :=
--- a/hott/algebra/category/groupoid.hlean
+++ b/hott/algebra/category/groupoid.hlean
@ -17,8 +17,8 @@ namespace category

  abbreviation all_iso := @groupoid.all_iso
  attribute groupoid.all_iso [instance] [priority 3000]
-
-  definition groupoid.mk [reducible] {ob : Type} (C : precategory ob)
+  attribute groupoid.to_precategory [unfold 2]
+  definition groupoid.mk [reducible] [constructor] {ob : Type} (C : precategory ob)
    (H : Π (a b : ob) (f : a ⟶ b), is_iso f) : groupoid ob :=
  precategory.rec_on C groupoid.mk' H

--- a/hott/hit/quotient.hlean
+++ b/hott/hit/quotient.hlean
@ -58,11 +58,18 @@ namespace quotient
    : transport (quotient.elim_type Pc Pp) (eq_of_rel R H) = to_fun (Pp H) :=
  by rewrite [tr_eq_cast_ap_fn, ↑quotient.elim_type, elim_eq_of_rel];apply cast_ua_fn

+  -- rename to elim_type_eq_of_rel_fn_inv
  theorem elim_type_eq_of_rel_inv (Pc : A → Type)
    (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') {a a' : A} (H : R a a')
    : transport (quotient.elim_type Pc Pp) (eq_of_rel R H)⁻¹ = to_inv (Pp H) :=
  by rewrite [tr_eq_cast_ap_fn, ↑quotient.elim_type, ap_inv, elim_eq_of_rel];apply cast_ua_inv_fn

+  -- remove '
+  theorem elim_type_eq_of_rel_inv' (Pc : A → Type)
+    (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') {a a' : A} (H : R a a') (x : Pc a')
+    : transport (quotient.elim_type Pc Pp) (eq_of_rel R H)⁻¹ x = to_inv (Pp H) x :=
+  ap10 (elim_type_eq_of_rel_inv Pc Pp H) x
+
  theorem elim_type_eq_of_rel.{u} (Pc : A → Type.{u})
    (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a ≃ Pc a') {a a' : A} (H : R a a') (p : Pc a)
    : transport (quotient.elim_type Pc Pp) (eq_of_rel R H) p = to_fun (Pp H) p :=
--- a/hott/homotopy/vankampen.hlean
+++ b/hott/homotopy/vankampen.hlean
@ -0,0 +1,275 @@
+/-
+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
+-/
+
+import hit.pushout algebra.category.constructions.pushout algebra.category.constructions.type
+       algebra.category.functor.equivalence
+
+open eq pushout category functor sum iso indexed_list set_quotient is_trunc trunc pi quotient
+     is_equiv
+
+namespace pushout
+  section
+  universe variables u v w
+  parameters {TL : Type.{u}} {BL : Type.{v}} {TR : Type.{w}} (f : TL → BL) (g : TL → TR)
+
+  definition pushout_of_sum [unfold 6] (x : BL + TR) : pushout f g :=
+  quotient.class_of _ x
+
+  local notation `C` := Groupoid_pushout (fundamental_groupoid_functor f)
+                                         (fundamental_groupoid_functor g)
+
+  local notation `R` := pushout_prehom_index (fundamental_groupoid_functor f)
+                                             (fundamental_groupoid_functor g)
+
+  local notation `Q` := pushout_hom_rel_index (fundamental_groupoid_functor f)
+                                              (fundamental_groupoid_functor g)
+
+  protected definition code [unfold 7] (x : BL + TR) (y : pushout f g) : Type.{max u v w} :=
+  begin
+    refine quotient.elim_type _ _ y,
+    { clear y, intro y, exact @hom C _ x y},
+    { clear y, intro y z r, induction r with y, fapply equiv_postcompose,
+      { apply class_of, exact [pushout_prehom_index.DE _ _ y]},
+      { refine all_iso _}}
+  end
+
+  definition is_set_code (x : BL + TR) (y : pushout f g) : is_set (code x y) :=
+  begin
+    induction y using pushout.rec_prop, apply is_set_hom, apply is_set_hom,
+  end
+  local attribute is_set_code [instance]
+
+  -- encode is easy
+  definition encode {x : BL + TR} {y : pushout f g} (p : trunc 0 (pushout_of_sum x = y)) :
+    code x y :=
+  begin
+    induction p with p,
+    exact transport (code x) p id
+  end
+
+  -- decode is harder
+  definition decode_reduction_rule [unfold 8] ⦃x x' : BL + TR⦄ (i : R x x') :
+    trunc 0 (pushout_of_sum x = pushout_of_sum x') :=
+  begin
+    induction i,
+    { exact tap inl f_1},
+    { exact tap inr g_1},
+    { exact tr (glue c)},
+    { exact tr (glue c)⁻¹},
+  end
+
+  definition decode_list ⦃x x' : BL + TR⦄ (l : indexed_list R x x') :
+    trunc 0 (pushout_of_sum x = pushout_of_sum x') :=
+  realize (λa a', trunc 0 (pushout_of_sum a = pushout_of_sum a'))
+          decode_reduction_rule
+          (λa, tidp)
+          (λa₁ a₂ a₃, tconcat) l
+
+  definition decode_list_nil (x : BL + TR) : decode_list (@nil _ _ x) = tidp :=
+  idp
+
+  definition decode_list_cons ⦃x₁ x₂ x₃ : BL + TR⦄ (r : R x₂ x₃) (l : indexed_list R x₁ x₂) :
+    decode_list (r :: l) = tconcat (decode_list l) (decode_reduction_rule r) :=
+  idp
+
+  definition decode_list_singleton ⦃x₁ x₂ : BL + TR⦄ (r : R x₁ x₂) :
+    decode_list [r] = decode_reduction_rule r :=
+  realize_singleton (λa b p, tidp_tcon p) r
+
+  definition decode_list_pair ⦃x₁ x₂ x₃ : BL + TR⦄ (r₂ : R x₂ x₃) (r₁ : R x₁ x₂) :
+    decode_list [r₂, r₁] = tconcat (decode_reduction_rule r₁) (decode_reduction_rule r₂) :=
+  realize_pair (λa b p, tidp_tcon p) r₂ r₁
+
+  definition decode_list_append ⦃x₁ x₂ x₃ : BL + TR⦄ (l₂ : indexed_list R x₂ x₃)
+    (l₁ : indexed_list R x₁ x₂) :
+    decode_list (l₂ ++ l₁) = tconcat (decode_list l₁) (decode_list l₂) :=
+  realize_append (λa b c d, tassoc) (λa b, tcon_tidp) l₂ l₁
+
+  theorem decode_list_rel ⦃x x' : BL + TR⦄ {l l' : indexed_list R x x'} (H : Q l l') :
+    decode_list l = decode_list l' :=
+  begin
+    induction H,
+    { rewrite [decode_list_pair, decode_list_singleton], exact !tap_tcon⁻¹},
+    { rewrite [decode_list_pair, decode_list_singleton], exact !tap_tcon⁻¹},
+    { rewrite [decode_list_pair, decode_list_nil], exact ap tr !con.right_inv},
+    { rewrite [decode_list_pair, decode_list_nil], exact ap tr !con.left_inv},
+    { apply decode_list_singleton},
+    { apply decode_list_singleton}
+  end
+
+  definition decode_point [unfold 8] {x x' : BL + TR} (c : @hom C _ x x') :
+    trunc 0 (pushout_of_sum x = pushout_of_sum x') :=
+  begin
+    induction c with l,
+    { exact decode_list l},
+    { induction H with H, refine realize_eq _ _ _ H,
+      { intros, apply tassoc},
+      { intros, apply tcon_tidp},
+      { clear H a a', intros, exact decode_list_rel a}}
+  end
+
+  theorem decode_coh (x : BL + TR) (y : TL) (p : trunc 0 (pushout_of_sum x = inl (f y))) :
+    p =[glue y] tconcat p (tr (glue y)) :=
+  begin
+    induction p with p,
+    apply trunc_pathover, apply eq_pathover_constant_left_id_right,
+    apply square_of_eq, exact !idp_con⁻¹
+  end
+
+  definition decode [unfold 7] {x : BL + TR} {y : pushout f g} (c : code x y) :
+    trunc 0 (pushout_of_sum x = y) :=
+  begin
+    induction y using quotient.rec with y,
+    { exact decode_point c},
+    { induction H with y, apply arrow_pathover_left, intro c,
+      revert c, apply @set_quotient.rec_prop, { intro z, apply is_trunc_pathover},
+      intro l,
+      refine _ ⬝op ap decode_point !quotient.elim_type_eq_of_rel⁻¹,
+      apply decode_coh}
+  end
+
+  -- report the failing of esimp in the commented-out proof below
+--   definition decode [unfold 7] {x : BL + TR} {y : pushout f g} (c : code x y) :
+--     trunc 0 (pushout_of_sum x = y) :=
+--   begin
+--     induction y using quotient.rec with y,
+--     { exact decode_point c},
+--     { induction H with y, apply arrow_pathover_left, intro c,
+--       revert c, apply @set_quotient.rec_prop, { intro z, apply is_trunc_pathover},
+--       intro l,
+--       refine _ ⬝op ap decode_point !quotient.elim_type_eq_of_rel⁻¹,
+-- -- REPORT THIS!!! esimp fails here, but works after this change
+--   --esimp,
+--       change pathover (λ (a : pushout f g), trunc 0 (eq (pushout_of_sum x) a))
+--       (decode_point (class_of l))
+--       (glue y)
+--       (decode_point (class_of ((pushout_prehom_index.lr (fundamental_groupoid_functor f)
+--         (fundamental_groupoid_functor g) id) :: l))),
+--     esimp, rewrite [▸*, decode_list_cons, ▸*], generalize (decode_list l), clear l,
+--     apply @trunc.rec, { intro z, apply is_trunc_pathover},
+--     intro p, apply trunc_pathover, apply eq_pathover_constant_left_id_right,
+--     apply square_of_eq, exact !idp_con⁻¹}
+--   end
+
+  -- decode-encode is easy
+  protected theorem decode_encode {x : BL + TR} {y : pushout f g}
+    (p : trunc 0 (pushout_of_sum x = y)) : decode (encode p) = p :=
+  begin
+    induction p with p, induction p, reflexivity
+  end
+
+  -- encode-decode is harder
+  definition code_comp [unfold 8] {x y : BL + TR} {z : pushout f g}
+    (c : code x (pushout_of_sum y)) (d : code y z) : code x z :=
+  begin
+    induction z using quotient.rec with z,
+    { exact d ∘ c},
+    { induction H with z,
+      apply arrow_pathover_left, intro d,
+      refine !pathover_tr ⬝op _,
+      refine !elim_type_eq_of_rel ⬝ _ ⬝ ap _ !elim_type_eq_of_rel⁻¹,
+      apply assoc}
+  end
+
+  theorem encode_tcon' {x y : BL + TR} {z : pushout f g}
+    (p : trunc 0 (pushout_of_sum x = pushout_of_sum y))
+    (q : trunc 0 (pushout_of_sum y = z)):
+    encode (tconcat p q) = code_comp (encode p) (encode q) :=
+  begin
+    induction q with q,
+    induction q,
+    refine ap encode !tcon_tidp ⬝ _,
+    symmetry, apply id_left
+  end
+
+  theorem encode_tcon {x y z : BL + TR}
+    (p : trunc 0 (pushout_of_sum x = pushout_of_sum y))
+    (q : trunc 0 (pushout_of_sum y = pushout_of_sum z)):
+    encode (tconcat p q) = encode q ∘ encode p :=
+  encode_tcon' p q
+
+  open category.pushout_hom_rel_index
+
+  theorem encode_decode_singleton {x y : BL + TR} (r : R x y) :
+    encode (decode_reduction_rule r) = class_of [r] :=
+  begin
+    have is_prop (encode (decode_reduction_rule r) = class_of [r]), from !is_trunc_eq,
+    induction r,
+    { induction f_1 with p, induction p, symmetry, apply eq_of_rel,
+      apply tr, apply indexed_list_rel_of_Q, apply idD},
+    { induction g_1 with p, induction p, symmetry, apply eq_of_rel,
+      apply tr, apply indexed_list_rel_of_Q, apply idE},
+    { refine !elim_type_eq_of_rel ⬝ _, apply eq_of_rel, apply tr, rewrite [append_nil]},
+    { refine !elim_type_eq_of_rel_inv' ⬝ _, apply eq_of_rel, apply tr, rewrite [append_nil]}
+  end
+
+  local attribute pushout [reducible]
+  protected theorem encode_decode {x : BL + TR} {y : pushout f g} (c : code x y) :
+    encode (decode c) = c :=
+  begin
+    induction y using quotient.rec_prop with y,
+    revert c, apply @set_quotient.rec_prop, { intro, apply is_trunc_eq}, intro l,
+    change encode (decode_list l) = class_of l,
+    -- do induction on l
+    induction l,
+    { reflexivity},
+    { rewrite [decode_list_cons, encode_tcon, encode_decode_singleton, v_0]}
+  end
+
+  definition pushout_teq_equiv [constructor] (x : BL + TR) (y : pushout f g) :
+    trunc 0 (pushout_of_sum x = y) ≃ code x y :=
+  equiv.MK encode
+           decode
+           encode_decode
+           decode_encode
+
+  definition vankampen [constructor] (x y : BL + TR) :
+    trunc 0 (pushout_of_sum x = pushout_of_sum y) ≃ @hom C _ x y :=
+  pushout_teq_equiv x (pushout_of_sum y)
+
+  definition decode_point_comp [unfold 8] {x₁ x₂ x₃ : BL + TR}
+    (c₂ : @hom C _ x₂ x₃) (c₁ : @hom C _ x₁ x₂) :
+    decode_point (c₂ ∘ c₁) = tconcat (decode_point c₁) (decode_point c₂) :=
+  begin
+    induction c₂ using set_quotient.rec_prop with l₂,
+    induction c₁ using set_quotient.rec_prop with l₁,
+    apply decode_list_append
+  end
+
+  definition vankampen_functor [constructor] : C ⇒ fundamental_groupoid (pushout f g) :=
+  begin
+    fconstructor,
+    { exact pushout_of_sum},
+    { intro x y c, exact decode_point c},
+    { intro x, reflexivity},
+    { intro x y z d c, apply decode_point_comp}
+  end
+
+  definition fully_faithful_vankampen_functor : fully_faithful vankampen_functor :=
+  begin
+    intro x x',
+    fapply adjointify,
+    { apply encode},
+    { intro p, apply decode_encode},
+    { intro c, apply encode_decode}
+  end
+
+  definition essentially_surjective_vankampen_functor : essentially_surjective vankampen_functor :=
+  begin
+    intro z, induction z using quotient.rec_prop with x,
+    apply exists.intro x, reflexivity
+  end
+
+  definition is_weak_equivalence_vankampen_functor [constructor] :
+    is_weak_equivalence vankampen_functor :=
+  begin
+    constructor,
+    { exact fully_faithful_vankampen_functor},
+    { exact essentially_surjective_vankampen_functor}
+  end
+
+  end
+end pushout
--- a/hott/types/eq.hlean
+++ b/hott/types/eq.hlean
@ -494,5 +494,4 @@ namespace eq
    { reflexivity}
  end

-
 end eq
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@ -446,7 +446,45 @@ end is_trunc open is_trunc

 namespace trunc
  universe variable u
-  variable {A : Type.{u}}
+  variables {n : ℕ₋₂} {A : Type.{u}} {B : Type} {a₁ a₂ a₃ a₄ : A}
+
+  definition trunc_functor2 [unfold 6 7] {n : ℕ₋₂} {A B C : Type} (f : A → B → C)
+    (x : trunc n A) (y : trunc n B) : trunc n C :=
+  by induction x with a; induction y with b; exact tr (f a b)
+
+  definition tconcat [unfold 6 7] (p : trunc n (a₁ = a₂)) (q : trunc n (a₂ = a₃)) :
+    trunc n (a₁ = a₃) :=
+  trunc_functor2 concat p q
+
+  definition tinverse [unfold 5] (p : trunc n (a₁ = a₂)) : trunc n (a₂ = a₁) :=
+  trunc_functor _ inverse p
+
+  definition tidp [reducible] [constructor] : trunc n (a₁ = a₁) :=
+  tr idp
+
+  definition tassoc (p : trunc n (a₁ = a₂)) (q : trunc n (a₂ = a₃))
+    (r : trunc n (a₃ = a₄)) : tconcat (tconcat p q) r = tconcat p (tconcat q r) :=
+  by induction p; induction q; induction r; exact ap tr !con.assoc
+
+  definition tidp_tcon (p : trunc n (a₁ = a₂)) : tconcat tidp p = p :=
+  by induction p; exact ap tr !idp_con
+
+  definition tcon_tidp (p : trunc n (a₁ = a₂)) : tconcat p tidp = p :=
+  by induction p; reflexivity
+
+  definition left_tinv (p : trunc n (a₁ = a₂)) : tconcat (tinverse p) p = tidp :=
+  by induction p; exact ap tr !con.left_inv
+
+  definition right_tinv (p : trunc n (a₁ = a₂)) : tconcat p (tinverse p) = tidp :=
+  by induction p; exact ap tr !con.right_inv
+
+  definition tap [unfold 7] (f : A → B) (p : trunc n (a₁ = a₂)) : trunc n (f a₁ = f a₂) :=
+  trunc_functor _ (ap f) p
+
+  definition tap_tidp (f : A → B) : tap f (@tidp n A a₁) = tidp := idp
+  definition tap_tcon (f : A → B) (p : trunc n (a₁ = a₂)) (q : trunc n (a₂ = a₃)) :
+    tap f (tconcat p q) = tconcat (tap f p) (tap f q) :=
+  by induction p; induction q; exact ap tr !ap_con

  /- characterization of equality in truncated types -/
  protected definition code [unfold 3 4] (n : ℕ₋₂) (aa aa' : trunc n.+1 A) : trunctype.{u} n :=
@ -483,22 +521,14 @@ namespace trunc
    : (tr a = tr a' :> trunc n.+1 A) ≃ trunc n (a = a') :=
  !trunc_eq_equiv

-  /- encode preserves concatenation -/
-  definition trunc_functor2 [unfold 6 7] {n : ℕ₋₂} {A B C : Type} (f : A → B → C)
-    (x : trunc n A) (y : trunc n B) : trunc n C :=
-  by induction x with a; induction y with b; exact tr (f a b)
-
-  definition trunc_concat [unfold 6 7] {n : ℕ₋₂} {A : Type} {a₁ a₂ a₃ : A}
-    (p : trunc n (a₁ = a₂)) (q : trunc n (a₂ = a₃)) : trunc n (a₁ = a₃) :=
-  trunc_functor2 concat p q
-
  definition code_mul {n : ℕ₋₂} {aa₁ aa₂ aa₃ : trunc n.+1 A}
    (g : trunc.code n aa₁ aa₂) (h : trunc.code n aa₂ aa₃) : trunc.code n aa₁ aa₃ :=
  begin
    induction aa₁ with a₁, induction aa₂ with a₂, induction aa₃ with a₃,
-    esimp at *, apply trunc_concat g h,
+    esimp at *, apply tconcat g h,
  end

+  /- encode preserves concatenation -/
  definition encode_con' {n : ℕ₋₂} {aa₁ aa₂ aa₃ : trunc n.+1 A} (p : aa₁ = aa₂) (q : aa₂ = aa₃)
    : trunc.encode (p ⬝ q) = code_mul (trunc.encode p) (trunc.encode q) :=
  begin
@ -507,7 +537,7 @@ namespace trunc

  definition encode_con {n : ℕ₋₂} {a₁ a₂ a₃ : A} (p : tr a₁ = tr a₂ :> trunc (n.+1) A)
    (q : tr a₂ = tr a₃ :> trunc (n.+1) A)
-    : trunc.encode (p ⬝ q) = trunc_concat (trunc.encode p) (trunc.encode q) :=
+    : trunc.encode (p ⬝ q) = tconcat (trunc.encode p) (trunc.encode q) :=
  encode_con' p q

  /- the principle of unique choice -/
@ -654,7 +684,7 @@ namespace trunc

  definition loop_ptrunc_pequiv_con {n : ℕ₋₂} {A : Type*} (p q : Ω (ptrunc (n+1) A)) :
    loop_ptrunc_pequiv n A (p ⬝ q) =
-      trunc_concat (loop_ptrunc_pequiv n A p) (loop_ptrunc_pequiv n A q) :=
+      tconcat (loop_ptrunc_pequiv n A p) (loop_ptrunc_pequiv n A q) :=
  encode_con p q

  definition iterated_loop_ptrunc_pequiv (n : ℕ₋₂) (k : ℕ) (A : Type*) :
@ -671,8 +701,8 @@ namespace trunc
  definition iterated_loop_ptrunc_pequiv_con {n : ℕ₋₂} {k : ℕ} {A : Type*}
    (p q : Ω[succ k] (ptrunc (n+succ k) A)) :
    iterated_loop_ptrunc_pequiv n (succ k) A (p ⬝ q) =
-    trunc_concat (iterated_loop_ptrunc_pequiv n (succ k) A p)
-                 (iterated_loop_ptrunc_pequiv n (succ k) A q)  :=
+    tconcat (iterated_loop_ptrunc_pequiv n (succ k) A p)
+            (iterated_loop_ptrunc_pequiv n (succ k) A q)  :=
  begin
    refine _ ⬝ loop_ptrunc_pequiv_con _ _,
    exact ap !loop_ptrunc_pequiv !loop_pequiv_loop_con
@ -680,10 +710,10 @@ namespace trunc

  definition iterated_loop_ptrunc_pequiv_inv_con {n : ℕ₋₂} {k : ℕ} {A : Type*}
    (p q : ptrunc n (Ω[succ k] A)) :
-    (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* (trunc_concat p q) =
+    (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* (tconcat p q) =
    (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* p ⬝
    (iterated_loop_ptrunc_pequiv n (succ k) A)⁻¹ᵉ* q :=
-  equiv.inv_preserve_binary (iterated_loop_ptrunc_pequiv n (succ k) A) concat trunc_concat
+  equiv.inv_preserve_binary (iterated_loop_ptrunc_pequiv n (succ k) A) concat tconcat
    (@iterated_loop_ptrunc_pequiv_con n k A) p q

  definition ptrunc_functor_pcompose [constructor] {X Y Z : Type*} (n : ℕ₋₂) (g : Y →* Z)
@ -730,6 +760,32 @@ namespace trunc

 end trunc open trunc

+/- The truncated encode-decode method -/
+namespace eq
+
+  definition truncated_encode {k : ℕ₋₂} {A : Type} {a₀ a : A} {code : A → Type}
+    [Πa, is_trunc k (code a)] (c₀ : code a₀) (p : trunc k (a₀ = a)) : code a :=
+  begin
+    induction p with p,
+    exact transport code p c₀
+  end
+
+  definition truncated_encode_decode_method {k : ℕ₋₂} {A : Type} (a₀ a : A) (code : A → Type)
+    [Πa, is_trunc k (code a)] (c₀ : code a₀)
+    (decode : Π(a : A) (c : code a), trunc k (a₀ = a))
+    (encode_decode : Π(a : A) (c : code a), truncated_encode c₀ (decode a c) = c)
+    (decode_encode : decode a₀ c₀ = tr idp) : trunc k (a₀ = a) ≃ code a :=
+  begin
+    fapply equiv.MK,
+    { exact truncated_encode c₀},
+    { apply decode},
+    { intro c, apply encode_decode},
+    { intro p, induction p with p, induction p, exact decode_encode},
+  end
+
+end eq
+
+
 /- some consequences for properties about functions (surjectivity etc.) -/
 namespace function
  variables {A B : Type}