diff --git a/hott/algebra/category/category.hlean b/hott/algebra/category/category.hlean
index 59b961b465..2db10a3454 100644
--- a/hott/algebra/category/category.hlean
+++ b/hott/algebra/category/category.hlean
@@ -6,7 +6,7 @@ Author: Jakob von Raumer
 
 import .iso
 
-open iso is_equiv equiv eq is_trunc
+open iso is_equiv equiv eq is_trunc sigma equiv.ops
 
 /-
   A category is a precategory extended by a witness
@@ -90,4 +90,41 @@ namespace category
   definition Category.eta (C : Category) : Category.mk C C = C :=
   Category.rec (λob c, idp) C
 
+  protected definition category.sigma_char.{u v} [constructor] (ob : Type)
+    : category.{u v} ob ≃ Σ(C : precategory.{u v} ob), is_univalent C :=
+  begin
+  fapply equiv.MK,
+    { intro x, induction x, constructor, assumption},
+    { intro y, induction y with y1 y2, induction y1, constructor, assumption},
+    { intro y, induction y with y1 y2, induction y1, reflexivity},
+    { intro x, induction x, reflexivity}
+  end
+
+
+  definition category_eq {ob : Type}
+    {C D : category ob}
+    (p : Π{a b}, @hom ob C a b = @hom ob D a b)
+    (q : Πa b c g f, cast p (@comp ob C a b c g f) = @comp ob D a b c (cast p g) (cast p f))
+      : C = D :=
+  begin
+    apply eq_of_fn_eq_fn !category.sigma_char,
+    fapply sigma_eq,
+    { induction C, induction D, esimp, exact precategory_eq @p q},
+    { unfold is_univalent, apply is_hprop.elimo},
+  end
+
+  definition category_eq_of_equiv {ob : Type}
+    {C D : category ob}
+    (p : Π⦃a b⦄, @hom ob C a b ≃ @hom ob D a b)
+    (q : Π{a b c} g f, p (@comp ob C a b c g f) = @comp ob D a b c (p g) (p f))
+      : C = D :=
+  begin
+    fapply category_eq,
+    { intro a b, exact ua !@p},
+    { intros, refine !cast_ua ⬝ !q ⬝ _, unfold [category.to_precategory],
+      apply ap011 !@category.comp !cast_ua⁻¹ᵖ !cast_ua⁻¹ᵖ},
+  end
+
+-- TODO: Category_eq[']
+
 end category
diff --git a/hott/algebra/category/constructions/discrete.hlean b/hott/algebra/category/constructions/discrete.hlean
index fa58ee94f4..6c4d8f7900 100644
--- a/hott/algebra/category/constructions/discrete.hlean
+++ b/hott/algebra/category/constructions/discrete.hlean
@@ -23,7 +23,7 @@ namespace category
 
   definition groupoid_of_1_type [constructor] (A : Type) [H : is_trunc 1 A] : groupoid A :=
   groupoid.mk !precategory_of_1_type
-              (λ (a b : A) (p : a = b), is_iso.mk !con.right_inv !con.left_inv)
+              (λ (a b : A) (p : a = b), is_iso.mk _ !con.right_inv !con.left_inv)
 
   definition Precategory_of_1_type [constructor] (A : Type) [H : is_trunc 1 A] : Precategory :=
   precategory.Mk (precategory_of_1_type A)
diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean
index c3910c0fbb..5b1e91af7d 100644
--- a/hott/algebra/category/constructions/functor.hlean
+++ b/hott/algebra/category/constructions/functor.hlean
@@ -24,7 +24,7 @@ namespace functor
   definition Precategory_functor [reducible] [constructor] (D C : Precategory) : Precategory :=
   precategory.Mk (precategory_functor D C)
 
-  infixr ` ^c `:35 := Precategory_functor
+  infixr ` ^c `:80 := Precategory_functor
 
   section
   /- we prove that if a natural transformation is pointwise an iso, then it is an iso -/
@@ -59,7 +59,7 @@ namespace functor
   end
 
   definition is_iso_nat_trans [constructor] [instance] : is_iso η :=
-  is_iso.mk (nat_trans_left_inverse η) (nat_trans_right_inverse η)
+  is_iso.mk _ (nat_trans_left_inverse η) (nat_trans_right_inverse η)
 
   variable (iso)
   definition functor_iso [constructor] : F ≅ G :=
@@ -189,6 +189,62 @@ namespace functor
 
   end
 
+  section
+  variables {C D E : Precategory} {G G' : D ⇒ E} {F F' : C ⇒ D} {J : D ⇒ D}
+
+  definition is_iso_nf_compose [constructor] (G : D ⇒ E) (η : F ⟹ F') [H : is_iso η]
+    : is_iso (G ∘fn η) :=
+  is_iso.mk
+    (G ∘fn @inverse (C ⇒ D) _ _ _ η _)
+    abstract !fn_n_distrib⁻¹ ⬝ ap (λx, G ∘fn x) (@left_inverse  (C ⇒ D) _ _ _ η _)  ⬝ !fn_id end
+    abstract !fn_n_distrib⁻¹ ⬝ ap (λx, G ∘fn x) (@right_inverse (C ⇒ D) _ _ _ η _) ⬝ !fn_id end
+
+  definition is_iso_fn_compose [constructor] (η : G ⟹ G') (F : C ⇒ D) [H : is_iso η]
+    : is_iso (η ∘nf F) :=
+  is_iso.mk
+    (@inverse (D ⇒ E) _ _ _ η _ ∘nf F)
+    abstract !n_nf_distrib⁻¹ ⬝ ap (λx, x ∘nf F) (@left_inverse  (D ⇒ E) _ _ _ η _)  ⬝ !id_nf end
+    abstract !n_nf_distrib⁻¹ ⬝ ap (λx, x ∘nf F) (@right_inverse (D ⇒ E) _ _ _ η _)  ⬝ !id_nf end
+
+  definition functor_iso_compose [constructor] (G : D ⇒ E) (η : F ≅ F') : G ∘f F ≅ G ∘f F' :=
+  @(iso.mk _) (is_iso_nf_compose G (to_hom η))
+
+  definition iso_functor_compose [constructor] (η : G ≅ G') (F : C ⇒ D) : G ∘f F ≅ G' ∘f F :=
+  @(iso.mk _) (is_iso_fn_compose (to_hom η) F)
+
+  infixr ` ∘fi ` :62 := functor_iso_compose
+  infixr ` ∘if ` :62 := iso_functor_compose
+
+
+/- TODO: also needs n_nf_distrib and id_nf for these compositions
+  definition nidf_compose [constructor] (η : J ⟹ 1) (F : C ⇒ D) [H : is_iso η]
+    : is_iso (η ∘n1f F) :=
+  is_iso.mk
+   (@inverse (D ⇒ D) _ _ _ η _ ∘1nf F)
+   abstract _ end
+            _
+
+  definition idnf_compose [constructor] (η : 1 ⟹ J) (F : C ⇒ D) [H : is_iso η]
+    : is_iso (η ∘1nf F) :=
+  is_iso.mk _
+            _
+            _
+
+  definition fnid_compose [constructor] (F : D ⇒ E) (η : J ⟹ 1) [H : is_iso η]
+    : is_iso (F ∘fn1 η) :=
+  is_iso.mk _
+            _
+            _
+
+  definition fidn_compose [constructor] (F : D ⇒ E) (η : 1 ⟹ J) [H : is_iso η]
+    : is_iso (F ∘f1n η) :=
+  is_iso.mk _
+            _
+            _
+-/
+
+  end
+
   namespace functor
 
     variables {C : Precategory} {D : Category} {F G : D ^c C}
@@ -271,6 +327,11 @@ namespace functor
 
   end functor
 
+  /-
+    functors involving only the functor category
+    (see ..functor.curry for some other functors involving also products)
+  -/
+
   variables {C D I : Precategory}
   definition constant2_functor [constructor] (F : I ⇒ D ^c C) (c : C) : I ⇒ D :=
   functor.mk (λi, to_fun_ob (F i) c)
@@ -289,5 +350,37 @@ namespace functor
              abstract begin intros, apply nat_trans_eq, intro i, esimp, apply respect_id end end
              abstract begin intros, apply nat_trans_eq, intro i, esimp, apply respect_comp end end
 
+  /- evaluation functor -/
+
+  definition eval_functor [constructor] (C D : Precategory) (d : D) : C ^c D ⇒ C :=
+  begin
+    fapply functor.mk: esimp,
+    { intro F, exact F d},
+    { intro G F η, exact η d},
+    { intro F, reflexivity},
+    { intro H G F η θ, reflexivity},
+  end
+
+  definition precomposition_functor [constructor] {C D} (E) (F : C ⇒ D)
+    : E ^c D ⇒ E ^c C :=
+  begin
+    fapply functor.mk: esimp,
+    { intro G, exact G ∘f F},
+    { intro G H η, exact η ∘nf F},
+    { intro G, reflexivity},
+    { intro G H I η θ, reflexivity},
+  end
+
+  definition postcomposition_functor [constructor] {C D} (E) (F : C ⇒ D)
+    : C ^c E ⇒ D ^c E :=
+  begin
+    fapply functor.mk: esimp,
+    { intro G, exact F ∘f G},
+    { intro G H η, exact F ∘fn η},
+    { intro G, apply fn_id},
+    { intro G H I η θ, apply fn_n_distrib},
+  end
+
+
 
 end functor
diff --git a/hott/algebra/category/constructions/product.hlean b/hott/algebra/category/constructions/product.hlean
index 8b854730b9..0a3cf87532 100644
--- a/hott/algebra/category/constructions/product.hlean
+++ b/hott/algebra/category/constructions/product.hlean
@@ -6,15 +6,15 @@ Authors: Floris van Doorn, Jakob von Raumer
 Product precategory and (TODO) category
 -/
 
-import ..category ..functor.functor hit.trunc
+import ..category ..nat_trans hit.trunc
 
-open eq prod is_trunc functor sigma trunc
+open eq prod is_trunc functor sigma trunc iso prod.ops nat_trans
 
 namespace category
-  definition precategory_prod [constructor] [reducible] {obC obD : Type}
-    (C : precategory obC) (D : precategory obD) : precategory (obC × obD) :=
-  precategory.mk' (λ a b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b))
-                  (λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f))
+  definition precategory_prod [constructor] [reducible] [instance] (obC obD : Type)
+    [C : precategory obC] [D : precategory obD] : precategory (obC × obD) :=
+  precategory.mk' (λ a b, hom a.1 b.1 × hom a.2 b.2)
+                  (λ a b c g f, (g.1 ∘ f.1, g.2 ∘ f.2))
                   (λ a, (id, id))
                   (λ a b c d h g f, pair_eq !assoc    !assoc   )
                   (λ a b c d h g f, pair_eq !assoc'   !assoc'  )
@@ -22,37 +22,76 @@ namespace category
                   (λ a b f,         prod_eq !id_right !id_right)
                   (λ a,             prod_eq !id_id    !id_id)
                   _
+
   definition Precategory_prod [reducible] [constructor] (C D : Precategory) : Precategory :=
   precategory.Mk (precategory_prod C D)
 
-  infixr `×c`:30 := Precategory_prod
+  infixr ` ×c `:70 := Precategory_prod
 
-  definition pr1_functor [constructor] {C D : Precategory} : C ×c D ⇒ C :=
+  variables {C C' D D' X : Precategory} {u v : carrier (C ×c D)}
+
+  theorem prod_hom_of_eq (p : u.1 = v.1) (q : u.2 = v.2)
+    : hom_of_eq (prod_eq p q) = (hom_of_eq p, hom_of_eq q) :=
+  by induction u; induction v; esimp at *; induction p; induction q; reflexivity
+
+  theorem prod_inv_of_eq (p : u.1 = v.1) (q : u.2 = v.2)
+    : inv_of_eq (prod_eq p q) = (inv_of_eq p, inv_of_eq q) :=
+  by induction u; induction v; esimp at *; induction p; induction q; reflexivity
+
+  theorem pr1_hom_of_eq (p : u.1 = v.1) (q : u.2 = v.2)
+    : (hom_of_eq (prod_eq p q)).1 = hom_of_eq p :=
+  by exact ap pr1 !prod_hom_of_eq
+
+  theorem pr1_inv_of_eq (p : u.1 = v.1) (q : u.2 = v.2)
+    : (inv_of_eq (prod_eq p q)).1 = inv_of_eq p :=
+  by exact ap pr1 !prod_inv_of_eq
+
+  theorem pr2_hom_of_eq (p : u.1 = v.1) (q : u.2 = v.2)
+    : (hom_of_eq (prod_eq p q)).2 = hom_of_eq q :=
+  by exact ap pr2 !prod_hom_of_eq
+
+  theorem pr2_inv_of_eq (p : u.1 = v.1) (q : u.2 = v.2)
+    : (inv_of_eq (prod_eq p q)).2 = inv_of_eq q :=
+  by exact ap pr2 !prod_inv_of_eq
+
+  definition pr1_functor [constructor] : C ×c D ⇒ C :=
   functor.mk pr1
              (λa b, pr1)
              (λa, idp)
              (λa b c g f, idp)
 
-  definition pr2_functor [constructor] {C D : Precategory} : C ×c D ⇒ D :=
+  definition pr2_functor [constructor] : C ×c D ⇒ D :=
   functor.mk pr2
              (λa b, pr2)
              (λa, idp)
              (λa b c g f, idp)
 
-  definition functor_prod [constructor] [reducible] {C D X : Precategory}
-    (F : X ⇒ C) (G : X ⇒ D) : X ⇒ C ×c D :=
+  definition functor_prod [constructor] [reducible] (F : X ⇒ C) (G : X ⇒ D) : X ⇒ C ×c D :=
   functor.mk (λ a,     pair (F a) (G a))
              (λ a b f, pair (F f) (G f))
              (λ a,         abstract pair_eq !respect_id   !respect_id   end)
              (λ a b c g f, abstract pair_eq !respect_comp !respect_comp end)
 
-  definition pr1_functor_prod {C D X : Precategory} (F : X ⇒ C) (G : X ⇒ D)
-    : pr1_functor ∘f functor_prod F G = F :=
+  infixr ` ×f `:70 := functor_prod
+
+  definition prod_functor_eta (F : X ⇒ C ×c D) : pr1_functor ∘f F ×f pr2_functor ∘f F = F :=
+  begin
+  fapply functor_eq: esimp,
+  { intro e, apply prod_eq: reflexivity},
+  { intro e e' f, apply prod_eq: esimp,
+    { refine ap (λx, x ∘ _ ∘ _) !pr1_hom_of_eq ⬝ _,
+      refine ap (λx, _ ∘ _ ∘ x) !pr1_inv_of_eq ⬝ _, esimp,
+      apply id_leftright},
+    { refine ap (λx, x ∘ _ ∘ _) !pr2_hom_of_eq ⬝ _,
+      refine ap (λx, _ ∘ _ ∘ x) !pr2_inv_of_eq ⬝ _, esimp,
+      apply id_leftright}}
+  end
+
+  definition pr1_functor_prod (F : X ⇒ C) (G : X ⇒ D) : pr1_functor ∘f (F ×f G) = F :=
   functor_eq (λx, idp)
              (λx y f, !id_leftright)
 
-  definition pr2_functor_prod {C D X : Precategory} (F : X ⇒ C) (G : X ⇒ D)
-    : pr2_functor ∘f functor_prod F G = G :=
+  definition pr2_functor_prod (F : X ⇒ C) (G : X ⇒ D) : pr2_functor ∘f (F ×f G) = G :=
   functor_eq (λx, idp)
              (λx y f, !id_leftright)
 
@@ -73,10 +112,31 @@ namespace category
   --     { exact sorry}
   --   end
 
-  definition prod_functor_prod [constructor] {C C' D D' : Precategory}
-    (F : C ⇒ D) (G : C' ⇒ D') : C ×c C' ⇒ D ×c D' :=
-  functor_prod (F ∘f pr1_functor) (G ∘f pr2_functor)
+  definition prod_functor_prod [constructor] (F : C ⇒ D) (G : C' ⇒ D') : C ×c C' ⇒ D ×c D' :=
+  (F ∘f pr1_functor) ×f (G ∘f pr2_functor)
+
+  definition prod_nat_trans [constructor] {C D D' : Precategory}
+    {F F' : C ⇒ D} {G G' : C ⇒ D'} (η : F ⟹ F') (θ : G ⟹ G') : F ×f G ⟹ F' ×f G' :=
+  begin
+    fapply nat_trans.mk: esimp,
+    { intro c, exact (η c, θ c)},
+    { intro c c' f, apply prod_eq: esimp:apply naturality}
+  end
+
+  definition prod_flip_functor [constructor] (C D : Precategory) : C ×c D ⇒ D ×c C :=
+  functor.mk (λp, (p.2, p.1))
+             (λp p' h, (h.2, h.1))
+             (λp, idp)
+             (λp p' p'' h' h, idp)
+
+  definition functor_prod_flip_functor_prod_flip (C D : Precategory)
+    : prod_flip_functor D C ∘f (prod_flip_functor C D) = functor.id :=
+  begin
+  fapply functor_eq,
+  { intro p, apply prod.eta},
+  { intro p p' h, cases p with c d, cases p' with c' d',
+    apply id_leftright}
+  end
 
-  infixr `×f`:30 := prod_functor
 
 end category
diff --git a/hott/algebra/category/constructions/sum.hlean b/hott/algebra/category/constructions/sum.hlean
index 9b0c6640d1..ee2771dbca 100644
--- a/hott/algebra/category/constructions/sum.hlean
+++ b/hott/algebra/category/constructions/sum.hlean
@@ -6,9 +6,9 @@ Authors: Floris van Doorn, Jakob von Raumer
 Sum precategory and (TODO) category
 -/
 
-import ..category ..functor.functor types.sum
+import ..category ..nat_trans types.sum
 
-open eq sum is_trunc functor lift
+open eq sum is_trunc functor lift nat_trans
 
 namespace category
 
@@ -26,8 +26,8 @@ namespace category
 
   local attribute is_hset_sum_hom [instance]
 
-  definition precategory_sum [constructor] {obC obD : Type}
-    (C : precategory obC) (D : precategory obD) : precategory (obC + obD) :=
+  definition precategory_sum [constructor] [instance] (obC obD : Type)
+    [C : precategory obC] [D : precategory obD] : precategory (obC + obD) :=
   precategory.mk (sum_hom C D)
                   (λ a b c g f, begin induction a: induction b: induction c: esimp at *;
                     induction f with f; induction g with g; (contradiction | exact up (g ∘ f)) end)
@@ -44,18 +44,69 @@ namespace category
   definition Precategory_sum [constructor] (C D : Precategory) : Precategory :=
   precategory.Mk (precategory_sum C D)
 
-  infixr `+c`:27 := Precategory_sum
+  infixr ` +c `:65 := Precategory_sum
+  variables {C C' D D' : Precategory}
 
-  definition sum_functor [constructor] {C C' D D' : Precategory}
-    (F : C ⇒ D) (G : C' ⇒ D') : C +c C' ⇒ D +c D' :=
-  functor.mk (λ a, by induction a: (exact inl (F a)|exact inr (G a)))
-             (λ a b f, begin induction a: induction b: esimp at *;
-                induction f with f; esimp; try contradiction: (exact up (F f)|exact up (G f)) end)
-             (λ a, abstract by induction a: esimp; exact ap up !respect_id end)
-             (λ a b c g f, abstract begin induction a: induction b: induction c: esimp at *;
+  definition inl_functor [constructor] : C ⇒ C +c D :=
+  functor.mk inl
+             (λa b, up)
+             (λa, idp)
+             (λa b c g f, idp)
+
+  definition inr_functor [constructor] : D ⇒ C +c D :=
+  functor.mk inr
+             (λa b, up)
+             (λa, idp)
+             (λa b c g f, idp)
+
+  definition sum_functor [constructor] (F : C ⇒ D) (G : C' ⇒ D) : C +c C' ⇒ D :=
+  begin
+    fapply functor.mk: esimp,
+    { intro a, induction a, exact F a, exact G a},
+    { intro a b f, induction a: induction b: esimp at *;
+     induction f with f; esimp; try contradiction: (exact F f|exact G f)},
+    { exact abstract begin intro a, induction a: esimp; apply respect_id end end},
+    { intros a b c g f, induction a: induction b: induction c: esimp at *;
                 induction f with f; induction g with g; try contradiction:
-                esimp; exact ap up !respect_comp end end)
+                esimp; apply respect_comp}, -- REPORT: abstracting this argument fails
+  end
+
+  infixr ` +f `:65 := sum_functor
+
+  definition sum_functor_eta (F : C +c C' ⇒ D) : F ∘f inl_functor +f F ∘f inr_functor = F :=
+  begin
+  fapply functor_eq: esimp,
+  { intro a, induction a: reflexivity},
+  { exact abstract begin esimp, intro a b f,
+    induction a: induction b: esimp at *; induction f with f; esimp;
+    try contradiction: apply id_leftright end end}
+  end
+
+  definition sum_functor_inl (F : C ⇒ D) (G : C' ⇒ D) : (F +f G) ∘f inl_functor = F :=
+  begin
+  fapply functor_eq,
+    reflexivity,
+    esimp, intros, apply id_leftright
+  end
+
+  definition sum_functor_inr (F : C ⇒ D) (G : C' ⇒ D) : (F +f G) ∘f inr_functor = G :=
+  begin
+  fapply functor_eq,
+    reflexivity,
+    esimp, intros, apply id_leftright
+  end
+
+  definition sum_functor_sum [constructor] (F : C ⇒ D) (G : C' ⇒ D') : C +c C' ⇒ D +c D' :=
+  (inl_functor ∘f F) +f (inr_functor ∘f G)
+
+  definition sum_nat_trans [constructor] {F F' : C ⇒ D} {G G' : C' ⇒ D} (η : F ⟹ F') (θ : G ⟹ G')
+    : F +f G ⟹ F' +f G' :=
+  begin
+    fapply nat_trans.mk,
+    { intro a, induction a: esimp, exact η a, exact θ a},
+    { intro a b f, induction a: induction b: esimp at *; induction f with f; esimp;
+      try contradiction: apply naturality}
+  end
 
-  infixr `+f`:27 := sum_functor
 
 end category
diff --git a/hott/algebra/category/constructions/terminal.hlean b/hott/algebra/category/constructions/terminal.hlean
index 24a40687ac..31ec7e1b75 100644
--- a/hott/algebra/category/constructions/terminal.hlean
+++ b/hott/algebra/category/constructions/terminal.hlean
@@ -42,7 +42,7 @@ namespace category
   definition terminal_functor_comp {C D : Precategory} (F : C ⇒ D)
     : (terminal_functor D) ∘f F = terminal_functor C := idp
 
-  definition point (C : Precategory) (c : C) : 1 ⇒ C :=
+  definition point [constructor] (C : Precategory) (c : C) : 1 ⇒ C :=
   functor.mk (λx, c)
              (λx y f, id)
              (λx, idp)
diff --git a/hott/algebra/category/functor/adjoint.hlean b/hott/algebra/category/functor/adjoint.hlean
index d313aaea5b..51022da4f0 100644
--- a/hott/algebra/category/functor/adjoint.hlean
+++ b/hott/algebra/category/functor/adjoint.hlean
@@ -17,6 +17,8 @@ namespace category
   --   (G : D ⇒ C) -- G
   --   (is_adjoint : adjoint F G)
 
+  --   infix `⊣`:55 := adjoint
+
   structure is_left_adjoint [class] {C D : Precategory} (F : C ⇒ D) :=
     (G : D ⇒ C)
     (η : 1 ⟹ G ∘f F)
diff --git a/hott/algebra/category/functor/attributes.hlean b/hott/algebra/category/functor/attributes.hlean
index c1108e9972..14aa11142d 100644
--- a/hott/algebra/category/functor/attributes.hlean
+++ b/hott/algebra/category/functor/attributes.hlean
@@ -20,18 +20,20 @@ namespace category
   definition fully_faithful [class] (F : C ⇒ D) := Π(c c' : C), is_equiv (@(to_fun_hom F) c c')
   definition split_essentially_surjective [class] (F : C ⇒ D) := Π(d : D), Σ(c : C), F c ≅ d
   definition essentially_surjective [class] (F : C ⇒ D) := Π(d : D), ∃(c : C), F c ≅ d
-  definition is_weak_equivalence [class] (F : C ⇒ D) := fully_faithful F × essentially_surjective F
+  definition is_weak_equivalence [class] (F : C ⇒ D) :=
+  fully_faithful F × essentially_surjective F
 
-  definition is_equiv_of_fully_faithful [instance] [reducible] (F : C ⇒ D) [H : fully_faithful F]
-    (c c' : C) : is_equiv (@(to_fun_hom F) c c') :=
+
+  definition is_equiv_of_fully_faithful [instance] [reducible] (F : C ⇒ D)
+    [H : fully_faithful F] (c c' : C) : is_equiv (@(to_fun_hom F) c c') :=
   !H
 
   definition hom_inv [reducible] (F : C ⇒ D) [H : fully_faithful F] (c c' : C) (f : F c ⟶ F c')
     : c ⟶ c' :=
   (to_fun_hom F)⁻¹ᶠ f
 
-  definition reflect_is_iso [constructor] (F : C ⇒ D) [H : fully_faithful F] {c c' : C} (f : c ⟶ c')
-    [H : is_iso (F f)] : is_iso f :=
+  definition reflect_is_iso [constructor] (F : C ⇒ D) [H : fully_faithful F] {c c' : C}
+    (f : c ⟶ c') [H : is_iso (F f)] : is_iso f :=
   begin
     fconstructor,
     { exact (to_fun_hom F)⁻¹ᶠ (F f)⁻¹},
@@ -91,19 +93,29 @@ namespace category
       esimp [iso_of_F_iso_F], apply right_inv end end},
   end
 
-  definition full_of_fully_faithful (H : fully_faithful F) : full F :=
+  definition full_of_fully_faithful [instance] (F : C ⇒ D) [H : fully_faithful F] : full F :=
   λc c' g, tr (fiber.mk ((@(to_fun_hom F) c c')⁻¹ᶠ g) !right_inv)
 
-  definition faithful_of_fully_faithful (H : fully_faithful F) : faithful F :=
+  definition faithful_of_fully_faithful [instance] (F : C ⇒ D) [H : fully_faithful F]
+    : faithful F :=
   λc c' f f' p, is_injective_of_is_embedding p
 
-  definition fully_faithful_of_full_of_faithful (H : faithful F) (K : full F) : fully_faithful F :=
+  definition is_embedding_of_faithful [instance] (F : C ⇒ D) [H : faithful F] (c c' : C)
+    : is_embedding (to_fun_hom F : c ⟶ c' → F c ⟶ F c') :=
+  begin
+    apply is_embedding_of_is_injective,
+    apply H
+  end
+
+  definition is_surjective_of_full [instance] (F : C ⇒ D) [H : full F] (c c' : C)
+    : is_surjective (to_fun_hom F : c ⟶ c' → F c ⟶ F c') :=
+  @H c c'
+
+  definition fully_faithful_of_full_of_faithful (H : faithful F) (K : full F)
+    : fully_faithful F :=
   begin
     intro c c',
     apply is_equiv_of_is_surjective_of_is_embedding,
-    { apply is_embedding_of_is_injective,
-      intros f f' p, exact H p},
-    { apply K}
   end
 
   theorem is_hprop_fully_faithful [instance] (F : C ⇒ D) : is_hprop (fully_faithful F) :=
@@ -123,7 +135,7 @@ namespace category
   by unfold is_weak_equivalence; exact _
 
   definition fully_faithful_equiv (F : C ⇒ D) : fully_faithful F ≃ (faithful F × full F) :=
-  equiv_of_is_hprop (λH, (faithful_of_fully_faithful H, full_of_fully_faithful H))
+  equiv_of_is_hprop (λH, (faithful_of_fully_faithful F, full_of_fully_faithful F))
                     (λH, fully_faithful_of_full_of_faithful (pr1 H) (pr2 H))
 
 /- alternative proof using direct calculation with equivalences
diff --git a/hott/algebra/category/functor/curry.hlean b/hott/algebra/category/functor/curry.hlean
index 4019e0b8b9..31352df7ce 100644
--- a/hott/algebra/category/functor/curry.hlean
+++ b/hott/algebra/category/functor/curry.hlean
@@ -12,7 +12,7 @@ open category prod nat_trans eq prod.ops iso equiv
 
 namespace functor
 
-  variables {C D E : Precategory} (F : C ×c D ⇒ E) (G : C ⇒ E ^c D)
+  variables {C D E : Precategory} (F F' : C ×c D ⇒ E) (G G' : C ⇒ E ^c D)
   definition functor_curry_ob [reducible] [constructor] (c : C) : E ^c D :=
   functor.mk (λd, F (c,d))
              (λd d' g, F (id, g))
@@ -22,11 +22,10 @@ namespace functor
                  ... = F ((id,g') ∘ (id, g))        : by esimp
                  ... = F (id,g') ∘ F (id, g)        : by rewrite respect_comp)
 
-  local abbreviation Fob := @functor_curry_ob
-
-  definition functor_curry_hom [constructor] ⦃c c' : C⦄ (f : c ⟶ c') : Fob F c ⟹ Fob F c' :=
+  definition functor_curry_hom [constructor] ⦃c c' : C⦄ (f : c ⟶ c')
+    : functor_curry_ob F c ⟹ functor_curry_ob F c' :=
   begin
-    fapply @nat_trans.mk,
+    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
@@ -37,7 +36,7 @@ namespace functor
                    ... = F (f, id) ∘ F (id, g) : (respect_comp F (f, id) (id, g))⁻¹ᵖ
         }
   end
-  local abbreviation Fhom := @functor_curry_hom
+  local abbreviation Fhom [constructor] := @functor_curry_hom
 
   theorem functor_curry_hom_def ⦃c c' : C⦄ (f : c ⟶ c') (d : D) :
     (Fhom F f) d = to_fun_hom F (f, id) := idp
@@ -65,9 +64,9 @@ namespace functor
 
   definition functor_uncurry_ob [reducible] (p : C ×c D) : E :=
   to_fun_ob (G p.1) p.2
-  local abbreviation Gob := @functor_uncurry_ob
 
-  definition functor_uncurry_hom ⦃p p' : C ×c D⦄ (f : hom p p') : Gob G p ⟶ Gob G p'  :=
+  definition functor_uncurry_hom ⦃p p' : C ×c D⦄ (f : hom p p')
+    : functor_uncurry_ob G p ⟶ functor_uncurry_ob G p'  :=
   to_fun_hom (to_fun_ob G p'.1) f.2 ∘ natural_map (to_fun_hom G f.1) p.2
   local abbreviation Ghom := @functor_uncurry_hom
 
@@ -119,16 +118,9 @@ namespace functor
     : functor_curry (functor_uncurry G) c = G c :=
   begin
   fapply functor_eq,
-   {intro d, reflexivity},
-   {intro d d' g,
-     apply concat, apply id_leftright,
-      show to_fun_hom (functor_curry (functor_uncurry G) c) g = to_fun_hom (G c) g,
-      from calc
-        to_fun_hom (functor_curry (functor_uncurry G) c) g
-            = to_fun_hom (G c) g ∘ natural_map (to_fun_hom G (ID c)) d : by esimp
-        ... = to_fun_hom (G c) g ∘ natural_map (ID (G c)) d            : by rewrite respect_id
-        ... = to_fun_hom (G c) g ∘ id                                  : by reflexivity
-        ... = to_fun_hom (G c) g                                       : by rewrite id_right}
+   { intro d, reflexivity},
+   { intro d d' g, refine !id_leftright ⬝ _, esimp,
+     rewrite [▸*, ↑functor_uncurry_hom, respect_id, ▸*, id_right]}
   end
 
   theorem functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G :=
@@ -156,18 +148,30 @@ namespace functor
            functor_curry_functor_uncurry
            functor_uncurry_functor_curry
 
-
-  definition functor_prod_flip [constructor] (C D : Precategory) : C ×c D ⇒ D ×c C :=
-  functor.mk (λp, (p.2, p.1))
-             (λp p' h, (h.2, h.1))
-             (λp, idp)
-             (λp p' p'' h' h, idp)
-
-  definition functor_prod_flip_functor_prod_flip (C D : Precategory)
-    : functor_prod_flip D C ∘f (functor_prod_flip C D) = functor.id :=
+  variables {F F' G G'}
+  definition nat_trans_curry_nat [constructor] (η : F ⟹ F') (c : C)
+    : functor_curry_ob F c ⟹ functor_curry_ob F' c :=
   begin
-  fapply functor_eq, {intro p, apply prod.eta},
-  intro p p' h, cases p with c d, cases p' with c' d',
-  apply id_leftright,
+    fapply nat_trans.mk: esimp,
+    { intro d, exact η (c, d)},
+    { intro d d' f, apply naturality}
   end
+
+  definition nat_trans_curry [constructor] (η : F ⟹ F')
+    : functor_curry F ⟹ functor_curry F' :=
+  begin
+    fapply nat_trans.mk: esimp,
+    { exact nat_trans_curry_nat η},
+    { intro c c' f, apply nat_trans_eq, intro d, esimp, apply naturality}
+  end
+
+  definition nat_trans_uncurry [constructor] (η : G ⟹ G')
+    : functor_uncurry G ⟹ functor_uncurry G' :=
+  begin
+    fapply nat_trans.mk: esimp,
+    { intro v, unfold functor_uncurry_ob, exact (η v.1) v.2},
+    { intro v w f, unfold functor_uncurry_hom,
+      rewrite [-assoc, ap010 natural_map (naturality η f.1) v.2, assoc, naturality, -assoc]}
+  end
+
 end functor
diff --git a/hott/algebra/category/functor/default.hlean b/hott/algebra/category/functor/default.hlean
new file mode 100644
index 0000000000..26b2b4a76d
--- /dev/null
+++ b/hott/algebra/category/functor/default.hlean
@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+-/
+
+import .functor
diff --git a/hott/algebra/category/functor/equivalence.hlean b/hott/algebra/category/functor/equivalence.hlean
index 16fa9fdfb1..39a2d729d4 100644
--- a/hott/algebra/category/functor/equivalence.hlean
+++ b/hott/algebra/category/functor/equivalence.hlean
@@ -32,25 +32,27 @@ namespace category
   structure isomorphism (C D : Precategory) :=
     (to_functor : C ⇒ D)
     (struct : is_isomorphism to_functor)
-  --   infix `⊣`:55 := adjoint
 
   infix ` ≃c `:25 := equivalence
   infix ` ≅c `:25 := isomorphism
 
+  attribute equivalence.struct isomorphism.struct [instance] [priority 1500]
+  attribute equivalence.to_functor isomorphism.to_functor [coercion]
+
   definition is_iso_unit [instance] (F : C ⇒ D) [H : is_equivalence F] : is_iso (unit F) :=
   !is_equivalence.is_iso_unit
 
   definition is_iso_counit [instance] (F : C ⇒ D) [H : is_equivalence F] : is_iso (counit F) :=
   !is_equivalence.is_iso_counit
 
-  definition iso_unit (F : C ⇒ D) [H : is_equivalence F] : F ⁻¹ᴱ ∘f F ≅ 1 :=
+  definition iso_unit (F : C ⇒ D) [H : is_equivalence F] : F⁻¹ᴱ ∘f F ≅ 1 :=
   (@(iso.mk _) !is_iso_unit)⁻¹ⁱ
 
-  definition iso_counit (F : C ⇒ D) [H : is_equivalence F] : F ∘f F ⁻¹ᴱ ≅ 1 :=
+  definition iso_counit (F : C ⇒ D) [H : is_equivalence F] : F ∘f F⁻¹ᴱ ≅ 1 :=
   @(iso.mk _) !is_iso_counit
 
-  definition split_essentially_surjective_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F]
-    : split_essentially_surjective F :=
+  definition split_essentially_surjective_of_is_equivalence (F : C ⇒ D)
+    [H : is_equivalence F] : split_essentially_surjective F :=
   begin
    intro d, fconstructor,
    { exact F⁻¹ d},
@@ -154,8 +156,8 @@ namespace category
       apply naturality (unit F)},
   end
 
-  definition is_isomorphism.mk {F : C ⇒ D} (G : D ⇒ C) (p : G ∘f F = 1) (q : F ∘f G = 1)
-    : is_isomorphism F :=
+  definition is_isomorphism.mk [constructor] {F : C ⇒ D} (G : D ⇒ C)
+    (p : G ∘f F = 1) (q : F ∘f G = 1) : is_isomorphism F :=
   begin
     constructor,
     { apply fully_faithful_of_is_equivalence, fapply is_equivalence.mk,
@@ -168,16 +170,18 @@ namespace category
       { exact ap010 to_fun_ob p}}
   end
 
-  definition is_equiv_of_is_isomorphism (F : C ⇒ D) [H : is_isomorphism F]
-    : is_equiv (to_fun_ob F) :=
+  definition isomorphism.MK [constructor] (F : C ⇒ D) (G : D ⇒ C)
+    (p : G ∘f F = 1) (q : F ∘f G = 1) : C ≅c D :=
+  isomorphism.mk F (is_isomorphism.mk G p q)
+
+  definition is_equiv_ob_of_is_isomorphism [instance] [unfold 4] (F : C ⇒ D)
+    [H : is_isomorphism F] : is_equiv (to_fun_ob F) :=
   pr2 H
 
-  definition is_fully_faithful_of_is_isomorphism (F : C ⇒ D) [H : is_isomorphism F]
-    : fully_faithful F :=
+  definition is_fully_faithful_of_is_isomorphism [instance] [unfold 4] (F : C ⇒ D)
+    [H : is_isomorphism F] : fully_faithful F :=
   pr1 H
 
-  local attribute is_fully_faithful_of_is_isomorphism is_equiv_of_is_isomorphism [instance]
-
   definition strict_inverse [constructor] (F : C ⇒ D) [H : is_isomorphism F] : D ⇒ C :=
   begin
     fapply functor.mk,
@@ -185,7 +189,7 @@ namespace category
     { intro d d' g, exact (to_fun_hom F)⁻¹ᶠ (inv_of_eq !right_inv ∘ g ∘ hom_of_eq !right_inv)},
     { intro d, apply inv_eq_of_eq, rewrite [respect_id,id_left], apply left_inverse},
     { intro d₁ d₂ d₃ g₂ g₁, apply inv_eq_of_eq, rewrite [respect_comp F,+right_inv (to_fun_hom F)],
-      rewrite [+assoc], esimp, /-apply ap (λx, _ ∘ x), FAILS-/ refine ap (λx, (x ∘ _) ∘ _) _,
+      rewrite [+assoc], esimp, /-apply ap (λx, (x ∘ _) ∘ _), FAILS-/ refine ap (λx, (x ∘ _) ∘ _) _,
       refine !id_right⁻¹ ⬝ _, rewrite [▸*,-+assoc], refine ap (λx, _ ∘ _ ∘ x) _,
       exact !right_inverse⁻¹},
   end
@@ -212,7 +216,7 @@ namespace category
       { rewrite [adj,▸*,respect_hom_of_eq F]}},
   end
 
-  definition is_equivalence_of_is_isomorphism [instance] (F : C ⇒ D) [H : is_isomorphism F]
+  definition is_equivalence_of_is_isomorphism [instance] [constructor] (F : C ⇒ D) [H : is_isomorphism F]
     : is_equivalence F :=
   begin
     fapply is_equivalence.mk,
@@ -221,7 +225,11 @@ namespace category
     { apply iso_of_eq !strict_right_inverse},
   end
 
-  theorem is_hprop_is_equivalence [instance] {C : Category} {D : Precategory} (F : C ⇒ D) : is_hprop (is_equivalence F) :=
+  definition equivalence_of_isomorphism [constructor] (F : C ≅c D) : C ≃c D :=
+  equivalence.mk F _
+
+  theorem is_hprop_is_equivalence [instance] {C : Category} {D : Precategory} (F : C ⇒ D)
+    : is_hprop (is_equivalence F) :=
   begin
     assert f : is_equivalence F ≃ Σ(H : is_left_adjoint F), is_iso (unit F) × is_iso (counit F),
     { fapply equiv.MK,
@@ -238,14 +246,15 @@ namespace category
 
   /- closure properties -/
 
-  definition is_isomorphism_id [instance] (C : Precategory) : is_isomorphism (1 : C ⇒ C) :=
+  definition is_isomorphism_id [instance] [constructor] (C : Precategory)
+    : is_isomorphism (1 : C ⇒ C) :=
   is_isomorphism.mk 1 !functor.id_right !functor.id_right
 
-  definition is_isomorphism_strict_inverse (F : C ⇒ D) [K : is_isomorphism F]
+  definition is_isomorphism_strict_inverse [constructor] (F : C ⇒ D) [K : is_isomorphism F]
     : is_isomorphism F⁻¹ˢ :=
   is_isomorphism.mk F !strict_right_inverse !strict_left_inverse
 
-  definition is_isomorphism_compose (G : D ⇒ E) (F : C ⇒ D)
+  definition is_isomorphism_compose [constructor] (G : D ⇒ E) (F : C ⇒ D)
     [H : is_isomorphism G] [K : is_isomorphism F] : is_isomorphism (G ∘f F) :=
   is_isomorphism.mk
     (F⁻¹ˢ ∘f G⁻¹ˢ)
@@ -258,58 +267,150 @@ namespace category
                strict_right_inverse]
     end end
 
-  definition is_equivalence_id (C : Precategory) : is_equivalence (1 : C ⇒ C) := _
+  definition is_equivalence_id [constructor] (C : Precategory) : is_equivalence (1 : C ⇒ C) := _
 
-  definition is_equivalence_strict_inverse (F : C ⇒ D) [K : is_equivalence F]
-    : is_equivalence F ⁻¹ᴱ :=
+  definition is_equivalence_inverse [constructor] (F : C ⇒ D) [K : is_equivalence F]
+    : is_equivalence F⁻¹ᴱ :=
   is_equivalence.mk F (iso_counit F) (iso_unit F)
 
-/-
-  definition is_equivalence_compose (G : D ⇒ E) (F : C ⇒ D)
+  definition is_equivalence_compose [constructor] (G : D ⇒ E) (F : C ⇒ D)
     [H : is_equivalence G] [K : is_equivalence F] : is_equivalence (G ∘f F) :=
   is_equivalence.mk
-    (F ⁻¹ᴱ ∘f G ⁻¹ᴱ)
+    (F⁻¹ᴱ ∘f G⁻¹ᴱ)
     abstract begin
-      rewrite [functor.assoc,-functor.assoc F ⁻¹ᴱ],
---      refine ((_ ∘fi _) ∘if _) ⬝i _,
+      rewrite [functor.assoc,-functor.assoc F⁻¹ᴱ],
+      refine ((_ ∘fi !iso_unit) ∘if _) ⬝i _,
+      refine (iso_of_eq !functor.id_right ∘if _) ⬝i _,
+      apply iso_unit
     end end
     abstract begin
-      rewrite [functor.assoc,-functor.assoc G,strict_right_inverse,functor.id_right,
-               strict_right_inverse]
+      rewrite [functor.assoc,-functor.assoc G],
+      refine ((_ ∘fi !iso_counit) ∘if _) ⬝i _,
+      refine (iso_of_eq !functor.id_right ∘if _) ⬝i _,
+      apply iso_counit
     end end
 
-  definition is_equivalence_equiv (F : C ⇒ D)
+  variable (C)
+  definition equivalence.refl [refl] [constructor] : C ≃c C :=
+  equivalence.mk _ !is_equivalence_id
+
+  definition isomorphism.refl [refl] [constructor] : C ≅c C :=
+  isomorphism.mk _ !is_isomorphism_id
+
+  variable {C}
+
+  definition equivalence.symm [symm] [constructor] (H : C ≃c D) : D ≃c C :=
+  equivalence.mk _ (is_equivalence_inverse H)
+
+  definition isomorphism.symm [symm] [constructor] (H : C ≅c D) : D ≅c C :=
+  isomorphism.mk _ (is_isomorphism_strict_inverse H)
+
+  definition equivalence.trans [trans] [constructor] (H : C ≃c D) (K : D ≃c E) : C ≃c E :=
+  equivalence.mk _ (is_equivalence_compose K H)
+
+  definition isomorphism.trans [trans] [constructor] (H : C ≅c D) (K : D ≅c E) : C ≅c E :=
+  isomorphism.mk _ (is_isomorphism_compose K H)
+
+  definition equivalence.to_strict_inverse [unfold 3] (H : C ≃c D) : D ⇒ C :=
+  H⁻¹ᴱ
+
+  definition isomorphism.to_strict_inverse [unfold 3] (H : C ≅c D) : D ⇒ C :=
+  H⁻¹ˢ
+
+  definition is_isomorphism_of_is_equivalence [constructor] {C D : Category} (F : C ⇒ D)
+    [H : is_equivalence F] : is_isomorphism F :=
+  begin
+    fapply is_isomorphism.mk,
+    { exact F⁻¹ᴱ},
+    { apply eq_of_iso, apply iso_unit},
+    { apply eq_of_iso, apply iso_counit},
+  end
+
+  definition isomorphism_of_equivalence [constructor] {C D : Category} (F : C ≃c D) : C ≅c D :=
+  isomorphism.mk F !is_isomorphism_of_is_equivalence
+
+  definition equivalence_eq {C : Category} {D : Precategory} {F F' : C ≃c D}
+    (p : equivalence.to_functor F = equivalence.to_functor F') : F = F' :=
+  begin
+    induction F, induction F', exact apd011 equivalence.mk p !is_hprop.elim
+  end
+
+  definition isomorphism_eq {F F' : C ≅c D}
+    (p : isomorphism.to_functor F = isomorphism.to_functor F') : F = F' :=
+  begin
+    induction F, induction F', exact apd011 isomorphism.mk p !is_hprop.elim
+  end
+
+  definition is_equiv_isomorphism_of_equivalence [constructor] (C D : Category)
+    : is_equiv (@equivalence_of_isomorphism C D) :=
+  begin
+    fapply adjointify,
+    { exact isomorphism_of_equivalence},
+    { intro F, apply equivalence_eq, reflexivity},
+    { intro F, apply isomorphism_eq, reflexivity},
+  end
+
+  definition isomorphism_equiv_equivalence [constructor] (C D : Category)
+    : (C ≅c D) ≃ (C ≃c D) :=
+  equiv.mk _ !is_equiv_isomorphism_of_equivalence
+
+  definition isomorphism_of_eq [constructor] {C D : Precategory} (p : C = D) : C ≅c D :=
+  isomorphism.MK (functor_of_eq p)
+                 (functor_of_eq p⁻¹)
+                 (by induction p; reflexivity)
+                 (by induction p; reflexivity)
+
+  definition equiv_ob_of_isomorphism [constructor] {C D : Precategory} (H : C ≅c D) : C ≃ D :=
+  equiv.mk H _
+
+  definition equiv_hom_of_isomorphism [constructor] {C D : Precategory} (H : C ≅c D) (c c' : C)
+    : c ⟶ c' ≃ H c ⟶ H c' :=
+  equiv.mk (to_fun_hom (isomorphism.to_functor H)) _
+
+  definition is_equiv_isomorphism_of_eq [constructor] (C D : Precategory)
+    : is_equiv (@isomorphism_of_eq C D) :=
+  begin
+    fapply adjointify,
+    { intro H, fapply Precategory_eq_of_equiv,
+      { apply equiv_ob_of_isomorphism H},
+      { exact equiv_hom_of_isomorphism H},
+      { /-exact sorry FAILS-/ intros, esimp, apply respect_comp}},
+    { intro H, apply isomorphism_eq, esimp, fapply functor_eq: esimp,
+      { intro c, exact sorry},
+      { exact sorry}},
+    { intro p, induction p, esimp, exact sorry},
+  end
+
+  definition eq_equiv_isomorphism [constructor] (C D : Precategory)
+    : (C = D) ≃ (C ≅c D) :=
+  equiv.mk _ !is_equiv_isomorphism_of_eq
+
+  definition equivalence_of_eq [unfold 3] [reducible] {C D : Precategory} (p : C = D) : C ≃c D :=
+  equivalence_of_isomorphism (isomorphism_of_eq p)
+
+  definition eq_equiv_equivalence [constructor] (C D : Category) : (C = D) ≃ (C ≃c D) :=
+  !eq_equiv_isomorphism ⬝e !isomorphism_equiv_equivalence
+
+  /- TODO
+  definition is_equivalence_equiv [constructor] (F : C ⇒ D)
     : is_equivalence F ≃ (fully_faithful F × split_essentially_surjective F) :=
   sorry
 
+  definition is_equivalence_equiv_is_weak_equivalence [constructor] {C D : Category}
+    (F : C ⇒ D) : is_equivalence F ≃ is_weak_equivalence F :=
+  sorry
+  -/
+
+
+/- TODO?
   definition is_isomorphism_equiv1 (F : C ⇒ D) : is_equivalence F
     ≃ Σ(G : D ⇒ C) (η : 1 = G ∘f F) (ε : F ∘f G = 1),
-        sorry ▸ ap (λ(H : C ⇒ C), F ∘f H) η = ap (λ(H : D ⇒ D), H ∘f F) ε⁻¹ :=
+        sorry ⬝ ap (λ(H : C ⇒ C), F ∘f H) η ⬝ sorry = ap (λ(H : D ⇒ D), H ∘f F) ε⁻¹ :=
   sorry
 
   definition is_isomorphism_equiv2 (F : C ⇒ D) : is_equivalence F
     ≃ ∃(G : D ⇒ C), 1 = G ∘f F × F ∘f G = 1 :=
   sorry
-
-  definition isomorphism_of_eq {C D : Precategory} (p : C = D) : C ≅c D :=
-  sorry
-
-  definition is_equiv_isomorphism_of_eq (C D : Precategory) : is_equiv (@isomorphism_of_eq C D) :=
-  sorry
-
-  definition equivalence_of_eq {C D : Precategory} (p : C = D) : C ≃c D :=
-  sorry
-
-  definition is_isomorphism_of_is_equivalence {C D : Category} {F : C ⇒ D} (H : is_equivalence F)
-    : is_isomorphism F :=
-  sorry
-
-  definition is_equivalence_equiv_is_weak_equivalence {C D : Category} (F : C ⇒ D)
-    : is_equivalence F ≃ is_weak_equivalence F :=
-  sorry
-
-  definition is_equiv_equivalence_of_eq (C D : Category) : is_equiv (@equivalence_of_eq C D) :=
-  sorry
-
 -/
+
 end category
diff --git a/hott/algebra/category/functor/exponential_laws.hlean b/hott/algebra/category/functor/exponential_laws.hlean
new file mode 100644
index 0000000000..7c325ab8fd
--- /dev/null
+++ b/hott/algebra/category/functor/exponential_laws.hlean
@@ -0,0 +1,226 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn, Jakob von Raumer
+
+Exponential laws
+-/
+
+import .functor.equivalence .functor.curry
+       .constructions.terminal .constructions.initial .constructions.product .constructions.sum
+
+open eq category functor is_trunc nat_trans iso unit prod sum prod.ops
+
+
+namespace category
+
+  /- C ^ 0 ≅ 1 -/
+
+  definition functor_zero_iso_one [constructor] (C : Precategory) : C ^c 0 ≅c 1 :=
+  begin
+    fapply isomorphism.MK,
+    { apply terminal_functor},
+    { apply point, apply initial_functor},
+    { fapply functor_eq: intros; esimp at *,
+      { apply eq_of_is_contr},
+      { apply nat_trans_eq, intro u, induction u}},
+    { fapply functor_eq: intros; esimp at *,
+      { induction x, reflexivity},
+      { induction f, reflexivity}},
+  end
+
+  /- 0 ^ C ≅ 0 if C is inhabited -/
+
+  definition zero_functor_functor_zero [constructor] (C : Precategory) (c : C) : 0 ^c C ⇒ 0 :=
+  begin
+    fapply functor.mk: esimp,
+    { intro F, exact F c},
+    { intro F, apply empty.elim (F c)},
+    { intro F, apply empty.elim (F c)},
+    { intro F, apply empty.elim (F c)},
+  end
+
+  definition zero_functor_iso_zero [constructor] (C : Precategory) (c : C) : 0 ^c C ≅c 0 :=
+  begin
+    fapply isomorphism.MK,
+    { exact zero_functor_functor_zero C c},
+    { apply initial_functor},
+    { fapply functor_eq: esimp,
+      { intro F, apply empty.elim (F c)},
+      { intro F, apply empty.elim (F c)}},
+    { fapply functor_eq: esimp,
+      { intro u, apply empty.elim u},
+      { apply empty.elim}},
+  end
+
+
+  /- C ^ 1 ≅ C -/
+
+  definition functor_one_iso [constructor] (C : Precategory) : C ^c 1 ≅c C :=
+  begin
+    fapply isomorphism.MK,
+    { exact !eval_functor star},
+    { apply functor_curry, apply pr1_functor},
+    { fapply functor_eq: esimp,
+      { intro F, fapply functor_eq: esimp,
+        { intro u, induction u, reflexivity},
+        { intro u v f, induction u, induction v, induction f, esimp, rewrite [+id_id,-respect_id]}},
+      { intro F G η, apply nat_trans_eq, intro u, esimp,
+        rewrite [natural_map_hom_of_eq _ u, natural_map_inv_of_eq _ u,▸*,+ap010_functor_eq _ _ u],
+        induction u, rewrite [▸*, id_leftright], }},
+    { fapply functor_eq: esimp,
+      { intro c d f, rewrite [▸*, id_leftright] }},
+  end
+
+  /- 1 ^ C ≅ 1 -/
+
+  definition one_functor_iso_one [constructor] (C : Precategory) : 1 ^c C ≅c 1 :=
+  begin
+    fapply isomorphism.MK,
+    { apply terminal_functor},
+    { apply functor_curry, apply pr1_functor},
+    { fapply functor_eq: esimp,
+      { intro F, fapply functor_eq: esimp,
+        { intro c, apply unit.eta},
+        { intro c d f, apply unit.eta}},
+      { intro F G η, fapply nat_trans_eq, esimp, intro c, apply unit.eta}},
+    { fapply functor_eq: esimp,
+      { intro u, apply unit.eta},
+      { intro u v f, apply unit.eta}},
+  end
+
+  /- C ^ (D + E) ≅ C ^ D × C ^ E -/
+
+  definition functor_sum_right [constructor] (C D E : Precategory)
+    : C ^c (D +c E) ⇒ C ^c D ×c C ^c E :=
+  begin
+    apply functor_prod,
+    { apply precomposition_functor, apply inl_functor},
+    { apply precomposition_functor, apply inr_functor}
+  end
+
+  definition functor_sum_left [constructor] (C D E : Precategory)
+    : C ^c D ×c C ^c E ⇒ C ^c (D +c E) :=
+  begin
+    fapply functor.mk: esimp,
+    { intro V, exact V.1 +f V.2},
+    { intro V W ν, apply sum_nat_trans, exact ν.1, exact ν.2},
+    { intro V, apply nat_trans_eq, intro a, induction a: reflexivity},
+    { intro U V W ν μ, apply nat_trans_eq, intro a, induction a: reflexivity}
+      -- REPORT: cannot abstract
+  end
+
+  /- TODO: optimize -/
+  definition functor_sum_iso [constructor] (C D E : Precategory)
+    : C ^c (D +c E) ≅c C ^c D ×c C ^c E :=
+  begin
+    fapply isomorphism.MK,
+    { apply functor_sum_right},
+    { apply functor_sum_left},
+    { fapply functor_eq: esimp,
+      { exact sum_functor_eta},
+      { intro F G η, fapply nat_trans_eq, intro a, esimp,
+        rewrite [@natural_map_hom_of_eq _ _ _ G _ a, @natural_map_inv_of_eq _ _ _ F _ a,
+                 ↑sum_functor_eta,+ap010_functor_eq _ _ a],
+        induction a: esimp: apply id_leftright}},
+    { fapply functor_eq: esimp,
+      { intro V, induction V with F G, apply prod_eq: esimp,
+        apply sum_functor_inl, apply sum_functor_inr},
+      { intro V W ν, induction V with F G, induction W with F' G', induction ν with η θ,
+        apply prod_eq: apply nat_trans_eq,
+        { intro d, rewrite [▸*,@pr1_hom_of_eq (C ^c D) (C ^c E), @pr1_inv_of_eq (C ^c D) (C ^c E),
+            @natural_map_hom_of_eq _ _ _ F' _ d, @natural_map_inv_of_eq _ _ _ F _ d,
+            ↑sum_functor_inl,+ap010_functor_eq _ _ d, ▸*], apply id_leftright},
+        { intro e, rewrite [▸*,@pr2_hom_of_eq (C ^c D) (C ^c E), @pr2_inv_of_eq (C ^c D) (C ^c E),
+            @natural_map_hom_of_eq _ _ _ G' _ e, @natural_map_inv_of_eq _ _ _ G _ e,
+            ↑sum_functor_inr,+ap010_functor_eq _ _ e, ▸*], apply id_leftright}}},
+  end
+
+  /- (C × D) ^ E ≅ C ^ E × D ^ E -/
+
+  definition prod_functor_right [constructor] (C D E : Precategory)
+    : (C ×c D) ^c E ⇒ C ^c E ×c D ^c E :=
+  begin
+    apply functor_prod,
+    { apply postcomposition_functor, apply pr1_functor},
+    { apply postcomposition_functor, apply pr2_functor}
+  end
+
+  definition prod_functor_left [constructor] (C D E : Precategory)
+    : C ^c E ×c D ^c E ⇒ (C ×c D) ^c E :=
+  begin
+    fapply functor.mk: esimp,
+    { intro V, exact V.1 ×f V.2},
+    { intro V W ν, exact prod_nat_trans ν.1 ν.2},
+    { intro V, apply nat_trans_eq, intro e, reflexivity},
+    { intro U V W ν μ, apply nat_trans_eq, intro e, reflexivity}
+  end
+
+  definition prod_functor_iso [constructor] (C D E : Precategory)
+    : (C ×c D) ^c E ≅c C ^c E ×c D ^c E :=
+  begin
+    fapply isomorphism.MK,
+    { apply prod_functor_right},
+    { apply prod_functor_left},
+    { fapply functor_eq: esimp,
+      { exact prod_functor_eta},
+      { intro F G η, fapply nat_trans_eq, intro e, esimp,
+        rewrite [@natural_map_hom_of_eq _ _ _ G, @natural_map_inv_of_eq _ _ _ F,↑prod_functor_eta,
+          +ap010_functor_eq, +hom_of_eq_inv, ▸*, pr1_hom_of_eq, pr2_hom_of_eq,
+          pr1_inv_of_eq, pr2_inv_of_eq, ▸*, +id_leftright, prod.eta]}},
+    { fapply functor_eq: esimp,
+      { intro V, apply prod_eq: esimp, apply pr1_functor_prod, apply pr2_functor_prod},
+      { intro V W ν, rewrite [@pr1_hom_of_eq (C ^c E) (D ^c E), @pr2_hom_of_eq (C ^c E) (D ^c E),
+          @pr1_inv_of_eq (C ^c E) (D ^c E), @pr2_inv_of_eq (C ^c E) (D ^c E)],
+        apply prod_eq: apply nat_trans_eq: intro v: esimp,
+        { rewrite [@natural_map_hom_of_eq _ _ _ W.1, @natural_map_inv_of_eq _ _ _ V.1, ▸*,
+            ↑pr1_functor_prod,+ap010_functor_eq, ▸*, id_leftright]},
+        { rewrite [@natural_map_hom_of_eq _ _ _ W.2, @natural_map_inv_of_eq _ _ _ V.2, ▸*,
+            ↑pr2_functor_prod,+ap010_functor_eq, ▸*, id_leftright]}}},
+  end
+
+  /- (C ^ D) ^ E ≅ C ^ (E × D) -/
+
+  definition functor_functor_right [constructor] (C D E : Precategory)
+    : (C ^c D) ^c E ⇒ C ^c (E ×c D) :=
+  begin
+    fapply functor.mk: esimp,
+    { exact functor_uncurry},
+    { apply @nat_trans_uncurry},
+    { intro F, apply nat_trans_eq, intro e, reflexivity},
+    { intro F G H η θ, apply nat_trans_eq, intro e, reflexivity}
+  end
+
+  definition functor_functor_left [constructor] (C D E : Precategory)
+    : C ^c (E ×c D) ⇒ (C ^c D) ^c E :=
+  begin
+    fapply functor.mk: esimp,
+    { exact functor_curry},
+    { apply @nat_trans_curry},
+    { intro F, apply nat_trans_eq, intro e, reflexivity},
+    { intro F G H η θ, apply nat_trans_eq, intro e, reflexivity}
+  end
+
+  definition functor_functor_iso [constructor] (C D E : Precategory)
+    : (C ^c D) ^c E ≅c C ^c (E ×c D) :=
+  begin
+    fapply isomorphism.MK: esimp,
+    { apply functor_functor_right},
+    { apply functor_functor_left},
+    { fapply functor_eq: esimp,
+      { exact functor_curry_functor_uncurry},
+      { intro F G η, fapply nat_trans_eq, intro e, esimp,
+        rewrite [@natural_map_hom_of_eq _ _ _ G, @natural_map_inv_of_eq _ _ _ F,
+          ↑functor_curry_functor_uncurry, +@ap010_functor_eq E (C ^c D)],
+        apply nat_trans_eq, intro d, rewrite [▸*, hom_of_eq_inv,
+          @natural_map_hom_of_eq _ _ _ (G e), @natural_map_inv_of_eq _ _ _ (F e),
+          ↑functor_curry_functor_uncurry_ob, +@ap010_functor_eq D C, ▸*, id_leftright]}},
+    { fapply functor_eq: esimp,
+      { intro F, apply functor_uncurry_functor_curry},
+      { intro F G η, fapply nat_trans_eq, esimp, intro v, induction v with c d,
+        rewrite [@natural_map_hom_of_eq _ _ _ G, @natural_map_inv_of_eq _ _ _ F,
+          ↑functor_uncurry_functor_curry, +@ap010_functor_eq, ▸*], apply id_leftright}},
+  end
+
+
+end category
diff --git a/hott/algebra/category/functor/functor.hlean b/hott/algebra/category/functor/functor.hlean
index 47ff01343a..f1ca688f24 100644
--- a/hott/algebra/category/functor/functor.hlean
+++ b/hott/algebra/category/functor/functor.hlean
@@ -38,7 +38,7 @@ namespace functor
       G (F (g ∘ f)) = G (F g ∘ F f)     : by rewrite respect_comp
                 ... = G (F g) ∘ G (F f) : by rewrite respect_comp end)
 
-  infixr ` ∘f `:60 := functor.compose
+  infixr ` ∘f `:75 := functor.compose
 
   protected definition id [reducible] [constructor] {C : Precategory} : functor C C :=
   mk (λa, a) (λ a b f, f) (λ a, idp) (λ a b c f g, idp)
@@ -52,6 +52,7 @@ namespace functor
              (λc, idp)
              (λa b c g f, !id_id⁻¹)
 
+  /- introduction rule for equalities between functors -/
   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₂)
@@ -149,7 +150,12 @@ namespace functor
   protected definition comp_id_eq_id_comp (F : C ⇒ D) : F ∘f 1 = 1 ∘f F :=
   !functor.id_right ⬝ !functor.id_left⁻¹
 
-  -- "functor C D" is equivalent to a certain sigma type
+  definition functor_of_eq [constructor] {C D : Precategory} (p : C = D :> Precategory) : C ⇒ D :=
+  functor.mk (transport carrier p)
+             (λa b f, by induction p; exact f)
+             (by intro c; induction p; reflexivity)
+             (by intros; induction p; reflexivity)
+
   protected definition sigma_char :
     (Σ (to_fun_ob : C → D)
     (to_fun_hom : Π ⦃a b : C⦄, hom a b → hom (to_fun_ob a) (to_fun_ob b)),
@@ -173,10 +179,11 @@ namespace functor
     by apply is_trunc_equiv_closed; apply functor.sigma_char
   end
 
+  /- higher equalities in the functor type -/
   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)),
+    fapply apd011 (apd01111 functor.mk idp idp),
     apply is_hset.elim,
     apply is_hset.elim
   end
@@ -188,7 +195,7 @@ namespace functor
       : functor_eq' (ap to_fun_ob p) (!tr_compose⁻¹ ⬝ apd to_fun_hom p) = p :=
   begin
     cases p, cases F₁,
-    apply concat, rotate_left 1, apply functor_eq'_idp,
+    refine _ ⬝ !functor_eq'_idp,
     esimp
   end
 
diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean
index 914f862e59..97578a9ed6 100644
--- a/hott/algebra/category/iso.hlean
+++ b/hott/algebra/category/iso.hlean
@@ -16,7 +16,7 @@ namespace iso
     {section_of : b ⟶ a}
     (comp_section : f ∘ section_of = id)
   structure is_iso [class] {ob : Type} [C : precategory ob] {a b : ob} (f : a ⟶ b) :=
-    {inverse : b ⟶ a}
+    (inverse : b ⟶ a)
     (left_inverse  : inverse ∘ f = id)
     (right_inverse : f ∘ inverse = id)
 
@@ -39,81 +39,82 @@ namespace iso
   variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a}
   include C
 
-  definition split_mono_of_is_iso [instance] [priority 300] [reducible]
+  definition split_mono_of_is_iso [constructor] [instance] [priority 300] [reducible]
     (f : a ⟶ b) [H : is_iso f] : split_mono f :=
   split_mono.mk !left_inverse
 
-  definition split_epi_of_is_iso [instance] [priority 300] [reducible]
+  definition split_epi_of_is_iso [constructor] [instance] [priority 300] [reducible]
     (f : a ⟶ b) [H : is_iso f] : split_epi f :=
   split_epi.mk !right_inverse
 
-  definition is_iso_id [instance] [priority 500] (a : ob) : is_iso (ID a) :=
-  is_iso.mk !id_id !id_id
+  definition is_iso_id [constructor] [instance] [priority 500] (a : ob) : is_iso (ID a) :=
+  is_iso.mk _ !id_id !id_id
 
-  definition is_iso_inverse [instance] [priority 200] (f : a ⟶ b) {H : is_iso f} : is_iso f⁻¹ :=
-  is_iso.mk !right_inverse !left_inverse
+  definition is_iso_inverse [constructor] [instance] [priority 200] (f : a ⟶ b) {H : is_iso f}
+    : is_iso f⁻¹ :=
+  is_iso.mk _ !right_inverse !left_inverse
 
-  definition left_inverse_eq_right_inverse {f : a ⟶ b} {g g' : hom b a}
+  theorem left_inverse_eq_right_inverse {f : a ⟶ b} {g g' : hom b a}
       (Hl : g ∘ f = id) (Hr : f ∘ g' = id) : g = g' :=
   by rewrite [-(id_right g), -Hr, assoc, Hl, id_left]
 
-  definition retraction_eq [H : split_mono f] (H2 : f ∘ h = id) : retraction_of f = h :=
+  theorem retraction_eq [H : split_mono f] (H2 : f ∘ h = id) : retraction_of f = h :=
   left_inverse_eq_right_inverse !retraction_comp H2
 
-  definition section_eq [H : split_epi f] (H2 : h ∘ f = id) : section_of f = h :=
+  theorem section_eq [H : split_epi f] (H2 : h ∘ f = id) : section_of f = h :=
   (left_inverse_eq_right_inverse H2 !comp_section)⁻¹
 
-  definition inverse_eq_right [H : is_iso f] (H2 : f ∘ h = id) : f⁻¹ = h :=
+  theorem inverse_eq_right [H : is_iso f] (H2 : f ∘ h = id) : f⁻¹ = h :=
   left_inverse_eq_right_inverse !left_inverse H2
 
-  definition inverse_eq_left [H : is_iso f] (H2 : h ∘ f = id) : f⁻¹ = h :=
+  theorem inverse_eq_left [H : is_iso f] (H2 : h ∘ f = id) : f⁻¹ = h :=
   (left_inverse_eq_right_inverse H2 !right_inverse)⁻¹
 
-  definition retraction_eq_section (f : a ⟶ b) [Hl : split_mono f] [Hr : split_epi f] :
+  theorem retraction_eq_section (f : a ⟶ b) [Hl : split_mono f] [Hr : split_epi f] :
       retraction_of f = section_of f :=
   retraction_eq !comp_section
 
-  definition is_iso_of_split_epi_of_split_mono (f : a ⟶ b) [Hl : split_mono f] [Hr : split_epi f]
-    : is_iso f :=
-  is_iso.mk ((retraction_eq_section f) ▸ (retraction_comp f)) (comp_section f)
+  definition is_iso_of_split_epi_of_split_mono [constructor] (f : a ⟶ b)
+    [Hl : split_mono f] [Hr : split_epi f] : is_iso f :=
+  is_iso.mk _ ((retraction_eq_section f) ▸ (retraction_comp f)) (comp_section f)
 
-  definition inverse_unique (H H' : is_iso f) : @inverse _ _ _ _ f H = @inverse _ _ _ _ f H' :=
+  theorem inverse_unique (H H' : is_iso f) : @inverse _ _ _ _ f H = @inverse _ _ _ _ f H' :=
   inverse_eq_left !left_inverse
 
-  definition inverse_involutive (f : a ⟶ b) [H : is_iso f] [H : is_iso (f⁻¹)]
+  theorem inverse_involutive (f : a ⟶ b) [H : is_iso f] [H : is_iso (f⁻¹)]
     : (f⁻¹)⁻¹ = f :=
   inverse_eq_right !left_inverse
 
-  definition inverse_eq_inverse {f g : a ⟶ b} [H : is_iso f] [H : is_iso g] (p : f = g)
+  theorem inverse_eq_inverse {f g : a ⟶ b} [H : is_iso f] [H : is_iso g] (p : f = g)
     : f⁻¹ = g⁻¹ :=
   by cases p;apply inverse_unique
 
-  definition retraction_id (a : ob) : retraction_of (ID a) = id :=
+  theorem retraction_id (a : ob) : retraction_of (ID a) = id :=
   retraction_eq !id_id
 
-  definition section_id (a : ob) : section_of (ID a) = id :=
+  theorem section_id (a : ob) : section_of (ID a) = id :=
   section_eq !id_id
 
-  definition id_inverse (a : ob) [H : is_iso (ID a)] : (ID a)⁻¹ = id :=
+  theorem id_inverse (a : ob) [H : is_iso (ID a)] : (ID a)⁻¹ = id :=
   inverse_eq_left !id_id
 
-  definition split_mono_comp [instance] [priority 150] (g : b ⟶ c) (f : a ⟶ b)
+  definition split_mono_comp [constructor] [instance] [priority 150] (g : b ⟶ c) (f : a ⟶ b)
     [Hf : split_mono f] [Hg : split_mono g] : split_mono (g ∘ f) :=
   split_mono.mk
     (show (retraction_of f ∘ retraction_of g) ∘ g ∘ f = id,
      by rewrite [-assoc, assoc _ g f, retraction_comp, id_left, retraction_comp])
 
-  definition split_epi_comp [instance] [priority 150] (g : b ⟶ c) (f : a ⟶ b)
+  definition split_epi_comp [constructor] [instance] [priority 150] (g : b ⟶ c) (f : a ⟶ b)
     [Hf : split_epi f] [Hg : split_epi g] : split_epi (g ∘ f) :=
   split_epi.mk
     (show (g ∘ f) ∘ section_of f ∘ section_of g = id,
      by rewrite [-assoc, {f ∘ _}assoc, comp_section, id_left, comp_section])
 
-  definition is_iso_comp [instance] [priority 150] (g : b ⟶ c) (f : a ⟶ b)
+  definition is_iso_comp [constructor] [instance] [priority 150] (g : b ⟶ c) (f : a ⟶ b)
     [Hf : is_iso f] [Hg : is_iso g] : is_iso (g ∘ f) :=
   !is_iso_of_split_epi_of_split_mono
 
-  definition is_hprop_is_iso [instance] (f : hom a b) : is_hprop (is_iso f) :=
+  theorem is_hprop_is_iso [instance] (f : hom a b) : is_hprop (is_iso f) :=
   begin
     apply is_hprop.mk, intro H H',
     cases H with g li ri, cases H' with g' li' ri',
@@ -132,6 +133,7 @@ structure iso {ob : Type} [C : precategory ob] (a b : ob) :=
   [struct : is_iso to_hom]
 
   infix ` ≅ `:50 := iso
+  notation c ` ≅[`:50 C:0 `] `:0 c':50 := @iso C _ c c'
   attribute iso.struct [instance] [priority 2000]
 
 namespace iso
@@ -143,7 +145,7 @@ namespace iso
 
   protected definition MK [constructor] (f : a ⟶ b) (g : b ⟶ a)
     (H1 : g ∘ f = id) (H2 : f ∘ g = id) :=
-  @(mk f) (is_iso.mk H1 H2)
+  @(mk f) (is_iso.mk _ H1 H2)
 
   variable {C}
   definition to_inv [reducible] [unfold 5] (f : a ≅ b) : b ⟶ a := (to_hom f)⁻¹
@@ -165,10 +167,10 @@ namespace iso
   infixl ` ⬝i `:75 := iso.trans
   postfix [parsing_only] `⁻¹ⁱ`:(max + 1) := iso.symm
 
-  definition change_hom (H : a ≅ b) (f : a ⟶ b) (p : to_hom H = f) : a ≅ b :=
+  definition change_hom [constructor] (H : a ≅ b) (f : a ⟶ b) (p : to_hom H = f) : a ≅ b :=
   iso.MK f (to_inv H) (p ▸ to_left_inverse H) (p ▸ to_right_inverse H)
 
-  definition change_inv (H : a ≅ b) (g : b ⟶ a) (p : to_inv H = g) : a ≅ b :=
+  definition change_inv [constructor] (H : a ≅ b) (g : b ⟶ a) (p : to_inv H = g) : a ≅ b :=
   iso.MK (to_hom H) g (p ▸ to_left_inverse H) (p ▸ to_right_inverse H)
 
   definition iso_mk_eq {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f')
@@ -210,6 +212,12 @@ namespace iso
   definition iso_of_eq_inv (p : a = b) : iso_of_eq p⁻¹ = iso.symm (iso_of_eq p) :=
   eq.rec_on p idp
 
+  theorem hom_of_eq_inv (p : a = b) : hom_of_eq p⁻¹ = inv_of_eq p :=
+  eq.rec_on p idp
+
+  theorem inv_of_eq_inv (p : a = b) : inv_of_eq p⁻¹ = hom_of_eq p :=
+  eq.rec_on p idp
+
   definition iso_of_eq_con (p : a = b) (q : b = c)
     : 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 !id_id⁻¹))
diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean
index e2fb4d08cd..a151f00a84 100644
--- a/hott/algebra/category/nat_trans.hlean
+++ b/hott/algebra/category/nat_trans.hlean
@@ -182,5 +182,5 @@ namespace nat_trans
 
 end nat_trans
 
-attribute nat_trans.compose_rev [trans] -- TODO: this doesn't work
+attribute nat_trans.compose_rev [trans]
 attribute nat_trans.id [refl]
diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean
index ee90e564f3..b3e25029a1 100644
--- a/hott/algebra/category/precategory.hlean
+++ b/hott/algebra/category/precategory.hlean
@@ -5,7 +5,7 @@ Authors: Floris van Doorn
 -/
 import types.trunc types.pi arity
 
-open eq is_trunc pi
+open eq is_trunc pi equiv equiv.ops
 
 namespace category
 
@@ -37,7 +37,7 @@ namespace category
   -- input ⟶ using \--> (this is a different arrow than \-> (→))
   infixl [parsing_only] ` ⟶ `:25 := precategory.hom
   namespace hom
-    infixl ` ⟶ `:25 := precategory.hom -- if you open this namespace, hom a b is printed as a ⟶ b
+    infixl ` ⟶ `:60 := precategory.hom -- if you open this namespace, hom a b is printed as a ⟶ b
   end hom
 
   abbreviation hom         [unfold 2] := @precategory.hom
@@ -143,7 +143,7 @@ namespace category
   definition precategory.MK [reducible] [constructor] (a b c d e f g h) : Precategory :=
   Precategory.mk a (@precategory.mk a b c d e f g h)
 
-  abbreviation carrier := @Precategory.carrier
+  abbreviation carrier [unfold 1] := @Precategory.carrier
 
   attribute Precategory.carrier [coercion]
   attribute Precategory.struct [instance] [priority 10000] [coercion]
@@ -157,93 +157,123 @@ namespace category
   Precategory.rec (λob c, idp) C
 
   /-Characterization of paths between precategories-/
+  -- introduction tule for paths between precategories
 
-  definition precategory_mk'_eq (ob : Type)
-    (hom1 : ob → ob → Type)
-    (hom2 : ob → ob → Type)
-    (homH1 : Π(a b : ob), is_hset (hom1 a b))
-    (homH2 : Π(a b : ob), is_hset (hom2 a b))
-    (comp1 : Π⦃a b c : ob⦄, hom1 b c → hom1 a b → hom1 a c)
-    (comp2 : Π⦃a b c : ob⦄, hom2 b c → hom2 a b → hom2 a c)
-    (ID1 : Π (a : ob), hom1 a a)
-    (ID2 : Π (a : ob), hom2 a a)
-    (assoc1 : Π ⦃a b c d : ob⦄ (h : hom1 c d) (g : hom1 b c) (f : hom1 a b),
-       comp1 h (comp1 g f) = comp1 (comp1 h g) f)
-    (assoc2 : Π ⦃a b c d : ob⦄ (h : hom2 c d) (g : hom2 b c) (f : hom2 a b),
-       comp2 h (comp2 g f) = comp2 (comp2 h g) f)
-    (assoc1' : Π ⦃a b c d : ob⦄ (h : hom1 c d) (g : hom1 b c) (f : hom1 a b),
-       comp1 (comp1 h g) f = comp1 h (comp1 g f))
-    (assoc2' : Π ⦃a b c d : ob⦄ (h : hom2 c d) (g : hom2 b c) (f : hom2 a b),
-       comp2 (comp2 h g) f = comp2 h (comp2 g f))
-    (id_left1 : Π ⦃a b : ob⦄ (f : hom1 a b), comp1 !ID1 f = f)
-    (id_left2 : Π ⦃a b : ob⦄ (f : hom2 a b), comp2 !ID2 f = f)
-    (id_right1 : Π ⦃a b : ob⦄ (f : hom1 a b), comp1 f !ID1 = f)
-    (id_right2 : Π ⦃a b : ob⦄ (f : hom2 a b), comp2 f !ID2 = f)
-    (id_id1 : Π (a : ob), comp1 !ID1 !ID1 = ID1 a)
-    (id_id2 : Π (a : ob), comp2 !ID2 !ID2 = ID2 a)
-    (p : hom1 = hom2)
-    (q : p ▸ comp1 = comp2)
-    (r : p ▸ ID1 = ID2) :
-    precategory.mk' hom1 comp1 ID1 assoc1 assoc1' id_left1 id_right1 id_id1 homH1
-    = precategory.mk' hom2 comp2 ID2 assoc2 assoc2' id_left2 id_right2 id_id2 homH2 :=
+  definition precategory_eq {ob : Type}
+    {C D : precategory ob}
+    (p : Π{a b}, @hom ob C a b = @hom ob D a b)
+    (q : Πa b c g f, cast p (@comp ob C a b c g f) = @comp ob D a b c (cast p g) (cast p f))
+      : C = D :=
   begin
-    cases p, cases q, cases r,
-    apply (ap0111111 (precategory.mk' hom2 comp2 ID2)),
-    repeat (apply is_hprop.elim),
+    induction C with hom1 comp1 ID1 a b il ir, induction D with hom2 comp2 ID2 a' b' il' ir',
+    esimp at *,
+    revert q, eapply homotopy2.rec_on @p, esimp, clear p, intro p q, induction p,
+    esimp at *,
+    assert H : comp1 = comp2,
+    { apply eq_of_homotopy3, intros, apply eq_of_homotopy2, intros, apply q},
+    induction H,
+    assert K : ID1 = ID2,
+    { apply eq_of_homotopy, intro a, exact !ir'⁻¹ ⬝ !il},
+    induction K,
+    apply ap0111111 (precategory.mk' hom1 comp1 ID1): apply is_hprop.elim
   end
 
-  definition precategory_eq (ob : Type)
-    (C D : precategory ob)
-    (p : @hom ob C = @hom ob D)
-    (q : transport (λ x, Πa b c, x b c → x a b → x a c) p
-           (@comp ob C) = @comp ob D)
-    (r : transport (λ x, Πa, x a a) p (@ID ob C) = @ID ob D) : C = D :=
-  begin
-    cases C, cases D,
-    apply precategory_mk'_eq, apply q, apply r,
-  end
 
-  definition precategory_mk_eq (ob : Type)
-    (hom1 : ob → ob → Type)
-    (hom2 : ob → ob → Type)
-    (homH1 : Π(a b : ob), is_hset (hom1 a b))
-    (homH2 : Π(a b : ob), is_hset (hom2 a b))
-    (comp1 : Π⦃a b c : ob⦄, hom1 b c → hom1 a b → hom1 a c)
-    (comp2 : Π⦃a b c : ob⦄, hom2 b c → hom2 a b → hom2 a c)
-    (ID1 : Π (a : ob), hom1 a a)
-    (ID2 : Π (a : ob), hom2 a a)
-    (assoc1 : Π ⦃a b c d : ob⦄ (h : hom1 c d) (g : hom1 b c) (f : hom1 a b),
-       comp1 h (comp1 g f) = comp1 (comp1 h g) f)
-    (assoc2 : Π ⦃a b c d : ob⦄ (h : hom2 c d) (g : hom2 b c) (f : hom2 a b),
-       comp2 h (comp2 g f) = comp2 (comp2 h g) f)
-    (id_left1 : Π ⦃a b : ob⦄ (f : hom1 a b), comp1 !ID1 f = f)
-    (id_left2 : Π ⦃a b : ob⦄ (f : hom2 a b), comp2 !ID2 f = f)
-    (id_right1 : Π ⦃a b : ob⦄ (f : hom1 a b), comp1 f !ID1 = f)
-    (id_right2 : Π ⦃a b : ob⦄ (f : hom2 a b), comp2 f !ID2 = f)
-    (p : Π (a b : ob), hom1 a b = hom2 a b)
-    (q : transport (λ x, Π a b c, x b c → x a b → x a c)
-      (eq_of_homotopy (λ a, eq_of_homotopy (λ b, p a b))) @comp1 = @comp2)
-    (r : transport (λ x, Π a, x a a)
-      (eq_of_homotopy (λ (x : ob), eq_of_homotopy (λ (x_1 : ob), p x x_1)))
-         ID1 = ID2) :
-    precategory.mk hom1 comp1 ID1 assoc1 id_left1 id_right1
-    = precategory.mk hom2 comp2 ID2 assoc2 id_left2 id_right2 :=
+  definition precategory_eq_of_equiv {ob : Type}
+    {C D : precategory ob}
+    (p : Π⦃a b⦄, @hom ob C a b ≃ @hom ob D a b)
+    (q : Π{a b c} g f, p (@comp ob C a b c g f) = @comp ob D a b c (p g) (p f))
+      : C = D :=
   begin
     fapply precategory_eq,
-        apply eq_of_homotopy, intros,
-        apply eq_of_homotopy, intros,
-        exact (p _ _),
-      exact q,
-    exact r,
+    { intro a b, exact ua !@p},
+    { intros, refine !cast_ua ⬝ !q ⬝ _, apply ap011 !@comp !cast_ua⁻¹ !cast_ua⁻¹},
   end
 
-  definition Precategory_eq (C D : Precategory)
-    (p : carrier C = carrier D)
-    (q : p ▸ (Precategory.struct C) = Precategory.struct D) : C = D :=
+/- if we need to prove properties about precategory_eq, it might be easier with the following proof:
   begin
-    cases C, cases D,
-    cases p, cases q,
-    apply idp,
+    induction C with hom1 comp1 ID1, induction D with hom2 comp2 ID2, esimp at *,
+    assert H : Σ(s : hom1 = hom2), (λa b, equiv_of_eq (apd100 s a b)) = p,
+    { fconstructor,
+      { apply eq_of_homotopy2, intros, apply ua, apply p},
+      { apply eq_of_homotopy2, intros, rewrite [to_right_inv !eq_equiv_homotopy2, equiv_of_eq_ua]}},
+    induction H with H1 H2, induction H1, esimp at H2,
+    assert K : (λa b, equiv.refl) = p,
+    { refine _ ⬝ H2, apply eq_of_homotopy2, intros, exact !equiv_of_eq_refl⁻¹},
+    induction K, clear H2,
+    esimp at *,
+    assert H : comp1 = comp2,
+    { apply eq_of_homotopy3, intros, apply eq_of_homotopy2, intros, apply q},
+    assert K : ID1 = ID2,
+    { apply eq_of_homotopy, intros, apply r},
+    induction H, induction K,
+    apply ap0111111 (precategory.mk' hom1 comp1 ID1): apply is_hprop.elim
   end
+-/
+
+  definition Precategory_eq {C D : Precategory}
+    (p : carrier C = carrier D)
+    (q : Π{a b : C}, a ⟶ b = cast p a ⟶ cast p b)
+    (r : Π{a b c : C} (g : b ⟶ c) (f : a ⟶ b), cast q (g ∘ f) = cast q g ∘ cast q f)
+       : C = D :=
+  begin
+    induction C with X C, induction D with Y D, esimp at *, induction p,
+    esimp at *,
+    apply ap (Precategory.mk X),
+    apply precategory_eq @q @r
+  end
+
+  definition Precategory_eq_of_equiv {C D : Precategory}
+    (p : carrier C ≃ carrier D)
+    (q : Π⦃a b : C⦄, a ⟶ b ≃ p a ⟶ p b)
+    (r : Π{a b c : C} (g : b ⟶ c) (f : a ⟶ b), q (g ∘ f) = q g ∘ q f)
+       : C = D :=
+  begin
+    induction C with X C, induction D with Y D, esimp at *,
+    revert q r, eapply equiv.rec_on_ua p, clear p, intro p, induction p, esimp,
+    intros,
+    apply ap (Precategory.mk X),
+    apply precategory_eq_of_equiv @q @r
+  end
+
+  -- elimination rules for paths between precategories.
+  -- The first elimination rule is "ap carrier"
+
+  definition Precategory_eq_hom [unfold 3] {C D : Precategory} (p : C = D) (a b : C)
+    : hom a b = hom (cast (ap carrier p) a) (cast (ap carrier p) b) :=
+  by induction p; reflexivity
+  --(ap10 (ap10 (apd (λx, @hom (carrier x) (Precategory.struct x)) p⁻¹ᵖ) a) b)⁻¹ᵖ ⬝ _
+
+
+  -- beta/eta rules
+  definition ap_Precategory_eq' {C D : Precategory}
+    (p : carrier C = carrier D)
+    (q : Π{a b : C}, a ⟶ b = cast p a ⟶ cast p b)
+    (r : Π{a b c : C} (g : b ⟶ c) (f : a ⟶ b), cast q (g ∘ f) = cast q g ∘ cast q f)
+    (s : Πa, cast q (ID a) = ID (cast p a)) : ap carrier (Precategory_eq p @q @r) = p :=
+  begin
+    induction C with X C, induction D with Y D, esimp at *, induction p,
+    rewrite [↑Precategory_eq, -ap_compose,↑function.compose,ap_constant]
+  end
+
+  theorem Precategory_eq'_eta {C D : Precategory} (p : C = D) :
+    Precategory_eq
+      (ap carrier p)
+      (Precategory_eq_hom p)
+      (by induction p; intros; reflexivity) = p :=
+  begin
+    induction p, induction C with X C, unfold Precategory_eq,
+    induction C, unfold precategory_eq, exact sorry
+  end
+
+/-
+  theorem Precategory_eq2 {C D : Precategory} (p q : C = D)
+    (r : ap carrier p = ap carrier q)
+    (s : Precategory_eq_hom p =[r] Precategory_eq_hom q)
+      : p = q :=
+  begin
+
+  end
+-/
 
 end category
diff --git a/hott/arity.hlean b/hott/arity.hlean
index cd1d4d2b32..d6856eeb9c 100644
--- a/hott/arity.hlean
+++ b/hott/arity.hlean
@@ -48,8 +48,8 @@ namespace eq
   definition homotopy4 [reducible] (f g : Πa b c d, E a b c d) : Type :=
   Πa b c d, f a b c d = g a b c d
 
-  notation f `~2`:50 g := homotopy2 f g
-  notation f `~3`:50 g := homotopy3 f g
+  infix ` ~2 `:50 := homotopy2
+  infix ` ~3 `:50 := homotopy3
 
   definition ap011 (f : U → V → W) (Hu : u = u') (Hv : v = v') : f u v = f u' v' :=
   by cases Hu; congruence; repeat assumption
@@ -58,7 +58,8 @@ namespace eq
       : f u v w = f u' v' w' :=
   by cases Hu; congruence; repeat assumption
 
-  definition ap01111 (f : U → V → W → X → Y) (Hu : u = u') (Hv : v = v') (Hw : w = w') (Hx : x = x')
+  definition ap01111 (f : U → V → W → X → Y)
+    (Hu : u = u') (Hv : v = v') (Hw : w = w') (Hx : x = x')
       : f u v w x = f u' v' w' x' :=
   by cases Hu; congruence; repeat assumption
 
@@ -181,9 +182,10 @@ namespace eq
 
 end eq
 
-open eq is_equiv
+open eq equiv is_equiv
 namespace funext
-  definition is_equiv_apd100 [instance] (f g : Πa b, C a b) : is_equiv (@apd100 A B C f g) :=
+  definition is_equiv_apd100 [instance] (f g : Πa b, C a b)
+    : is_equiv (@apd100 A B C f g) :=
   adjointify _
              eq_of_homotopy2
              begin
@@ -213,6 +215,8 @@ namespace funext
              end
 end funext
 
+attribute funext.is_equiv_apd100 funext.is_equiv_apd1000 [constructor]
+
 namespace eq
   open funext
   local attribute funext.is_equiv_apd100 [instance]
@@ -224,6 +228,12 @@ namespace eq
     (p : f ~3 g) (H : Π(q : f = g), P (apd1000 q)) : P p :=
   right_inv apd1000 p ▸ H (eq_of_homotopy3 p)
 
+  definition eq_equiv_homotopy2 [constructor] (f g : Πa b, C a b) : (f = g) ≃ (f ~2 g) :=
+  equiv.mk apd100 _
+
+  definition eq_equiv_homotopy3 [constructor] (f g : Πa b c, D a b c) : (f = g) ≃ (f ~3 g) :=
+  equiv.mk apd1000 _
+
   definition apd10_ap (f : X → Πa, B a) (p : x = x')
     : apd10 (ap f p) = ap010 f p :=
   eq.rec_on p idp
diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 879e19e878..e5cb21b127 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -190,7 +190,7 @@ namespace eq
   eq.rec_on p u
 
   -- This idiom makes the operation right associative.
-  infixr `▸` := transport _
+  infixr ` ▸ ` := transport _
 
   definition cast [reducible] [unfold 3] {A B : Type} (p : A = B) (a : A) : B :=
   p ▸ a
diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean
index 7d1ae986b0..64448ee0c0 100644
--- a/hott/types/prod.hlean
+++ b/hott/types/prod.hlean
@@ -16,7 +16,7 @@ namespace prod
 
   /- Paths in a product space -/
 
-  protected definition eta (u : A × B) : (pr₁ u, pr₂ u) = u :=
+  protected definition eta [unfold 3] (u : A × B) : (pr₁ u, pr₂ u) = u :=
   by cases u; apply idp
 
   definition pair_eq [unfold 7 8] (pa : a = a') (pb : b = b') : (a, b) = (a', b') :=
@@ -25,10 +25,10 @@ namespace prod
   definition prod_eq [unfold 3 4 5 6] (H₁ : u.1 = v.1) (H₂ : u.2 = v.2) : u = v :=
   by cases u; cases v; exact pair_eq H₁ H₂
 
-  definition eq_pr1 (p : u = v) : u.1 = v.1 :=
+  definition eq_pr1 [unfold 5] (p : u = v) : u.1 = v.1 :=
   ap pr1 p
 
-  definition eq_pr2 (p : u = v) : u.2 = v.2 :=
+  definition eq_pr2 [unfold 5] (p : u = v) : u.2 = v.2 :=
   ap pr2 p
 
   namespace ops
@@ -39,7 +39,7 @@ namespace prod
 
   definition pair_prod_eq (p : u.1 = v.1) (q : u.2 = v.2)
     : ((prod_eq p q)..1, (prod_eq p q)..2) = (p, q) :=
-  by induction u; induction v;esimp at *;induction p;induction q;reflexivity
+  by induction u; induction v; esimp at *; induction p; induction q; reflexivity
 
   definition prod_eq_pr1 (p : u.1 = v.1) (q : u.2 = v.2) : (prod_eq p q)..1 = p :=
   (pair_prod_eq p q)..1
diff --git a/hott/types/unit.hlean b/hott/types/unit.hlean
index b77ac5be8a..92f60dfc77 100644
--- a/hott/types/unit.hlean
+++ b/hott/types/unit.hlean
@@ -6,10 +6,13 @@ Authors: Floris van Doorn
 Theorems about the unit type
 -/
 
-open equiv option
+open equiv option eq
 
 namespace unit
 
+  protected definition eta : Π(u : unit), ⋆ = u
+  | eta ⋆ := idp
+
   definition unit_equiv_option_empty : unit ≃ option empty :=
   begin
     fapply equiv.MK,
diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el
index 961adfcc0d..0c6e943cdc 100644
--- a/src/emacs/lean-input.el
+++ b/src/emacs/lean-input.el
@@ -348,6 +348,7 @@ order for the change to take effect."
   ("-1p"       . ("⁻¹ᵖ"))
   ("-1s"       . ("⁻¹ˢ"))
   ("-1v"       . ("⁻¹ᵛ"))
+  ("-1E"       . ("⁻¹ᴱ"))
   ("-2"        . ("⁻²"))
   ("-2o"       . ("⁻²ᵒ"))
   ("-3"        . ("⁻³"))
@@ -669,7 +670,7 @@ order for the change to take effect."
   ("Ge"  . ("ε"))  ("GE"  . ("Ε"))  ("eps" . ("ε"))
   ("Gz"  . ("ζ"))  ("GZ"  . ("Ζ"))
   ;; \eta \Eta
-  ("Gth" . ("θ"))  ("GTH" . ("Θ"))
+  ("Gth" . ("θ"))  ("GTH" . ("Θ"))  ("th"  . ("θ"))
   ("Gi"  . ("ι"))  ("GI"  . ("Ι"))
   ("Gk"  . ("κ"))  ("GK"  . ("Κ"))
   ("Gl"  . ("λ"))  ("GL"  . ("Λ"))  ("Gl-" . ("ƛ"))
@@ -679,7 +680,7 @@ order for the change to take effect."
   ;; \omicron \Omicron
   ;; \pi \Pi
   ("Gr"  . ("ρ"))  ("GR"  . ("Ρ"))
-  ("Gs"  . ("σ"))  ("GS"  . ("Σ")) 
+  ("Gs"  . ("σ"))  ("GS"  . ("Σ"))
   ("Gt"  . ("τ"))  ("GT"  . ("Τ"))
   ("Gu"  . ("υ"))  ("GU"  . ("Υ"))
   ("Gf"  . ("φ"))  ("GF"  . ("Φ"))
@@ -687,7 +688,7 @@ order for the change to take effect."
   ("Gp"  . ("ψ"))  ("GP"  . ("Ψ"))
   ("Go"  . ("ω"))  ("GO"  . ("Ω"))
   ;; even shorter versions for central type constructors
-  ("S"   . ("Σ"))  ("P"   . ("Π")) 
+  ("S"   . ("Σ"))  ("P"   . ("Π"))
 
   ;; Mathematical characters