diff --git a/hott/hit/circle.hlean b/hott/hit/circle.hlean
index b31c20b0a9..ae018a1ba2 100644
--- a/hott/hit/circle.hlean
+++ b/hott/hit/circle.hlean
@@ -12,61 +12,62 @@ import .sphere
 
 open eq suspension bool sphere_index equiv equiv.ops
 
-definition circle [reducible] := suspension bool --redefine this as sphere 1
+definition circle [reducible] := sphere 1
 
 namespace circle
 
   definition base1 : circle := !north
   definition base2 : circle := !south
-  definition seg1 : base1 = base2 := merid tt
-  definition seg2 : base2 = base1 := (merid ff)⁻¹
+  definition seg1 : base1 = base2 := merid !north
+  definition seg2 : base1 = base2 := merid !south
 
   definition base : circle := base1
-  definition loop : base = base := seg1 ⬝ seg2
+  definition loop : base = base := seg1 ⬝ seg2⁻¹
 
   definition rec2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
-    (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1) (x : circle) : P x :=
+    (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb1 = Pb2) (x : circle) : P x :=
   begin
     fapply (suspension.rec_on x),
     { exact Pb1},
     { exact Pb2},
-    { intro b, cases b,
-        apply tr_eq_of_eq_inv_tr, exact Ps2⁻¹,
-        exact Ps1},
+    { esimp, intro b, fapply (suspension.rec_on b),
+      { exact Ps1},
+      { exact Ps2},
+      { intro x, cases x}},
   end
 
   definition rec2_on [reducible] {P : circle → Type} (x : circle) (Pb1 : P base1) (Pb2 : P base2)
-    (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1) : P x :=
+    (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb1 = Pb2) : P x :=
   circle.rec2 Pb1 Pb2 Ps1 Ps2 x
 
   theorem rec2_seg1 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
-    (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1)
+    (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb1 = Pb2)
       : apd (rec2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 :=
   !rec_merid
 
   theorem rec2_seg2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
-    (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb2 = Pb1)
+    (Ps1 : seg1 ▹ Pb1 = Pb2) (Ps2 : seg2 ▹ Pb1 = Pb2)
       : apd (rec2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
-  sorry
+  !rec_merid
 
-  definition elim2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1) (x : circle) : P :=
+  definition elim2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2) (x : circle) : P :=
   rec2 Pb1 Pb2 (!tr_constant ⬝ Ps1) (!tr_constant ⬝ Ps2) x
 
   definition elim2_on [reducible] {P : Type} (x : circle) (Pb1 Pb2 : P)
-    (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1) : P :=
+    (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2) : P :=
   elim2 Pb1 Pb2 Ps1 Ps2 x
 
