diff --git a/hott/algebra/category/constructions.hlean b/hott/algebra/category/constructions.hlean
index 3c263555ab..e337ab414b 100644
--- a/hott/algebra/category/constructions.hlean
+++ b/hott/algebra/category/constructions.hlean
@@ -103,10 +103,6 @@ namespace category
         apply inverse, apply naturality_iso}
     end
 
-    --the following error is a bug?
-    -- 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_eq_eq_of_iso_functor (η : F ≅ G) : iso_of_eq (eq_of_iso_functor η) = η :=
     begin
     apply iso.eq_mk,
diff --git a/hott/algebra/precategory/adjoint.hlean b/hott/algebra/precategory/adjoint.hlean
index c6efababae..65405b30fc 100644
--- a/hott/algebra/precategory/adjoint.hlean
+++ b/hott/algebra/precategory/adjoint.hlean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Module: algebra.precategory.yoneda
@@ -69,6 +69,8 @@ structure isomorphism (C D : Precategory) :=
 
 namespace category
 
+  --   infix `⊣`:55 := adjoint
+
   infix `⋍`:25 := equivalence -- \backsimeq
   infix `≌`:25 := isomorphism -- \backcong
   --TODO: add shortcuts for Σ⋍≌▹
diff --git a/hott/algebra/precategory/basic.hlean b/hott/algebra/precategory/basic.hlean
index 63575e9b19..10dca7c633 100644
--- a/hott/algebra/precategory/basic.hlean
+++ b/hott/algebra/precategory/basic.hlean
@@ -139,5 +139,3 @@ namespace category
   Precategory.rec (λob c, idp) C
 
 end category
-
-open category
diff --git a/hott/algebra/precategory/constructions.hlean b/hott/algebra/precategory/constructions.hlean
index 966d985416..3c877c937e 100644
--- a/hott/algebra/precategory/constructions.hlean
+++ b/hott/algebra/precategory/constructions.hlean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Module: algebra.precategory.constructions
@@ -166,8 +166,6 @@ namespace category
     definition Precategory_functor [reducible] (D C : Precategory) : Precategory :=
     precategory.Mk (precategory_functor D C)
 
-    -- definition Precategory_functor_rev [reducible] (C D : Precategory) : Precategory :=
-    -- Precategory_functor D C
   end
   namespace ops
     infixr `^c`:35 := Precategory_functor
diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean
index f11dc65f58..0a320bc777 100644
--- a/hott/algebra/precategory/functor.hlean
+++ b/hott/algebra/precategory/functor.hlean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Module: algebra.precategory.functor
@@ -77,13 +77,6 @@ namespace functor
         apply idp
       end))))
 
-  -- 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))
@@ -109,7 +102,6 @@ namespace functor
 
   set_option apply.class_instance false
   -- "functor C D" is equivalent to a certain sigma type
-  set_option unifier.max_steps 38500
   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)),
@@ -123,7 +115,7 @@ namespace functor
         exact (pr₁ S.2.2), exact (pr₂ S.2.2)},
       {intro F,
         cases F with (d1, d2, d3, d4),
-        exact (sigma.mk d1 (sigma.mk d2 (pair d3 (@d4))))},
+        exact ⟨d1, d2, (d3, @d4)⟩},
       {intro F,
         cases F,
         apply idp},
@@ -150,11 +142,6 @@ namespace functor
        apply is_trunc_eq, apply is_trunc_succ, apply !homH},
   end
 
---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
@@ -166,7 +153,6 @@ namespace functor
   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
@@ -176,36 +162,6 @@ namespace functor
     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_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
diff --git a/hott/algebra/precategory/iso.hlean b/hott/algebra/precategory/iso.hlean
index 09d64f5f42..c12309f055 100644
--- a/hott/algebra/precategory/iso.hlean
+++ b/hott/algebra/precategory/iso.hlean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Module: algebra.precategory.iso
diff --git a/hott/algebra/precategory/nat_trans.hlean b/hott/algebra/precategory/nat_trans.hlean
index 99ec566e1c..912c7147e4 100644
--- a/hott/algebra/precategory/nat_trans.hlean
+++ b/hott/algebra/precategory/nat_trans.hlean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Module: algebra.precategory.nat_trans
diff --git a/hott/algebra/precategory/yoneda.hlean b/hott/algebra/precategory/yoneda.hlean
index 363e8f6cb0..32de74b009 100644
--- a/hott/algebra/precategory/yoneda.hlean
+++ b/hott/algebra/precategory/yoneda.hlean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2014 Floris van Doorn. All rights reserved.
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Module: algebra.precategory.yoneda
@@ -15,7 +15,6 @@ set_option pp.beta true
 namespace yoneda
   set_option class.conservative false
 
-  --TODO: why does this take so much steps? (giving more information than "assoc" hardly helps)
   definition representable_functor_assoc [C : Precategory] {a1 a2 a3 a4 a5 a6 : C}
     (f1 : hom a5 a6) (f2 : hom a4 a5) (f3 : hom a3 a4) (f4 : hom a2 a3) (f5 : hom a1 a2)
       : (f1 ∘ f2) ∘ f3 ∘ (f4 ∘ f5) = f1 ∘ (f2 ∘ f3 ∘ f4) ∘ f5 :=
@@ -25,7 +24,6 @@ namespace yoneda
       ... = f1 ∘ ((f2 ∘ f3) ∘ f4) ∘ f5 : by rewrite -(assoc (f2 ∘ f3) _ _)
       ... = _                          : by rewrite (assoc f2 f3 f4)
 
-  --disturbing behaviour: giving the type of f "(x ⟶ y)" explicitly makes the unifier loop
   definition hom_functor (C : Precategory) : Cᵒᵖ ×c C ⇒ set :=
   functor.mk (λ(x : Cᵒᵖ ×c C), homset x.1 x.2)
              (λ(x y : Cᵒᵖ ×c C) (f : _) (h : homset x.1 x.2), f.2 ∘⁅ C ⁆ (h ∘⁅ C ⁆ f.1))
@@ -200,7 +198,7 @@ end functor
 open functor
 
 namespace yoneda
-  -- or should this be defined as "yoneda_embedding Cᵒᵖ"?
+  --should this be defined as "yoneda_embedding Cᵒᵖ"?
   definition contravariant_yoneda_embedding (C : Precategory) : Cᵒᵖ ⇒ set ^c C :=
   functor_curry !hom_functor
 
@@ -208,23 +206,3 @@ namespace yoneda
   functor_curry (!hom_functor ∘f !functor_prod_flip)
 
 end yoneda
-
--- Coq uses unit/counit definitions as basic
-
--- open yoneda precategory.product precategory.opposite functor morphism
---   --universe levels are given explicitly because Lean uses 6 variables otherwise
-
---   structure adjoint.{u v} [C D : Precategory.{u v}] (F : C ⇒ D) (G : D ⇒ C) : Type.{max u v} :=
---   (nat_iso : (hom_functor D) ∘f (prod_functor (opposite_functor F) (functor.ID D)) ⟹
---              (hom_functor C) ∘f (prod_functor (functor.ID (Cᵒᵖ)) G))
---   (is_iso_nat_iso : is_iso nat_iso)
-
---   infix `⊣`:55 := adjoint
-
--- namespace adjoint
---   universe variables l1 l2
---   variables [C D : Precategory.{l1 l2}] (F : C ⇒ D) (G : D ⇒ C)
-
-
-
--- end adjoint