From ea7694ca32ca015a3beab0f5fa1bd581879ecc39 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 13 May 2015 22:32:07 -0700
Subject: [PATCH] fix(tests/lean/slow/path_groupoids): to reflect changes in
 the libraries

---
 tests/lean/slow/path_groupoids.lean | 138 ++++++++++++++--------------
 1 file changed, 69 insertions(+), 69 deletions(-)

diff --git a/tests/lean/slow/path_groupoids.lean b/tests/lean/slow/path_groupoids.lean
index 6c7e25908..7c76280e2 100644
--- a/tests/lean/slow/path_groupoids.lean
+++ b/tests/lean/slow/path_groupoids.lean
@@ -29,10 +29,10 @@ definition inverse {A : Type} {x y : A} (p : x ≈ y) : y ≈ x :=
 path.rec (idpath x) p
 
 infixl `⬝` := concat
-postfix `^`:100 := inverse
+postfix `**`:100 := inverse
 
 -- In Coq, these are not needed, because concat and inv are kept transparent
-definition inv_1 {A : Type} (x : A) : (idpath x)^ ≈ idpath x := idp
+definition inv_1 {A : Type} (x : A) : (idpath x)** ≈ idpath x := idp
 
 definition concat_11 {A : Type} (x : A) : idpath x ⬝ idpath x ≈ idpath x := idp
 
@@ -58,45 +58,45 @@ definition concat_pp_p {A : Type} {x y z t : A} (p : x ≈ y) (q : y ≈ z) (r :
 path.rec_on r (path.rec_on q idp)
 
 -- The left inverse law.
-definition concat_pV {A : Type} {x y : A} (p : x ≈ y) : p ⬝ p^ ≈ idp :=
+definition concat_pV {A : Type} {x y : A} (p : x ≈ y) : p ⬝ p** ≈ idp :=
 path.rec_on p idp
 
 -- The right inverse law.
-definition concat_Vp {A : Type} {x y : A} (p : x ≈ y) : p^ ⬝ p ≈ idp :=
+definition concat_Vp {A : Type} {x y : A} (p : x ≈ y) : p** ⬝ p ≈ idp :=
 path.rec_on p idp
 
 
 -- Several auxiliary theorems about canceling inverses across associativity. These are somewhat
 -- redundant, following from earlier theorems.
 
-definition concat_V_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : p^ ⬝ (p ⬝ q) ≈ q :=
+definition concat_V_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : p** ⬝ (p ⬝ q) ≈ q :=
 path.rec_on q (path.rec_on p idp)
 
-definition concat_p_Vp {A : Type} {x y z : A} (p : x ≈ y) (q : x ≈ z) : p ⬝ (p^ ⬝ q) ≈ q :=
+definition concat_p_Vp {A : Type} {x y z : A} (p : x ≈ y) (q : x ≈ z) : p ⬝ (p** ⬝ q) ≈ q :=
 path.rec_on q (path.rec_on p idp)
 
-definition concat_pp_V {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q) ⬝ q^ ≈ p :=
+definition concat_pp_V {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q) ⬝ q** ≈ p :=
 path.rec_on q (path.rec_on p idp)
 
-definition concat_pV_p {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q^) ⬝ q ≈ p :=
+definition concat_pV_p {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) : (p ⬝ q**) ⬝ q ≈ p :=
 path.rec_on q (take p, path.rec_on p idp) p
 
 -- Inverse distributes over concatenation
-definition inv_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q)^ ≈ q^ ⬝ p^ :=
+definition inv_pp {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) : (p ⬝ q)** ≈ q** ⬝ p** :=
 path.rec_on q (path.rec_on p idp)
 
-definition inv_Vp {A : Type} {x y z : A} (p : y ≈ x) (q : y ≈ z) : (p^ ⬝ q)^ ≈ q^ ⬝ p :=
+definition inv_Vp {A : Type} {x y z : A} (p : y ≈ x) (q : y ≈ z) : (p** ⬝ q)** ≈ q** ⬝ p :=
 path.rec_on q (path.rec_on p idp)
 
 -- universe metavariables
