feat(vankampen): prove the van Kampen theorem with basepoints

2016-06-23 21:09:18 +01:00 · 2016-06-23 21:09:18 +01:00 · fcf06ae2f5
commit fcf06ae2f5
parent e5ab514263
5 changed files with 222 additions and 44 deletions
--- a/hott/algebra/category/constructions/pushout.hlean
+++ b/hott/algebra/category/constructions/pushout.hlean
@ -117,7 +117,7 @@ end paths
 open paths

 namespace category
-
+section
  /- We use this for the pushout of categories -/
  inductive pushout_prehom_index {C : Type} (D E : Precategory) (F : C → D) (G : C → E) :
    D + E → D + E → Type :=
@ -150,7 +150,7 @@ namespace category
  Precategory_paths (pushout_hom_rel_index D E F G)

  /- We can also take the pushout of groupoids -/
-
+  section
  variables {C : Type} (D E : Groupoid) (F : C → D) (G : C → E)
  variables ⦃x x' x₁ x₂ x₃ x₄ : Precategory_pushout D E F G⦄

@ -201,6 +201,97 @@ namespace category
  definition Groupoid_pushout [constructor] : Groupoid :=
  Groupoid_paths (pushout_hom_rel_index D E F G) (pushout_index_inv D E F G)
    (pushout_index_reverse D E F G) (pushout_index_li D E F G) (pushout_index_ri D E F G)
+  end
+end
+  /- We also define the pushout of two groupoids with a type of basepoints,
+     which are surjectively mapped into C -/

