diff --git a/library/standard/hott/path.lean b/library/standard/hott/path.lean
index 9d28d81dc..e21429b8e 100644
--- a/library/standard/hott/path.lean
+++ b/library/standard/hott/path.lean
@@ -2,10 +2,15 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Jeremy Avigad
 -- Ported from Coq HoTT
+--
+-- TODO: things to test:
+-- o To what extent can we use opaque definitions outside the file?
+-- o Try doing these proofs with tactics.
+-- o Try using the simplifier on some of these proofs. 
 
-import general_notation struc.function tools.tactic
+import general_notation struc.function 
 
-using tactic function
+using function
 
 -- Path
 -- ----
@@ -185,13 +190,10 @@ induction_on p (take q h, h @ (concat_1p _)) q
 -- Transport
 -- ---------
 
--- keep transparent, so transport _ idp p is definitionally equal to p
+-- TODO: keep transparent?
 abbreviation transport {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) : P y :=
 path.induction_on p u
 
-definition transport_1 {A : Type} (P : A → Type) {x : A} (u : P x) : transport _ idp u ≈ u :=
-idp
-
 -- This idiom makes the operation right associative.
 notation p `#`:65 x:64 := transport _ p x
 
@@ -218,6 +220,14 @@ definition apD {A:Type} {B : A → Type} (f : Πa:A, B a) {x y : A} (p : x ≈ y
 induction_on p idp
 
 
+-- calc enviroment
+-- ---------------
+
+calc_subst transport
+calc_trans concat
+calc_refl idpath
+
+
 -- More theorems for moving things around in equations
 -- ---------------------------------------------------
 
@@ -247,7 +257,7 @@ induction_on p (take u v, id) u v
 -- Functions take identity paths to identity paths
 definition ap_1 {A B : Type} (x : A) (f : A → B) : (ap f idp) ≈ idp :> (f x ≈ f x) := idp
 
-definition apD_1 {A B} (x : A) (f : forall x : A, B x) : apD f idp ≈ idp :> (f x ≈ f x) := idp
+definition apD_1 {A B} (x : A) (f : Π x : A, B x) : apD f idp ≈ idp :> (f x ≈ f x) := idp
 
 -- Functions commute with concatenation.
 definition ap_pp {A B : Type} (f : A → B) {x y z : A} (p : x ≈ y) (q : y ≈ z) :
@@ -261,28 +271,6 @@ induction_on p (take r q, induction_on q (concat_p_pp r idp idp)) r q
 definition ap_pp_p {A B : Type} (f : A → B) {w x y z : A} (p : x ≈ y) (q : y ≈ z) (r : f z ≈ f w) :
   (ap f (p @ q)) @ r ≈ (ap f p) @ (ap f q @ r) :=
 induction_on p (take q, induction_on q (take r, concat_pp_p _ _ _)) q r
--- induction_on p (take q : x ≈ z, induction_on q (take r : f x ≈ f w, concat_pp_p idp idp r)) q r
-
--- TODO: can we do this proof using tactics?
--- proof
---   apply (induction_on p _ q r),
---   apply (take q, induction_on q _),
---   apply (concat_pp_p idp idp r)
--- qed
-
--- proof
---   apply (induction_on p _ q r),
---   take q, proof 
---     apply (induction_on q),
---     take r, 
---     apply concat_pp_p
---   qed  
--- qed
-
--- Coq proof:
--- Proof.
---   destruct p, q. simpl. exact (concat_pp_p idp idp r).
--- Defined.
 
 -- Functions commute with path inverses.
 definition inverse_ap {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : (ap f p)^ ≈ ap f (p^) :=
@@ -293,7 +281,6 @@ induction_on p idp
 
 -- [ap] itself is functorial in the first argument.
 
--- TODO: rename id to idmap?
 definition ap_idmap {A : Type} {x y : A} (p : x ≈ y) : ap id p ≈ p :=
 induction_on p idp
 
@@ -312,135 +299,72 @@ definition ap_const {A B : Type} {x y : A} (p : x ≈ y) (z : B) :
 induction_on p idp
 
 -- Naturality of [ap].
-definition concat_Ap {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x) {x y : A} (q : x ≈ y) :
+definition concat_Ap {A B : Type} {f g : A → B} (p : Π x, f x ≈ g x) {x y : A} (q : x ≈ y) :
   (ap f q) @ (p y) ≈ (p x) @ (ap g q) :=
 induction_on q (concat_1p _ @ (concat_p1 _)^)
 
 -- Naturality of [ap] at identity.
-definition concat_A1p {A : Type} {f : A → A} (p : forall x, f x ≈ x) {x y : A} (q : x ≈ y) :
+definition concat_A1p {A : Type} {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y) :
   (ap f q) @ (p y) ≈ (p x) @ q :=
 induction_on q (concat_1p _ @ (concat_p1 _)^)
 
-definition concat_pA1 {A : Type} {f : A → A} (p : forall x, x ≈ f x) {x y : A} (q : x ≈ y) :
+definition concat_pA1 {A : Type} {f : A → A} (p : Πx, x ≈ f x) {x y : A} (q : x ≈ y) :
   (p x) @ (ap f q) ≈  q @ (p y) :=
 induction_on q (concat_p1 _ @ (concat_1p _)^)
 
--- TODO: move these
-calc_subst transport
-calc_trans concat
-calc_refl idpath
-
 -- Naturality with other paths hanging around.
 
-definition concat_pA_pp {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x)
-    {x y : A} (q : x ≈ y)
+definition concat_pA_pp {A B : Type} {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y)
     {w z : B} (r : w ≈ f x) (s : g y ≈ z) :
   (r @ ap f q) @ (p y @ s) ≈ (r @ p x) @ (ap g q @ s) :=
-induction_on q (induction_on s
-  (calc 
-    (r @ (ap f q)) @ ((p y) @ (idpath (g y))) ≈ (r @ (ap f q)) @ (p y) : {concat_p1 _}
-      ... ≈ r @ ((ap f q) @ (p y)) : concat_pp_p _ _ _
-      ... ≈ r @ ((p x) @ (ap g q)) : {concat_Ap p q}
-      ... ≈ (r @ (p x)) @ ((ap g q)) : concat_p_pp _ _ _
-      ... ≈ (r @ (p x)) @ ((ap g q) @ (idpath (g y))) : {concat_p1 _}))
+induction_on s (induction_on q idp)
 
--- TODO: the Coq proof of the previous theorem is much shorter:
--- Proof.
---   destruct q, s; simpl.
---   repeat rewrite concat_p1.
---   reflexivity.
--- Defined.
+definition concat_pA_p {A B : Type} {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y) 
+    {w : B} (r : w ≈ f x) :
+  (r @ ap f q) @ p y ≈ (r @ p x) @ ap g q :=
+induction_on q idp
 
-(-- TODO: These are similar
+-- TODO: try this using the simplifier, and compare proofs
+definition concat_A_pp {A B : Type} {f g : A → B} (p : Πx, f x ≈ g x) {x y : A} (q : x ≈ y) 
+    {z : B} (s : g y ≈ z) :
+  (ap f q) @ (p y @ s) ≈ (p x) @ (ap g q @ s) :=
+induction_on s (induction_on q 
+  (calc
+    (ap f idp) @ (p x @ idp) ≈ idp @ p x : idp 
+      ... ≈ p x : concat_1p _
+      ... ≈ (p x) @ (ap g idp @ idp) : idp))
+-- This also works:
+-- induction_on s (induction_on q (concat_1p _ # idp))
 
-definition concat_pA_p {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x)
-  {x y : A} (q : x ≈ y)
-  {w : B} (r : w ≈ f x)
-  :
-  (r @ ap f q) @ p y ≈ (r @ p x) @ ap g q.
-Proof.
-  destruct q; simpl.
-  repeat rewrite concat_p1.
-  reflexivity.
-Defined.
+definition concat_pA1_pp {A : Type} {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y)
+    {w z : A} (r : w ≈ f x) (s : y ≈ z) :
+  (r @ ap f q) @ (p y @ s) ≈ (r @ p x) @ (q @ s) :=
+induction_on s (induction_on q idp)
 
-definition concat_A_pp {A B : Type} {f g : A → B} (p : forall x, f x ≈ g x)
-  {x y : A} (q : x ≈ y)
-  {z : B} (s : g y ≈ z)
-  :
-  (ap f q) @ (p y @ s) ≈ (p x) @ (ap g q @ s).
-Proof.
-  destruct q, s; simpl.
-  repeat rewrite concat_p1, concat_1p.
-  reflexivity.
-Defined.
+definition concat_pp_A1p {A : Type} {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y)
+    {w z : A} (r : w ≈ x) (s : g y ≈ z) :
+  (r @ p x) @ (ap g q @ s) ≈ (r @ q) @ (p y @ s) :=
+induction_on s (induction_on q idp)
 
-definition concat_pA1_pp {A : Type} {f : A → A} (p : forall x, f x ≈ x)
-  {x y : A} (q : x ≈ y)
-  {w z : A} (r : w ≈ f x) (s : y ≈ z)
-  :
-  (r @ ap f q) @ (p y @ s) ≈ (r @ p x) @ (q @ s).
-Proof.
-  destruct q, s; simpl.
-  repeat rewrite concat_p1.
-  reflexivity.
-Defined.
+definition concat_pA1_p {A : Type} {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y)
+    {w : A} (r : w ≈ f x) :
+  (r @ ap f q) @ p y ≈ (r @ p x) @ q :=
+induction_on q idp
 
-definition concat_pp_A1p {A : Type} {g : A → A} (p : forall x, x ≈ g x)
-  {x y : A} (q : x ≈ y)
-  {w z : A} (r : w ≈ x) (s : g y ≈ z)
-  :
-  (r @ p x) @ (ap g q @ s) ≈ (r @ q) @ (p y @ s).
-Proof.
-  destruct q, s; simpl.
-  repeat rewrite concat_p1.
-  reflexivity.
-Defined.
+definition concat_A1_pp {A : Type} {f : A → A} (p : Πx, f x ≈ x) {x y : A} (q : x ≈ y)
+    {z : A} (s : y ≈ z) :
+  (ap f q) @ (p y @ s) ≈ (p x) @ (q @ s) :=
+induction_on s (induction_on q (concat_1p _ # idp))
 
-definition concat_pA1_p {A : Type} {f : A → A} (p : forall x, f x ≈ x)
-  {x y : A} (q : x ≈ y)
-  {w : A} (r : w ≈ f x)
-  :
-  (r @ ap f q) @ p y ≈ (r @ p x) @ q.
-Proof.
-  destruct q; simpl.
-  repeat rewrite concat_p1.
-  reflexivity.
-Defined.
+definition concat_pp_A1 {A : Type} {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y)
+    {w : A} (r : w ≈ x) :
+  (r @ p x) @ ap g q ≈ (r @ q) @ p y := 
+induction_on q idp
 
-definition concat_A1_pp {A : Type} {f : A → A} (p : forall x, f x ≈ x)
-  {x y : A} (q : x ≈ y)
-  {z : A} (s : y ≈ z)
-  :
-  (ap f q) @ (p y @ s) ≈ (p x) @ (q @ s).
-Proof.
-  destruct q, s; simpl.
-  repeat rewrite concat_p1, concat_1p.
-  reflexivity.
-Defined.
-
-definition concat_pp_A1 {A : Type} {g : A → A} (p : forall x, x ≈ g x)
-  {x y : A} (q : x ≈ y)
-  {w : A} (r : w ≈ x)
-  :
-  (r @ p x) @ ap g q ≈ (r @ q) @ p y.
-Proof.
-  destruct q; simpl.
-  repeat rewrite concat_p1.
-  reflexivity.
-Defined.
-
-definition concat_p_A1p {A : Type} {g : A → A} (p : forall x, x ≈ g x)
-  {x y : A} (q : x ≈ y)
-  {z : A} (s : g y ≈ z)
-  :
-  p x @ (ap g q @ s) ≈ q @ (p y @ s).
-Proof.
-  destruct q, s; simpl.
-  repeat rewrite concat_p1, concat_1p.
-  reflexivity.
-Defined.
---)
+definition concat_p_A1p {A : Type} {g : A → A} (p : Πx, x ≈ g x) {x y : A} (q : x ≈ y)
+    {z : A} (s : g y ≈ z) :
+  p x @ (ap g q @ s) ≈ q @ (p y @ s) :=
+induction_on s (induction_on q (concat_1p _ # idp))
 
 
 -- Action of [apD10] and [ap10] on paths
@@ -474,9 +398,8 @@ induction_on p idp
 -- Transport and the groupoid structure of paths
 -- ---------------------------------------------
 
--- TODO: move from above?
--- definition transport_1 {A : Type} (P : A → Type) {x : A} (u : P x)
---   : idp # u ≈ u := idp
+definition transport_1 {A : Type} (P : A → Type) {x : A} (u : P x) : 
+  idp # u ≈ u := idp
 
 definition transport_pp {A : Type} (P : A → Type) {x y z : A} (p : x ≈ y) (q : y ≈ z) (u : P x) :
   p @ q # u ≈ q # p # u :=
@@ -490,142 +413,18 @@ definition transport_Vp {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z :
   p^ # p # z ≈ z := 
 (transport_pp P p (p^) z)^ @ ap (λr, transport P r z) (concat_pV p)
 
-
------------------------------------------------
--- TODO: Examples of difficult induction problems
------------------------------------------------
-
-theorem double_induction 
-    {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z)
-    {C : Π(x y z : A), Π(p : x ≈ y), Π(q : y ≈ z), Type} 
-    (H : C x x x (idpath x) (idpath x)) : 
-  C x y z p q := 
-induction_on p (take z q, induction_on q H) z q
-
-theorem double_induction2 
-    {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y)
-    {C : Π(x y z : A), Π(p : x ≈ y), Π(q : z ≈ y), Type}
-    (H : C z z z (idpath z) (idpath z)) :
-  C x y z p q := 
-induction_on p (take y q, induction_on q H) y q
-
-theorem double_induction2' 
-  {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y)
-  {C : Π(x y z : A), Π(p : x ≈ y), Π(q : z ≈ y), Type}
-  (H : C z z z (idpath z) (idpath z)) : C x y z p q := 
-induction_on p (take y q, induction_on q H) y q
-
-theorem triple_induction 
-    {A : Type} {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w)
-    {C : Π(x y z w : A), Π(p : x ≈ y), Π(q : y ≈ z), Π(r: z ≈ w), Type} 
-    (H : C x x x x (idpath x) (idpath x) (idpath x)) :
-  C x y z w p q r := 
-induction_on p (take z q, induction_on q (take w r, induction_on r H)) z q w r
-
--- try this again
-definition concat_pV_p_new {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p @ q^) @ q ≈ p :=
-double_induction2 p q idp
-
--- old proof:
--- induction_on q (take p, induction_on p idp) p
-
--- This is an attempt to do it as a tactic proof
--- proof
---   apply (induction_on q _ p),
---   take p,
---   apply (induction_on p idp)
--- qed
-
--- set_option unifier.max_steps 1000000
-
--- TODO: update: this no longer works, but it used to (it took a couple of seconds)
-
--- theorem test {A : Type} (P : A → Type) (x : A) (u_1 : P x) :
--- path
---     (concat
---        (concat (ap (λ (e : path x x), transport P e u_1) (concat_p_pp (idpath x) (idpath x) (idpath x)))
---           (transport_pp P (concat (idpath x) (idpath x)) (idpath x) u_1))
---        (ap (transport P (idpath x)) (transport_pp P (idpath x) (idpath x) u_1)))
---     (concat (transport_pp P (idpath x) (concat (idpath x) (idpath x)) u_1)
---        (transport_pp P (idpath x) (idpath x) (transport P (idpath x) u_1))) := 
--- idp
-
--- definition transport_p_pp {A : Type} (P : A → Type)
---     {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) : 
---   ap (λe, e # u) (concat_p_pp p q r) @ (transport_pp P (p @ q) r u) @ 
---       ap (transport P r) (transport_pp P p q u)
---     ≈ (transport_pp P p (q @ r) u) @ (transport_pp P q r (p # u))
---     :> ((p @ (q @ r)) # u ≈ r # q # p # u) := 
--- triple_induction p q r _ u
--- triple_induction p q r (take u, test P x u) u
-
--- this doesn't work, even with max_steps = 100000
---double_induction p q (take r, induction_on r (take u, test P x u))) r u
-
--- even this doesn't work!
--- definition transport_p_pp' {A : Type} (P : A → Type)
---     {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) : 
---   ap (λe, e # u) (concat_p_pp p q r) @ (transport_pp P (p @ q) r u) @ 
---       ap (transport P r) (transport_pp P p q u)
---     ≈ (transport_pp P p (q @ r) u) @ (transport_pp P q r (p # u))
---     :> ((p @ (q @ r)) # u ≈ r # q # p # u) :=
--- have aux:
---  Πu_1 : P x, path
---     (concat
---        (concat (ap (λ (e : path x x), transport' e u_1) (concat_p_pp (idpath x) (idpath x) (idpath x)))
---           (transport_pp P (concat (idpath x) (idpath x)) (idpath x) u_1))
---        (ap (transport P (idpath x)) (transport_pp P (idpath x) (idpath x) u_1)))
---     (concat (transport_pp P (idpath x) (concat (idpath x) (idpath x)) u_1)
---        (transport_pp P (idpath x) (idpath x) (transport' (idpath x) u_1))), from take u_1, idp,
--- triple_induction p q r (take u, aux u) u
-
--- This works with max_steps = 10000
--- definition transport_p_pp {A : Type} (P : A → Type)
---     {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) : 
---   ap (λe, e # u) (concat_p_pp p q r) @ (transport_pp P (p @ q) r u) @ 
---       ap (transport P r) (transport_pp P p q u)
---     ≈ (transport_pp P p (q @ r) u) @ (transport_pp P q r (p # u))
---     :> ((p @ (q @ r)) # u ≈ r # q # p # u) :=
--- induction_on p (take q, induction_on q (take r, induction_on r (take u, test P x u))) q r u
-
--- This shows the goal, with max_steps = 100000
--- definition transport_p_pp {A : Type} (P : A → Type)
---     {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) : 
---   ap (λe, e # u) (concat_p_pp p q r) @ (transport_pp P (p @ q) r u) @ 
---       ap (transport P r) (transport_pp P p q u)
---     ≈ (transport_pp P p (q @ r) u) @ (transport_pp P q r (p # u))
---     :> ((p @ (q @ r)) # u ≈ r # q # p # u) :=
--- induction_on p (take q, induction_on q (take r, induction_on r (take u, _)))) q r u
-
-
-
--- Back to the regular development
-
--- In the future, we may expect to need some higher coherence for transport:
---  for instance, that transport acting on the associator is trivial.
-
--- set_option unifier.max_steps 1000000
-
--- TODO: we cannot get this yet
--- in Coq, the type annotation is only for clarity -- it is not needed
-definition transport_p_pp {A : Type} (P : A → Type)
+definition transport_p_pp {A : Type} (P : A → Type) 
     {x y z w : A} (p : x ≈ y) (q : y ≈ z) (r : z ≈ w) (u : P x) : 
   ap (λe, e # u) (concat_p_pp p q r) @ (transport_pp P (p @ q) r u) @ 
       ap (transport P r) (transport_pp P p q u)
     ≈ (transport_pp P p (q @ r) u) @ (transport_pp P q r (p # u))
-    :> ((p @ (q @ r)) # u ≈ r # q # p # u) := 
-sorry
-
-(-- Coq proof:
-Proof.
-  destruct p, q, r.  simpl.  exact 1.
-Defined.
---)
+    :> ((p @ (q @ r)) # u ≈ r # q # p # u) :=
+induction_on r (induction_on q (induction_on p idp))
 
 --  Here is another coherence lemma for transport.
 definition transport_pVp {A} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) : 
-  transport_pV P p (transport P p z) ≈ ap (transport P p) (transport_Vp P p z)
-:= induction_on p idp
+  transport_pV P p (transport P p z) ≈ ap (transport P p) (transport_Vp P p z) := 
+induction_on p idp
 
 -- Dependent transport in a doubly dependent type.
 definition transportD {A : Type} (B : A → Type) (C : Π a : A, B a → Type)
@@ -635,7 +434,8 @@ induction_on p z
 
 -- Transporting along higher-dimensional paths
 definition transport2 {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : P x) : 
-  p # z ≈ q # z := ap (λp', p' # z) r
+  p # z ≈ q # z := 
+ap (λp', p' # z) r
 
 -- An alternative definition.
 definition transport2_is_ap10 {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) 
@@ -793,22 +593,7 @@ definition pentagon {A : Type} {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r :
     @ concat_p_pp p (q @ r) s
     @ whiskerR (concat_p_pp p q r) s
   ≈ concat_p_pp p q (r @ s) @ concat_p_pp (p @ q) r s :=
-sorry
--- induction_on p (induction_on q (induction_on r (induction_on s idp)))
-
-(-- The Coq proof:
-
--- The "pentagonator": the 3-cell witnessing the associativity pentagon.
-definition pentagon {A : Type} {v w x y z : A} (p : v ≈ w) (q : w ≈ x) (r : x ≈ y) (s : y ≈ z)
-  : whiskerL p (concat_p_pp q r s)
-      @ concat_p_pp p (q@r) s
-      @ whiskerR (concat_p_pp p q r) s
-  ≈ concat_p_pp p q (r@s) @ concat_p_pp (p@q) r s.
-Proof.
-  case p, q, r, s.  reflexivity.
-Defined.
-
---)
+induction_on p (take q, induction_on q (take r, induction_on r (take s, induction_on s idp))) q r s
 
 -- The 3-cell witnessing the left unit triangle.
 definition triangulator {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : 
@@ -824,7 +609,6 @@ definition eckmann_hilton {A : Type} {x:A} (p q : idp ≈ idp :> (x ≈ x)) : p
   @ (concat_p1 _ @@ concat_p1 _)^
   @ (whiskerL_1p q @@ whiskerR_p1 p)
 
-
 -- The action of functions on 2-dimensional paths
 definition ap02 {A B : Type} (f:A → B) {x y : A} {p q : x ≈ y} (r : p ≈ q) : ap f p ≈ ap f q :=
 induction_on r idp
@@ -838,7 +622,8 @@ definition ap02_p2p {A B} (f : A → B) {x y z : A} {p p' : x ≈ y} {q q' :y 
   ap02 f (r @@ s) ≈   ap_pp f p q
                       @ (ap02 f r  @@  ap02 f s)
                       @ (ap_pp f p' q')^ :=
-sorry
+induction_on r (induction_on s (induction_on q (induction_on p idp)))
+
 -- induction_on r (induction_on s (induction_on p (induction_on q idp)))
 
 definition apD02 {A : Type} {B : A → Type} {x y : A} {p q : x ≈ y} (f : Π x, B x) (r : p ≈ q) : 
@@ -852,29 +637,16 @@ definition apD02_pp {A} (B : A → Type) (f : Π x:A, B x) {x y : A}
     @ whiskerL (transport2 B r1 (f x)) (apD02 f r2)
     @ concat_p_pp _ _ _
     @ (whiskerR ((transport2_p2p B r1 r2 (f x))^) (apD f p3)) :=
-sorry
--- induction_on r1 (take r2, induction_on r2 (take p1, induction_on p1 idp)) r2 p1
+induction_on r1 (take r2, induction_on r2 (induction_on p1 idp)) r2 
 
-(--
 
-The Coq proof:
-definition apD02_pp {A} (B : A → Type) (f : Π x:A, B x) {x y : A}
-  {p1 p2 p3 : x ≈ y} (r1 : p1 ≈ p2) (r2 : p2 ≈ p3)
-  : apD02 f (r1 @ r2)
-  ≈ apD02 f r1
-  @ whiskerL (transport2 B r1 (f x)) (apD02 f r2)
-  @ concat_p_pp _ _ _
-  @ (whiskerR (transport2_p2p B r1 r2 (f x))^ (apD f p3)).
-Proof.
-  destruct r1, r2. destruct p1. reflexivity.
-Defined.
+(-- From the Coq version:
 
---)
-
-(--
 -- ** Tactics, hints, and aliases
 
--- [concat], with arguments flipped. Useful mainly in the idiom [apply (concatR (expression))]. Given as a notation not a definition so that the resultant terms are literally instances of [concat], with no unfolding required.
+-- [concat], with arguments flipped. Useful mainly in the idiom [apply (concatR (expression))]. 
+-- Given as a notation not a definition so that the resultant terms are literally instances of 
+-- [concat], with no unfolding required.
 Notation concatR := (λp q, concat q p).
 
 Hint Resolve