-  theorem elim2_seg1 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1)
+  theorem elim2_seg1 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2)
     : ap (elim2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 :=
   begin
     apply (@cancel_left _ _ _ _ (tr_constant seg1 (elim2 Pb1 Pb2 Ps1 Ps2 base1))),
     rewrite [-apd_eq_tr_constant_con_ap,↑elim2,rec2_seg1],
   end
 
-  theorem elim2_seg2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb2 = Pb1)
+  theorem elim2_seg2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2)
     : ap (elim2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
   begin
-    apply (@cancel_left _ _ _ _ (tr_constant seg2 (elim2 Pb1 Pb2 Ps1 Ps2 base2))),
+    apply (@cancel_left _ _ _ _ (tr_constant seg2 (elim2 Pb1 Pb2 Ps1 Ps2 base1))),
     rewrite [-apd_eq_tr_constant_con_ap,↑elim2,rec2_seg2],
   end
 
@@ -77,7 +78,7 @@ namespace circle
     { exact Pbase},
     { exact (transport P seg1 Pbase)},
     { apply idp},
-    { apply eq_tr_of_inv_tr_eq, rewrite -tr_con, apply Ploop},
+    { apply tr_eq_of_eq_inv_tr, rewrite -tr_con, exact Ploop⁻¹},
   end
 
   example {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) : rec Pbase Ploop base = Pbase := idp
@@ -85,10 +86,14 @@ namespace circle
   protected definition rec_on [reducible] {P : circle → Type} (x : circle) (Pbase : P base)
     (Ploop : loop ▹ Pbase = Pbase) : P x :=
   rec Pbase Ploop x
-
+  set_option pp.beta false
   theorem rec_loop {P : circle → Type} (Pbase : P base) (Ploop : loop ▹ Pbase = Pbase) :
     apd (rec Pbase Ploop) loop = Ploop :=
   sorry
+  -- begin
+  --   rewrite [↑loop,apd_con,↑rec,↑rec2_on,↑base,rec2_seg1,apd_inv,rec2_seg2,↑ap,↑eq.rec_on,▸*],
+  --   esimp
+  -- end
 
   protected definition elim {P : Type} (Pbase : P) (Ploop : Pbase = Pbase)
     (x : circle) : P :=
diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 3d73fc10dc..a656e2f517 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -227,7 +227,7 @@ namespace eq
   definition ap11 {f g : A → B} (H : f = g) {x y : A} (p : x = y) : f x = g y :=
   eq.rec_on H (eq.rec_on p idp)
 
-  definition apd (f : Πa:A, P a) {x y : A} (p : x = y) : p ▹ (f x) = f y :=
+  definition apd (f : Πa:A, P a) {x y : A} (p : x = y) : p ▹ f x = f y :=
   eq.rec_on p idp
 
   /- calc enviroment -/
@@ -261,20 +261,19 @@ namespace eq
   -- functorial.
 
   -- Functions take identity paths to identity paths
-  definition ap_idp  (x : A) (f : A → B)   : ap  f idp = idp :> (f x = f x) := idp
-  definition apd_idp (x : A) (f : Πx, P x) : apd f idp = idp :> (f x = f x) := idp
+  definition ap_idp (x : A) (f : A → B) : ap f idp = idp :> (f x = f x) := idp
 
   -- Functions commute with concatenation.
   definition ap_con (f : A → B) {x y z : A} (p : x = y) (q : y = z) :
-    ap f (p ⬝ q) = (ap f p) ⬝ (ap f q) :=
+    ap f (p ⬝ q) = ap f p ⬝ ap f q :=
   eq.rec_on q (eq.rec_on p idp)
 
   definition con_ap_con_eq_con_ap_con_ap (f : A → B) {w x y z : A} (r : f w = f x) (p : x = y) (q : y = z) :
-    r ⬝ (ap f (p ⬝ q)) = (r ⬝ ap f p) ⬝ (ap f q) :=
+    r ⬝ ap f (p ⬝ q) = (r ⬝ ap f p) ⬝ ap f q :=
   eq.rec_on q (take p, eq.rec_on p (con.assoc' r idp idp)) p
 
   definition ap_con_con_eq_ap_con_ap_con (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) :=
+    ap f (p ⬝ q) ⬝ r = ap f p ⬝ (ap f q ⬝ r) :=
   eq.rec_on q (eq.rec_on p (take r, con.assoc _ _ _)) r
 
   -- Functions commute with path inverses.
@@ -431,6 +430,17 @@ namespace eq
     tr_inv_tr P p (transport P p z) = ap (transport P p) (inv_tr_tr P p z) :=
   eq.rec_on p idp
 
+  /- some properties for apd -/
+
+  definition apd_idp (x : A) (f : Πx, P x) : apd f idp = idp :> (f x = f x) := idp
+  definition apd_con (f : Πx, P x) {x y z : A} (p : x = y) (q : y = z)
+    : apd f (p ⬝ q) = tr_con P p q (f x) ⬝ ap (transport P q) (apd f p) ⬝ apd f q :=
+  by cases p;cases q;apply idp
+  definition apd_inv (f : Πx, P x) {x y : A} (p : x = y)
+    : apd f p⁻¹ = (eq_inv_tr_of_tr_eq P (apd f p))⁻¹ :=
+  by cases p;apply idp
+
+
   -- Dependent transport in a doubly dependent type.
   definition transportD {P : A → Type} (Q : Π a : A, P a → Type)
       {a a' : A} (p : a = a') (b : P a) (z : Q a b) : Q a' (p ▹ b) :=