diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean
index 8aa783b23..b6407dc16 100644
--- a/hott/algebra/category/constructions/functor.hlean
+++ b/hott/algebra/category/constructions/functor.hlean
@@ -124,7 +124,7 @@ namespace category
         esimp [eq_of_iso_ob, inv_of_eq, hom_of_eq, eq_of_iso],
         rewrite [*right_inv iso_of_eq],
         esimp [function.id],
-        symmetry, apply naturality_iso
+        symmetry, apply @naturality_iso _ _ _ _ _ (iso.struct _)
       }
     end
 
diff --git a/hott/algebra/category/constructions/hset.hlean b/hott/algebra/category/constructions/hset.hlean
index ecca369eb..819dde294 100644
--- a/hott/algebra/category/constructions/hset.hlean
+++ b/hott/algebra/category/constructions/hset.hlean
@@ -33,10 +33,11 @@ namespace category
            (eq_of_homotopy (right_inv (to_fun f)))
 
     definition equiv_of_iso {A B : Precategory_hset} (f : A ≅ B) : A ≃ B :=
-    equiv.MK (to_hom f)
-             (iso.to_inv f)
-             (ap10 (right_inverse (to_hom f)))
-             (ap10 (left_inverse  (to_hom f)))
+    begin
+      apply equiv.MK (to_hom f) (iso.to_inv f),
+       exact ap10 (right_inverse (to_hom f)),
+       exact ap10 (left_inverse  (to_hom f))
+    end
 
     definition is_equiv_iso_of_equiv (A B : Precategory_hset) : is_equiv (@iso_of_equiv A B) :=
     adjointify _ (λf, equiv_of_iso f)
@@ -61,12 +62,12 @@ namespace category
 
     definition equiv_equiv_iso (A B : Precategory_hset) : (A ≃ B) ≃ (A ≅ B) :=
     equiv.MK (λf, iso_of_equiv f)
-             (λf, equiv.MK (to_hom f)
+             (λf, proof equiv.MK (to_hom f)
                            (iso.to_inv f)
                            (ap10 (right_inverse (to_hom f)))
-                           (ap10 (left_inverse  (to_hom f))))
-             (λf, iso_eq idp)
-             (λf, equiv_eq idp)
+                           (ap10 (left_inverse  (to_hom f))) qed)
+             (λf, proof iso_eq idp qed)
+             (λf, proof equiv_eq idp qed)
 
     definition equiv_eq_iso (A B : Precategory_hset) : (A ≃ B) = (A ≅ B) :=
     ua !equiv_equiv_iso
diff --git a/hott/algebra/category/constructions/opposite.hlean b/hott/algebra/category/constructions/opposite.hlean
index 62ce724c1..93a0f47f1 100644
--- a/hott/algebra/category/constructions/opposite.hlean
+++ b/hott/algebra/category/constructions/opposite.hlean
@@ -29,7 +29,8 @@ namespace category
 
   variables {C : Precategory} {a b c : C}
 
-  definition compose_op {f : hom a b} {g : hom b c} : f ∘op g = g ∘ f := idp
+  definition compose_op {f : hom a b} {g : hom b c} : f ∘op g = g ∘ f :=
+  by reflexivity
 
   definition opposite_opposite' {ob : Type} (C : precategory ob) : opposite (opposite C) = C :=
   by cases C; apply idp
diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean
index 5ee35dac4..794d8341d 100644
--- a/hott/algebra/category/nat_trans.hlean
+++ b/hott/algebra/category/nat_trans.hlean
@@ -100,18 +100,18 @@ namespace nat_trans
 
   definition nf_fn_eq_fn_nf (η : F ⟹ G) (θ : F' ⟹ G')
     : (θ ∘nf G) ∘n (F' ∘fn η) = (G' ∘fn η) ∘n (θ ∘nf F) :=