-definition inv_pV {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y) : (p ⬝ q^)^ ≈ q ⬝ p^ :=
+definition inv_pV {A : Type} {x y z : A} (p : x ≈ y) (q : z ≈ y) : (p ⬝ q**)** ≈ q ⬝ p** :=
 path.rec_on p (λq, path.rec_on q idp) q
 
-definition inv_VV {A : Type} {x y z : A} (p : y ≈ x) (q : z ≈ y) : (p^ ⬝ q^)^ ≈ q ⬝ p :=
+definition inv_VV {A : Type} {x y z : A} (p : y ≈ x) (q : z ≈ y) : (p** ⬝ q**)** ≈ q ⬝ p :=
 path.rec_on p (path.rec_on q idp)
 
 -- Inverse is an involution.
-definition inv_V {A : Type} {x y : A} (p : x ≈ y) : p^^ ≈ p :=
+definition inv_V {A : Type} {x y : A} (p : x ≈ y) : p**** ≈ p :=
 path.rec_on p idp
 
 
@@ -104,72 +104,72 @@ path.rec_on p idp
 -- ----------------------------------------------
 
 definition moveR_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
-  p ≈ (r^ ⬝ q) → (r ⬝ p) ≈ q :=
-have gen : Πp q, p ≈ (r^ ⬝ q) → (r ⬝ p) ≈ q, from
+  p ≈ (r** ⬝ q) → (r ⬝ p) ≈ q :=
+have gen : Πp q, p ≈ (r** ⬝ q) → (r ⬝ p) ≈ q, from
   path.rec_on r
     (take p q,
-      assume h : p ≈ idp^ ⬝ q,
+      assume h : p ≈ idp** ⬝ q,
       show idp ⬝ p ≈ q, from concat_1p _ ⬝ h ⬝ concat_1p _),
 gen p q
 
 definition moveR_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
-  r ≈ q ⬝ p^ → r ⬝ p ≈ q :=
+  r ≈ q ⬝ p** → r ⬝ p ≈ q :=
 path.rec_on p (take q r h, (concat_p1 _ ⬝ h ⬝ concat_p1 _)) q r
 
 definition moveR_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) :
-  p ≈ r ⬝ q → r^ ⬝ p ≈ q :=
+  p ≈ r ⬝ q → r** ⬝ p ≈ q :=
 path.rec_on r (take p q h, concat_1p _ ⬝ h ⬝ concat_1p _) p q
 
 definition moveR_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) :
-  r ≈ q ⬝ p → r ⬝ p^ ≈ q :=
+  r ≈ q ⬝ p → r ⬝ p** ≈ q :=
 path.rec_on p (take q r h, concat_p1 _ ⬝ h ⬝ concat_p1 _) q r
 
 definition moveL_Mp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
-  r^ ⬝ q ≈ p → q ≈ r ⬝ p :=
-path.rec_on r (take p q h, (concat_1p _)^ ⬝ h ⬝ (concat_1p _)^) p q
+  r** ⬝ q ≈ p → q ≈ r ⬝ p :=
+path.rec_on r (take p q h, (concat_1p _)** ⬝ h ⬝ (concat_1p _)**) p q
 
 definition moveL_pM {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : y ≈ x) :
-  q ⬝ p^ ≈ r → q ≈ r ⬝ p :=
-path.rec_on p (take q r h, (concat_p1 _)^ ⬝ h ⬝ (concat_p1 _)^) q r
+  q ⬝ p** ≈ r → q ≈ r ⬝ p :=
+path.rec_on p (take q r h, (concat_p1 _)** ⬝ h ⬝ (concat_p1 _)**) q r
 
 definition moveL_Vp {A : Type} {x y z : A} (p : x ≈ z) (q : y ≈ z) (r : x ≈ y) :
