fix(hott): small fixes after rebasing

hott/algebra/category/nat_trans.hlean

@@ -182,7 +182,7 @@ namespace nat_trans
   nat_trans.mk (λc, hom_of_eq (ap010 to_fun_ob p c))
                (λa b f, eq.rec_on p (!id_right ⬝ !id_left⁻¹))
 
-  definition compose_rev [unfold-full] (θ : F ⟹ G) (η : G ⟹ H) : F ⟹ H := η ∘n θ
+  definition compose_rev [unfold_full] (θ : F ⟹ G) (η : G ⟹ H) : F ⟹ H := η ∘n θ
 
 end nat_trans
 

hott/algebra/category/precategory.hlean

@@ -35,7 +35,7 @@ namespace category
 
   infixr ∘ := precategory.comp
   -- input ⟶ using \--> (this is a different arrow than \-> (→))
-  infixl [parsing_only] ` ⟶ `:25 := precategory.hom
+  infixl [parsing_only] ` ⟶ `:60 := precategory.hom
   namespace hom
     infixl ` ⟶ `:60 := precategory.hom -- if you open this namespace, hom a b is printed as a ⟶ b
   end hom

hott/init/types.hlean

@@ -51,7 +51,7 @@ end sigma
 namespace sum
   infixr ⊎ := sum
   infixr + := sum
-  infixr [parsing-only] `+t`:25 := sum -- notation which is never overloaded
+  infixr [parsing_only] `+t`:25 := sum -- notation which is never overloaded
   namespace low_precedence_plus
     reserve infixr ` + `:25  -- conflicts with notation for addition
     infixr ` + ` := sum
@@ -84,7 +84,7 @@ namespace prod
   -- notation for n-ary tuples
   notation `(` h `, ` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
   infixr × := prod
-  infixr [parsing-only] `×t`:30 := prod -- notation which is never overloaded
+  infixr [parsing_only] `×t`:30 := prod -- notation which is never overloaded
 
   namespace ops
   infixr [parsing_only] * := prod