diff --git a/hott/algebra/category/basic.hlean b/hott/algebra/category/basic.hlean
index ce7bb5a568..91ba7f3cce 100644
--- a/hott/algebra/category/basic.hlean
+++ b/hott/algebra/category/basic.hlean
@@ -36,7 +36,7 @@ namespace category
   -- TODO: Unsafe class instance?
   attribute iso_of_path_equiv [instance]
 
-  definition eq_of_iso {a b : ob} : a ≅ b → a = b :=
+  definition eq_of_iso [reducible] {a b : ob} : a ≅ b → a = b :=
   iso_of_eq⁻¹ᵉ
 
   set_option apply.class_instance false -- disable class instance resolution in the apply tactic
diff --git a/hott/algebra/category/constructions.hlean b/hott/algebra/category/constructions.hlean
index 8115b37df1..3c263555ab 100644
--- a/hott/algebra/category/constructions.hlean
+++ b/hott/algebra/category/constructions.hlean
@@ -93,9 +93,9 @@ namespace category
 
     definition eq_of_iso_functor (η : F ≅ G) : F = G :=
     begin
-    fapply functor_eq_mk,
+    fapply functor_eq,
       {exact (eq_of_iso_functor_ob η)},
-      {intros (c, c', f),
+      {intros (c, c', f), --unfold eq_of_iso_functor_ob, --TODO: report: this fails
         apply concat,
           {apply (ap (λx, to_hom x ∘ to_fun_hom F f ∘ _)), apply (retr iso_of_eq)},
         apply concat,
@@ -107,33 +107,42 @@ namespace category
     -- definition is_univalent_functor (C : Precategory) (D : Category) : is_univalent (D ^c C) :=
     -- λ(F G : D ^c C), adjointify _ eq_of_iso_functor sorry sorry
 
---    definition iso_of_hom
-
     definition iso_of_eq_eq_of_iso_functor (η : F ≅ G) : iso_of_eq (eq_of_iso_functor η) = η :=
     begin
     apply iso.eq_mk,
     apply nat_trans_eq_mk,
     intro c,
-    apply concat, apply natural_map_hom_of_eq,
-    apply concat, {apply (ap hom_of_eq), apply ap010_functor_eq_mk},
-    apply concat, {apply (ap to_hom), apply (retr iso_of_eq)},
-    apply idp
-    end
---check natural_map_
-    definition eq_of_iso_functor_iso_of_eq (p : F = G) : eq_of_iso_functor (iso_of_eq p) = p :=
-    begin
-    apply sorry
+    rewrite natural_map_hom_of_eq, esimp {eq_of_iso_functor},
+    rewrite ap010_functor_eq, esimp {hom_of_eq,eq_of_iso_functor_ob},
+    rewrite (retr iso_of_eq),
     end
 
-    definition is_univalent_functor (C : Precategory) (D : Category) : is_univalent (D ^c C) :=
+    definition eq_of_iso_functor_iso_of_eq (p : F = G) : eq_of_iso_functor (iso_of_eq p) = p :=
+    begin
+    apply functor_eq2,
+    intro c,
+    esimp {eq_of_iso_functor},
+    rewrite ap010_functor_eq,
+    esimp {eq_of_iso_functor_ob},
+    rewrite componentwise_iso_iso_of_eq,
+    rewrite (sect iso_of_eq)
+    end
+
+    definition is_univalent_functor (D : Category) (C : Precategory) : is_univalent (D ^c C) :=
     λF G, adjointify _ eq_of_iso_functor
                        iso_of_eq_eq_of_iso_functor
                        eq_of_iso_functor_iso_of_eq
 
   end functor
 
+  definition Category_functor_of_precategory (D : Category) (C : Precategory) : Category :=
+  category.MK (D ^c C) (is_univalent_functor D C)
 
-  definition category_functor (C : Precategory) (D : Category) : Category :=
-  category.MK (D ^c C) (is_univalent_functor C D)
+  definition Category_functor (D : Category) (C : Category) : Category :=
+  Category_functor_of_precategory D C
+
+  namespace ops
+    infixr `^c2`:35 := Category_functor
+  end ops
 
 end category
diff --git a/hott/algebra/precategory/basic.hlean b/hott/algebra/precategory/basic.hlean
index 17131420ba..63575e9b19 100644
--- a/hott/algebra/precategory/basic.hlean
+++ b/hott/algebra/precategory/basic.hlean
@@ -47,7 +47,8 @@ namespace category
 
     definition id_comp (a : ob) : ID a ∘ ID a = ID a := !id_left
 
-    definition id_leftright (f : hom a b) : id ∘ f ∘ id = f := !id_left ⬝ !id_right
+    definition id_leftright       (f : hom a b) : id ∘ f ∘ id = f := !id_left ⬝ !id_right
+    definition comp_id_eq_id_comp (f : hom a b) : f ∘ id = id ∘ f := !id_right ⬝ !id_left⁻¹
 
     definition left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id :=
     calc i = i ∘ id : by rewrite id_right
diff --git a/hott/algebra/precategory/constructions.hlean b/hott/algebra/precategory/constructions.hlean
index 67dd3e3c23..966d985416 100644
--- a/hott/algebra/precategory/constructions.hlean
+++ b/hott/algebra/precategory/constructions.hlean
@@ -244,6 +244,13 @@ namespace category
     @iso.mk _ _ _ _ (natural_map (to_hom η) c)
                     (@componentwise_is_iso _ _ _ _ (to_hom η) (struct η) c)
 
+    definition componentwise_iso_id (c : C) : componentwise_iso (iso.refl F) c = iso.refl (F c) :=
+    iso.eq_mk (idpath id)
+
+    definition componentwise_iso_iso_of_eq (p : F = G) (c : C)
+      : componentwise_iso (iso_of_eq p) c = iso_of_eq (ap010 to_fun_ob p c) :=
+    eq.rec_on p !componentwise_iso_id
+
     definition natural_map_hom_of_eq (p : F = G) (c : C)
       : natural_map (hom_of_eq p) c = hom_of_eq (ap010 to_fun_ob p c) :=
     eq.rec_on p idp
diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean
index e4d493475a..f11dc65f58 100644
--- a/hott/algebra/precategory/functor.hlean
+++ b/hott/algebra/precategory/functor.hlean
@@ -21,7 +21,7 @@ structure functor (C D : Precategory) : Type :=
 namespace functor
 
   infixl `⇒`:25 := functor
-  variables {C D E : Precategory}
+  variables {A B C D E : Precategory}
 
   attribute to_fun_ob [coercion]
   attribute to_fun_hom [coercion]
@@ -46,17 +46,22 @@ namespace functor
 
   protected definition ID [reducible] (C : Precategory) : functor C C := id
 
-  definition functor_eq_mk'' {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
+  definition functor_mk_eq' {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
     {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂)
     (pF : F₁ = F₂) (pH : pF ▹ H₁ = H₂)
       : functor.mk F₁ H₁ id₁ comp₁ = functor.mk F₂ H₂ id₂ comp₂ :=
   apD01111 functor.mk pF pH !is_hprop.elim !is_hprop.elim
 
-  definition functor_eq_mk' {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
+  definition functor_eq' {F₁ F₂ : C ⇒ D}
+    : Π(p : to_fun_ob F₁ = to_fun_ob F₂),
+          (transport (λx, Πa b f, hom (x a) (x b)) p (to_fun_hom F₁) = to_fun_hom F₂) → F₁ = F₂ :=
+  functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_mk_eq'))
+
+  definition functor_mk_eq {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
     {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂) (pF : F₁ ∼ F₂)
     (pH : Π(a b : C) (f : hom a b), hom_of_eq (pF b) ∘ H₁ a b f ∘ inv_of_eq (pF a) = H₂ a b f)
       : functor.mk F₁ H₁ id₁ comp₁ = functor.mk F₂ H₂ id₂ comp₂ :=
-  functor_eq_mk'' id₁ id₂ comp₁ comp₂ (eq_of_homotopy pF)
+  functor_mk_eq' id₁ id₂ comp₁ comp₂ (eq_of_homotopy pF)
     (eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (λf,
       begin
         apply concat, rotate_left 1, exact (pH c c' f),
@@ -72,26 +77,35 @@ namespace functor
         apply idp
       end))))
 
-  definition functor_eq_mk_constant {F : C → D} {H₁ : Π(a b : C), hom a b → hom (F a) (F b)}
+  -- definition functor_mk_eq_constant {F : C → D} {H₁ : Π(a b : C), hom a b → hom (F a) (F b)}
+  --   {H₂ : Π(a b : C), hom a b → hom (F a) (F b)} (id₁ id₂ comp₁ comp₂)
+  --   (pH : Π(a b : C) (f : hom a b), H₁ a b f = H₂ a b f)
+  --     : functor.mk F H₁ id₁ comp₁ = functor.mk F H₂ id₂ comp₂ :=
+  -- functor_mk_eq' id₁ id₂ comp₁ comp₂ idp
+  --                 (eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (pH c c'))))
+
+  definition functor_eq {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ ∼ to_fun_ob F₂),
+    (Π(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a) = F₂ f) → F₁ = F₂ :=
+  functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_mk_eq))
+
+  definition functor_mk_eq_constant {F : C → D} {H₁ : Π(a b : C), hom a b → hom (F a) (F b)}
     {H₂ : Π(a b : C), hom a b → hom (F a) (F b)} (id₁ id₂ comp₁ comp₂)
     (pH : Π(a b : C) (f : hom a b), H₁ a b f = H₂ a b f)
       : functor.mk F H₁ id₁ comp₁ = functor.mk F H₂ id₂ comp₂ :=
-  functor_eq_mk'' id₁ id₂ comp₁ comp₂ idp
-                  (eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (pH c c'))))
+  functor_eq (λc, idp) (λa b f, !id_leftright ⬝ !pH)
 
-  definition functor_eq_mk {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ ∼ to_fun_ob F₂),
-    (Π(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a) = F₂ f) → F₁ = F₂ :=
-  functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_eq_mk'))
-
-  protected definition assoc {A B C D : Precategory} (H : functor C D) (G : functor B C) (F : functor A B) :
+  protected definition assoc (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
       H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
-  !functor_eq_mk_constant (λa b f, idp)
+  !functor_mk_eq_constant (λa b f, idp)
 
-  protected definition id_left  (F : functor C D) : id ∘f F = F :=
-  functor.rec_on F (λF1 F2 F3 F4, !functor_eq_mk_constant (λa b f, idp))
+  protected definition id_left  (F : C ⇒ D) : id ∘f F = F :=
+  functor.rec_on F (λF1 F2 F3 F4, !functor_mk_eq_constant (λa b f, idp))
 
-  protected definition id_right (F : functor C D) : F ∘f id = F :=
-  functor.rec_on F (λF1 F2 F3 F4, !functor_eq_mk_constant (λa b f, idp))
+  protected definition id_right (F : C ⇒ D) : F ∘f id = F :=
+  functor.rec_on F (λF1 F2 F3 F4, !functor_mk_eq_constant (λa b f, idp))
+
+  protected definition comp_id_eq_id_comp (F : C ⇒ D) : F ∘f functor.id = functor.id ∘f F :=
+  !functor.id_right ⬝ !functor.id_left⁻¹
 
   set_option apply.class_instance false
   -- "functor C D" is equivalent to a certain sigma type
@@ -136,39 +150,75 @@ namespace functor
        apply is_trunc_eq, apply is_trunc_succ, apply !homH},
   end
 
-  definition functor_eq_eta' {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂}
-    (p : functor.mk ob₁ hom₁ id₁ comp₁ = functor.mk ob₂ hom₂ id₂ comp₂)
-      : p = p := --functor_eq_mk' _ _ _ _ (ap010 to_fun_ob p) _ :=
-  sorry
+--STRANGE ERROR:
+  -- definition functor_mk_eq'_idp {F₁ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
+  --   (id₁ id₂ comp₁ comp₂) : functor_mk_eq' id₁ id₂ comp₁ comp₂ idp idp = idp :=
+  -- sorry
+
+  definition functor_mk_eq'_idp (F : C → D) (H : Π(a b : C), hom a b → hom (F a) (F b))
+    (id comp) : functor_mk_eq' id id comp comp (idpath F) (idpath H) = idp :=
+  begin
+    fapply (apD011 (apD01111 functor.mk idp idp)),
+    apply is_hset.elim,
+    apply is_hset.elim
+  end
+
+  definition functor_eq'_idp (F : C ⇒ D) : functor_eq' idp idp = (idpath F) :=
+  by (cases F; apply functor_mk_eq'_idp)
+
+  --TODO: do we want a similar theorem for functor_eq?
+  definition functor_eq_eta' {F₁ F₂ : C ⇒ D} (p : F₁ = F₂)
+      : functor_eq' (ap to_fun_ob p) (!transport_compose⁻¹ ⬝ apD to_fun_hom p) = p :=
+  begin
+    cases p, cases F₁,
+    apply concat, rotate_left 1, apply functor_eq'_idp,
+    apply (ap (functor_eq' idp)),
+    apply idp_con,
+  end
+
+  -- definition functor_eq_eta {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂}
+  --   (p : functor.mk ob₁ hom₁ id₁ comp₁ = functor.mk ob₂ hom₂ id₂ comp₂)
+  --     : functor_mk_eq' _ _ _ _ (ap010 to_fun_ob p) _ = p :=
+  -- sorry
   --set_option pp.universes true
   -- set_option pp.notation false
   -- set_option pp.implicit true
-  -- TODO: REMOVE?
-  definition functor_eq2'' {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂}
-    {pob₁ pob₂ : ob₁ = ob₂} (phom₁ : pob₁ ▹ hom₁ = hom₂) (phom₂ : pob₂ ▹ hom₁ = hom₂)
-    (r : pob₁ = pob₂) : functor_eq_mk'' id₁ id₂ comp₁ comp₂ pob₁ phom₁
-                      = functor_eq_mk'' id₁ id₂ comp₁ comp₂ pob₂ phom₂ :=
-  begin
-    cases r,
-    apply (ap (functor_eq_mk'' id₁ id₂ @comp₁ @comp₂ pob₂)),
-    apply is_hprop.elim
-  end
 
-  definition functor_eq2' {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂} {pob₁ pob₂ : ob₁ ∼ ob₂}
-(phom₁ : Π(a b : C) (f : hom a b), hom_of_eq (pob₁ b) ∘ hom₁ a b f ∘ inv_of_eq (pob₁ a) = hom₂ a b f)
-(phom₂ : Π(a b : C) (f : hom a b), hom_of_eq (pob₂ b) ∘ hom₁ a b f ∘ inv_of_eq (pob₂ a) = hom₂ a b f)
-    (r : pob₁ = pob₂) : functor_eq_mk' id₁ id₂ comp₁ comp₂ pob₁ phom₁
-                      = functor_eq_mk' id₁ id₂ comp₁ comp₂ pob₂ phom₂ :=
-  begin
-    cases r,
-    apply (ap (functor_eq_mk' id₁ id₂ @comp₁ @comp₂ pob₂)),
-    apply is_hprop.elim
-  end
+  -- TODO: REMOVE?
+--   definition functor_mk_eq'2 {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂}
+--     {pob₁ pob₂ : ob₁ = ob₂} (phom₁ : pob₁ ▹ hom₁ = hom₂) (phom₂ : pob₂ ▹ hom₁ = hom₂)
+--     (r : pob₁ = pob₂) : functor_mk_eq' id₁ id₂ comp₁ comp₂ pob₁ phom₁
+--                       = functor_mk_eq' id₁ id₂ comp₁ comp₂ pob₂ phom₂ :=
+--   begin
+--     cases r,
+--     apply (ap (functor_mk_eq' id₁ id₂ @comp₁ @comp₂ pob₂)),
+--     apply is_hprop.elim
+--   end
+
+--   definition functor_mk_eq2 {ob₁ ob₂ : C → D} {hom₁ hom₂ id₁ id₂ comp₁ comp₂} {pob₁ pob₂ : ob₁ ∼ ob₂}
+-- (phom₁ : Π(a b : C) (f : hom a b), hom_of_eq (pob₁ b) ∘ hom₁ a b f ∘ inv_of_eq (pob₁ a) = hom₂ a b f)
+-- (phom₂ : Π(a b : C) (f : hom a b), hom_of_eq (pob₂ b) ∘ hom₁ a b f ∘ inv_of_eq (pob₂ a) = hom₂ a b f)
+--     (r : pob₁ = pob₂) : functor_mk_eq id₁ id₂ comp₁ comp₂ pob₁ phom₁
+--                       = functor_mk_eq id₁ id₂ comp₁ comp₂ pob₂ phom₂ :=
+--   begin
+--     cases r,
+--     apply (ap (functor_mk_eq id₁ id₂ @comp₁ @comp₂ pob₂)),
+--     apply is_hprop.elim
+--   end
+
+  definition functor_eq2' {F₁ F₂ : C ⇒ D} {p₁ p₂ : to_fun_ob F₁ = to_fun_ob F₂} (q₁ q₂)
+    (r : p₁ = p₂) : functor_eq' p₁ q₁ = functor_eq' p₂ q₂ :=
+  by cases r; apply (ap (functor_eq' p₂)); apply is_hprop.elim
 
   definition functor_eq2 {F₁ F₂ : C ⇒ D} (p q : F₁ = F₂) (r : ap010 to_fun_ob p ∼ ap010 to_fun_ob q)
     : p = q :=
   begin
-    apply sorry
+    cases F₁ with (ob₁, hom₁, id₁, comp₁),
+    cases F₂ with (ob₂, hom₂, id₂, comp₂),
+    rewrite [-functor_eq_eta' p, -functor_eq_eta' q],
+    apply functor_eq2',
+    apply ap_eq_ap_of_homotopy,
+    exact r,
   end
 
   -- definition ap010_functor_eq_mk' {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ = to_fun_ob F₂)
@@ -180,28 +230,45 @@ namespace functor
   -- end
 
   -- TODO: remove sorry
-  -- maybe some lemma "recursion on homotopy (and equiv)" could be useful
-  definition ap010_functor_eq_mk {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ ∼ to_fun_ob F₂)
+  definition ap010_functor_eq {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ ∼ to_fun_ob F₂)
     (q : (λ(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a)) ∼3 to_fun_hom F₂) (c : C) :
-    ap010 to_fun_ob (functor_eq_mk p q) c = p c :=
+    ap010 to_fun_ob (functor_eq p q) c = p c :=
   begin
     cases F₂, revert q, apply (homotopy.rec_on p), clear p, esimp, intros (p, q),
     apply sorry,
-    --cases p, clears (e_1, e_2, p),
-
-    --exact (homotopy3.rec_on q sorry)
---    apply (homotopy3.rec_on q),
+    --apply (homotopy3.rec_on q), clear q, intro q,
+    --cases p, --TODO: report: this fails
   end
 
-  -- definition ap010_functor_eq_mk {F₁ F₂ : C ⇒ D} (p : to_fun_ob F₁ ∼ to_fun_ob F₂)
-  --   (q : Π(a b : C) (f : hom a b), hom_of_eq (p b) ∘ F₁ f ∘ inv_of_eq (p a) = F₂ f) (c : C) :
-  --   ap010 to_fun_ob (functor_eq_mk p q) c = p c :=
+  definition ap010_functor_mk_eq_constant {F : C → D} {H₁ : Π(a b : C), hom a b → hom (F a) (F b)}
+    {H₂ : Π(a b : C), hom a b → hom (F a) (F b)} {id₁ id₂ comp₁ comp₂}
+    (pH : Π(a b : C) (f : hom a b), H₁ a b f = H₂ a b f) (c : C) :
+  ap010 to_fun_ob (functor_mk_eq_constant id₁ id₂ comp₁ comp₂ pH) c = idp :=
+  !ap010_functor_eq
+
+  --do we need this theorem?
+  definition compose_pentagon (K : D ⇒ E) (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
+    (calc K ∘f H ∘f G ∘f F = (K ∘f H) ∘f G ∘f F : functor.assoc
+      ... = ((K ∘f H) ∘f G) ∘f F : functor.assoc)
+    =
+    (calc K ∘f H ∘f G ∘f F = K ∘f (H ∘f G) ∘f F : ap (λx, K ∘f x) !functor.assoc
+      ... = (K ∘f H ∘f G) ∘f F : functor.assoc
+      ... = ((K ∘f H) ∘f G) ∘f F : ap (λx, x ∘f F) !functor.assoc) :=
+  sorry
   -- begin
-  --   cases F₂, revert q, apply (homotopy.rec_on p), clear p, esimp, intros (p, q),
-  --   cases p, clears (e_1, e_2, p),
-  --   apply (homotopy3.rec_on q),
+  -- apply functor_eq2,
+  -- intro a,
+  -- rewrite +ap010_con,
+  -- -- rewrite +ap010_ap,
+  -- -- apply sorry
+  -- /-to prove this we need a stronger ap010-lemma, something like
+  --     ap010 (λy, to_fun_ob (f y)) (functor_mk_eq_constant ...) c = idp
+  --   or something another way of getting ap out of ap010
+  -- -/
+  -- --rewrite +ap010_ap,
+  -- --unfold functor.assoc,
+  -- --rewrite ap010_functor_mk_eq_constant,
   -- end
--- ⊢ ap010 to_fun_ob (functor_eq_mk rfl q) c = rfl
 
 end functor
 
diff --git a/hott/algebra/precategory/iso.hlean b/hott/algebra/precategory/iso.hlean
index 1ef412efa3..09d64f5f42 100644
--- a/hott/algebra/precategory/iso.hlean
+++ b/hott/algebra/precategory/iso.hlean
@@ -10,6 +10,8 @@ import algebra.precategory.basic types.sigma arity
 
 open eq category prod equiv is_equiv sigma sigma.ops is_trunc
 
+
+
 namespace iso
   structure split_mono [class] {ob : Type} [C : precategory ob] {a b : ob} (f : a ⟶ b) :=
     {retraction_of : b ⟶ a}
@@ -193,10 +195,10 @@ namespace iso
   definition iso_of_eq (p : a = b) : a ≅ b :=
   eq.rec_on p (iso.refl a)
 
-  definition hom_of_eq (p : a = b) : a ⟶ b :=
+  definition hom_of_eq [reducible] (p : a = b) : a ⟶ b :=
   iso.to_hom (iso_of_eq p)
 
-  definition inv_of_eq (p : a = b) : b ⟶ a :=
+  definition inv_of_eq [reducible] (p : a = b) : b ⟶ a :=
   iso.to_inv (iso_of_eq p)
 
   definition iso_of_eq_inv (p : a = b) : iso_of_eq p⁻¹ = iso.symm (iso_of_eq p) :=
@@ -206,7 +208,6 @@ namespace iso
     : iso_of_eq (p ⬝ q) = iso.trans (iso_of_eq p) (iso_of_eq q) :=
   eq.rec_on q (eq.rec_on p (iso.eq_mk !id_comp⁻¹))
 
-
   section
     open funext
     variables {X : Type} {x y : X} {F G : X → ob}
diff --git a/hott/algebra/precategory/nat_trans.hlean b/hott/algebra/precategory/nat_trans.hlean
index 298f483b84..99ec566e1c 100644
--- a/hott/algebra/precategory/nat_trans.hlean
+++ b/hott/algebra/precategory/nat_trans.hlean
@@ -7,7 +7,7 @@ Author: Floris van Doorn, Jakob von Raumer
 -/
 
 import .functor .iso
-open eq category functor is_trunc equiv sigma.ops sigma is_equiv function pi funext
+open eq category functor is_trunc equiv sigma.ops sigma is_equiv function pi funext iso
 
 structure nat_trans {C D : Precategory} (F G : C ⇒ D) :=
  (natural_map : Π (a : C), hom (F a) (G a))
@@ -16,7 +16,7 @@ structure nat_trans {C D : Precategory} (F G : C ⇒ D) :=
 namespace nat_trans
 
   infixl `⟹`:25 := nat_trans -- \==>
-  variables {C D : Precategory} {F G H I : C ⇒ D}
+  variables {C D E : Precategory} {F G H I : C ⇒ D} {F' G' : D ⇒ E}
 
   attribute natural_map [coercion]
 
@@ -88,4 +88,27 @@ namespace nat_trans
     apply is_trunc_eq, apply is_trunc_succ, exact (@homH (Precategory.carrier D) _ (F a) (G b)),
   end
 
+  definition nat_trans_functor_compose [reducible] (η : G ⟹ H) (F : E ⇒ C) : G ∘f F ⟹ H ∘f F :=
+  nat_trans.mk
+    (λ a, η (F a))
+    (λ a b f, naturality η (F f))
+
+  definition functor_nat_trans_compose [reducible] (F : D ⇒ E) (η : G ⟹ H) : F ∘f G ⟹ F ∘f H :=
+  nat_trans.mk
+    (λ a, F (η a))
+    (λ a b f, calc
+      F (H f) ∘ F (η a) = F (H f ∘ η a) : respect_comp
+        ... = F (η b ∘ G f) : by rewrite (naturality η f)
+        ... = F (η b) ∘ F (G f) : respect_comp)
+
+  infixr `∘nf`:60 := nat_trans_functor_compose
+  infixr `∘fn`:60 := functor_nat_trans_compose
+
+  definition functor_nat_trans_compose_commute (η : F ⟹ G) (θ : F' ⟹ G')
+    : (θ ∘nf G) ∘n (F' ∘fn η) = (G' ∘fn η) ∘n (θ ∘nf F) :=
+  nat_trans_eq_mk (λc, (naturality θ (η c))⁻¹)
+
+  definition nat_trans_of_eq [reducible] (p : F = G) : F ⟹ G :=
+  nat_trans.mk (λc, hom_of_eq (ap010 to_fun_ob p c))
+               (λa b f, eq.rec_on p (!id_right ⬝ !id_left⁻¹))
 end nat_trans
diff --git a/hott/algebra/precategory/yoneda.hlean b/hott/algebra/precategory/yoneda.hlean
index 47b8c0dcee..363e8f6cb0 100644
--- a/hott/algebra/precategory/yoneda.hlean
+++ b/hott/algebra/precategory/yoneda.hlean
@@ -128,7 +128,7 @@ namespace functor
              (functor_uncurry_comp G)
 
   theorem functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F :=
-  functor_eq_mk (λp, ap (to_fun_ob F) !prod.eta)
+  functor_eq (λp, ap (to_fun_ob F) !prod.eta)
   begin
     intros (cd, cd', fg),
     cases cd with (c,d), cases cd' with (c',d'), cases fg with (f,g),
@@ -144,7 +144,7 @@ namespace functor
   definition functor_curry_functor_uncurry_ob (c : C)
     : functor_curry (functor_uncurry G) c = G c :=
   begin
-  fapply functor_eq_mk,
+  fapply functor_eq,
    {intro d, apply idp},
    {intros (d, d', g),
      apply concat, apply id_leftright,
@@ -159,17 +159,17 @@ namespace functor
 
   theorem functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G :=
   begin
-  fapply functor_eq_mk, exact (functor_curry_functor_uncurry_ob G),
+  fapply functor_eq, exact (functor_curry_functor_uncurry_ob G),
   intros (c, c', f),
   fapply nat_trans_eq_mk,
   intro d,
   apply concat,
     {apply (ap (λx, x ∘ _)),
-      apply concat, apply natural_map_hom_of_eq, apply (ap hom_of_eq), apply ap010_functor_eq_mk},
+      apply concat, apply natural_map_hom_of_eq, apply (ap hom_of_eq), apply ap010_functor_eq},
    apply concat,
      {apply (ap (λx, _ ∘ x)), apply (ap (λx, _ ∘ x)),
        apply concat, apply natural_map_inv_of_eq,
-       apply (ap (λx, hom_of_eq x⁻¹)), apply ap010_functor_eq_mk},
+       apply (ap (λx, hom_of_eq x⁻¹)), apply ap010_functor_eq},
   apply concat, apply id_leftright,
   apply concat, apply (ap (λx, x ∘ _)), apply respect_id,
   apply id_left
@@ -192,7 +192,7 @@ namespace functor
   definition functor_prod_flip_functor_prod_flip (C D : Precategory)
     : functor_prod_flip D C ∘f (functor_prod_flip C D) = functor.id :=
   begin
-  fapply functor_eq_mk, {intro p, apply prod.eta},
+  fapply functor_eq, {intro p, apply prod.eta},
   intros (p, p', h), cases p with (c, d), cases p' with (c', d'),
   apply id_leftright,
   end
diff --git a/hott/arity.hlean b/hott/arity.hlean
index 4ece88c3af..58ed580f15 100644
--- a/hott/arity.hlean
+++ b/hott/arity.hlean
@@ -10,7 +10,7 @@ Theorems about functions with multiple arguments
 
 variables {A U V W X Y Z : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type}
           {E : Πa b c, D a b c → Type}
-variables {a a' : A} {u u' : U} {v v' : V} {w w' : W} {x x' : X} {y y' : Y}
+variables {a a' : A} {u u' : U} {v v' : V} {w w' : W} {x x' x'' : X} {y y' : Y}
           {b : B a} {b' : B a'}
           {c : C a b} {c' : C a' b'}
           {d : D a b c} {d' : D a' b' c'}
@@ -88,6 +88,18 @@ namespace eq
   definition apD1000 {f g : Πa b c, D a b c} (p : f = g) : f ∼3 g :=
   λa b c, apD100 (apD10 p a) b c
 
+  /- some properties of these variants of ap -/
+
+  -- we only prove what is needed somewhere
+
+  definition ap010_con (f : X → Πa, B a) (p : x = x') (q : x' = x'') :
+    ap010 f (p ⬝ q) a = ap010 f p a ⬝ ap010 f q a :=
+  eq.rec_on q (eq.rec_on p idp)
+
+  definition ap010_ap (f : X → Πa, B a) (g : Y → X) (p : y = y') :
+    ap010 f (ap g p) a = ap010 (λy, f (g y)) p a :=
+  eq.rec_on p idp
+
   /- the following theorems are function extentionality for functions with multiple arguments -/
 
   definition eq_of_homotopy2 {f g : Πa b, C a b} (H : f ∼2 g) : f = g :=
@@ -111,9 +123,10 @@ namespace eq
       {apply (ap (λx, eq_of_homotopy x)), apply eq_of_homotopy, intro a, apply eq_of_homotopy2_id},
     apply eq_of_homotopy_id
   end
+
 end eq
 
-open is_equiv eq
+open eq is_equiv
 namespace funext
   definition is_equiv_apD100 [instance] (f g : Πa b, C a b) : is_equiv (@apD100 A B C f g) :=
   adjointify _
@@ -156,4 +169,20 @@ namespace eq
   protected definition homotopy3.rec_on {f g : Πa b c, D a b c} {P : (f ∼3 g) → Type}
     (p : f ∼3 g) (H : Π(q : f = g), P (apD1000 q)) : P p :=
   retr apD1000 p ▹ H (eq_of_homotopy3 p)
+
+  definition apD10_ap (f : X → Πa, B a) (p : x = x')
+    : apD10 (ap f p) = ap010 f p :=
+  eq.rec_on p idp
+
+  definition eq_of_homotopy_ap010 (f : X → Πa, B a) (p : x = x')
+    : eq_of_homotopy (ap010 f p) = ap f p :=
+  inv_eq_of_eq !apD10_ap⁻¹
+
+  definition ap_eq_ap_of_homotopy {f : X → Πa, B a} {p q : x = x'} (H : ap010 f p ∼ ap010 f q)
+    : ap f p = ap f q :=
+  calc
+    ap f p = eq_of_homotopy (ap010 f p) : eq_of_homotopy_ap010
+       ... = eq_of_homotopy (ap010 f q) : eq_of_homotopy H
+       ... = ap f q                     : eq_of_homotopy_ap010
+
 end eq
diff --git a/hott/init/axioms/funext_varieties.hlean b/hott/init/axioms/funext_varieties.hlean
index 46026758a8..16396a1044 100644
--- a/hott/init/axioms/funext_varieties.hlean
+++ b/hott/init/axioms/funext_varieties.hlean
@@ -85,7 +85,7 @@ context
   local attribute weak_funext [reducible]
   local attribute homotopy_ind [reducible]
   definition homotopy_ind_comp : homotopy_ind f (homotopy.refl f) = d :=
-    (@hprop_eq _ _ _ _ !center_eq idp)⁻¹ ▹ idp
+    (@hprop_eq_of_is_contr _ _ _ _ !center_eq idp)⁻¹ ▹ idp
 
 end
 
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index 53eaf97633..3e29114930 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -139,39 +139,20 @@ namespace is_equiv
   end
 
   section
-  variables {A B: Type} (f : A → B)
-
-  --The inverse of an equivalence is, again, an equivalence.
-  definition is_equiv_inv [instance] [Hf : is_equiv f] : (is_equiv (inv f)) :=
-    adjointify (inv f) f (sect f) (retr f)
-  end
-
-  section
-  variables {A B C : Type} (f : A → B) {f' : A → B} [Hf : is_equiv f]
+  variables {A B C : Type} (f : A → B) {f' : A → B} [Hf : is_equiv f] (g : B → C)
   include Hf
 
-  variable (g : B → C)
+  --The inverse of an equivalence is, again, an equivalence.
+  definition is_equiv_inv [instance] : (is_equiv f⁻¹) :=
+  adjointify f⁻¹ f (sect f) (retr f)
 
   definition cancel_right (g : B → C) [Hgf : is_equiv (g ∘ f)] : (is_equiv g) :=
-    have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f,
-    @homotopy_closed _ _ _ _ (is_equiv_compose f⁻¹ (g ∘ f)) (λb, ap g (@retr _ _ f _ b))
+  have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f,
+  @homotopy_closed _ _ _ _ (is_equiv_compose f⁻¹ (g ∘ f)) (λb, ap g (@retr _ _ f _ b))
 
   definition cancel_left (g : C → A) [Hgf : is_equiv (f ∘ g)] : (is_equiv g) :=
-    have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f,
-    @homotopy_closed _ _ _ _ (is_equiv_compose (f ∘ g) f⁻¹) (λa, sect f (g a))
-
-  --Rewrite rules
-  definition eq_of_eq_inv {x : A} {y : B} (p : x = (inv f) y) : (f x = y) :=
-    (ap f p) ⬝ (@retr _ _ f _ y)
-
-  definition eq_of_inv_eq {x : A} {y : B} (p : (inv f) y = x) : (y = f x) :=
-    (eq_of_eq_inv f p⁻¹)⁻¹
-
-  definition inv_eq_of_eq {x : B} {y : A} (p : x = f y) : (inv f) x = y :=
-    ap f⁻¹ p ⬝ sect f y
-
-  definition eq_inv_of_eq {x : B} {y : A} (p : f y = x) : y = (inv f) x :=
-    (inv_eq_of_eq f p⁻¹)⁻¹
+  have Hfinv [visible] : is_equiv f⁻¹, from is_equiv_inv f,
+  @homotopy_closed _ _ _ _ (is_equiv_compose (f ∘ g) f⁻¹) (λa, sect f (g a))
 
   definition is_equiv_ap [instance] (x y : A) : is_equiv (ap f) :=
     adjointify (ap f)
@@ -211,6 +192,25 @@ namespace is_equiv
 
   end
 
+  section
+  variables {A B : Type} {f : A → B} [Hf : is_equiv f] {a : A} {b : B}
+  include Hf
+
+  --Rewrite rules
+  definition eq_of_eq_inv (p : a = f⁻¹ b) : f a = b :=
+  ap f p ⬝ retr f b
+
+  definition eq_of_inv_eq (p : f⁻¹ b = a) : b = f a :=
+  (eq_of_eq_inv p⁻¹)⁻¹
+
+  definition inv_eq_of_eq (p : b = f a) : f⁻¹ b = a :=
+  ap f⁻¹ p ⬝ sect f a
+
+  definition eq_inv_of_eq (p : f a = b) : a = f⁻¹ b :=
+  (inv_eq_of_eq p⁻¹)⁻¹
+
+  end
+
   --Transporting is an equivalence
   definition is_equiv_tr [instance] {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 p) (inv_tr_tr P p) (tr_inv_tr_lemma P p)
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index 6c5aae39ad..0cb548ae5c 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -101,16 +101,16 @@ namespace is_trunc
   definition contr [H : is_contr A] (a : A) : !center = a :=
   @contr_internal.contr A !is_trunc.to_internal a
 
+  --TODO: rename
   definition center_eq [H : is_contr A] (x y : A) : x = y :=
   (contr x)⁻¹ ⬝ (contr y)
 
-  definition hprop_eq {A : Type} [H : is_contr A] {x y : A} (p q : x = y) : p = q :=
+  definition hprop_eq_of_is_contr {A : Type} [H : is_contr A] {x y : A} (p q : x = y) : p = q :=
   have K : ∀ (r : x = y), center_eq x y = r, from (λ r, eq.rec_on r !con.left_inv),
   (K p)⁻¹ ⬝ K q
 
-  definition is_contr_eq {A : Type} [H : is_contr A] (x y : A) : is_contr (x = y)
-  :=
-  is_contr.mk !center_eq (λ p, !hprop_eq)
+  definition is_contr_eq {A : Type} [H : is_contr A] (x y : A) : is_contr (x = y) :=
+  is_contr.mk !center_eq (λ p, !hprop_eq_of_is_contr)
   local attribute is_contr_eq [instance]
 
   /- truncation is upward close -/
@@ -210,11 +210,12 @@ namespace is_trunc
 
   --should we remove the following two theorems as they are special cases of
   --"is_trunc_is_equiv_closed"
-  definition is_contr_is_equiv_closed (f : A → B) [Hf : is_equiv f] [HA: is_contr A] : (is_contr B) :=
-    is_contr.mk (f (center A)) (λp, eq_of_eq_inv f !contr)
+  definition is_contr_is_equiv_closed (f : A → B) [Hf : is_equiv f] [HA: is_contr A]
+    : (is_contr B) :=
+  is_contr.mk (f (center A)) (λp, eq_of_eq_inv !contr)
 
   theorem is_contr_equiv_closed (H : A ≃ B) [HA: is_contr A] : is_contr B :=
-    @is_contr_is_equiv_closed _ _ (to_fun H) (to_is_equiv H) _
+  @is_contr_is_equiv_closed _ _ (to_fun H) (to_is_equiv H) _
 
   definition equiv_of_is_contr_of_is_contr [HA : is_contr A] [HB : is_contr B] : A ≃ B :=
   equiv.mk
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index 9b578bbff7..6bae143891 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -270,7 +270,7 @@ namespace sigma
   equiv.mk _ (adjointify
     (λu, (contr u.1)⁻¹ ▹ u.2)
     (λb, ⟨!center, b⟩)
-    (λb, ap (λx, x ▹ b) !hprop_eq)
+    (λb, ap (λx, x ▹ b) !hprop_eq_of_is_contr)
     (λu, sigma_eq !contr !tr_inv_tr))
 
   /- Associativity -/