diff --git a/hott/algebra/e_closure.hlean b/hott/algebra/e_closure.hlean
index 0d5993b64..c1ad224f3 100644
--- a/hott/algebra/e_closure.hlean
+++ b/hott/algebra/e_closure.hlean
@@ -8,7 +8,7 @@ A more appropriate intuition is the type of words formed from the relation,
   and inverses, concatenations and reflexivity
 -/
 
-import .relation eq2 arity
+import algebra.relation eq2 arity cubical.pathover2
 
 open eq equiv
 
@@ -24,7 +24,7 @@ namespace e_closure
   notation `[`:max a `]`:0 := e_closure.of_rel a
   abbreviation rfl {A : Type} {R : A → A → Type} {a : A} := of_path R (idpath a)
 end e_closure
-
+open e_closure
 namespace relation
 
 section
@@ -57,11 +57,37 @@ section
       exact ap_con g (e_closure.elim e r) (e_closure.elim e r') ⬝ (IH₁ ◾ IH₂)
   end
 
+/-  definition ap_e_closure_elim_h_inv [unfold_full] {B C : Type} {f : A → B} {g : B → C}
+    (e : Π⦃a a' : A⦄, R a a' → f a = f a')
+    {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')}
+    (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a')
+    : ap_e_closure_elim_h e p t⁻¹ʳ = ap_inv g (e_closure.elim e t) ⬝ (ap_e_closure_elim_h e p t)⁻² :=
+  by reflexivity
+
+  definition ap_e_closure_elim_h_con [unfold_full] {B C : Type} {f : A → B} {g : B → C}
+    (e : Π⦃a a' : A⦄, R a a' → f a = f a')
+    {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')}
+    (p : Π⦃a a' : A⦄ (s : R a a'), ap g (e s) = e' s) (t : T a a') (t' : T a' a'')
+    : ap_e_closure_elim_h e p (t ⬝r t') = ap_con g (e_closure.elim e t) (e_closure.elim e t') ⬝
+        (ap_e_closure_elim_h e p t ◾ ap_e_closure_elim_h e p t') :=
+  by reflexivity-/
+
   definition ap_e_closure_elim [unfold 10] {B C : Type} {f : A → B} (g : B → C)
- (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a')
+    (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a')
     : ap g (e_closure.elim e t) = e_closure.elim (λa a' r, ap g (e r)) t :=
   ap_e_closure_elim_h e (λa a' s, idp) t
 
+  definition ap_e_closure_elim_inv [unfold_full] {B C : Type} {f : A → B} (g : B → C)
+    (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a')
+    : ap_e_closure_elim g e t⁻¹ʳ = ap_inv g (e_closure.elim e t) ⬝ (ap_e_closure_elim g e t)⁻² :=
+  by reflexivity
+
+  definition ap_e_closure_elim_con [unfold_full] {B C : Type} {f : A → B} (g : B → C)
+    (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') (t' : T a' a'')
+    : ap_e_closure_elim g e (t ⬝r t') = ap_con g (e_closure.elim e t) (e_closure.elim e t') ⬝
+      (ap_e_closure_elim g e t ◾ ap_e_closure_elim g e t') :=
+  by reflexivity
+
   definition ap_e_closure_elim_h_eq {B C : Type} {f : A → B} {g : B → C}
     (e : Π⦃a a' : A⦄, R a a' → f a = f a')
     {e' : Π⦃a a' : A⦄, R a a' → g (f a) = g (f a')}
@@ -107,7 +133,6 @@ section
              (ap_e_closure_elim h (λa a' r, ap g (e r)) t) :=
   !ap_ap_e_closure_elim_h
 
-  open e_closure
   definition is_equivalence_e_closure : is_equivalence T :=
   begin
     constructor,
@@ -131,13 +156,12 @@ section
     : e_closure.elim e (p ▸ t) = (ap f p)⁻¹ ⬝ e_closure.elim e t ⬝ (ap f p) :=
   by induction p; esimp; exact !idp_con⁻¹
 
-  --dependent elimination:
+  /- dependent elimination -/
 
   variables {P : B → Type} {Q : C → Type} {f : A → B} {g : B → C} {f' : Π(a : A), P (f a)}
-  protected definition e_closure.elimo [unfold 11]
-    (p : Π⦃a a' : A⦄, R a a' → f a = f a')
-    (po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a')
-    (t : T a a') : f' a =[e_closure.elim p t] f' a' :=
+  protected definition e_closure.elimo [unfold 11] (p : Π⦃a a' : A⦄, R a a' → f a = f a')
+    (po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a') (t : T a a')
+    : f' a =[e_closure.elim p t] f' a' :=
   begin
     induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂,
       exact po r,
@@ -146,6 +170,16 @@ section
       exact IH₁ ⬝o IH₂
   end
 
+  definition elimo_inv [unfold_full] (p : Π⦃a a' : A⦄, R a a' → f a = f a')
+    (po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a') (t : T a a')
+    : e_closure.elimo p po t⁻¹ʳ = (e_closure.elimo p po t)⁻¹ᵒ :=
+  by reflexivity
+
+  definition elimo_con [unfold_full] (p : Π⦃a a' : A⦄, R a a' → f a = f a')
+    (po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a') (t : T a a') (t' : T a' a'')
+    : e_closure.elimo p po (t ⬝r t') = e_closure.elimo p po t ⬝o e_closure.elimo p po t' :=
+  by reflexivity
+
   definition ap_e_closure_elimo_h [unfold 12]  {g' : Πb, Q (g b)}
     (p : Π⦃a a' : A⦄, R a a' → f a = f a')
     (po : Π⦃a a' : A⦄ (s : R a a'), g' (f a) =[p s] g' (f a'))
@@ -160,29 +194,21 @@ section
       exact apdo_con g' (e_closure.elim p r) (e_closure.elim p r') ⬝ (IH₁ ◾o IH₂)
   end
 
-/-
-  definition e_closure_elimo_ap {g' : Π(a : A), Q (g (f a))}
+  theorem e_closure_elimo_ap {g' : Π(a : A), Q (g (f a))}
     (p : Π⦃a a' : A⦄, R a a' → f a = f a')
     (po : Π⦃a a' : A⦄ (s : R a a'), g' a =[ap g (p s)] g' a')
-    (t : T a a') : e_closure.elimo (λa a' r, ap g (p r)) po t =
-    change_path (ap_e_closure_elim g p t)
-      (pathover_ap Q g (e_closure.elimo p (λa a' s, pathover_of_pathover_ap Q g (po s)) t)) :=
+    (t : T a a') : e_closure.elimo p (λa a' s, pathover_of_pathover_ap Q g (po s)) t =
+      pathover_of_pathover_ap Q g (change_path (ap_e_closure_elim g p t)⁻¹
+        (e_closure.elimo (λa a' r, ap g (p r)) po t)) :=
   begin
     induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂,
-    { esimp, exact (to_right_inv !pathover_compose (po r))⁻¹},
-    { induction pp, reflexivity},
-    { exact sorry},
-    { exact sorry},
+    { reflexivity},
+    { induction pp; reflexivity},
+    { rewrite [+elimo_inv, ap_e_closure_elim_inv, IH, con_inv, change_path_con, ▸*, -inv2_inv,
+               change_path_invo, pathover_of_pathover_ap_invo]},
+    { rewrite [+elimo_con, ap_e_closure_elim_con, IH₁, IH₂, con_inv, change_path_con, ▸*, con2_inv,
+               change_path_cono, pathover_of_pathover_ap_cono]},
   end
 
-  definition e_closure_elimo_ap' {g' : Π(a : A), Q (g (f a))}
-    (p : Π⦃a a' : A⦄, R a a' → f a = f a')
-    (po : Π⦃a a' : A⦄ (s : R a a'), g' a =[ap g (p s)] g' a')
-    (t : T a a') :
-      pathover_of_pathover_ap Q g (change_path (ap_e_closure_elim g p t)⁻¹ (e_closure.elimo (λa a' r, ap g (p r)) po t)) =
-      e_closure.elimo p (λa a' s, pathover_of_pathover_ap Q g (po s)) t :=
-  sorry
--/
-
 end
 end relation
diff --git a/hott/cubical/cubical.md b/hott/cubical/cubical.md
index 4008f1ff0..62fce5fa5 100644
--- a/hott/cubical/cubical.md
+++ b/hott/cubical/cubical.md
@@ -8,4 +8,8 @@ The files [path](../init/path.hlean) and [pathover](../init/pathover.hlean) are
 * [square](square.hlean): square in a type
 * [cube](cube.hlean): cube in a type
 * [squareover](squareover.hlean): square over a square
-* [cubeover](cubeover.hlean): cube over a cube
\ No newline at end of file
+* [cubeover](cubeover.hlean): cube over a cube
+
+The following files are higher coherence laws between operators defined in the basic files
+* [pathover2](pathover2.hlean)
+* [square2](square2.hlean)
diff --git a/hott/cubical/pathover2.hlean b/hott/cubical/pathover2.hlean
index 71371e311..addbf9ace 100644
--- a/hott/cubical/pathover2.hlean
+++ b/hott/cubical/pathover2.hlean
@@ -6,12 +6,15 @@ Author: Floris van Doorn
 Coherence conditions for operations on pathovers
 -/
 
-open function
+open function equiv
 
 namespace eq
 
-  variables {A A' A'' : Type} {a a' a₂ : A} (B : A → Type) {p : a = a₂}
-    {b b' : B a} {b₂ : B a₂}
+  variables {A A' A'' : Type} {B B' : A → Type} {B'' : A' → Type} {C : Π⦃a⦄, B a → Type}
+            {a a₂ a₃ a₄ : A} {p p' p'' : a = a₂} {p₂ p₂' : a₂ = a₃} {p₃ : a₃ = a₄} {p₁₃ : a = a₃}
+            {a' : A'}
+            {b b' : B a} {b₂ b₂' : B a₂} {b₃ : B a₃} {b₄ : B a₄}
+            {c : C b} {c₂ : C b₂}
 
   definition pathover_ap_id (q : b =[p] b₂) : pathover_ap B id q = change_path (ap_id p)⁻¹ q :=
   by induction q; reflexivity
@@ -27,10 +30,6 @@ namespace eq
       = change_path (ap_compose g f p) (pathover_ap B (g ∘ f) q) :=
   by induction q; reflexivity
 
-  definition apdo_eq_apdo_ap {B : A' → Type} (g : Πb, B b) (f : A → A') (p : a = a')
-    : apdo (λx, g (f x)) p = pathover_of_pathover_ap B f (apdo g (ap f p)) :=
-  by induction p; reflexivity
-
   definition pathover_of_tr_eq_idp (r : b = b') : pathover_of_tr_eq r = pathover_idp_of_eq r :=
   idp
 
@@ -42,4 +41,88 @@ namespace eq
       : apo011 f p q = eq_of_pathover (apo11 (apdo f p) q) :=
   by induction q; reflexivity
 
+  definition change_path_con (q : p = p') (q' : p' = p'') (r : b =[p] b₂) :
+    change_path (q ⬝ q') r = change_path q' (change_path q r) :=
+  by induction q; induction q'; reflexivity
+
+  definition change_path_invo (q : p = p') (r : b =[p] b₂) :
+    change_path (inverse2 q) r⁻¹ᵒ = (change_path q r)⁻¹ᵒ :=
+  by induction q; reflexivity
+
+  definition change_path_cono (q : p = p') (q₂ : p₂ = p₂') (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃):
+    change_path (q ◾ q₂) (r ⬝o r₂) = change_path q r ⬝o change_path q₂ r₂ :=
+  by induction q; induction q₂; reflexivity
+
+  definition pathover_of_pathover_ap_invo (B' : A' → Type) (f : A → A')
+    {b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[ap f p] b₂) :
+    pathover_of_pathover_ap B' f (change_path (ap_inv f p)⁻¹ q⁻¹ᵒ) =
+      (pathover_of_pathover_ap B' f q)⁻¹ᵒ:=
+  by induction p; eapply idp_rec_on q; reflexivity
+
+  definition pathover_of_pathover_ap_cono (B' : A' → Type) (f : A → A')
+    {b : B' (f a)} {b₂ : B' (f a₂)} {b₃ : B' (f a₃)} (q : b =[ap f p] b₂) (q₂ : b₂ =[ap f p₂] b₃) :
+    pathover_of_pathover_ap B' f (change_path (ap_con f p p₂)⁻¹ (q ⬝o q₂)) =
+      pathover_of_pathover_ap B' f q ⬝o pathover_of_pathover_ap B' f q₂ :=
+  by induction p; induction p₂; eapply idp_rec_on q; eapply idp_rec_on q₂; reflexivity
+
+  definition pathover_ap_pathover_of_pathover_ap (P : A'' → Type) (g : A' → A'') (f : A → A')
+    {p : a = a₂} {b : P (g (f a))} {b₂ : P (g (f a₂))} (q : b =[ap f p] b₂) :
+    pathover_ap P (g ∘ f) (pathover_of_pathover_ap (P ∘ g) f q) =
+    change_path (ap_compose g f p)⁻¹ (pathover_ap P g q) :=
+  by induction p; eapply (idp_rec_on q); reflexivity
+
+  definition change_path_pathover_of_pathover_ap (B' : A' → Type) (f : A → A') {p p' : a = a₂}
+    (r : p = p') {b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[ap f p] b₂) :
+    change_path r (pathover_of_pathover_ap B' f q) =
+      pathover_of_pathover_ap B' f (change_path (ap02 f r) q) :=
+  by induction r; reflexivity
+
+  definition pathover_ap_change_path (B' : A' → Type) (f : A → A') {p p' : a = a₂}
+    (r : p = p') {b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[p] b₂) :
+    pathover_ap B' f (change_path r q) = change_path (ap02 f r) (pathover_ap B' f q) :=
+  by induction r; reflexivity
+
+  definition change_path_equiv [constructor] (b : B a) (b₂ : B a₂) (q : p = p')
+    : (b =[p] b₂) ≃ (b =[p'] b₂) :=
+  begin
+    fapply equiv.MK,
+    { exact change_path q},
+    { exact change_path q⁻¹},
+    { intro r, induction q, reflexivity},
+    { intro r, induction q, reflexivity},
+  end
+
+  definition apdo_ap {B : A' → Type} (g : Πb, B b) (f : A → A') (p : a = a₂)
+    :  apdo g (ap f p) = pathover_ap B f (apdo (λx, g (f x)) p)  :=
+  by induction p; reflexivity
+
+  definition apdo_eq_apdo_ap {B : A' → Type} (g : Πb, B b) (f : A → A') (p : a = a₂)
+    : apdo (λx, g (f x)) p = pathover_of_pathover_ap B f (apdo g (ap f p)) :=
+  by induction p; reflexivity
+
+  definition ap_compose_ap02_constant {A B C : Type} {a a' : A} (p : a = a') (b : B) (c : C) :
+  ap_compose (λc, b) (λa, c) p ⬝ ap02 (λc, b) (ap_constant p c) = ap_constant p b :=
+  by induction p; reflexivity
+
+  theorem apdo_constant (b : B'' a') (p : a = a) :
+    pathover_ap B'' (λa, a') (apdo (λa, b) p) = change_path (ap_constant p a')⁻¹ idpo :=
+  begin
+    rewrite [apdo_eq_apdo_ap _ _ p],
+    let y := !change_path_of_pathover (apdo (apdo id) (ap_constant p b))⁻¹ᵒ,
+    rewrite -y, esimp, clear y,
+    refine !pathover_ap_pathover_of_pathover_ap ⬝ _,
+    rewrite pathover_ap_change_path,
+    rewrite -change_path_con, apply ap (λx, change_path x idpo),
+    unfold ap02, rewrite [ap_inv,-con_inv], apply inverse2,
+    apply ap_compose_ap02_constant
+  end
+
+  definition apdo_change_path {B : A → Type} {a a₂ : A} (f : Πa, B a) {p p' : a = a₂} (s : p = p')
+    : apdo f p' = change_path s (apdo f p) :=
+  by induction s; reflexivity
+
+  definition cono_invo_eq_idpo {q q' : b =[p] b₂} (r : q = q')
+    : change_path (con.right_inv p) (q ⬝o q'⁻¹ᵒ) = idpo :=
+  by induction r; induction q; reflexivity
+
 end eq
diff --git a/hott/cubical/square2.hlean b/hott/cubical/square2.hlean
new file mode 100644
index 000000000..40a0c41b6
--- /dev/null
+++ b/hott/cubical/square2.hlean
@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Floris van Doorn
+
+Coherence conditions for operations on squares
+-/
+
+import .square
+
+namespace eq
+
+  variables {A B C : Type} {a a' a'' a₀₀ a₂₀ a₄₀ a₀₂ a₂₂ a₂₄ a₀₄ a₄₂ a₄₄ a₁ a₂ a₃ a₄ : A}
+            {b : B} {c : C}
+            /-a₀₀-/ {p₁₀ p₁₀' : a₀₀ = a₂₀} /-a₂₀-/ {p₃₀ : a₂₀ = a₄₀} /-a₄₀-/
+       {p₀₁ p₀₁' : a₀₀ = a₀₂} /-s₁₁-/ {p₂₁ p₂₁' : a₂₀ = a₂₂} /-s₃₁-/ {p₄₁ : a₄₀ = a₄₂}
+            /-a₀₂-/ {p₁₂ 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₄₄-/
+
+  theorem whisker_bl_whisker_tl_eq (p : a = a')
+    : whisker_bl p (whisker_tl p ids) = con.right_inv p ⬝ph vrfl :=
+  by induction p; reflexivity
+
+  theorem ap_is_constant_natural_square {g : B → C} {f : A → B} (H : Πa, g (f a) = c) (p : a = a') :
+    (ap_is_constant H p)⁻¹ ⬝ph natural_square_tr H p ⬝hp ap_constant p c =
+      whisker_bl (H a') (whisker_tl (H a) ids) :=
+  begin induction p, esimp, rewrite inv_inv, rewrite whisker_bl_whisker_tl_eq end
+
+  definition inv_ph_eq_of_eq_ph {p : a₀₀ = a₀₂} {r : p₀₁ = p} {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁}
+    {s₁₁' : square p₁₀ p₁₂ p p₂₁} (t : s₁₁ = r ⬝ph s₁₁') : r⁻¹ ⬝ph s₁₁ = s₁₁' :=
+  by induction r; exact t
+
+end eq
diff --git a/hott/cubical/squareover.hlean b/hott/cubical/squareover.hlean
index 83215b4dd..b37c5065c 100644
--- a/hott/cubical/squareover.hlean
+++ b/hott/cubical/squareover.hlean
@@ -262,4 +262,19 @@ namespace eq
     induction p, esimp at s, apply pathover_idp_of_eq, apply eq_of_vdeg_squareover, exact s
   end
 
+  definition squareover_change_path_left {p₀₁' : a₀₀ = a₀₂} (r : p₀₁' = p₀₁)
+    {q₀₁ : b₀₀ =[p₀₁'] b₀₂} (t : squareover B (r ⬝ph s₁₁) q₁₀ q₁₂ q₀₁ q₂₁)
+  : squareover B s₁₁ q₁₀ q₁₂ (change_path r q₀₁) q₂₁ :=
+  by induction r; exact t
+
+  definition squareover_change_path_right {p₂₁' : a₂₀ = a₂₂} (r : p₂₁' = p₂₁)
+    {q₂₁ : b₂₀ =[p₂₁'] b₂₂} (t : squareover B (s₁₁ ⬝hp r⁻¹) q₁₀ q₁₂ q₀₁ q₂₁)
+  : squareover B s₁₁ q₁₀ q₁₂ q₀₁ (change_path r q₂₁) :=
+  by induction r; exact t
+
+  definition squareover_change_path_right' {p₂₁' : a₂₀ = a₂₂} (r : p₂₁ = p₂₁')
+    {q₂₁ : b₂₀ =[p₂₁'] b₂₂} (t : squareover B (s₁₁ ⬝hp r) q₁₀ q₁₂ q₀₁ q₂₁)
+  : squareover B s₁₁ q₁₀ q₁₂ q₀₁ (change_path r⁻¹ q₂₁) :=
+  by induction r; exact t
+
 end eq
diff --git a/hott/eq2.hlean b/hott/eq2.hlean
index 1942e40cc..493ab7d79 100644
--- a/hott/eq2.hlean
+++ b/hott/eq2.hlean
@@ -90,6 +90,10 @@ namespace eq
            (ap_compose g f q) :=
   natural_square (ap_compose g f) r
 
+  theorem whisker_right_eq_of_con_inv_eq_idp {p q : a₁ = a₂} (r : p ⬝ q⁻¹ = idp) :
+    whisker_right (eq_of_con_inv_eq_idp r) q⁻¹ ⬝ con.right_inv q = r :=
+  by induction q; esimp at r; cases r; reflexivity
+
   theorem ap_eq_of_con_inv_eq_idp (f : A → B) {p q : a₁ = a₂} (r : p ⬝ q⁻¹ = idp)
   : ap02 f (eq_of_con_inv_eq_idp r) =
            eq_of_con_inv_eq_idp (whisker_left _ !ap_inv⁻¹ ⬝ !ap_con⁻¹ ⬝ ap02 f r)
@@ -101,12 +105,6 @@ namespace eq
   : eq_of_con_inv_eq_idp (r ◾ inverse2 s ⬝ t) = r ⬝ eq_of_con_inv_eq_idp t ⬝ s⁻¹ :=
   by induction s;induction r;induction q;reflexivity
 
--- definition naturality_apdo {A : Type} {B : A → Type} {a a₂ : A} {f g : Πa, B a}
---   (H : f ~ g) (p : a = a₂)
---   : squareover B vrfl (apdo f p) (apdo g p)
---                       (pathover_idp_of_eq (H a)) (pathover_idp_of_eq (H a₂)) :=
--- by induction p;esimp;exact hrflo
-
   definition naturality_apdo_eq {A : Type} {B : A → Type} {a a₂ : A} {f g : Πa, B a}
     (H : f ~ g) (p : a = a₂)
     : apdo f p = concato_eq (eq_concato (H a) (apdo g p)) (H a₂)⁻¹ :=
diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean
index 7463a5f70..d8fa7d12e 100644
--- a/hott/hit/two_quotient.hlean
+++ b/hott/hit/two_quotient.hlean
@@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 
-import homotopy.circle eq2 algebra.e_closure cubical.cube
+import homotopy.circle eq2 algebra.e_closure cubical.squareover cubical.cube cubical.square2
 
-open quotient eq circle sum sigma equiv function relation
+open quotient eq circle sum sigma equiv function relation e_closure
 
   /-
     This files defines a general class of nonrecursive HITs using just quotients.
@@ -21,7 +21,7 @@ open quotient eq circle sum sigma equiv function relation
     where p, p' are of the form
     - refl (f a), for some a : A;
     - e r, for some r : R a a';
-    - ap f q, where q : a = a';
+    - ap f q, where q : a = a' :> A;
     - inverses of such paths;
     - concatenations of such paths.
 
@@ -92,9 +92,15 @@ namespace simple_two_quotient
     : ap (pre_elim Pj Pa Pe) (et t) = e_closure.elim Pe t :=
   ap_e_closure_elim_h e (elim_e Pj Pa Pe) t
 
+  protected definition rec_et {P : C → Type}
+    (Pj : Πa, P (j a)) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), P (pre_aux q))
+    (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a =[e s] Pj a') ⦃a a' : A⦄ (t : T a a')
+    : apdo (pre_rec Pj Pa Pe) (et t) = e_closure.elimo e Pe t :=
+  ap_e_closure_elimo_h e Pe (rec_e Pj Pa Pe) t
+
   inductive simple_two_quotient_rel : C → C → Type :=
   | Rmk {} : Π{a : A} {r : T a a} (q : Q r) (x : circle),
-               simple_two_quotient_rel (f q x) (pre_aux q)
+      simple_two_quotient_rel (f q x) (pre_aux q)
 
   open simple_two_quotient_rel
   definition simple_two_quotient := quotient simple_two_quotient_rel
@@ -104,6 +110,7 @@ namespace simple_two_quotient
   protected definition aux (q : Q r) : D := i (pre_aux q)
   definition incl1 (s : R a a') : incl0 a = incl0 a' := ap i (e s)
   definition inclt (t : T a a') : incl0 a = incl0 a' := e_closure.elim incl1 t
+
   -- "wrong" version inclt, which is ap i (p ⬝ q) instead of ap i p ⬝ ap i q
   -- it is used in the proof, because incltw is easier to work with
   protected definition incltw (t : T a a') : incl0 a = incl0 a' := ap i (et t)
@@ -125,6 +132,75 @@ namespace simple_two_quotient
 
   local attribute simple_two_quotient f i D incl0 aux incl1 incl2' inclt [reducible]
   local attribute i aux incl0 [constructor]
+
+  protected definition rec {P : D → Type} (P0 : Π(a : A), P (incl0 a))
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
+    (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r),
+      change_path (incl2 q) (e_closure.elimo incl1 P1 r) = idpo) (x : D) : P x :=
+  begin
+    induction x,
+    { refine (pre_rec _ _ _ a),
+      { exact P0},
+      { intro a r q, exact incl2' q base ▸ P0 a},
+      { intro a a' s, exact pathover_of_pathover_ap P i (P1 s)}},
+    { exact abstract [irreducible] begin induction H, induction x,
+      { esimp, exact pathover_tr (incl2' q base) (P0 a)},
+      { apply pathover_pathover,
+        esimp, fold [i, incl2' q],
+        refine eq_hconcato _ _, apply _,
+        { transitivity _,
+          { apply ap (pathover_ap _ _),
+            transitivity _, apply apdo_compose2 (pre_rec P0 _ _) (f q) loop,
+            apply ap (pathover_of_pathover_ap _ _),
+            transitivity _, apply apdo_change_path, exact !elim_loop⁻¹,
+            transitivity _,
+              apply ap (change_path _),
+              transitivity _, apply rec_et,
+              transitivity (pathover_of_pathover_ap P i (change_path (inclt_eq_incltw r)
+                (e_closure.elimo incl1 (λ (a a' : A) (s : R a a'), P1 s) r))),
+              apply e_closure_elimo_ap,
+              exact idp,
+            apply change_path_pathover_of_pathover_ap},
+          esimp, transitivity _, apply pathover_ap_pathover_of_pathover_ap P i (f q),
+          transitivity _, apply ap (change_path _), apply to_right_inv !pathover_compose,
+          do 2 (transitivity _; exact !change_path_con⁻¹),
+          transitivity _, apply ap (change_path _),
+            exact (to_left_inv (change_path_equiv _ _ (incl2 q)) _)⁻¹, esimp,
+          rewrite P2, transitivity _; exact !change_path_con⁻¹, apply ap (λx, change_path x _),
+          rewrite [↑incl2, con_inv], transitivity _, exact !con.assoc⁻¹,
+          rewrite [inv_con_cancel_right, ↑incl2w, ↑ap02, +con_inv, +ap_inv, +inv_inv, -+con.assoc,
+            +con_inv_cancel_right], reflexivity},
+        rewrite [change_path_con, apdo_constant],
+        apply squareover_change_path_left, apply squareover_change_path_right',
+        apply squareover_change_path_left,
+        refine change_square _ vrflo,
+        symmetry, apply inv_ph_eq_of_eq_ph, rewrite [ap_is_constant_natural_square],
+        apply whisker_bl_whisker_tl_eq} end end},
+  end
+
+  protected definition rec_on [reducible] {P : D → Type} (x : D) (P0 : Π(a : A), P (incl0 a))
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
+    (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r),
+      change_path (incl2 q) (e_closure.elimo incl1 P1 r) = idpo) : P x :=
+  rec P0 P1 P2 x
+
+  theorem rec_incl1 {P : D → Type} (P0 : Π(a : A), P (incl0 a))
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
+    (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r),
+      change_path (incl2 q) (e_closure.elimo incl1 P1 r) = idpo) ⦃a a' : A⦄ (s : R a a')
+    : apdo (rec P0 P1 P2) (incl1 s) = P1 s :=
+  begin
+    unfold [rec, incl1], refine !apdo_ap ⬝ _, esimp, rewrite rec_e,
+    apply to_right_inv !pathover_compose
+  end
+
+  theorem rec_inclt {P : D → Type} (P0 : Π(a : A), P (incl0 a))
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
+    (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r),
+      change_path (incl2 q) (e_closure.elimo incl1 P1 r) = idpo) ⦃a a' : A⦄ (t : T a a')
+    : apdo (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t :=
+  ap_e_closure_elimo_h incl1 P1 (rec_incl1 P0 P1 P2) t
+
   protected definition elim {P : Type} (P0 : A → P)
     (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
     (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp)
@@ -142,8 +218,7 @@ namespace simple_two_quotient
               ap _ !elim_loop ⬝
               !elim_et ⬝
               P2 q ⬝
-              !ap_constant⁻¹ end
-} end end},
+              !ap_constant⁻¹ end} end end},
   end
   local attribute elim [unfold 8]
 
@@ -194,7 +269,6 @@ namespace simple_two_quotient
     ⦃a : A⦄ ⦃r : T a a⦄ (q : Q r) : ap (elim P0 P1 P2) (incl2' q base) = idpath (P0 a) :=
   !elim_eq_of_rel
 
-  -- set_option pp.implicit true
   protected theorem elim_incl2w {P : Type} (P0 : A → P)
     (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
     (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), e_closure.elim P1 r = idp)
@@ -257,14 +331,14 @@ namespace simple_two_quotient
 end
 end simple_two_quotient
 
---attribute simple_two_quotient.j [constructor] --TODO
-attribute /-simple_two_quotient.rec-/ simple_two_quotient.elim [unfold 8] [recursor 8]
---attribute simple_two_quotient.elim_type [unfold 9]
-attribute /-simple_two_quotient.rec_on-/ simple_two_quotient.elim_on [unfold 5]
---attribute simple_two_quotient.elim_type_on [unfold 6]
+attribute simple_two_quotient.j [constructor]
+attribute simple_two_quotient.rec simple_two_quotient.elim [unfold 8] [recursor 8]
+--attribute simple_two_quotient.elim_type [unfold 9] -- TODO
+attribute simple_two_quotient.rec_on simple_two_quotient.elim_on [unfold 5]
+--attribute simple_two_quotient.elim_type_on [unfold 6] -- TODO
 
 namespace two_quotient
-  open e_closure simple_two_quotient
+  open simple_two_quotient
   section
   parameters {A : Type}
              (R : A → A → Type)
@@ -272,7 +346,6 @@ namespace two_quotient
   parameter  (Q : Π⦃a a'⦄, T a a' → T a a' → Type)
   variables ⦃a a' : A⦄ {s : R a a'} {t t' : T a a'}
 
-
   inductive two_quotient_Q : Π⦃a : A⦄, e_closure R a a → Type :=
   | Qmk : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄, Q t t' → two_quotient_Q (t ⬝r t'⁻¹ʳ)
   open two_quotient_Q
@@ -285,6 +358,46 @@ namespace two_quotient
   definition incl2 (q : Q t t') : inclt t = inclt t' :=
   eq_of_con_inv_eq_idp (incl2 _ _ (Qmk R q))
 
+  protected definition rec {P : two_quotient → Type} (P0 : Π(a : A), P (incl0 a))
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
+      change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t')
+    (x : two_quotient) : P x :=
+  begin
+    induction x,
+    { exact P0 a},
+    { exact P1 s},
+    { induction q with a a' t t' q,
+      rewrite [elimo_con (simple_two_quotient.incl1 R Q2) P1,
+               elimo_inv (simple_two_quotient.incl1 R Q2) P1,
+               -whisker_right_eq_of_con_inv_eq_idp (simple_two_quotient.incl2 R Q2 (Qmk R q)),
+               change_path_con],
+      xrewrite [change_path_cono],
+      refine ap (λx, change_path _ (_ ⬝o x)) !change_path_invo ⬝ _, esimp,
+      apply cono_invo_eq_idpo, apply P2}
+  end
+
+  protected definition rec_on [reducible] {P : two_quotient → Type} (x : two_quotient)
+    (P0 : Π(a : A), P (incl0 a))
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
+      change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t') : P x :=
+  rec P0 P1 P2 x
+
+  theorem rec_incl1 {P : two_quotient → Type} (P0 : Π(a : A), P (incl0 a))
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
+      change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t')
+    ⦃a a' : A⦄ (s : R a a') : apdo (rec P0 P1 P2) (incl1 s) = P1 s :=
+  rec_incl1 _ _ _ _ _ s
+
+  theorem rec_inclt {P : two_quotient → Type} (P0 : Π(a : A), P (incl0 a))
+    (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
+    (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
+      change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t')
+    ⦃a a' : A⦄ (t : T a a') : apdo (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t :=
+  rec_inclt _ _ _ _ _ t
+
   protected definition elim {P : Type} (P0 : A → P)
     (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
     (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
@@ -294,7 +407,7 @@ namespace two_quotient
     { exact P0 a},
     { exact P1 s},
     { exact abstract [unfold 10] begin induction q with a a' t t' q,
-      rewrite [↑e_closure.elim],
+      esimp [e_closure.elim],
       apply con_inv_eq_idp, exact P2 q end end},
   end
   local attribute elim [unfold 8]
@@ -315,7 +428,7 @@ namespace two_quotient
     {P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a'}
     (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'), e_closure.elim P1 t = e_closure.elim P1 t')
     ⦃a a' : A⦄ (t : T a a') : ap (elim P0 P1 P2) (inclt t) = e_closure.elim P1 t :=
-  !elim_inclt --ap_e_closure_elim_h incl1 (elim_incl1 P2) t
+  !elim_inclt
 
   theorem elim_incl2 {P : Type} (P0 : A → P)
     (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a = P0 a')
@@ -325,7 +438,6 @@ namespace two_quotient
   begin
     rewrite [↑[incl2,elim],ap_eq_of_con_inv_eq_idp],
     xrewrite [eq_top_of_square (elim_incl2 R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2) (Qmk R q))],
---    esimp, --doesn't fold elim_inclt back. The following tactic is just a "custom esimp"
     xrewrite [{simple_two_quotient.elim_inclt R Q2 (elim_1 A R Q P P0 P1 P2)
            (t ⬝r t'⁻¹ʳ)}
       idpath (ap_con (simple_two_quotient.elim R Q2 P0 P1 (elim_1 A R Q P P0 P1 P2))
@@ -344,8 +456,8 @@ namespace two_quotient
 end
 end two_quotient
 
---attribute two_quotient.j [constructor] --TODO
-attribute /-two_quotient.rec-/ two_quotient.elim [unfold 8] [recursor 8]
+attribute two_quotient.incl0 [constructor]
+attribute two_quotient.rec two_quotient.elim [unfold 8] [recursor 8]
 --attribute two_quotient.elim_type [unfold 9]
-attribute /-two_quotient.rec_on-/ two_quotient.elim_on [unfold 5]
+attribute two_quotient.rec_on two_quotient.elim_on [unfold 5]
 --attribute two_quotient.elim_type_on [unfold 6]
diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean
index 4a554ae34..fc24d191b 100644
--- a/hott/init/pathover.hlean
+++ b/hott/init/pathover.hlean
@@ -293,11 +293,8 @@ namespace eq
     : eq_concato q⁻¹ (pathover_idp_of_eq q) = (idpo : b' =[refl a] b') :=
   by induction q;constructor
 
-  definition change_path_equiv (f : Π{a}, B a ≃ B' a) (r : b =[p] b₂) : f b =[p] f b₂ :=
-  by induction r;constructor
-
-  definition change_path_equiv' (f : Π{a}, B a ≃ B' a) (r : f b =[p] f b₂) : b =[p] b₂ :=
-  (left_inv f b)⁻¹ ⬝po change_path_equiv (λa, f⁻¹ᵉ) r ⬝op left_inv f b₂
+  definition pathover_of_fn_pathover_fn (f : Π{a}, B a ≃ B' a) (r : f b =[p] f b₂) : b =[p] b₂ :=
+  (left_inv f b)⁻¹ ⬝po apo (λa, f⁻¹ᵉ) r ⬝op left_inv f b₂
 
   definition change_path_of_pathover (s : p = p') (r : b =[p] b₂) (r' : b =[p'] b₂)
     (q : r =[s] r') : change_path s r = r' :=
diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean
index 03b3bb383..c9ca55f39 100644
--- a/hott/types/equiv.hlean
+++ b/hott/types/equiv.hlean
@@ -175,7 +175,7 @@ namespace equiv
     {B : A → Type} {C : A → Type} (f : B a ≃ C a) (g : B a' ≃ C a')
     (r : Π(b : B a) (b' : B a') (q : b =[p] b'), f b =[p] g b') : f =[p] g :=
   begin
-    fapply change_path_equiv',
+    fapply pathover_of_fn_pathover_fn,
     { intro a, apply equiv.sigma_char},
     { fapply sigma_pathover,
         esimp, apply arrow_pathover, exact r,