diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
index bd1d19d3c..3214923be 100644
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@@ -40,7 +40,7 @@ empty.rec _ H
 /- eq -/
 
 infix = := eq
-definition rfl {A : Type} {a : A} := eq.refl a
+definition rfl [constructor] {A : Type} {a : A} := eq.refl a
 
 /-
   These notions are here only to make porting from the standard library easier.
diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index bece16eb6..cce40ab90 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -567,7 +567,7 @@ namespace eq
 
   -- 2-dimensional path inversion
   definition inverse2 [unfold 6] {p q : x = y} (h : p = q) : p⁻¹ = q⁻¹ :=
-  eq.rec_on h idp
+  ap inverse h
 
   infixl ` ◾ `:75 := concat2
   postfix [parsing_only] `⁻²`:(max+10) := inverse2 --this notation is abusive, should we use it?
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index 9e511575b..2b7d46d35 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -331,7 +331,7 @@ namespace pointed
     { exact !to_homotopy_pt⁻¹}
   end
 
-  definition pwhisker_left (h : B →* C) (p : f ~* g) : h ∘* f ~* h ∘* g :=
+  definition pwhisker_left [constructor] (h : B →* C) (p : f ~* g) : h ∘* f ~* h ∘* g :=
   begin
     fconstructor,
     { intro a, exact ap h (p a)},
@@ -340,7 +340,7 @@ namespace pointed
       induction p with p p', esimp at *, induction ph, induction pg, induction p', reflexivity}
   end
 
-  definition pwhisker_right (h : C →* A) (p : f ~* g) : f ∘* h ~* g ∘* h :=
+  definition pwhisker_right [constructor] (h : C →* A) (p : f ~* g) : f ∘* h ~* g ∘* h :=
   begin
     fconstructor,
     { intro a, exact p (h a)},
@@ -362,7 +362,7 @@ namespace pointed
     pequiv A B :=
   pequiv.mk to_pmap is_equiv_to_pmap
 
-  definition pequiv_of_equiv [constructor] 
+  definition pequiv_of_equiv [constructor]
     (eqv : A ≃ B) (resp : equiv.to_fun eqv (point A) = point B) : A ≃* B :=
   pequiv.mk' (pmap.mk (equiv.to_fun eqv) resp)