-  nat_trans_eq (λc, !nf_fn_eq_fn_nf_pt)
+  nat_trans_eq (λ c, nf_fn_eq_fn_nf_pt η θ c)
 
   definition fn_n_distrib (F' : D ⇒ E) (η : G ⟹ H) (θ : F ⟹ G)
     : F' ∘fn (η ∘n θ) = (F' ∘fn η) ∘n (F' ∘fn θ) :=
-  nat_trans_eq (λc, !respect_comp)
+  nat_trans_eq (λc, by apply respect_comp)
 
   definition n_nf_distrib (η : G ⟹ H) (θ : F ⟹ G) (F' : B ⇒ C)
     : (η ∘n θ) ∘nf F' = (η ∘nf F') ∘n (θ ∘nf F') :=
   nat_trans_eq (λc, idp)
 
   definition fn_id (F' : D ⇒ E) : F' ∘fn nat_trans.ID F = nat_trans.id :=
-  nat_trans_eq (λc, !respect_id)
+  nat_trans_eq (λc, by apply respect_id)
 
   definition id_nf (F' : B ⇒ C) : nat_trans.ID F ∘nf F' = nat_trans.id :=
   nat_trans_eq (λc, idp)
diff --git a/hott/algebra/category/yoneda.hlean b/hott/algebra/category/yoneda.hlean
index d7460aeac..2fdb50d06 100644
--- a/hott/algebra/category/yoneda.hlean
+++ b/hott/algebra/category/yoneda.hlean
@@ -22,18 +22,15 @@ namespace yoneda
       ... = _                          : by rewrite (assoc f2 f3 f4)
 
   definition hom_functor (C : Precategory) : Cᵒᵖ ×c C ⇒ set :=
-  functor.mk (λ(x : Cᵒᵖ ×c C), homset x.1 x.2)
-             (λ(x y : Cᵒᵖ ×c C) (f : _) (h : homset x.1 x.2), f.2 ∘⁅ C ⁆ (h ∘⁅ C ⁆ f.1))
-             begin
-               intro x, apply eq_of_homotopy, intro h, exact (!id_left ⬝ !id_right)
-             end
-             begin
-               intro x y z g f, apply eq_of_homotopy, intro h,
-               exact (representable_functor_assoc g.2 f.2 h f.1 g.1),
-             end
+  functor.mk
+    (λ (x : Cᵒᵖ ×c C), @homset (Cᵒᵖ) C x.1 x.2)
+    (λ (x y : Cᵒᵖ ×c C) (f : @category.precategory.hom (Cᵒᵖ ×c C) (Cᵒᵖ ×c C) x y) (h : @homset (Cᵒᵖ) C x.1 x.2),
+       f.2 ∘⁅ C ⁆ (h ∘⁅ C ⁆ f.1))
+    (λ x, @eq_of_homotopy _ _ _ (ID (@homset Cᵒᵖ C x.1 x.2)) (λ h, concat (by apply @id_left) (by apply @id_right)))
+    (λ x y z g f,
+       eq_of_homotopy (by intros; apply @representable_functor_assoc))
 end yoneda
 
-
 open is_equiv equiv
 
 namespace functor
@@ -51,15 +48,18 @@ namespace functor
   local abbreviation Fob := @functor_curry_ob
 
   definition functor_curry_hom ⦃c c' : C⦄ (f : c ⟶ c') : Fob F c ⟹ Fob F c' :=
-  nat_trans.mk (λd, F (f, id))
-               (λd d' g, calc
-                 F (id, g) ∘ F (f, id) = F (id ∘ f, g ∘ id) : respect_comp F
+  begin
+    fapply @nat_trans.mk,
+      {intro d, exact F (f, id)},
+      {intro d d' g, calc
+        F (id, g) ∘ F (f, id) = F (id ∘ f, g ∘ id) : respect_comp F
                    ... = F (f, g ∘ id)         : by rewrite id_left
                    ... = F (f, g)              : by rewrite id_right
                    ... = F (f ∘ id, g)         : by rewrite id_right
                    ... = F (f ∘ id, id ∘ g)    : by rewrite id_left
-                   ... = F (f, id) ∘ F (id, g) :  (respect_comp F (f, id) (id, g))⁻¹ᵖ)
-
+                   ... = F (f, id) ∘ F (id, g) : (respect_comp F (f, id) (id, g))⁻¹ᵖ
+        }
+  end
   local abbreviation Fhom := @functor_curry_hom
 
   theorem functor_curry_hom_def ⦃c c' : C⦄ (f : c ⟶ c') (d : D) :
@@ -70,12 +70,15 @@ namespace functor
 
   theorem functor_curry_comp ⦃c c' c'' : C⦄ (f' : c' ⟶ c'') (f : c ⟶ c')
     : Fhom F (f' ∘ f) = Fhom F f' ∘n Fhom F f :=
-  nat_trans_eq (λd, calc
+  begin
+    apply @nat_trans_eq,
+    intro d, calc
     natural_map (Fhom F (f' ∘ f)) d = F (f' ∘ f, id) : by rewrite functor_curry_hom_def
       ... = F (f' ∘ f, id ∘ id)                      : by rewrite id_comp
       ... = F ((f',id) ∘ (f, id))                    : by esimp
       ... = F (f',id) ∘ F (f, id)                    : by rewrite [respect_comp F]
-      ... = natural_map ((Fhom F f') ∘ (Fhom F f)) d : by esimp)
+      ... = natural_map ((Fhom F f') ∘ (Fhom F f)) d : by esimp
+  end
 
   definition functor_curry [reducible] : C ⇒ E ^c D :=
   functor.mk (functor_curry_ob F)
diff --git a/hott/init/datatypes.hlean b/hott/init/datatypes.hlean
index 15416c0b8..8b8ea04bf 100644
--- a/hott/init/datatypes.hlean
+++ b/hott/init/datatypes.hlean
@@ -28,8 +28,16 @@ refl : eq a a
 structure lift.{l₁ l₂} (A : Type.{l₁}) : Type.{max l₁ l₂} :=
 up :: (down : A)
 
-structure prod (A B : Type) :=
-mk :: (pr1 : A) (pr2 : B)
+inductive prod (A B : Type) :=
+mk : A → B → prod A B
+
+definition prod.pr1 [reducible] [unfold-c 3] {A B : Type} (p : prod A B) : A :=
+prod.rec (λ a b, a) p
+
+definition prod.pr2 [reducible] [unfold-c 3] {A B : Type} (p : prod A B) : B :=
+prod.rec (λ a b, b) p
+
+definition prod.destruct [reducible] := @prod.cases_on
 
 inductive sum (A B : Type) : Type :=
 | inl {} : A → sum A B
@@ -41,8 +49,14 @@ sum.inl a
 definition sum.intro_right [reducible] (A : Type) {B : Type} (b : B) : sum A B :=
 sum.inr b
 
-structure sigma {A : Type} (B : A → Type) :=
-mk :: (pr1 : A) (pr2 : B pr1)
+inductive sigma {A : Type} (B : A → Type) :=
+mk : Π (a : A), B a → sigma B
+
+definition sigma.pr1 [reducible] [unfold-c 3] {A : Type} {B : A → Type} (p : sigma B) : A :=
+sigma.rec (λ a b, a) p
+
+definition sigma.pr2 [reducible] [unfold-c 3] {A : Type} {B : A → Type} (p : sigma B) : B (sigma.pr1 p) :=
+sigma.rec (λ a b, b) p
 
 -- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
 -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index 5759be360..6bd67e46e 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -103,7 +103,7 @@ namespace is_trunc
   contr_internal.center (is_trunc.to_internal -2 A)
 
   definition center_eq [H : is_contr A] (a : A) : !center = a :=
-  contr_internal.center_eq !is_trunc.to_internal a
+  contr_internal.center_eq (is_trunc.to_internal -2 A) a
 
   definition eq_of_is_contr [H : is_contr A] (x y : A) : x = y :=
   (center_eq x)⁻¹ ⬝ (center_eq y)
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index a017bcb58..0710de320 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -17,6 +17,8 @@ namespace sigma
             {D : Πa b, C a b → Type}
             {a a' a'' : A} {b b₁ b₂ : B a} {b' : B a'} {b'' : B a''} {u v w : Σa, B a}
 
+  definition destruct := @sigma.cases_on
+
   protected definition eta : Π (u : Σa, B a), ⟨u.1 , u.2⟩ = u
   | eta ⟨u₁, u₂⟩ := idp