-  r ⬝ q ≈ p → q ≈ r^ ⬝ p :=
-path.rec_on r (take p q h, (concat_1p _)^ ⬝ h ⬝ (concat_1p _)^) p q
+  r ⬝ q ≈ p → q ≈ r** ⬝ p :=
+path.rec_on r (take p q h, (concat_1p _)** ⬝ h ⬝ (concat_1p _)**) p q
 
 definition moveL_pV {A : Type} {x y z : A} (p : z ≈ x) (q : y ≈ z) (r : y ≈ x) :
-  q ⬝ p ≈ r → q ≈ r ⬝ p^ :=
-path.rec_on p (take q r h, (concat_p1 _)^ ⬝ h ⬝ (concat_p1 _)^) q r
+  q ⬝ p ≈ r → q ≈ r ⬝ p** :=
+path.rec_on p (take q r h, (concat_p1 _)** ⬝ h ⬝ (concat_p1 _)**) q r
 
 definition moveL_1M {A : Type} {x y : A} (p q : x ≈ y) :
-  p ⬝ q^ ≈ idp → p ≈ q :=
-path.rec_on q (take p h, (concat_p1 _)^ ⬝ h)  p
+  p ⬝ q** ≈ idp → p ≈ q :=
+path.rec_on q (take p h, (concat_p1 _)** ⬝ h)  p
 
 definition moveL_M1 {A : Type} {x y : A} (p q : x ≈ y) :
-  q^ ⬝ p ≈ idp → p ≈ q :=
-path.rec_on q (take p h, (concat_1p _)^ ⬝ h)  p
+  q** ⬝ p ≈ idp → p ≈ q :=
+path.rec_on q (take p h, (concat_1p _)** ⬝ h)  p
 
 definition moveL_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
-  p ⬝ q ≈ idp → p ≈ q^ :=
-path.rec_on q (take p h, (concat_p1 _)^ ⬝ h)  p
+  p ⬝ q ≈ idp → p ≈ q** :=
+path.rec_on q (take p h, (concat_p1 _)** ⬝ h)  p
 
 definition moveL_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
-  q ⬝ p ≈ idp → p ≈ q^ :=
-path.rec_on q (take p h, (concat_1p _)^ ⬝ h)  p
+  q ⬝ p ≈ idp → p ≈ q** :=
+path.rec_on q (take p h, (concat_1p _)** ⬝ h)  p
 
 definition moveR_M1 {A : Type} {x y : A} (p q : x ≈ y) :
-  idp ≈ p^ ⬝ q → p ≈ q :=
+  idp ≈ p** ⬝ q → p ≈ q :=
 path.rec_on p (take q h, h ⬝ (concat_1p _)) q
 
 definition moveR_1M {A : Type} {x y : A} (p q : x ≈ y) :
