fix(init/equiv): make transport not an instance

hott/init/equiv.hlean

@@ -41,7 +41,7 @@ namespace is_equiv
   protected abbreviation mk [constructor] := @is_equiv.mk' A B f
 
   -- The identity function is an equivalence.
-  definition is_equiv_id (A : Type) : (is_equiv (id : A → A)) :=
+  definition is_equiv_id [instance] (A : Type) : (is_equiv (id : A → A)) :=
   is_equiv.mk id id (λa, idp) (λa, idp) (λa, idp)
 
   -- The composition of two equivalences is, again, an equivalence.
@@ -218,7 +218,7 @@ namespace is_equiv
   end
 
   --Transporting is an equivalence
-  definition is_equiv_tr [instance] [constructor] {A : Type} (P : A → Type) {x y : A}
+  definition is_equiv_tr [constructor] {A : Type} (P : A → Type) {x y : A}
     (p : x = y) : (is_equiv (transport P p)) :=
   is_equiv.mk _ (transport P p⁻¹) (tr_inv_tr p) (inv_tr_tr p) (tr_inv_tr_lemma p)
 
@@ -245,6 +245,8 @@ end is_equiv
 open is_equiv
 
 namespace eq
+  local attribute is_equiv_tr [instance]
+
   definition tr_inv_fn {A : Type} {B : A → Type} {a a' : A} (p : a = a') :
     transport B p⁻¹ = (transport B p)⁻¹ := idp
   definition tr_inv {A : Type} {B : A → Type} {a a' : A} (p : a = a') (b : B a') :

hott/types/equiv.hlean

@@ -23,7 +23,7 @@ namespace is_equiv
         right_inv f b = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ((ap (f ∘ f⁻¹) p) ⬝ right_inv f b)
                                                            : by rewrite inv_con_cancel_left
       ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (right_inv f (f a) ⬝ p)   : by rewrite ap_con_eq_con
-      ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p) : by rewrite adj
+      ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ (ap f (left_inv f a) ⬝ p) : by rewrite [adj f]
       ... = (ap (f ∘ f⁻¹) p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p   : by rewrite con.assoc
       ... = (ap f (ap f⁻¹ p))⁻¹ ⬝ ap f (left_inv f a) ⬝ p  : by rewrite ap_compose
       ... = ap f (ap f⁻¹ p)⁻¹ ⬝ ap f (left_inv f a) ⬝ p    : by rewrite ap_inv