+  inductive bpushout_prehom_index {S : Type} {C D E : Precategory} (k : S → C) (F : C ⇒ D)
+    (G : C ⇒ E) : D + E → D + E → Type :=
+  | iD : Π{d d' : D} (f : d ⟶ d'), bpushout_prehom_index k F G (inl d) (inl d')
+  | iE : Π{e e' : E} (g : e ⟶ e'), bpushout_prehom_index k F G (inr e) (inr e')
+  | DE : Π(s : S), bpushout_prehom_index k F G (inl (F (k s))) (inr (G (k s)))
+  | ED : Π(s : S), bpushout_prehom_index k F G (inr (G (k s))) (inl (F (k s)))

+  open bpushout_prehom_index
+
+  definition bpushout_prehom {S : Type} {C D E : Precategory} (k : S → C) (F : C ⇒ D) (G : C ⇒ E) :
+    D + E → D + E → Type :=
+  paths (bpushout_prehom_index k F G)
+
+  inductive bpushout_hom_rel_index {S : Type} {C D E : Precategory} (k : S → C) (F : C ⇒ D)
+    (G : C ⇒ E) : Π⦃x x' : D + E⦄,
+    bpushout_prehom k F G x x' → bpushout_prehom k F G x x' → Type :=
+  | DD  : Π{d₁ d₂ d₃ : D} (g : d₂ ⟶ d₃) (f : d₁ ⟶ d₂),
+      bpushout_hom_rel_index k F G [iD k F G g, iD k F G f] [iD k F G (g ∘ f)]
+  | EE  : Π{e₁ e₂ e₃ : E} (g : e₂ ⟶ e₃) (f : e₁ ⟶ e₂),
+      bpushout_hom_rel_index k F G [iE k F G g, iE k F G f] [iE k F G (g ∘ f)]
+  | DED : Π(s : S), bpushout_hom_rel_index k F G [ED k F G s, DE k F G s] nil
+  | EDE : Π(s : S), bpushout_hom_rel_index k F G [DE k F G s, ED k F G s] nil
+  | idD : Π(d : D), bpushout_hom_rel_index k F G [iD k F G (ID d)] nil
+  | idE : Π(e : E), bpushout_hom_rel_index k F G [iE k F G (ID e)] nil
+  | cohDE : Π{s₁ s₂ : S} (h : k s₁ ⟶ k s₂),
+        bpushout_hom_rel_index k F G [iE k F G (G h), DE k F G s₁] [DE k F G s₂, iD k F G (F h)]
+  | cohED : Π{s₁ s₂ : S} (h : k s₁ ⟶ k s₂),
+        bpushout_hom_rel_index k F G [ED k F G s₂, iE k F G (G h)] [iD k F G (F h), ED k F G s₁]
+
+  open bpushout_hom_rel_index
+
+  definition Precategory_bpushout [constructor] {S : Type} {C D E : Precategory} (k : S → C)
+    (F : C ⇒ D) (G : C ⇒ E) : Precategory :=
+  Precategory_paths (bpushout_hom_rel_index k F G)
+
+  /- Pushout of groupoids with a type of basepoints -/
+  section
+  variables {S : Type} {C D E : Groupoid} (k : S → C) (F : C ⇒ D) (G : C ⇒ E)
+  variables ⦃x x' x₁ x₂ x₃ x₄ : Precategory_bpushout k F G⦄
+
+  definition bpushout_index_inv [unfold 8] (i : bpushout_prehom_index k F G x x') :
+    bpushout_prehom_index k F G x' x :=
+  begin
+    induction i,
+    { exact iD k F G f⁻¹},
+    { exact iE k F G g⁻¹},
+    { exact ED k F G s},
+    { exact DE k F G s},
+  end
+
+  open paths.paths_rel
+  theorem bpushout_index_reverse {l l' : bpushout_prehom k F G x x'}
+    (q : bpushout_hom_rel_index k F G l l') : paths_rel (bpushout_hom_rel_index k F G)
+      (reverse (bpushout_index_inv k F G) l) (reverse (bpushout_index_inv k F G) l') :=
+  begin
+    induction q: apply paths_rel_of_Q;
+    try rewrite reverse_singleton; rewrite *reverse_pair; try rewrite reverse_nil; esimp;
+    try rewrite [comp_inverse]; try rewrite [id_inverse]; rewrite [-*respect_inv]; constructor
+  end
+
+  theorem bpushout_index_li (i : bpushout_prehom_index k F G x x') :
+    paths_rel (bpushout_hom_rel_index k F G) [bpushout_index_inv k F G i, i] nil :=
+  begin
+    induction i: esimp,
+    { refine rtrans (paths_rel_of_Q !DD) _,
+      rewrite [comp.left_inverse], exact paths_rel_of_Q !idD},
+    { refine rtrans (paths_rel_of_Q !EE) _,
+      rewrite [comp.left_inverse], exact paths_rel_of_Q !idE},
+    { exact paths_rel_of_Q !DED},
+    { exact paths_rel_of_Q !EDE}
+  end
+
+  theorem bpushout_index_ri (i : bpushout_prehom_index k F G x x') :
+    paths_rel (bpushout_hom_rel_index k F G) [i, bpushout_index_inv k F G i] nil :=
+  begin
+    induction i: esimp,
+    { refine rtrans (paths_rel_of_Q !DD) _,
+      rewrite [comp.right_inverse], exact paths_rel_of_Q !idD},
+    { refine rtrans (paths_rel_of_Q !EE) _,
+      rewrite [comp.right_inverse], exact paths_rel_of_Q !idE},
+    { exact paths_rel_of_Q !EDE},
+    { exact paths_rel_of_Q !DED}
+  end
+
+  definition Groupoid_bpushout [constructor] : Groupoid :=
+  Groupoid_paths (bpushout_hom_rel_index k F G) (bpushout_index_inv k F G)
+    (bpushout_index_reverse k F G) (bpushout_index_li k F G) (bpushout_index_ri k F G)
+  end
 end category
--- a/hott/book.md
+++ b/hott/book.md
@ -22,7 +22,7 @@ The rows indicate the chapters, the columns the sections.
 | Ch 5  | - | . | ½ | - | - | . | . | ½ |   |    |    |    |    |    |    |
 | Ch 6  | . | + | + | + | + | + | + | + | ¾ | ¼  | ¾  | +  | .  |    |    |
 | Ch 7  | + | + | + | - | ¾ | - | - |   |   |    |    |    |    |    |    |
-| Ch 8  | + | + | + | + | + | ¾ | ½ | + | + | ¼  |    |    |    |    |    |
+| Ch 8  | + | + | + | + | + | ¾ | + | + | + | ¼  |    |    |    |    |    |
 | Ch 9  | ¾ | + | + | ½ | ¾ | ½ | - | - | - |    |    |    |    |    |    |
 | Ch 10 | ¼ | - | - | - | - |   |   |   |   |    |    |    |    |    |    |
 | Ch 11 | - | - | - | - | - | - |   |   |   |    |    |    |    |    |    |
@ -151,7 +151,7 @@ Every file is in the folder [homotopy](homotopy/homotopy.md)
 - 8.4 (Fiber sequences and the long exact sequence): Mostly in [homotopy.chain_complex](homotopy/chain_complex.hlean), [homotopy.LES_of_homotopy_groups](homotopy/LES_of_homotopy_groups.hlean). Definitions 8.4.1 and 8.4.2 in [types.pointed](types/pointed.hlean), Corollary 8.4.8 in [homotopy.homotopy_group](homotopy/homotopy_group.hlean).
 - 8.5 (The Hopf fibration): [hit.pushout](hit/pushout.hlean) (Lemma 8.5.3), [hopf](homotopy/hopf.hlean) (The Hopf construction, Lemmas 8.5.5 and 8.5.7), [susp](homotopy/susp.hlean) (Definition 8.5.6), [circle](homotopy/circle.hlean) (multiplication on the circle, Lemma 8.5.8), [join](homotopy/join.hlean) (join is associative, Lemma 8.5.9), [complex_hopf](homotopy/complex_hopf.hlean) (the H-space structure on the circle and the complex Hopf fibration, i.e. Theorem 8.5.1), [sphere2](homotopy/sphere2.hlean) (Corollary 8.5.2)
 - 8.6 (The Freudenthal suspension theorem): [connectedness](homotopy/connectedness.hlean) (Lemma 8.6.1), [wedge](homotopy/wedge.hlean) (Wedge connectivity, Lemma 8.6.2). Corollary 8.6.14 is proven directly in [freudenthal](homotopy/freudenthal.hlean), however, we don't prove Theorem 8.6.4. Stability of iterated suspensions is also in [freudenthal](homotopy/freudenthal.hlean). The homotopy groups of spheres in this section are computed in [sphere2](homotopy/sphere2.hlean).
- 8.7 (The van Kampen theorem): Naive van Kampen is proven in [vankampen](homotopy/vankampen.hlean) (the pushout of Groupoids is formalized in [algebra.category.constructions.pushout](algebra/category/constructions/pushout.hlean)
+- 8.7 (The van Kampen theorem): [vankampen](homotopy/vankampen.hlean) (the pushout of Groupoids is formalized in [algebra.category.constructions.pushout](algebra/category/constructions/pushout.hlean) with some definitions in [algebra.graph](algebra/graph.hlean))
 - 8.8 (Whitehead’s theorem and Whitehead’s principle): 8.8.1 and 8.8.2 at the bottom of [types.trunc](types/trunc.hlean), 8.8.3 in [homotopy_group](homotopy/homotopy_group.hlean). [Rest to be moved]
 - 8.9 (A general statement of the encode-decode method): [types.eq](types/eq.hlean).
 - 8.10 (Additional Results): Theorem 8.10.3 is formalized in [homotopy.EM](homotopy/EM.hlean).
--- a/hott/hit/prop_trunc.hlean
+++ b/hott/hit/prop_trunc.hlean
@ -32,17 +32,6 @@ open eq is_trunc unit quotient seq_colim pi nat equiv sum algebra is_conn functi
  See the comment below for a sketch of the proof that (trunc A) is actually a mere proposition.
 -/

-
-/-
-  Call a function f weakly constant if (Πa a', f a = f a')
-  This theorem states that if f is weakly constant, then (ap f) is weakly constant.
-/
-  -- definition weakly_constant_ap {A B : Type} {f : A → B} {a a' : A} (p q : a = a')
-  --   (H : Π(a a' : A), f a = f a') : ap f p = ap f q :=
-  -- have L : Π{b c : A} {r : b = c}, (H a b)⁻¹ ⬝ H a c = ap f r, from
-  --   (λb c r, eq.rec_on r !con.left_inv),
-  -- L⁻¹ ⬝ L
-
 /- definition of "one step truncation" in terms of quotients -/

 namespace one_step_tr
@ -416,7 +405,7 @@ namespace prop_trunc

 end prop_trunc

-open prop_trunc
+open prop_trunc trunc
 -- Corollaries for the actual truncation.
 namespace is_trunc
  local attribute is_prop_trunc_one_step_tr [instance]
@ -431,8 +420,8 @@ namespace is_trunc
    { exact p a a'}
  end

-  example {A : Type} {P : Type} [is_set P] (f : A → P) (p : Πa a', f a = f a') (a : A) :
-    is_prop.elim_set f p (trunc.tr a) = f a :=
+  definition is_prop.elim_set_tr {A : Type} {P : Type} {H : is_set P} (f : A → P)
+    (p : Πa a', f a = f a') (a : A) : is_prop.elim_set f p (tr a) = f a :=
  by reflexivity

 end is_trunc
--- a/hott/homotopy/homotopy.md
+++ b/hott/homotopy/homotopy.md
@ -23,9 +23,11 @@ folder (sorted such that files only import previous files).
 * [quaternionic_hopf](quaternionic_hopf.hlean) (the quaternionic Hopf fibration)
 * [chain_complex](chain_complex.hlean)
 * [LES_of_homotopy_groups](LES_of_homotopy_groups.hlean)
+* [vankampen](vankampen.hlean) (the Seifert-van Kampen theorem)
 * [homotopy_group](homotopy_group.hlean) (theorems about homotopy groups. The definition and basic facts about homotopy groups is in [algebra/homotopy_group](../algebra/homotopy_group.hlean))
 * [sphere2](sphere2.hlean) (calculation of the homotopy group of spheres)

+
 The following files depend on
 [hit.two_quotient](../hit/two_quotient.hlean) which on turn depends on
 [circle](circle.hlean).
--- a/hott/homotopy/vankampen.hlean
+++ b/hott/homotopy/vankampen.hlean
@ -4,33 +4,110 @@ 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
+import hit.pushout hit.prop_trunc algebra.category.constructions.pushout
+       algebra.category.constructions.fundamental_groupoid algebra.category.functor.equivalence

 open eq pushout category functor sum iso paths set_quotient is_trunc trunc pi quotient
-     is_equiv
+     is_equiv fiber 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)
-
+  parameters {S TL : Type.{u}} -- do we want to put these in different universe levels?
+             {BL : Type.{v}} {TR : Type.{w}} (k : S → TL) (f : TL → BL) (g : TL → TR)
+             [ksurj : is_surjective k]
+  include ksurj
  definition pushout_of_sum [unfold 6] (x : BL + TR) : pushout f g :=
  quotient.class_of _ x

-  local notation `C` := Groupoid_pushout      (fundamental_groupoid BL) (fundamental_groupoid TR) f g
-  local notation `R` := pushout_prehom_index  (fundamental_groupoid BL) (fundamental_groupoid TR) f g
-  local notation `Q` := pushout_hom_rel_index (fundamental_groupoid BL) (fundamental_groupoid TR) f g
+  local notation `F` := fundamental_groupoid_functor f
+  local notation `G` := fundamental_groupoid_functor g
+  local notation `C` := Groupoid_bpushout k F G
+  local notation `R` := bpushout_prehom_index k F G
+  local notation `Q` := bpushout_hom_rel_index k F G
+  local attribute is_trunc_equiv [instance]

-  protected definition code [unfold 7] (x : BL + TR) (y : pushout f g) : Type.{max u v w} :=
+  open category.bpushout_prehom_index category.bpushout_hom_rel_index paths.paths_rel
+  protected definition code_equiv_pt (x : BL + TR) {y : TL} {s : S} (p : k s = y) :
+    @hom C _ x (sum.inl (f y)) ≃ @hom C _ x (sum.inr (g y)) :=
+  begin
+    fapply equiv_postcompose,
+    { apply class_of,
+      refine [iE k F G (tap g (tr p)), DE k F G s, iD k F G (tap f (tr p⁻¹))]},
+    refine all_iso _
+  end
+
+  protected definition code_equiv_pt_constant (x : BL + TR) {y : TL} {s s' : S}
+    (p : k s = y) (p' : k s' = y) : code_equiv_pt x p = code_equiv_pt x p' :=
+  begin
+    apply equiv_eq, intro g,
+    apply ap (λx, x ∘ _),
+    induction p',
+    refine eq_of_rel (tr _) ⬝ (eq_of_rel (tr _))⁻¹,
+    { exact [DE k _ _ s']},
+    { refine rtrans (rel [_] (cohDE F G (tr p))) _,
+      refine rtrans (rcons _ (rel [] !DD)) _,
+      refine tr_rev (λx, paths_rel _ [_ , iD k F G (tr x)] _)
+                    (!ap_con⁻¹ ⬝ ap02 f !con.left_inv) _,
+      exact rcons _ (rel [] !idD)},
+    refine rtrans (rel _ !idE) _,
+    exact rcons _ (rel [] !idD)
+  end
+
+  protected definition code_equiv (x : BL + TR) (y : TL) :
+    @hom C _ x (sum.inl (f y)) ≃ @hom C _ x (sum.inr (g y)) :=
+  begin
+    refine @is_prop.elim_set _ _ _ _ _ (ksurj y), { apply @is_trunc_equiv: apply is_set_hom},
+    { intro v, cases v with s p,
+      exact code_equiv_pt x p},
+    intro v v', cases v with s p, cases v' with s' p',
+    exact code_equiv_pt_constant x p p'
+  end
+
+  theorem code_equiv_eq (x : BL + TR) (s : S) :
+    code_equiv x (k s) = @(equiv_postcompose (class_of [DE k F G s])) !all_iso :=
+  begin
+    apply equiv_eq, intro h,
+--    induction h using set_quotient.rec_prop with l,
+    refine @set_quotient.rec_prop _ _ _ _ _ h, {intro l, apply is_trunc_eq, apply is_set_hom},
+    intro l,
+    have ksurj (k s) = tr (fiber.mk s idp), from !is_prop.elim,
+    refine ap (λz, to_fun (@is_prop.elim_set _ _ _ _ _ z) (class_of l)) this ⬝ _,
+    change class_of ([iE k F G (tr idp), DE k F G s, iD k F G (tr idp)] ++ l) =
+           class_of (DE k F G s :: l) :> @hom C _ _ _,
+    refine eq_of_rel (tr _) ⬝ (eq_of_rel (tr _)),
+    { exact DE k F G s :: iD k F G (tr idp) :: l},
+    { change paths_rel Q ([iE k F G (tr idp)] ++ (DE k F G s :: iD k F G (tr idp) :: l))
+                         (nil ++ (DE k F G s :: iD k F G (tr idp) :: l)),
+      apply rel ([DE k F G s, iD k F G (tr idp)] ++ l),
+      apply idE},
+    { apply rcons, rewrite [-nil_append l at {2}, -singleton_append], apply rel l, apply idD}
+  end
+
+  theorem to_fun_code_equiv (x : BL + TR) (s : S) (h : @hom C _ x (sum.inl (f (k s)))) :
+    (to_fun (code_equiv x (k s)) h) = @comp C _ _ _ _ (class_of [DE k F G s]) h :=
+  ap010 to_fun !code_equiv_eq h
+
+  protected definition code [unfold 10] (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 _}}
+    clear y, intro y z r, induction r with y,
+    exact code_equiv x y
  end

+/-
+[iE (ap g p), DE s, iD (ap f p⁻¹)]
+-->
+[DE s', iD (ap f p), iD (ap f p⁻¹)]
+-->
+[DE s', iD (ap f p ∘ ap f p⁻¹)]
+-->
+[DE s']
+<--
+[iE 1, DE s', iD 1]
+-/
+
  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,
@ -46,14 +123,14 @@ namespace pushout
  end

  -- decode is harder
-  definition decode_reduction_rule [unfold 8] ⦃x x' : BL + TR⦄ (i : R x x') :
+  definition decode_reduction_rule [unfold 11] ⦃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)⁻¹},
+    { exact tr (glue (k s))},
+    { exact tr (glue (k s))⁻¹},
  end

  definition decode_list ⦃x x' : BL + TR⦄ (l : paths R x x') :
@ -92,10 +169,14 @@ namespace pushout
    { 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}
+    { apply decode_list_singleton},
+    { rewrite [+decode_list_pair], induction h with p, apply ap tr, rewrite [-+ap_compose'],
+      exact !ap_con_eq_con_ap⁻¹},
+    { rewrite [+decode_list_pair], induction h with p, apply ap tr, rewrite [-+ap_compose'],
+      apply ap_con_eq_con_ap}
  end

-  definition decode_point [unfold 8] {x x' : BL + TR} (c : @hom C _ x x') :
+  definition decode_point [unfold 11] {x x' : BL + TR} (c : @hom C _ x x') :
    trunc 0 (pushout_of_sum x = pushout_of_sum x') :=
  begin
    induction c with l,
@ -123,7 +204,19 @@ namespace pushout
      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}
+      change pathover (λ a, trunc 0 (eq (pushout_of_sum x) a))
+    (decode_list l)
+    (eq_of_rel (pushout_rel f g) (pushout_rel.Rmk f g y))
+    (decode_point
+       (code_equiv x y (class_of l))),
+      note z := ksurj y, revert z,
+      apply @image.rec, { intro, apply is_trunc_pathover},
+      intro s p, induction p, rewrite to_fun_code_equiv,
+      refine _ ⬝op (decode_list_cons (DE k F G s) l)⁻¹,
+      esimp, generalize decode_list l,
+      apply @trunc.rec, { intro p, apply is_trunc_pathover},
+      intro p, apply trunc_pathover, apply eq_pathover_constant_left_id_right,
+      apply square_of_eq, exact !idp_con⁻¹}
  end

  -- report the failing of esimp in the commented-out proof below
@ -141,8 +234,7 @@ namespace pushout
 --       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))),
+--       (decode_point (class_of ((pushout_prehom_index.lr F 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,
@ -156,6 +248,10 @@ namespace pushout
    induction p with p, induction p, reflexivity
  end

+  definition is_surjective.rec {A B : Type} {f : A → B} (Hf : is_surjective f)
+    {P : B → Type} [Πb, is_prop (P b)] (H : Πa, P (f a)) (b : B) : P b :=
+  by induction Hf b; exact p ▸ H a
+
  -- 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 :=
@ -166,7 +262,9 @@ namespace pushout
      apply arrow_pathover_left, intro d,
      refine !pathover_tr ⬝op _,
      refine !elim_type_eq_of_rel ⬝ _ ⬝ ap _ !elim_type_eq_of_rel⁻¹,
-      apply assoc}
+      note q := ksurj z, revert q, apply @image.rec, { intro, apply is_trunc_eq, apply is_set_code},
+      intro s p, induction p,
+      refine !to_fun_code_equiv ⬝ _ ⬝ ap (λh, h ∘ c) !to_fun_code_equiv⁻¹, apply assoc}
  end

  theorem encode_tcon' {x y : BL + TR} {z : pushout f g}
@ -186,8 +284,7 @@ namespace pushout
    encode (tconcat p q) = encode q ∘ encode p :=
  encode_tcon' p q

-  open category.pushout_hom_rel_index
-
+  open category.bpushout_hom_rel_index
  theorem encode_decode_singleton {x y : BL + TR} (r : R x y) :
    encode (decode_reduction_rule r) = class_of [r] :=
  begin
@ -197,8 +294,8 @@ namespace pushout
      apply tr, apply paths_rel_of_Q, apply idD},
    { induction g_1 with p, induction p, symmetry, apply eq_of_rel,
      apply tr, apply paths_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]}
+    { refine !elim_type_eq_of_rel ⬝ _, apply to_fun_code_equiv},
+    { refine !elim_type_eq_of_rel_inv' ⬝ _, apply ap010 to_inv !code_equiv_eq}
  end

  local attribute pushout [reducible]
@ -208,7 +305,6 @@ namespace pushout
    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]}