-  idp ≈ q ⬝ p^ → p ≈ q :=
+  idp ≈ q ⬝ p** → p ≈ q :=
 path.rec_on p (take q h, h ⬝ (concat_p1 _)) q
 
 definition moveR_1V {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
-  idp ≈ q ⬝ p → p^ ≈ q :=
+  idp ≈ q ⬝ p → p** ≈ q :=
 path.rec_on p (take q h, h ⬝ (concat_p1 _)) q
 
 definition moveR_V1 {A : Type} {x y : A} (p : x ≈ y) (q : y ≈ x) :
-  idp ≈ p ⬝ q → p^ ≈ q :=
+  idp ≈ p ⬝ q → p** ≈ q :=
 path.rec_on p (take q h, h ⬝ (concat_1p _)) q
 
 
@@ -218,19 +218,19 @@ path.rec_on p idp
 -- ---------------------------------------------------
 
 definition moveR_transport_p {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) :
-  u ≈ p^ # v → p # u ≈ v :=
+  u ≈ p** # v → p # u ≈ v :=
 path.rec_on p (take u v, id) u v
 
 definition moveR_transport_V {A : Type} (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) :
-  u ≈ p # v → p^ # u ≈ v :=
+  u ≈ p # v → p** # u ≈ v :=
 path.rec_on p (take u v, id) u v
 
 definition moveL_transport_V {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (u : P x) (v : P y) :
-  p # u ≈ v → u ≈ p^ # v :=
+  p # u ≈ v → u ≈ p** # v :=
 path.rec_on p (take u v, id) u v
 
 definition moveL_transport_p {A : Type} (P : A → Type) {x y : A} (p : y ≈ x) (u : P x) (v : P y) :
-  p^ # u ≈ v → u ≈ p # v :=
+  p** # u ≈ v → u ≈ p # v :=
 path.rec_on p (take u v, id) u v
 
 
@@ -259,10 +259,10 @@ definition ap_pp_p {A B : Type} (f : A → B) {w x y z : A} (p : x ≈ y) (q : y
 path.rec_on p (take q, path.rec_on q (take r, concat_pp_p _ _ _)) q r
 
 -- 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^) :=
+definition inverse_ap {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : (ap f p)** ≈ ap f (p**) :=
 path.rec_on p idp
 
-definition ap_V {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : ap f (p^) ≈ (ap f p)^ :=
+definition ap_V {A B : Type} (f : A → B) {x y : A} (p : x ≈ y) : ap f (p**) ≈ (ap f p)** :=
 path.rec_on p idp
 
 -- TODO: rename id to idmap?
@@ -286,21 +286,21 @@ path.rec_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) :
   (ap f q) ⬝ (p y) ≈ (p x) ⬝ (ap g q) :=
-path.rec_on q (concat_1p _ ⬝ (concat_p1 _)^)
+path.rec_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) :
   (ap f q) ⬝ (p y) ≈ (p x) ⬝ q :=
-path.rec_on q (concat_1p _ ⬝ (concat_p1 _)^)
+path.rec_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) :
   (p x) ⬝ (ap f q) ≈  q ⬝ (p y) :=
-path.rec_on q (concat_p1 _ ⬝ (concat_1p _)^)
+path.rec_on q (concat_p1 _ ⬝ (concat_1p _)**)
 
 --TODO: note that the Coq proof for the preceding is
 --
 --  match q as i in (_ ≈ y) return (p x ⬝ ap f i ≈ i ⬝ p y) with
---    | idpath => concat_p1 _ ⬝ (concat_1p _)^
+--    | idpath => concat_p1 _ ⬝ (concat_1p _)**
 --   end.
 --
 -- It is nice that we don't have to give the predicate.
@@ -324,7 +324,7 @@ definition apD10_pp {A} {B : A → Type} {f f' f'' : Πx, B x} (h : f ≈ f') (h
 path.rec_on h (take h', path.rec_on h' idp) h'
 
 definition apD10_V {A : Type} {B : A → Type} {f g : Πx : A, B x} (h : f ≈ g) (x : A) :
-  apD10 (h^) x ≈ (apD10 h x)^ :=
+  apD10 (h**) x ≈ (apD10 h x)** :=
 path.rec_on h idp
 
 definition ap10_1 {A B} {f : A → B} (x : A) : ap10 (idpath f) x ≈ idp := idp
@@ -332,7 +332,7 @@ definition ap10_1 {A B} {f : A → B} (x : A) : ap10 (idpath f) x ≈ idp := idp
 definition ap10_pp {A B} {f f' f'' : A → B} (h : f ≈ f') (h' : f' ≈ f'') (x : A) :
   ap10 (h ⬝ h') x ≈ ap10 h x ⬝ ap10 h' x := apD10_pp h h' x
 
-definition ap10_V {A B} {f g : A→B} (h : f ≈ g) (x:A) : ap10 (h^) x ≈ (ap10 h x)^ := apD10_V h x
+definition ap10_V {A B} {f g : A→B} (h : f ≈ g) (x:A) : ap10 (h**) x ≈ (ap10 h x)** := apD10_V h x
 
 -- [ap10] also behaves nicely on paths produced by [ap]
 definition ap_ap10 {A B C} (f g : A → B) (h : B → C) (p : f ≈ g) (a : A) :
@@ -352,12 +352,12 @@ definition transport_pp {A : Type} (P : A → Type) {x y z : A} (p : x ≈ y) (q
 path.rec_on q (path.rec_on p idp)
 
 definition transport_pV {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P y) :
-  p # p^ # z ≈ z :=
-(transport_pp P (p^) p z)^ ⬝ ap (λr, transport P r z) (concat_Vp p)
+  p # p** # z ≈ z :=
+(transport_pp P (p**) p z)** ⬝ ap (λr, transport P r z) (concat_Vp p)
 
 definition transport_Vp {A : Type} (P : A → Type) {x y : A} (p : x ≈ y) (z : P x) :
-  p^ # p # z ≈ z :=
-(transport_pp P p (p^) z)^ ⬝ ap (λr, transport P r z) (concat_pV p)
+  p** # p # z ≈ z :=
+(transport_pp P p (p**) z)** ⬝ ap (λr, transport P r z) (concat_pV p)
 
 
 -----------------------------------------------
@@ -392,7 +392,7 @@ theorem triple_induction
 path.rec_on p (take z q, path.rec_on q (take w r, path.rec_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 :=
+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
 
 definition transport_p_pp {A : Type} (P : A → Type)
@@ -431,14 +431,14 @@ path.rec_on r1 (path.rec_on r2 idp)
 
 -- TODO: another interesting case
 definition transport2_V {A : Type} (Q : A → Type) {x y : A} {p q : x ≈ y} (r : p ≈ q) (z : Q x) :
-  transport2 Q (r^) z ≈ ((transport2 Q r z)^) :=
+  transport2 Q (r**) z ≈ ((transport2 Q r z)**) :=
 -- path.rec_on r idp -- doesn't work
 path.rec_on r (idpath (inverse (transport2 Q (idpath p) z)))
 
 definition concat_AT {A : Type} (P : A → Type) {x y : A} {p q : x ≈ y} {z w : P x} (r : p ≈ q)
     (s : z ≈ w) :
   ap (transport P p) s  ⬝  transport2 P r w ≈ transport2 P r z  ⬝  ap (transport P q) s :=
-path.rec_on r (concat_p1 _ ⬝ (concat_1p _)^)
+path.rec_on r (concat_p1 _ ⬝ (concat_1p _)**)
 
 -- TODO (from Coq library): What should this be called?
 definition ap_transport {A} {P Q : A → Type} {x y : A} (p : x ≈ y) (f : Πx, P x → Q x) (z : P x) :
@@ -465,7 +465,7 @@ path.rec_on p idp
 
 definition transport2_const {A B : Type} {x1 x2 : A} {p q : x1 ≈ x2} (r : p ≈ q) (y : B) :
   transport_const p y ≈ transport2 (λu, B) r y ⬝ transport_const q y :=
-path.rec_on r (concat_1p _)^
+path.rec_on r (concat_1p _)**
 
 -- Transporting in a pulled back fibration.
 definition transport_compose {A B} {x y : A} (P : B → Type) (f : A → B) (p : x ≈ y) (z : P (f x)) :
@@ -511,7 +511,7 @@ path.rec_on h (path.rec_on h' idp)
 infixl `⬝⬝`:75 := concat2
 
 -- 2-dimensional path inversion
-definition inverse2 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : p^ ≈ q^ :=
+definition inverse2 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) : p** ≈ q** :=
 path.rec_on h idp
 
 -- Whiskering
@@ -528,7 +528,7 @@ h ⬝⬝ idp
 -- -------------------------------
 
 definition cancelL {A} {x y z : A} (p : x ≈ y) (q r : y ≈ z) : (p ⬝ q ≈ p ⬝ r) → (q ≈ r) :=
-path.rec_on p (take r, path.rec_on r (take q a, (concat_1p q)^ ⬝ a)) r q
+path.rec_on p (take r, path.rec_on r (take q a, (concat_1p q)** ⬝ a)) r q
 
 definition cancelR {A} {x y z : A} (p q : x ≈ y) (r : y ≈ z) : (p ⬝ r ≈ q ⬝ r) → (p ≈ q) :=
 path.rec_on r (take p, path.rec_on p (take q a, a ⬝ concat_p1 q)) p q
@@ -536,7 +536,7 @@ path.rec_on r (take p, path.rec_on p (take q a, a ⬝ concat_p1 q)) p q
 -- Whiskering and identity paths.
 
 definition whiskerR_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
-  (concat_p1 p)^ ⬝ whiskerR h idp ⬝ concat_p1 q ≈ h :=
+  (concat_p1 p)** ⬝ whiskerR h idp ⬝ concat_p1 q ≈ h :=
 path.rec_on h (path.rec_on p idp)
 
 definition whiskerR_1p {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
@@ -548,7 +548,7 @@ definition whiskerL_p1 {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
 path.rec_on q idp
 
 definition whiskerL_1p {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
-  (concat_1p p) ^ ⬝ whiskerL idp h ⬝ concat_1p q ≈ h :=
+  (concat_1p p) ** ⬝ whiskerL idp h ⬝ concat_1p q ≈ h :=
 path.rec_on h (path.rec_on p idp)
 
 definition concat2_p1 {A : Type} {x y : A} {p q : x ≈ y} (h : p ≈ q) :
@@ -568,7 +568,7 @@ path.rec_on d (path.rec_on c (path.rec_on b (path.rec_on a idp)))
 
 definition concat_whisker {A} {x y z : A} (p p' : x ≈ y) (q q' : y ≈ z) (a : p ≈ p') (b : q ≈ q') :
   (whiskerR a q) ⬝ (whiskerL p' b) ≈ (whiskerL p b) ⬝ (whiskerR a q') :=
-path.rec_on b (path.rec_on a (concat_1p _)^)
+path.rec_on b (path.rec_on a (concat_1p _)**)
 
 -- Structure corresponding to the coherence equations of a bicategory.
 
@@ -586,12 +586,12 @@ definition triangulator {A : Type} {x y z : A} (p : x ≈ y) (q : y ≈ z) :
 path.rec_on p (take q, path.rec_on q idp) q
 
 definition eckmann_hilton {A : Type} {x:A} (p q : idp ≈ idp :> (x ≈ x)) : p ⬝ q ≈ q ⬝ p :=
-  (whiskerR_p1 p ⬝⬝ whiskerL_1p q)^
+  (whiskerR_p1 p ⬝⬝ whiskerL_1p q)**
   ⬝ (concat_p1 _ ⬝⬝ concat_p1 _)
   ⬝ (concat_1p _ ⬝⬝ concat_1p _)
   ⬝ (concat_whisker _ _ _ _ p q)
-  ⬝ (concat_1p _ ⬝⬝ concat_1p _)^
-  ⬝ (concat_p1 _ ⬝⬝ concat_p1 _)^
+  ⬝ (concat_1p _ ⬝⬝ concat_1p _)**
+  ⬝ (concat_p1 _ ⬝⬝ concat_p1 _)**
   ⬝ (whiskerL_1p q ⬝⬝ whiskerR_p1 p)
 
 
@@ -607,10 +607,10 @@ definition ap02_p2p {A B} (f : A→B) {x y z : A} {p p' : x ≈ y} {q q' :y ≈
     (s : q ≈ q') :
   ap02 f (r ⬝⬝ s) ≈   ap_pp f p q
                       ⬝ (ap02 f r  ⬝⬝  ap02 f s)
-                      ⬝ (ap_pp f p' q')^ :=
+                      ⬝ (ap_pp f p' q')** :=
 path.rec_on r (path.rec_on s (path.rec_on q (path.rec_on p idp)))
 
 definition apD02 {A : Type} {B : A → Type} {x y : A} {p q : x ≈ y} (f : Π x, B x) (r : p ≈ q) :
   apD f p ≈ transport2 B r (f x) ⬝ apD f q :=
-path.rec_on r (concat_1p _)^
+path.rec_on r (concat_1p _)**
 end path