diff --git a/library/algebra/category/adjoint.lean b/library/algebra/category/adjoint.lean
index ec6cb8c84..fb858f2ae 100644
--- a/library/algebra/category/adjoint.lean
+++ b/library/algebra/category/adjoint.lean
@@ -2,32 +2,31 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn
 
-import .basic .constructions
+import .constructions
 
 open eq eq.ops category functor natural_transformation category.ops prod category.product
 
 namespace adjoint
 --representable functor
 
-  definition foo {obC : Type} (C : category obC) : C ×c C ⇒ C ×c C := functor.id
+  definition foo (C : Category) : C ×c C ⇒ C ×c C := functor.id
 
-  definition Hom {obC : Type} (C : category obC) : Cᵒᵖ ×c C ⇒ type :=
-  @functor.mk _ _ _ _ (λ a, hom (pr1 a) (pr2 a))
-             (λ a b f h, pr2 f ∘ h ∘ pr1 f)
-             (λ a, funext (λh, !id_left ⬝ !id_right))
-             (λ a b c g f, funext (λh,
-    show (pr2 g ∘ pr2 f) ∘ h ∘ (pr1 f ∘ pr1 g) = pr2 g ∘ (pr2 f ∘ h ∘ pr1 f) ∘ pr1 g, from sorry))
+  -- definition Hom (C : Category) : Cᵒᵖ ×c C ⇒ type :=
+  -- functor.mk (λ a, hom (pr1 a) (pr2 a))
+  --            (λ a b f h, pr2 f ∘ h ∘ pr1 f)
+  --            (λ a, funext (λh, !id_left ⬝ !id_right))
+  --            (λ a b c g f, funext (λh,
+  --   show (pr2 g ∘ pr2 f) ∘ h ∘ (pr1 f ∘ pr1 g) = pr2 g ∘ (pr2 f ∘ h ∘ pr1 f) ∘ pr1 g, from sorry))
   --I'm lazy, waiting for automation to fill this
 
-  variables {obC obD : Type} (C : category obC) {D : category obD}
+  variables (C D : Category)
 
-  variables (f : Cᵒᵖ ×c C ⇒ C ×c C) (g : C ×c C ⇒ C ×c C)
-  check g ∘f f
+  -- private definition aux_prod_cat [instance] : category (obD × obD) := prod_category (opposite.opposite D) D
 
-  check natural_transformation (Hom D)
-
-  definition adjoint (F : C ⇒ D) (G : D ⇒ C) :=
-  natural_transformation (@functor.compose _ _ _ _ _ _ (Hom D) sorry)
+--   definition adjoint.{l} (F : C ⇒ D) (G : D ⇒ C) := 
+--   --@natural_transformation _ Type.{l} (Dᵒᵖ ×c D) type_category.{l+1} (Hom D) (Hom D)
+-- sorry
+--(@functor.compose _ _ _ _ _ _ (Hom D) (@product.prod_functor _ _ _ _ _ _ (Dᵒᵖ) D sorry sorry))
                        --(Hom C ∘f sorry)
   --product.prod_functor (opposite.opposite_functor F) (functor.ID D)
 end adjoint
diff --git a/library/algebra/category/basic.lean b/library/algebra/category/basic.lean
index 134f1c737..723f1298e 100644
--- a/library/algebra/category/basic.lean
+++ b/library/algebra/category/basic.lean
@@ -20,13 +20,14 @@ namespace category
   variables {ob : Type} [C : category ob]
   variables {a b c d : ob}
   include C
+
   definition hom [reducible] : ob → ob → Type := rec (λ hom compose id assoc idr idl, hom) C
   -- note: needs to be reducible to typecheck composition in opposite category
   definition compose [reducible] : Π {a b c : ob}, hom b c → hom a b → hom a c :=
   rec (λ hom compose id assoc idr idl, compose) C
 
   definition id [reducible] : Π {a : ob}, hom a a := rec (λ hom compose id assoc idr idl, id) C
-  definition ID [reducible] : Π (a : ob), hom a a := @id ob C
+  definition ID [reducible] (a : ob) : hom a a := id
 
   infixr `∘`:60 := compose
   infixl `⟶`:25 := hom -- input ⟶ using \--> (this is a different arrow than \-> (→))
@@ -42,6 +43,7 @@ namespace category
   theorem id_right : Π ⦃a b : ob⦄ (f : hom a b), f ∘ id = f :=
   rec (λ hom comp id assoc idl idr, idr) C
 
+  --the following is the only theorem for which "include C" is necessary if C is a variable (why?)
   theorem id_compose (a : ob) : (ID a) ∘ id = id := !id_left
 
   theorem left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id :=
@@ -56,145 +58,18 @@ end category
 inductive Category : Type := mk : Π (ob : Type), category ob → Category
 
 namespace category
-  definition objects [coercion] (C : Category) : Type
+  definition Mk {ob} (C) : Category := Category.mk ob C
+  definition MK (a b c d e f g) : Category := Category.mk a (category.mk b c d e f g)
+
+  definition objects [coercion] [reducible] (C : Category) : Type 
   := Category.rec (fun c s, c) C
 
-  definition category_instance [instance] (C : Category) : category (objects C)
+  definition category_instance [instance] [coercion] [reducible] (C : Category) : category (objects C)
   := Category.rec (fun c s, s) C
+
 end category
 
 open category
 
-inductive functor {obC obD : Type} (C : category obC) (D : category obD) : Type :=
-mk : Π (obF : obC → obD) (homF : Π⦃a b : obC⦄, hom a b → hom (obF a) (obF b)),
-    (Π ⦃a : obC⦄, homF (ID a) = ID (obF a)) →
-    (Π ⦃a b c : obC⦄ {g : hom b c} {f : hom a b}, homF (g ∘ f) = homF g ∘ homF f) →
-     functor C D
-
-inductive Functor (C D : Category) : Type :=
-mk : functor (category_instance C) (category_instance D) → Functor C D
-
-infixl `⇒`:25 := functor
-
-namespace functor
-  variables {obC obD obE : Type} {C : category obC} {D : category obD} {E : category obE}
-  definition object [coercion] (F : C ⇒ D) : obC → obD := rec (λ obF homF Hid Hcomp, obF) F
-
-  definition morphism [coercion] (F : C ⇒ D) : Π{a b : obC}, hom a b → hom (F a) (F b) :=
-  rec (λ obF homF Hid Hcomp, homF) F
-
-  theorem respect_id (F : C ⇒ D) : Π (a : obC), F (ID a) = id :=
-  rec (λ obF homF Hid Hcomp, Hid) F
-
-  theorem respect_comp (F : C ⇒ D) : Π ⦃a b c : obC⦄ (g : hom b c) (f : hom a b),
-      F (g ∘ f) = F g ∘ F f :=
-  rec (λ obF homF Hid Hcomp, Hcomp) F
-
-  protected definition compose (G : D ⇒ E) (F : C ⇒ D) : C ⇒ E :=
-  functor.mk
-    (λx, G (F x))
-    (λ a b f, G (F f))
-    (λ a, calc
-      G (F (ID a)) = G id : respect_id F a
-               ... = id   : respect_id G (F a))
-    (λ a b c g f, calc
-      G (F (g ∘ f)) = G (F g ∘ F f)     : respect_comp F g f
-                ... = G (F g) ∘ G (F f) : respect_comp G (F g) (F f))
-
-  infixr `∘f`:60 := compose
-
-  protected theorem assoc {obA obB obC obD : Type} {A : category obA} {B : category obB}
-      {C : category obC} {D : category obD} (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
-      H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
-  rfl
-
-  -- later check whether we want implicit or explicit arguments here. For the moment, define both
-  protected definition id {ob : Type} {C : category ob} : functor C C :=
-  mk (λa, a) (λ a b f, f) (λ a, rfl) (λ a b c f g, rfl)
-  protected definition ID {ob : Type} (C : category ob) : functor C C := id
-  protected definition Id {C : Category} : Functor C C := Functor.mk id
-  protected definition iD (C : Category) : Functor C C := Functor.mk id
-
-  protected theorem id_left  (F : C ⇒ D) : id ∘f F = F := rec (λ obF homF idF compF, rfl) F
-  protected theorem id_right (F : C ⇒ D) : F ∘f id = F := rec (λ obF homF idF compF, rfl) F
-
-  variables {C₁ C₂ C₃ C₄: Category}
-  definition Functor_functor (F : Functor C₁ C₂) :
-      functor (category_instance C₁) (category_instance C₂) :=
-  Functor.rec (λ x, x) F
-
-  protected definition Compose (G : Functor C₂ C₃) (F : Functor C₁ C₂) : Functor C₁ C₃ :=
-  Functor.mk (compose (Functor_functor G) (Functor_functor F))
-
-  infixr `∘F`:60 := Compose
-
-  protected definition Assoc (H : Functor C₃ C₄) (G : Functor C₂ C₃) (F : Functor C₁ C₂)
-    :  H ∘F (G ∘F F) = (H ∘F G) ∘F F :=
-  rfl
-
-  protected theorem Id_left (F : Functor C₁ C₂) : Id ∘F F = F :=
-  Functor.rec (λ f, subst !id_left rfl) F
-
-  protected theorem Id_right {F : Functor C₁ C₂} : F ∘F Id = F :=
-  Functor.rec (λ f, subst !id_right rfl) F
-end functor
-
-open functor
-
-inductive natural_transformation {obC obD : Type} {C : category obC} {D : category obD}
-    (F G : functor C D) : Type :=
-mk : Π (η : Π(a : obC), hom (F a) (G a)), (Π{a b : obC} (f : hom a b), G f ∘ η a = η b ∘ F f)
- → natural_transformation F G
-
--- inductive Natural_transformation {C D : Category} (F G : Functor C D) : Type :=
--- mk : natural_transformation (Functor_functor F) (Functor_functor G) → Natural_transformation F G
-
-infixl `⟹`:25 := natural_transformation
-
-namespace natural_transformation
-  variables {obC obD : Type} {C : category obC} {D : category obD} {F G H : C ⇒ D}
-
-  definition natural_map [coercion] (η : F ⟹ G) :
-      Π(a : obC), hom (F a) (G a) :=
-  rec (λ x y, x) η
-
-  definition naturality (η : F ⟹ G) :
-      Π{a b : obC} (f : hom a b), G f ∘ η a = η b ∘ F f :=
-  rec (λ x y, y) η
-
-  protected definition compose (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H :=
-  natural_transformation.mk
-    (λ a, η a ∘ θ a)
-    (λ a b f,
-      calc
-        H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : assoc
-                      ... = (η b ∘ G f) ∘ θ a : naturality η f
-                      ... = η b ∘ (G f ∘ θ a) : assoc
-                      ... = η b ∘ (θ b ∘ F f) : naturality θ f
-                      ... = (η b ∘ θ b) ∘ F f : assoc)
-
-  precedence `∘n` : 60
-  infixr `∘n` := compose
-
-  variables {F₁ F₂ F₃ F₄ : C ⇒ D}
-  protected theorem assoc (η₃ : F₃ ⟹ F₄) (η₂ : F₂ ⟹ F₃) (η₁ : F₁ ⟹ F₂) :
-      η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ :=
-  congr_arg2_dep mk (funext (take x, !assoc)) !proof_irrel
-
-  --TODO: check whether some of the below identities are superfluous
-  protected definition id {obC obD : Type} {C : category obC} {D : category obD} {F : C ⇒ D}
-      : natural_transformation F F :=
-  mk (λa, id) (λa b f, !id_right ⬝ symm !id_left)
-  protected definition ID {obC obD : Type} {C : category obC} {D : category obD} (F : C ⇒ D)
-      : natural_transformation F F := id
-  -- protected definition Id {C D : Category} {F : Functor C D} : Natural_transformation F F :=
-  -- Natural_transformation.mk id
-  -- protected definition iD {C D : Category} (F : Functor C D) : Natural_transformation F F :=
-  -- Natural_transformation.mk id
-
-  protected theorem id_left (η : F₁ ⟹ F₂) : natural_transformation.compose id η = η :=
-  rec (λf H, congr_arg2_dep mk (funext (take x, !id_left)) !proof_irrel) η
-
-  protected theorem id_right (η : F₁ ⟹ F₂) : natural_transformation.compose η id = η :=
-  rec (λf H, congr_arg2_dep mk (funext (take x, !id_right)) !proof_irrel) η
-end natural_transformation
+theorem Category.equal (C : Category) : Category.mk C C = C :=
+Category.rec (λ ob c, rfl) C
diff --git a/library/algebra/category/constructions.lean b/library/algebra/category/constructions.lean
index efaf4a043..39ad0c154 100644
--- a/library/algebra/category/constructions.lean
+++ b/library/algebra/category/constructions.lean
@@ -5,48 +5,46 @@
 -- This file contains basic constructions on categories, including common categories
 
 
-import .basic
+import .natural_transformation
 import data.unit data.sigma data.prod data.empty data.bool
 
 open eq eq.ops prod
 namespace category
-  section
-  open unit
-  definition category_one : category unit :=
-  mk (λa b, unit)
-     (λ a b c f g, star)
-     (λ a, star)
-     (λ a b c d f g h, !unit.equal)
-     (λ a b f, !unit.equal)
-     (λ a b f, !unit.equal)
-  end
-
   namespace opposite
   section
-  variables {ob : Type} {C : category ob} {a b c : ob}
-  definition opposite (C : category ob) : category ob :=
+  definition opposite {ob : Type} (C : category ob) : category ob :=
   mk (λa b, hom b a)
      (λ a b c f g, g ∘ f)
      (λ a, id)
      (λ a b c d f g h, symm !assoc)
      (λ a b f, !id_right)
      (λ a b f, !id_left)
-  --definition compose_opposite {C : category ob} {a b c : ob} {g : a => b} {f : b => c} : compose
-  precedence `∘op` : 60
-  infixr `∘op` := @compose _ (opposite _) _ _ _
 
-  theorem compose_op {f : @hom ob C a b} {g : hom b c} : f ∘op g = g ∘ f :=
-  rfl
+  definition Opposite (C : Category) : Category := Mk (opposite C)
+  --direct construction:
+  -- MK C
+  --    (λa b, hom b a)
+  --    (λ a b c f g, g ∘ f)
+  --    (λ a, id)
+  --    (λ a b c d f g h, symm !assoc)
+  --    (λ a b f, !id_right)
+  --    (λ a b f, !id_left)
 
-  theorem op_op {C : category ob} : opposite (opposite C) = C :=
+  infixr `∘op`:60 := @compose _ (opposite _) _ _ _
+
+  variables {C : Category} {a b c : C}
+
+  theorem compose_op {f : hom a b} {g : hom b c} : f ∘op g = g ∘ f := rfl
+
+  theorem op_op' {ob : Type} (C : category ob) : opposite (opposite C) = C :=
   category.rec (λ hom comp id assoc idl idr, refl (mk _ _ _ _ _ _)) C
-  end
 
-  definition Opposite (C : Category) : Category :=
-  Category.mk (objects C) (opposite (category_instance C))
+  theorem op_op : Opposite (Opposite C) = C :=
+  (@congr_arg _ _ _ _ (Category.mk C) (op_op' C)) ⬝ !Category.equal
+
+  end
   end opposite
 
-  section
   definition type_category : category Type :=
   mk (λa b, a → b)
      (λ a b c, function.compose)
@@ -54,7 +52,8 @@ namespace category
      (λ a b c d h g f, symm (function.compose_assoc h g f))
      (λ a b f, function.compose_id_left f)
      (λ a b f, function.compose_id_right f)
-  end
+
+  definition Type_category : Category := Mk type_category
 
   section
   open decidable unit empty
@@ -70,32 +69,24 @@ namespace category
       (λ Hab f, rec_on_true (trans Hab Hbc) ⋆)
       (λh f, empty.rec _ f) f)
     (λh (g : empty), empty.rec _ g) g
-
+  omit H
   definition set_category (A : Type) [H : decidable_eq A] : category A :=
   mk (λa b, set_hom a b)
      (λ a b c g f, set_compose g f)
-     (λ a, rec_on_true rfl ⋆)
-     (λ a b c d h g f, subsingleton.elim _ _ _)
-     (λ a b f, subsingleton.elim _ _ _)
-     (λ a b f, subsingleton.elim _ _ _)
+     (λ a, decidable.rec_on_true rfl ⋆)
+     (λ a b c d h g f, @subsingleton.elim (set_hom a d) _ _ _)
+     (λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
+     (λ a b f, @subsingleton.elim (set_hom a b) _ _ _)
+  definition Set_category (A : Type) [H : decidable_eq A] := Mk (set_category A)
   end
-
   section
-  open bool
+  open unit bool
+  definition category_one := set_category unit
+  definition Category_one := Mk category_one
   definition category_two := set_category bool
+  definition Category_two := Mk category_two
   end
 
-
-  section cat_of_cat
-  definition category_of_categories : category Category :=
-  mk (λ a b, Functor a b)
-     (λ a b c g f, functor.Compose g f)
-     (λ a, functor.Id)
-     (λ a b c d h g f, !functor.Assoc)
-     (λ a b f, !functor.Id_left)
-     (λ a b f, !functor.Id_right)
-  end cat_of_cat
-
   namespace product
   section
   open prod
@@ -107,25 +98,28 @@ namespace category
      (λ a b c d h g f, pair_eq    !assoc    !assoc   )
      (λ a b f,         prod.equal !id_left  !id_left )
      (λ a b f,         prod.equal !id_right !id_right)
+
+  definition Prod_category (C D : Category) : Category := Mk (prod_category C D)
+
   end
   end product
 
-namespace ops
-  notation `Cat` := category_of_categories
-  notation `type` := type_category
-  notation 1 := category_one
-  postfix `ᵒᵖ`:max := opposite.opposite
-  infixr `×c`:30 := product.prod_category
-  instance [persistent] category_of_categories type_category category_one product.prod_category
-end ops
+  namespace ops
+    notation `type`:max := Type_category
+    notation 1 := Category_one --it was confusing for me (Floris) that no ``s are needed here
+    notation 2 := Category_two
+    postfix `ᵒᵖ`:max := opposite.Opposite
+    infixr `×c`:30 := product.Prod_category
+    instance [persistent] type_category category_one 
+                          category_two product.prod_category
+  end ops
+
   open ops
   namespace opposite
   section
   open ops functor
-  --set_option pp.implicit true
-  definition opposite_functor {obC obD : Type} {C : category obC} {D : category obD} (F : C ⇒ D)
-      : Cᵒᵖ ⇒ Dᵒᵖ :=
-  @functor.mk obC obD (Cᵒᵖ) (Dᵒᵖ)
+  definition opposite_functor {C D : Category} (F : C ⇒ D) : Cᵒᵖ ⇒ Dᵒᵖ :=
+  @functor.mk (Cᵒᵖ) (Dᵒᵖ)
               (λ a, F a)
               (λ a b f, F f)
               (λ a, !respect_id)
@@ -136,8 +130,7 @@ end ops
   namespace product
   section
   open ops functor
-  definition prod_functor {obC obC' obD obD' : Type} {C : category obC} {C' : category obC'}
-    {D : category obD} {D' : category obD'} (F : C ⇒ D) (G : C' ⇒ D') : C ×c C' ⇒ D ×c D' :=
+  definition prod_functor {C C' D D' : Category} (F : C ⇒ D) (G : C' ⇒ D') : C ×c C' ⇒ D ×c D' :=
   functor.mk (λ a, pair (F (pr1 a)) (G (pr2 a)))
              (λ a b f, pair (F (pr1 f)) (G (pr2 f)))
              (λ a, pair_eq !respect_id !respect_id)
@@ -151,7 +144,7 @@ end ops
   end ops
 
   section functor_category
-  variables {obC obD : Type} (C : category obC) (D : category obD)
+  variables (C D : Category)
   definition functor_category : category (functor C D) :=
   mk (λa b, natural_transformation a b)
      (λ a b c g f, natural_transformation.compose g f)
@@ -161,79 +154,136 @@ end ops
      (λ a b f, !natural_transformation.id_right)
   end functor_category
 
-  section
-  open sigma
+  namespace slice
+  open sigma function
+  variables {ob : Type} {C : category ob} {c : ob}
+  protected definition slice_obs (C : category ob) (c : ob) := Σ(b : ob), hom b c
+  variables {a b : slice_obs C c}
+  protected definition to_ob  (a : slice_obs C c) : ob              := dpr1 a
+  protected definition to_ob_def (a : slice_obs C c) : to_ob a = dpr1 a := rfl
+  protected definition ob_hom (a : slice_obs C c) : hom (to_ob a) c := dpr2 a
+  -- protected theorem slice_obs_equal (H₁ : to_ob a = to_ob b) 
+  --     (H₂ : eq.drec_on H₁ (ob_hom a) = ob_hom b) : a = b :=
+  -- sigma.equal H₁ H₂
 
-  definition slice_category [reducible] {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), hom b c) :=
-  mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)), dpr2 b ∘ g = dpr2 a)
-     (λ a b c g f, dpair (dpr1 g ∘ dpr1 f)
-       (show dpr2 c ∘ (dpr1 g ∘ dpr1 f) = dpr2 a,
+
+  protected definition slice_hom (a b : slice_obs C c) : Type :=
+  Σ(g : hom (to_ob a) (to_ob b)), ob_hom b ∘ g = ob_hom a
+
+  protected definition hom_hom  (f : slice_hom a b) : hom (to_ob a) (to_ob b)          := dpr1 f
+  protected definition commute (f : slice_hom a b) : ob_hom b ∘ (hom_hom f) = ob_hom a := dpr2 f
+  -- protected theorem slice_hom_equal (f g : slice_hom a b) (H : hom_hom f = hom_hom g) : f = g :=
+  -- sigma.equal H !proof_irrel
+
+  definition slice_category (C : category ob) (c : ob) : category (slice_obs C c) :=
+  mk (λa b, slice_hom a b)
+     (λ a b c g f, dpair (hom_hom g ∘ hom_hom f)
+       (show ob_hom c ∘ (hom_hom g ∘ hom_hom f) = ob_hom a,
          proof
          calc
-           dpr2 c ∘ (dpr1 g ∘ dpr1 f) = (dpr2 c ∘ dpr1 g) ∘ dpr1 f : !assoc
-             ... = dpr2 b ∘ dpr1 f : {dpr2 g}
-             ... = dpr2 a : {dpr2 f}
+           ob_hom c ∘ (hom_hom g ∘ hom_hom f) = (ob_hom c ∘ hom_hom g) ∘ hom_hom f : !assoc
+             ... = ob_hom b ∘ hom_hom f : {commute g}
+             ... = ob_hom a : {commute f}
          qed))
      (λ a, dpair id !id_right)
      (λ a b c d h g f, dpair_eq    !assoc    !proof_irrel)
      (λ a b f,         sigma.equal !id_left  !proof_irrel)
      (λ a b f,         sigma.equal !id_right !proof_irrel)
   -- We use !proof_irrel instead of rfl, to give the unifier an easier time
-  end --remove
-  namespace slice
-  section --remove
-  open sigma category.ops --remove sigma
+
+  -- definition slice_category {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), hom b c) 
+  -- :=
+  -- mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)), dpr2 b ∘ g = dpr2 a)
+  --    (λ a b c g f, dpair (dpr1 g ∘ dpr1 f)
+  --      (show dpr2 c ∘ (dpr1 g ∘ dpr1 f) = dpr2 a,
+  --        proof
+  --        calc
+  --          dpr2 c ∘ (dpr1 g ∘ dpr1 f) = (dpr2 c ∘ dpr1 g) ∘ dpr1 f : !assoc
+  --            ... = dpr2 b ∘ dpr1 f : {dpr2 g}
+  --            ... = dpr2 a : {dpr2 f}
+  --        qed))
+  --    (λ a, dpair id !id_right)
+  --    (λ a b c d h g f, dpair_eq    !assoc    !proof_irrel)
+  --    (λ a b f,         sigma.equal !id_left  !proof_irrel)
+  --    (λ a b f,         sigma.equal !id_right !proof_irrel)
+  -- We use !proof_irrel instead of rfl, to give the unifier an easier time
+
+  definition Slice_category [reducible] (C : Category) (c : C) := Mk (slice_category C c)
+  open category.ops
   instance [persistent] slice_category
-  variables {ob : Type} (C : category ob)
-  definition forgetful (x : ob) : (slice_category C x) ⇒ C :=
-  functor.mk (λ a, dpr1 a)
-             (λ a b f, dpr1 f)
+  variables {D : Category}
+  definition forgetful (x : D) : (Slice_category D x) ⇒ D :=
+  functor.mk (λ a, to_ob a)
+             (λ a b f, hom_hom f)
              (λ a, rfl)
              (λ a b c g f, rfl)
-  definition composition_functor {x y : ob} (h : x ⟶ y) : slice_category C x ⇒ slice_category C y :=
-  functor.mk (λ a, dpair (dpr1 a) (h ∘ dpr2 a))
-             (λ a b f, dpair (dpr1 f)
-               (calc
-                 (h ∘ dpr2 b) ∘ dpr1 f = h ∘ (dpr2 b ∘ dpr1 f) : !assoc⁻¹
-                    ... = h ∘ dpr2 a : {dpr2 f}))
+
+  definition postcomposition_functor {x y : D} (h : x ⟶ y) 
+      : Slice_category D x ⇒ Slice_category D y :=
+  functor.mk (λ a, dpair (to_ob a) (h ∘ ob_hom a))
+             (λ a b f, dpair (hom_hom f)
+       (calc
+         (h ∘ ob_hom b) ∘ hom_hom f = h ∘ (ob_hom b ∘ hom_hom f) : assoc h (ob_hom b) (hom_hom f)⁻¹
+           ... = h ∘ ob_hom a : congr_arg (λx, h ∘ x) (commute f)))
              (λ a, rfl)
              (λ a b c g f, dpair_eq rfl !proof_irrel)
-  -- the following definition becomes complicated
-  -- definition slice_functor : C ⇒ category_of_categories :=
-  -- functor.mk (λ a, Category.mk _ (slice_category C a))
-  --            (λ a b f, Functor.mk (composition_functor f))
-  --            (λ a, congr_arg Functor.mk
-  --              (congr_arg4_dep functor.mk
-  --             (funext (λx, sigma.equal rfl !id_left))
-  --             sorry
+
+  -- -- in the following comment I tried to have (A = B) in the type of a == b, but that doesn't solve the problems
+  -- definition heq2 {A B : Type} (H : A = B) (a : A) (b : B) := a == b
+  -- definition heq2.intro {A B : Type} {a : A} {b : B} (H : a == b) : heq2 (heq.type_eq H) a b := H
+  -- definition heq2.elim {A B : Type} {a : A} {b : B} (H : A = B) (H2 : heq2 H a b) : a == b := H2
+  -- definition heq2.proof_irrel {A B : Prop} (a : A) (b : B) (H : A = B) : heq2 H a b := 
+  -- hproof_irrel H a b
+  -- theorem functor.mk_eq2 {C D : Category} {obF obG : C → D} {homF homG idF idG compF compG} 
+  --    (Hob : ∀x, obF x = obG x)
+  --    (Hmor : ∀(a b : C) (f : a ⟶ b), heq2 (congr_arg (λ x, x a ⟶ x b) (funext Hob)) (homF a b f) (homG a b f))
+  --      : functor.mk obF homF idF compF = functor.mk obG homG idG compG :=
+  -- hddcongr_arg4 functor.mk
+  --             (funext Hob)
+  --             (hfunext (λ a, hfunext (λ b, hfunext (λ f, !Hmor))))
   --             !proof_irrel
-  --             !proof_irrel))
-  --            (λ a b c g f, sorry)
-  end
+  --             !proof_irrel
+
+--  set_option pp.implicit true
+--  set_option pp.coercions true
+
+  -- definition slice_functor : D ⇒ Category_of_categories :=
+  -- functor.mk (λ a, Category.mk (slice_obs D a) (slice_category D a))
+  --            (λ a b f, postcomposition_functor f)
+  --            (λ a, functor.mk_heq
+  --              (λx, sigma.equal rfl !id_left)
+  --              (λb c f, sigma.hequal sorry !heq.refl (hproof_irrel sorry _ _)))
+  --            (λ a b c g f, functor.mk_heq
+  --                    (λx, sigma.equal (sorry ⬝ refl (dpr1 x)) sorry)
+  --                    (λb c f, sorry))
+
+  --the error message generated here is really confusing: the type of the above refl should be
+  -- "@dpr1 D (λ (a_1 : D), a_1 ⟶ a) x = @dpr1 D (λ (a_1 : D), a_1 ⟶ c) x", but the second dpr1 is not even well-typed
+
   end slice
 
-  section coslice
-  open sigma
+  -- section coslice
+  -- open sigma
 
-  definition coslice {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), hom c b) :=
-  mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)), g ∘ dpr2 a = dpr2 b)
-     (λ a b c g f, dpair (dpr1 g ∘ dpr1 f)
-       (show (dpr1 g ∘ dpr1 f) ∘ dpr2 a = dpr2 c,
-         proof
-         calc
-           (dpr1 g ∘ dpr1 f) ∘ dpr2 a = dpr1 g ∘ (dpr1 f ∘ dpr2 a): symm !assoc
-             ... = dpr1 g ∘ dpr2 b : {dpr2 f}
-             ... = dpr2 c : {dpr2 g}
-         qed))
-     (λ a, dpair id !id_left)
-     (λ a b c d h g f, dpair_eq    !assoc    !proof_irrel)
-     (λ a b f,         sigma.equal !id_left  !proof_irrel)
-     (λ a b f,         sigma.equal !id_right !proof_irrel)
+  -- definition coslice {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), hom c b) :=
+  -- mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)), g ∘ dpr2 a = dpr2 b)
+  --    (λ a b c g f, dpair (dpr1 g ∘ dpr1 f)
+  --      (show (dpr1 g ∘ dpr1 f) ∘ dpr2 a = dpr2 c,
+  --        proof
+  --        calc
+  --          (dpr1 g ∘ dpr1 f) ∘ dpr2 a = dpr1 g ∘ (dpr1 f ∘ dpr2 a): symm !assoc
+  --            ... = dpr1 g ∘ dpr2 b : {dpr2 f}
+  --            ... = dpr2 c : {dpr2 g}
+  --        qed))
+  --    (λ a, dpair id !id_left)
+  --    (λ a b c d h g f, dpair_eq    !assoc    !proof_irrel)
+  --    (λ a b f,         sigma.equal !id_left  !proof_irrel)
+  --    (λ a b f,         sigma.equal !id_right !proof_irrel)
 
-  -- theorem slice_coslice_opp {ob : Type} (C : category ob) (c : ob) :
-  --     coslice C c = opposite (slice (opposite C) c) :=
-  -- sorry
-  end coslice
+  -- -- theorem slice_coslice_opp {ob : Type} (C : category ob) (c : ob) :
+  -- --     coslice C c = opposite (slice (opposite C) c) :=
+  -- -- sorry
+  -- end coslice
 
   section arrow
   open sigma eq.ops
@@ -287,9 +337,9 @@ end ops
          qed)
        ))
      (λ a, dpair id (dpair id (!id_right ⬝ (symm !id_left))))
-     (λ a b c d h g f, dtrip_eq_ndep   !assoc    !assoc    !proof_irrel)
-     (λ a b f,         trip.equal_ndep !id_left  !id_left  !proof_irrel)
-     (λ a b f,         trip.equal_ndep !id_right !id_right !proof_irrel)
+     (λ a b c d h g f, ndtrip_eq       !assoc    !assoc    !proof_irrel)
+     (λ a b f,         ndtrip_equal !id_left  !id_left  !proof_irrel)
+     (λ a b f,         ndtrip_equal !id_right !id_right !proof_irrel)
 
   end arrow
 
diff --git a/library/algebra/category/default.lean b/library/algebra/category/default.lean
index a5d646e76..a36d75c3d 100644
--- a/library/algebra/category/default.lean
+++ b/library/algebra/category/default.lean
@@ -2,4 +2,4 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn
 
-import .basic .constructions
+import .basic .morphism .functor .constructions
diff --git a/library/algebra/category/functor.lean b/library/algebra/category/functor.lean
new file mode 100644
index 000000000..b07275ce4
--- /dev/null
+++ b/library/algebra/category/functor.lean
@@ -0,0 +1,145 @@
+-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Floris van Doorn
+
+import .basic
+import logic.cast
+import algebra.function --remove if "typeof" is moved
+open function --remove if "typeof" is moved
+open category eq eq.ops heq
+
+inductive functor (C D : Category) : Type :=
+mk : Π (obF : C → D) (homF : Π(a b : C), hom a b → hom (obF a) (obF b)),
+    (Π (a : C), homF a a (ID a) = ID (obF a)) →
+    (Π (a b c : C) {g : hom b c} {f : hom a b}, homF a c (g ∘ f) = homF b c g ∘ homF a b f) →
+     functor C D
+
+infixl `⇒`:25 := functor
+
+namespace functor
+  variables {C D E : Category}
+  definition object [coercion] (F : functor C D) : C → D := rec (λ obF homF Hid Hcomp, obF) F
+
+  definition morphism [coercion] (F : functor C D) : Π⦃a b : C⦄, hom a b → hom (F a) (F b) :=
+  rec (λ obF homF Hid Hcomp, homF) F
+
+  theorem respect_id (F : functor C D) : Π (a : C), F (ID a) = id :=
+  rec (λ obF homF Hid Hcomp, Hid) F
+
+  theorem respect_comp (F : functor C D) : Π ⦃a b c : C⦄ (g : hom b c) (f : hom a b),
+      F (g ∘ f) = F g ∘ F f :=
+  rec (λ obF homF Hid Hcomp, Hcomp) F
+
+  protected definition compose (G : functor D E) (F : functor C D) : functor C E :=
+  functor.mk
+    (λx, G (F x))
+    (λ a b f, G (F f))
+    (λ a, calc
+      G (F (ID a)) = G id : {respect_id F a} --not giving the braces explicitly makes the elaborator compute a couple more seconds
+               ... = id   : respect_id G (F a))
+    (λ a b c g f, calc
+      G (F (g ∘ f)) = G (F g ∘ F f)     : respect_comp F g f
+                ... = G (F g) ∘ G (F f) : respect_comp G (F g) (F f))
+
+  infixr `∘f`:60 := compose
+
+  protected theorem assoc {A B C D : Category} (H : functor C D) (G : functor B C) (F : functor A B) :
+      H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
+  rfl
+
+  protected definition id {C : Category} : functor C C :=
+  mk (λa, a) (λ a b f, f) (λ a, rfl) (λ a b c f g, rfl)
+  protected definition ID (C : Category) : functor C C := id
+
+  protected theorem id_left  (F : functor C D) : id ∘f F = F :=
+  functor.rec (λ obF homF idF compF, dcongr_arg4 mk rfl rfl !proof_irrel !proof_irrel) F
+  protected theorem id_right (F : functor C D) : F ∘f id = F :=
+  functor.rec (λ obF homF idF compF, dcongr_arg4 mk rfl rfl !proof_irrel !proof_irrel) F
+
+end functor
+
+namespace category
+  open functor
+  definition category_of_categories [reducible] : category Category :=
+  mk (λ a b, functor a b)
+     (λ a b c g f, functor.compose g f)
+     (λ a, functor.id)
+     (λ a b c d h g f, !functor.assoc)
+     (λ a b f, !functor.id_left)
+     (λ a b f, !functor.id_right)
+  definition Category_of_categories [reducible] := Mk category_of_categories
+
+  namespace ops
+    notation `Cat`:max := Category_of_categories
+    instance [persistent] category_of_categories
+  end ops
+end category
+
+namespace functor
+--  open category.ops
+--   universes l m
+   variables {C D : Category}
+--   check hom C D
+--   variables (F : C ⟶ D) (G : D ⇒ C)
+--   check G ∘ F
+--   check F ∘f G
+--   variables (a b : C) (f : a ⟶ b)
+--   check F a
+--   check F b
+--   check F f
+--   check G (F f)
+--   print "---"
+-- --  check (G ∘ F) f --error
+--   check (λ(x : functor C C), x) (G ∘ F) f
+--   check (G ∘f F) f
+--   print "---"
+-- --  check (G ∘ F) a --error
+--   check (G ∘f F) a
+--   print "---"
+-- --  check λ(H : hom C D) (x : C), H x  --error
+--   check λ(H : @hom _ Cat C D) (x : C), H x
+--   check λ(H : C ⇒ D) (x : C), H x
+--   print "---"
+--   -- variables {obF obG : C → D} (Hob : ∀x, obF x = obG x) (homF : Π(a b : C) (f : a ⟶ b), obF a ⟶ obF b) (homG : Π(a b : C) (f : a ⟶ b), obG a ⟶ obG b)
+-- --  check eq.rec_on (funext Hob) homF = homG
+
+  theorem mk_heq {obF obG : C → D} {homF homG idF idG compF compG} (Hob : ∀x, obF x = obG x)
+     (Hmor : ∀(a b : C) (f : a ⟶ b), homF a b f == homG a b f)
+       : mk obF homF idF compF = mk obG homG idG compG :=
+  hddcongr_arg4 mk
+              (funext Hob)
+              (hfunext (λ a, hfunext (λ b, hfunext (λ f, !Hmor))))
+              !proof_irrel
+              !proof_irrel
+
+  protected theorem hequal {F G : C ⇒ D} : Π (Hob : ∀x, F x = G x)
+      (Hmor : ∀a b (f : a ⟶ b), F f == G f), F = G :=
+  functor.rec
+    (λ obF homF idF compF,
+      functor.rec
+        (λ obG homG idG compG Hob Hmor, mk_heq Hob Hmor)
+      G)
+    F
+
+--   theorem mk_eq {obF obG : C → D} {homF homG idF idG compF compG} (Hob : ∀x, obF x = obG x)
+--      (Hmor : ∀(a b : C) (f : a ⟶ b), cast (congr_arg (λ x, x a ⟶ x b) (funext Hob)) (homF a b f)
+--                                        = homG a b f)
+--        : mk obF homF idF compF = mk obG homG idG compG :=
+--   dcongr_arg4 mk
+--               (funext Hob)
+--               (funext (λ a, funext (λ b, funext (λ f, sorry ⬝ Hmor a b f))))
+-- -- to fill this sorry use (a generalization of) cast_pull
+--               !proof_irrel
+--               !proof_irrel
+
+--   protected theorem equal {F G : C ⇒ D} : Π (Hob : ∀x, F x = G x)
+--       (Hmor : ∀a b (f : a ⟶ b), cast (congr_arg (λ x, x a ⟶ x b) (funext Hob)) (F f) = G f), F = G :=
+--   functor.rec
+--     (λ obF homF idF compF,
+--       functor.rec
+--         (λ obG homG idG compG Hob Hmor, mk_eq Hob Hmor)
+--       G)
+--     F
+
+
+end functor
diff --git a/library/algebra/category/limit.lean b/library/algebra/category/limit.lean
index b8d6c8f84..79ad76119 100644
--- a/library/algebra/category/limit.lean
+++ b/library/algebra/category/limit.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn
 
-import .basic
+import .natural_transformation
 import data.sigma
 
 open eq eq.ops category functor natural_transformation
@@ -10,15 +10,15 @@ open eq eq.ops category functor natural_transformation
 namespace limits
 --representable functor
   section
-  variables {obI ob : Type} {I : category obI} {C : category ob} {D : I ⇒ C}
+  variables {I C : Category} {D : I ⇒ C}
 
-  definition constant_diagram (a : ob) : I ⇒ C :=
+  definition constant_diagram (a : C) : I ⇒ C :=
   mk (λ i, a)
      (λ i j u, id)
      (λ i, rfl)
      (λ i j k v u, symm !id_compose)
 
-  definition cone := Σ(a : ob), constant_diagram a ⟹ D
+  definition cone := Σ(a : C), constant_diagram a ⟹ D
   -- definition cone_category : category cone :=
   -- mk (λa b, sorry)
   --    (λ a b c g f, sorry)
diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean
index 8c88abe54..9f7cb31f1 100644
--- a/library/algebra/category/morphism.lean
+++ b/library/algebra/category/morphism.lean
@@ -7,41 +7,40 @@ import .basic algebra.relation algebra.binary
 open eq eq.ops category
 
 namespace morphism
-  section
   variables {ob : Type} [C : category ob] include C
-  variables {a b c d : ob} {h : hom c d} {g : hom b c} {f : hom a b} {i : hom b a}
-  inductive is_section    [class] (f : hom a b) : Type
+  variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a}
+  inductive is_section    [class] (f : a ⟶ b) : Type
   := mk : ∀{g}, g ∘ f = id → is_section f
-  inductive is_retraction [class] (f : hom a b) : Type
+  inductive is_retraction [class] (f : a ⟶ b) : Type
   := mk : ∀{g}, f ∘ g = id → is_retraction f
-  inductive is_iso        [class] (f : hom a b) : Type
+  inductive is_iso        [class] (f : a ⟶ b) : Type
   := mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
-  --remove implicit arguments in above lines
-  definition retraction_of (f : hom a b) [H : is_section f] : hom b a :=
+
+  definition retraction_of (f : a ⟶ b) [H : is_section f] : hom b a :=
   is_section.rec (λg h, g) H
-  definition section_of    (f : hom a b) [H : is_retraction f] : hom b a :=
+  definition section_of    (f : a ⟶ b) [H : is_retraction f] : hom b a :=
   is_retraction.rec (λg h, g) H
-  definition inverse       (f : hom a b) [H : is_iso f] : hom b a :=
+  definition inverse       (f : a ⟶ b) [H : is_iso f] : hom b a :=
   is_iso.rec (λg h1 h2, g) H
 
   notation H ⁻¹ := inverse H
 
-  theorem inverse_compose (f : hom a b) [H : is_iso f] : f⁻¹ ∘ f = id :=
+  theorem inverse_compose (f : a ⟶ b) [H : is_iso f] : f⁻¹ ∘ f = id :=
   is_iso.rec (λg h1 h2, h1) H
 
-  theorem compose_inverse (f : hom a b) [H : is_iso f] : f ∘ f⁻¹ = id :=
+  theorem compose_inverse (f : a ⟶ b) [H : is_iso f] : f ∘ f⁻¹ = id :=
   is_iso.rec (λg h1 h2, h2) H
 
-  theorem retraction_compose (f : hom a b) [H : is_section f] : retraction_of f ∘ f = id :=
+  theorem retraction_compose (f : a ⟶ b) [H : is_section f] : retraction_of f ∘ f = id :=
   is_section.rec (λg h, h) H
 
-  theorem compose_section (f : hom a b) [H : is_retraction f] : f ∘ section_of f = id :=
+  theorem compose_section (f : a ⟶ b) [H : is_retraction f] : f ∘ section_of f = id :=
   is_retraction.rec (λg h, h) H
 
-  theorem iso_imp_retraction [instance] (f : hom a b) [H : is_iso f] : is_section f :=
+  theorem iso_imp_retraction [instance] (f : a ⟶ b) [H : is_iso f] : is_section f :=
   is_section.mk !inverse_compose
 
-  theorem iso_imp_section [instance] (f : hom a b) [H : is_iso f] : is_retraction f :=
+  theorem iso_imp_section [instance] (f : a ⟶ b) [H : is_iso f] : is_retraction f :=
   is_retraction.mk !compose_inverse
 
   theorem id_is_iso [instance] : is_iso (ID a) :=
@@ -50,7 +49,7 @@ namespace morphism
   theorem inverse_is_iso [instance] (f : a ⟶ b) [H : is_iso f] : is_iso (f⁻¹) :=
   is_iso.mk !compose_inverse !inverse_compose
 
-  theorem left_inverse_eq_right_inverse {f : hom 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' :=
   calc
     g = g ∘ id : symm !id_right
@@ -59,16 +58,16 @@ namespace morphism
      ... = id ∘ g' : {Hl}
      ... = g' : !id_left
 
-  theorem retraction_eq_intro [H : is_section f] (H2 : f ∘ i = id) : retraction_of f = i
+  theorem retraction_eq_intro [H : is_section f] (H2 : f ∘ h = id) : retraction_of f = h
   := left_inverse_eq_right_inverse !retraction_compose H2
 
-  theorem section_eq_intro [H : is_retraction f] (H2 : i ∘ f = id) : section_of f = i
+  theorem section_eq_intro [H : is_retraction f] (H2 : h ∘ f = id) : section_of f = h
   := symm (left_inverse_eq_right_inverse H2 !compose_section)
 
-  theorem inverse_eq_intro_right [H : is_iso f] (H2 : f ∘ i = id) : f⁻¹ = i
+  theorem inverse_eq_intro_right [H : is_iso f] (H2 : f ∘ h = id) : f⁻¹ = h
   := left_inverse_eq_right_inverse !inverse_compose H2
 
-  theorem inverse_eq_intro_left [H : is_iso f] (H2 : i ∘ f = id) : f⁻¹ = i
+  theorem inverse_eq_intro_left [H : is_iso f] (H2 : h ∘ f = id) : f⁻¹ = h
   := symm (left_inverse_eq_right_inverse H2 !compose_inverse)
 
   theorem section_eq_retraction (f : a ⟶ b) [Hl : is_section f] [Hr : is_retraction f] :
@@ -120,34 +119,25 @@ namespace morphism
 
   inductive isomorphic (a b : ob) : Type := mk : ∀(g : a ⟶ b) [H : is_iso g], isomorphic a b
 
-  end -- remove
   namespace isomorphic
-  section --remove
-  variables {ob : Type} {C : category ob} include C --remove
-  variables {a b c d : ob} {h : @hom ob C c d} {g : @hom ob C b c} {f : @hom ob C a b} --remove
   open relation
   -- should these be coercions?
-  definition iso [coercion] (H : isomorphic a b) : hom a b :=
+  definition iso [coercion] (H : isomorphic a b) : a ⟶ b :=
   isomorphic.rec (λg h, g) H
-  theorem is_iso [coercion][instance] (H : isomorphic a b) : is_iso (isomorphic.iso H) :=
+  theorem is_iso [instance] (H : isomorphic a b) : is_iso (isomorphic.iso H) :=
   isomorphic.rec (λg h, h) H
-  infix `≅`:50 := morphism.isomorphic -- why does "isomorphic" not work here?
+  infix `≅`:50 := isomorphic
 
-  theorem refl (a : ob)                                : a ≅ a := mk id
-  theorem symm ⦃a b : ob⦄    (H  : a ≅ b)              : b ≅ a := mk (inverse (iso H))
+  theorem refl  (a     : ob)                            : a ≅ a := mk id
+  theorem symm  ⦃a b   : ob⦄ (H  : a ≅ b)              : b ≅ a := mk (inverse (iso H))
   theorem trans ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c := mk (iso H2 ∘ iso H1)
   theorem is_equivalence_eq [instance] (T : Type) : is_equivalence isomorphic :=
   is_equivalence.mk (is_reflexive.mk refl) (is_symmetric.mk symm) (is_transitive.mk trans)
-
-  end -- remove
   end isomorphic
-  section --remove
-  variables {ob : Type} {C : category ob} include C --remove
-  variables {a b c d : ob} {h : @hom ob C c d} {g : @hom ob C b c} {f : @hom ob C a b} --remove
-  --remove implicit arguments below
-  inductive is_mono [class] (f : @hom ob C a b) : Prop :=
+
+  inductive is_mono [class] (f : a ⟶ b) : Prop :=
   mk : (∀c (g h : hom c a), f ∘ g = f ∘ h → g = h) → is_mono f
-  inductive is_epi  [class] (f : @hom ob C a b) : Prop :=
+  inductive is_epi  [class] (f : a ⟶ b) : Prop :=
   mk : (∀c (g h : hom b c), g ∘ f = h ∘ f → g = h) → is_epi f
 
   theorem mono_elim [H : is_mono f] {g h : c ⟶ a} (H2 : f ∘ g = f ∘ h) : g = h
@@ -155,7 +145,7 @@ namespace morphism
   theorem epi_elim [H : is_epi f] {g h : b ⟶ c} (H2 : g ∘ f = h ∘ f) : g = h
   := is_epi.rec  (λH3, H3 c g h H2) H
 
-  theorem section_is_mono [instance] (f : hom a b) [H : is_section f] : is_mono f :=
+  theorem section_is_mono [instance] (f : a ⟶ b) [H : is_section f] : is_mono f :=
   is_mono.mk
     (λ c g h H,
       calc
@@ -167,7 +157,7 @@ namespace morphism
       ... = id ∘ h : {retraction_compose f}
       ... = h : !id_left)
 
-  theorem retraction_is_epi [instance] (f : hom a b) [H : is_retraction f] : is_epi f :=
+  theorem retraction_is_epi [instance] (f : a ⟶ b) [H : is_retraction f] : is_epi f :=
   is_epi.mk
     (λ c g h H,
       calc
@@ -195,17 +185,16 @@ namespace morphism
     (λ d h₁ h₂ H,
     have H2 : (h₁ ∘ g) ∘ f = (h₂ ∘ g) ∘ f, from assoc h₁ g f  ▸ assoc h₂ g f ▸ H,
     epi_elim (epi_elim H2))
-  end
-
+end morphism
+namespace morphism
 --rewrite lemmas for inverses, modified from
 --https://github.com/JasonGross/HoTT-categories/blob/master/theories/Categories/Category/Morphisms.v
-
   namespace iso
   section
   variables {ob : Type} [C : category ob] include C
-  variables {a b c d : ob}                                         (f : @hom ob C b a)
-                           (r : @hom ob C c d) (q : @hom ob C b c) (p : @hom ob C a b)
-                           (g : @hom ob C d c)
+  variables {a b c d : ob}                                         (f : b ⟶ a)
+                           (r : c ⟶ d) (q : b ⟶ c) (p : a ⟶ b)
+                           (g : d ⟶ c)
   variable [Hq : is_iso q] include Hq
   theorem compose_pV : q ∘ q⁻¹ = id := !compose_inverse
   theorem compose_Vp : q⁻¹ ∘ q = id := !inverse_compose
@@ -235,7 +224,7 @@ namespace morphism
   have H2 : (p⁻¹) ∘ (q⁻¹ ∘ (q ∘ p)) = p⁻¹ ∘ p, from congr_arg _ (compose_V_pp q p),
   have H3 : p⁻¹ ∘ p = id, from inverse_compose p,
   inverse_eq_intro_left (H1 ⬝ H2 ⬝ H3)
-  --the following calc proof is hard for the unifier (needs ~90k steps)
+  --the proof using calc is hard for the unifier (needs ~90k steps)
   -- inverse_eq_intro_left
   --   (calc
   --     (p⁻¹ ∘ (q⁻¹)) ∘ q ∘ p = p⁻¹ ∘ (q⁻¹ ∘ (q ∘ p)) : assoc (p⁻¹) (q⁻¹) (q ∘ p)⁻¹
@@ -244,16 +233,15 @@ namespace morphism
   theorem inv_Vp [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q := inverse_involutive q ▸ inv_pp (q⁻¹) g
   theorem inv_pV [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ := inverse_involutive f ▸ inv_pp q (f⁻¹)
   theorem inv_VV [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q := inverse_involutive r ▸ inv_Vp q (r⁻¹)
-
   end
   section
   variables {ob : Type} {C : category ob} include C
-  variables {d                   c                   b                   a : ob}
-                                  {i : @hom ob C b c} {f : @hom ob C b a}
-              {r : @hom ob C c d} {q : @hom ob C b c} {p : @hom ob C a b}
-              {g : @hom ob C d c} {h : @hom ob C c b}
-                       {x : @hom ob C b d} {z : @hom ob C a c}
-                       {y : @hom ob C d b} {w : @hom ob C c a}
+  variables {d           c           b           a : ob}
+                          {i : b ⟶ c} {f : b ⟶ a}
+              {r : c ⟶ d} {q : b ⟶ c} {p : a ⟶ b}
+              {g : d ⟶ c} {h : c ⟶ b}
+                   {x : b ⟶ d} {z : a ⟶ c}
+                   {y : d ⟶ b} {w : c ⟶ a}
   variable [Hq : is_iso q] include Hq
 
   theorem moveR_Mp (H : y = q⁻¹ ∘ g) : q ∘ y = g := H⁻¹ ▸ compose_p_Vp q g
diff --git a/library/algebra/category/natural_transformation.lean b/library/algebra/category/natural_transformation.lean
new file mode 100644
index 000000000..827ab7bf2
--- /dev/null
+++ b/library/algebra/category/natural_transformation.lean
@@ -0,0 +1,49 @@
+-- Copyright (c) 2014 Floris van Doorn. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Floris van Doorn
+
+import .functor
+open category eq eq.ops functor
+
+inductive natural_transformation {C D : Category} (F G : C ⇒ D) : Type :=
+mk : Π (η : Π(a : C), hom (F a) (G a)), (Π{a b : C} (f : hom a b), G f ∘ η a = η b ∘ F f)
+ → natural_transformation F G
+
+infixl `⟹`:25 := natural_transformation -- \==>
+
+namespace natural_transformation
+  variables {C D : Category} {F G H I : functor C D}
+
+  definition natural_map [coercion] (η : F ⟹ G) : Π(a : C), F a ⟶ G a :=
+  rec (λ x y, x) η
+
+  theorem naturality (η : F ⟹ G) : Π⦃a b : C⦄ (f : a ⟶ b), G f ∘ η a = η b ∘ F f :=
+  rec (λ x y, y) η
+
+  protected definition compose (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H :=
+  natural_transformation.mk
+    (λ a, η a ∘ θ a)
+    (λ a b f,
+      calc
+	H f ∘ (η a ∘ θ a) = (H f ∘ η a) ∘ θ a : assoc
+		      ... = (η b ∘ G f) ∘ θ a : naturality η f
+		      ... = η b ∘ (G f ∘ θ a) : assoc
+		      ... = η b ∘ (θ b ∘ F f) : naturality θ f
+		      ... = (η b ∘ θ b) ∘ F f : assoc)
+--congr_arg (λx, η b ∘ x) (naturality θ f) -- this needed to be explicit for some reason (on Oct 24)
+
+  infixr `∘n`:60 := compose
+  protected theorem assoc (η₃ : H ⟹ I) (η₂ : G ⟹ H) (η₁ : F ⟹ G) :
+      η₃ ∘n (η₂ ∘n η₁) = (η₃ ∘n η₂) ∘n η₁ :=
+  dcongr_arg2 mk (funext (take x, !assoc)) !proof_irrel
+
+  protected definition id {C D : Category} {F : functor C D} : natural_transformation F F :=
+  mk (λa, id) (λa b f, !id_right ⬝ symm !id_left)
+  protected definition ID {C D : Category} (F : functor C D) : natural_transformation F F := id
+
+  protected theorem id_left (η : F ⟹ G) : natural_transformation.compose id η = η :=
+  rec (λf H, dcongr_arg2 mk (funext (take x, !id_left)) !proof_irrel) η
+
+  protected theorem id_right (η : F ⟹ G) : natural_transformation.compose η id = η :=
+  rec (λf H, dcongr_arg2 mk (funext (take x, !id_right)) !proof_irrel) η
+end natural_transformation
diff --git a/library/algebra/category/yoneda.lean b/library/algebra/category/yoneda.lean
index 56b1f9314..72176d657 100644
--- a/library/algebra/category/yoneda.lean
+++ b/library/algebra/category/yoneda.lean
@@ -2,27 +2,13 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn
 
-import .basic .constructions
+import .constructions
 
 open eq eq.ops category functor category.ops prod
 
 namespace yoneda
 --representable functor
   section
-  variables {ob : Type} {C : category ob}
-  set_option pp.universes true
-  check @type_category
-  section
-    variables {a a' b b' : ob} (f : @hom ob C a' a) (g : @hom ob C b b')
---    definition Hom_fun_fun :
-  end
-  definition Hom : Cᵒᵖ ×c C ⇒ type :=
-  @functor.mk _ _ _ _ (λ a, hom (pr1 a) (pr2 a))
-	     (λ a b f h, pr2 f ∘ h ∘ pr1 f)
-	     (λ a, funext (λh, !id_left ⬝ !id_right))
-	     (λ a b c g f, funext (λh,
-    show (pr2 g ∘ pr2 f) ∘ h ∘ (pr1 f ∘ pr1 g) = pr2 g ∘ (pr2 f ∘ h ∘ pr1 f) ∘ pr1 g, from sorry))
-  --I'm lazy, waiting for automation to fill this
 
 
 
diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean
index 611016a4a..558a69a04 100644
--- a/library/data/quotient/basic.lean
+++ b/library/data/quotient/basic.lean
@@ -115,19 +115,19 @@ R_intro Q Ha Hc Hac
 
 definition rec {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
   (Q : is_quotient R abs rep) {C : B → Type} (f : forall (a : A), C (abs a)) (b : B) : C b :=
-eq.drec_on (abs_rep Q b) (f (rep b))
+eq.rec_on (abs_rep Q b) (f (rep b))
 
 theorem comp {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
   (Q : is_quotient R abs rep) {C : B → Type} {f : forall (a : A), C (abs a)}
-  (H : forall (r s : A) (H' : R r s), eq.drec_on (eq_abs Q H') (f r) = f s)
+  (H : forall (r s : A) (H' : R r s), eq.rec_on (eq_abs Q H') (f r) = f s)
   {a : A} (Ha : R a a) : rec Q f (abs a) = f a :=
 have H2  [visible] : R a (rep (abs a)), from
   R_rep_abs Q Ha,
 have Heq [visible] : abs (rep (abs a)) = abs a, from
   abs_rep Q (abs a),
 calc
-  rec Q f (abs a) =  eq.drec_on Heq (f (rep (abs a))) : rfl
-    ... = eq.drec_on Heq (eq.drec_on (Heq⁻¹) (f a))   : {(H _ _ H2)⁻¹}
+  rec Q f (abs a) =  eq.rec_on Heq (f (rep (abs a))) : rfl
+    ... = eq.rec_on Heq (eq.rec_on (Heq⁻¹) (f a))   : {(H _ _ H2)⁻¹}
     ... = f a                                         : eq.rec_on_compose (eq_abs Q H2) _ _
 
 definition rec_constant {A B : Type} {R : A → A → Prop} {abs : A → B} {rep : B → A}
diff --git a/library/data/sigma.lean b/library/data/sigma.lean
index 10438836f..411d4fa33 100644
--- a/library/data/sigma.lean
+++ b/library/data/sigma.lean
@@ -1,7 +1,7 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
-import logic.inhabited logic.eq
+import logic.inhabited logic.cast
 open inhabited eq.ops
 
 inductive sigma {A : Type} (B : A → Type) : Type :=
@@ -10,7 +10,8 @@ dpair : Πx : A, B x → sigma B
 notation `Σ` binders `,` r:(scoped P, sigma P) := r
 
 namespace sigma
-  variables {A : Type} {B : A → Type}
+  universe variables u v
+  variables {A A' : Type.{u}} {B : A → Type.{v}} {B' : A' → Type.{v}}
 
   --without reducible tag, slice.composition_functor in algebra.category.constructions fails
   definition dpr1 [reducible] (p : Σ x, B x) : A := rec (λ a b, a) p
@@ -25,18 +26,30 @@ namespace sigma
   protected theorem eta (p : sigma B) : dpair (dpr1 p) (dpr2 p) = p :=
   destruct p (take a b, rfl)
 
-  theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.drec_on H₁ b₁ = b₂) :
+  theorem dpair_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) :
     dpair a₁ b₁ = dpair a₂ b₂ :=
-  congr_arg2_dep dpair H₁ H₂
+  dcongr_arg2 dpair H₁ H₂
 
-  protected theorem equal {p₁ p₂ : Σx : A, B x} :
-    ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : eq.drec_on H₁ (dpr2 p₁) = dpr2 p₂), p₁ = p₂ :=
+  theorem dpair_heq {a : A} {a' : A'} {b : B a} {b' : B' a'}
+      (HB : B == B') (Ha : a == a') (Hb : b == b') : dpair a b == dpair a' b' :=
+  hcongr_arg4 @dpair (heq.type_eq Ha) HB Ha Hb
+
+  protected theorem equal {p₁ p₂ : Σa : A, B a} :
+    ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : eq.rec_on H₁ (dpr2 p₁) = dpr2 p₂), p₁ = p₂ :=
   destruct p₁ (take a₁ b₁, destruct p₂ (take a₂ b₂ H₁ H₂, dpair_eq H₁ H₂))
 
+  protected theorem hequal {p : Σa : A, B a} {p' : Σa' : A', B' a'} (HB : B == B') :
+    ∀(H₁ : dpr1 p == dpr1 p') (H₂ : dpr2 p == dpr2 p'), p == p' :=
+  destruct p (take a₁ b₁, destruct p' (take a₂ b₂ H₁ H₂, dpair_heq HB H₁ H₂))
+
   protected definition is_inhabited [instance] (H₁ : inhabited A) (H₂ : inhabited (B (default A))) :
     inhabited (sigma B) :=
   inhabited.destruct H₁ (λa, inhabited.destruct H₂ (λb, inhabited.mk (dpair (default A) b)))
 
+  theorem eq_rec_dpair_commute {C : Πa, B a → Type} {a a' : A} (H : a = a') (b : B a) (c : C a b) :
+      eq.rec_on H (dpair b c) = dpair (eq.rec_on H b) (eq.rec_on (dcongr_arg2 C H rfl) c) :=
+  eq.drec_on H (dpair_eq rfl (!eq.rec_on_id⁻¹))
+
   variables {C : Πa, B a → Type} {D : Πa b, C a b → Type}
 
   definition dtrip (a : A) (b : B a) (c : C a b) := dpair a (dpair b c)
@@ -49,20 +62,20 @@ namespace sigma
   definition dpr4  (x : Σ a b c, D a b c) := dpr2 (dpr2 (dpr2 x))
 
   theorem dtrip_eq {a₁ a₂ : A} {b₁ : B a₁} {b₂ : B a₂} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
-      (H₁ : a₁ = a₂)  (H₂ : eq.drec_on H₁ b₁ = b₂) (H₃ : eq.drec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) :
+      (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂) (H₃ : cast (dcongr_arg2 C H₁ H₂) c₁ = c₂) :
     dtrip a₁ b₁ c₁ = dtrip a₂ b₂ c₂ :=
-  congr_arg3_dep dtrip H₁ H₂ H₃
+  dcongr_arg3 dtrip H₁ H₂ H₃
 
-  theorem dtrip_eq_ndep {A B : Type} {C : A → B → Type} {a₁ a₂ : A} {b₁ b₂ : B}
-      {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (H₁ : a₁ = a₂)  (H₂ : b₁ = b₂)
-      (H₃ : eq.drec_on (congr_arg2 C H₁ H₂) c₁ = c₂) :
+  theorem ndtrip_eq {A B : Type} {C : A → B → Type} {a₁ a₂ : A} {b₁ b₂ : B}
+      {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (H₁ : a₁ = a₂) (H₂ : b₁ = b₂)
+      (H₃ : cast (congr_arg2 C H₁ H₂) c₁ = c₂) :
     dtrip a₁ b₁ c₁ = dtrip a₂ b₂ c₂ :=
-  congr_arg3_ndep_dep dtrip H₁ H₂ H₃
+  hdcongr_arg3 dtrip H₁ (heq.from_eq H₂) H₃
 
-  theorem trip.equal_ndep {A B : Type} {C : A → B → Type} {p₁ p₂ : Σa b, C a b} :
+  theorem ndtrip_equal {A B : Type} {C : A → B → Type} {p₁ p₂ : Σa b, C a b} :
       ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : dpr2' p₁ = dpr2' p₂)
-      (H₃ : eq.drec_on (congr_arg2 C H₁ H₂) (dpr3 p₁) = dpr3 p₂), p₁ = p₂ :=
+      (H₃ : eq.rec_on (congr_arg2 C H₁ H₂) (dpr3 p₁) = dpr3 p₂), p₁ = p₂ :=
   destruct p₁ (take a₁ q₁, destruct q₁ (take b₁ c₁, destruct p₂ (take a₂ q₂, destruct q₂
-    (take b₂ c₂ H₁ H₂ H₃, dtrip_eq_ndep H₁ H₂ H₃))))
+    (take b₂ c₂ H₁ H₂ H₃, ndtrip_eq H₁ H₂ H₃))))
 
 end sigma
diff --git a/library/logic/axioms/funext.lean b/library/logic/axioms/funext.lean
index 57b4325b8..802cc46eb 100644
--- a/library/logic/axioms/funext.lean
+++ b/library/logic/axioms/funext.lean
@@ -5,11 +5,11 @@
 -- logic.axioms.funext
 -- ===================
 
-import logic.eq algebra.function
-open function
+import logic.cast algebra.function data.sigma
+open function eq.ops
 
 -- Function extensionality
-axiom funext : ∀ {A : Type} {B : A → Type} {f g : Π x, B x} (H : ∀ x, f x = g x), f = g
+axiom funext : ∀ {A : Type} {B : A → Type} {f g : Π a, B a} (H : ∀ a, f a = g a), f = g
 
 namespace function
   variables {A B C D: Type}
@@ -25,4 +25,10 @@ namespace function
 
   theorem compose_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) :=
   funext (take x, rfl)
+
+  theorem hfunext {A : Type} {B : A → Type} {B' : A → Type} {f : Π x, B x} {g : Π x, B' x}
+      (H : ∀ a, f a == g a) : f == g :=
+  let HH : B = B' := (funext (λ x, heq.type_eq (H x))) in
+  cast_to_heq (funext (λ a, heq.to_eq (heq.trans (cast_app' HH f a) (H a))))
+
 end function
diff --git a/library/logic/axioms/piext.lean b/library/logic/axioms/piext.lean
index 44e5985b6..e7db9e63a 100644
--- a/library/logic/axioms/piext.lean
+++ b/library/logic/axioms/piext.lean
@@ -10,6 +10,7 @@ open inhabited
 axiom piext {A : Type} {B B' : A → Type} [H : inhabited (Π x, B x)] :
    (Π x, B x) = (Π x, B' x) → B = B'
 
+-- TODO: generalize to eq_rec
 theorem cast_app {A : Type} {B B' : A → Type} (H : (Π x, B x) = (Π x, B' x)) (f : Π x, B x)
   (a : A) : cast H f a == f a :=
 have Hi [visible] : inhabited (Π x, B x), from inhabited.mk f,
diff --git a/library/logic/cast.lean b/library/logic/cast.lean
index 8909be365..a4021001b 100644
--- a/library/logic/cast.lean
+++ b/library/logic/cast.lean
@@ -6,56 +6,63 @@ open eq.ops
 
 -- cast.lean
 -- =========
-definition cast {A B : Type} (H : A = B) (a : A) : B :=
-eq.rec a H
 
-theorem cast_refl {A : Type} (a : A) : cast (eq.refl A) a = a :=
-rfl
+section
+  universe variable u
+  variables {A B : Type.{u}}
+  definition cast (H : A = B) (a : A) : B :=
+  eq.rec a H
 
-theorem cast_proof_irrel {A B : Type} (H₁ H₂ : A = B) (a : A) : cast H₁ a = cast H₂ a :=
-rfl
+  theorem cast_refl (a : A) : cast (eq.refl A) a = a :=
+  rfl
 
-theorem cast_eq {A : Type} (H : A = A) (a : A) : cast H a = a :=
-rfl
+  theorem cast_proof_irrel (H₁ H₂ : A = B) (a : A) : cast H₁ a = cast H₂ a :=
+  rfl
+
+  theorem cast_eq (H : A = A) (a : A) : cast H a = a :=
+  rfl
+end
 
 inductive heq {A : Type} (a : A) : Π {B : Type}, B → Prop :=
 refl : heq a a
 infixl `==`:50 := heq
 
 namespace heq
-  theorem drec_on {A B : Type} {a : A} {b : B} {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) : C b H₁ :=
+  universe variable u
+  variables {A B C : Type.{u}} {a a' : A} {b b' : B} {c : C}
+  theorem drec_on {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) : C b H₁ :=
   rec (λ H₁ : a == a, show C a H₁, from H₂) H₁ H₁
 
-  theorem subst {A B : Type} {a : A} {b : B} {P : ∀T : Type, T → Prop} (H₁ : a == b) (H₂ : P A a) : P B b :=
+  theorem subst {P : ∀T : Type, T → Prop} (H₁ : a == b) (H₂ : P A a) : P B b :=
   rec_on H₁ H₂
 
-  theorem symm {A B : Type} {a : A} {b : B} (H : a == b) : b == a :=
+  theorem symm (H : a == b) : b == a :=
   subst H (refl a)
 
-  theorem type_eq {A B : Type} {a : A} {b : B} (H : a == b) : A = B :=
+  theorem type_eq (H : a == b) : A = B :=
   subst H (eq.refl A)
 
-  theorem from_eq {A : Type} {a b : A} (H : a = b) : a == b :=
+  theorem from_eq (H : a = a') : a == a' :=
   eq.subst H (refl a)
 
-  theorem trans {A B C : Type} {a : A} {b : B} {c : C} (H₁ : a == b) (H₂ : b == c) : a == c :=
+  theorem trans (H₁ : a == b) (H₂ : b == c) : a == c :=
   subst H₂ H₁
 
-  theorem trans_left {A B : Type} {a : A} {b c : B} (H₁ : a == b) (H₂ : b = c) : a == c :=
+  theorem trans_left (H₁ : a == b) (H₂ : b = b') : a == b' :=
   trans H₁ (from_eq H₂)
 
-  theorem trans_right {A C : Type} {a b : A} {c : C} (H₁ : a = b) (H₂ : b == c) : a == c :=
+  theorem trans_right (H₁ : a = a') (H₂ : a' == b) : a == b :=
   trans (from_eq H₁) H₂
 
-  theorem to_cast_eq {A B : Type} {a : A} {b : B} (H : a == b) : cast (type_eq H) a = b :=
+  theorem to_cast_eq (H : a == b) : cast (type_eq H) a = b :=
   drec_on H !cast_eq
 
-  theorem to_eq {A : Type} {a b : A} (H : a == b) : a = b :=
-  calc a = cast (eq.refl A) a : !cast_eq⁻¹
-     ... = b                  : to_cast_eq H
+  theorem to_eq (H : a == a') : a = a' :=
+  calc 
+    a = cast (eq.refl A) a : cast_eq
+  ... = a'                 : to_cast_eq H
 
-  theorem elim {A B : Type} {C : Prop} {a : A} {b : B} (H₁ : a == b)
-    (H₂ : ∀ (Hab : A = B), cast Hab a = b → C) : C :=
+  theorem elim {D : Type} (H₁ : a == b) (H₂ : ∀ (Hab : A = B), cast Hab a = b → D) : D :=
   H₂ (type_eq H₁) (to_cast_eq H₁)
 
 end heq
@@ -65,53 +72,140 @@ calc_trans heq.trans_left
 calc_trans heq.trans_right
 calc_symm  heq.symm
 
-theorem cast_heq {A B : Type} (H : A = B) (a : A) : cast H a == a :=
-have H₁ : ∀ (H : A = A) (a : A), cast H a == a, from
-assume H a, heq.from_eq (cast_eq H a),
-eq.subst H H₁ H a
+section
+  universe variables u v
+  variables {A A' B C : Type.{u}} {P P' : A → Type.{v}} {a a' : A} {b : B}
 
-theorem cast_eq_to_heq {A B : Type} {a : A} {b : B} {H : A = B} (H₁ : cast H a = b) : a == b :=
-calc a  == cast H a : heq.symm (cast_heq H a)
-    ... =  b        : H₁
+  theorem eq_rec_heq (H : a = a') (p : P a) : eq.rec_on H p == p :=
+  eq.drec_on H !heq.refl
 
-theorem heq.true_elim {a : Prop} (H : a == true) : a :=
-eq_true_elim (heq.to_eq H)
+  -- should H₁ be explicit (useful in e.g. hproof_irrel)
+  theorem eq_rec_to_heq {H₁ : a = a'} {p : P a} {p' : P a'} (H₂ : eq.rec_on H₁ p = p') : p == p' :=
+  calc 
+    p == eq.rec_on H₁ p : heq.symm (eq_rec_heq H₁ p)
+   ... =  p'            : H₂
 
-theorem cast_trans {A B C : Type} (Hab : A = B) (Hbc : B = C) (a : A) :
-  cast Hbc (cast Hab a) = cast (Hab ⬝ Hbc) a :=
-heq.to_eq (calc cast Hbc (cast Hab a)   == cast Hab a          : cast_heq Hbc (cast Hab a)
-                                   ...  == a                   : cast_heq Hab a
-                                   ...  == cast (Hab ⬝ Hbc) a : heq.symm (cast_heq (Hab ⬝ Hbc) a))
+  theorem cast_to_heq {H₁ : A = B} (H₂ : cast H₁ a = b) : a == b :=
+  eq_rec_to_heq H₂
 
-theorem pi_eq {A : Type} {B B' : A → Type} (H : B = B') : (Π x, B x) = (Π x, B' x) :=
-H ▸ (eq.refl (Π x, B x))
+  theorem hproof_irrel {a b : Prop} (H : a = b) (H₁ : a) (H₂ : b) : H₁ == H₂ :=
+  eq_rec_to_heq (proof_irrel (cast H H₁) H₂)
 
-theorem dcongr_arg {A : Type} {B : A → Type} (f : Πx, B x) {a b : A} (H : a = b) : f a == f b :=
-have e1 : ∀ (H : B a = B a), cast H (f a) = f a, from
-  assume H, cast_eq H (f a),
-have e2 : ∀ (H : B a = B b), cast H (f a) = f b, from
-  H ▸ e1,
-have e3 : cast (congr_arg B H) (f a) = f b, from
-  e2 (congr_arg B H),
-cast_eq_to_heq e3
+  theorem heq.true_elim {a : Prop} (H : a == true) : a :=
+  eq_true_elim (heq.to_eq H)
 
-theorem cast_app' {A : Type} {B B' : A → Type} (H : B = B') (f : Π x, B x) (a : A) :
-  cast (pi_eq H) f a == f a :=
-have H₁ : ∀ (H : (Π x, B x) = (Π x, B x)), cast H f a == f a, from
-  assume H, heq.from_eq (congr_fun (cast_eq H f) a),
-have H₂ : ∀ (H : (Π x, B x) = (Π x, B' x)), cast H f a == f a, from
-  H ▸ H₁,
-H₂ (pi_eq H)
+  --TODO: generalize to eq.rec. This is a special case of rec_on_compose in eq.lean
+  theorem cast_trans (Hab : A = B) (Hbc : B = C) (a : A) : 
+    cast Hbc (cast Hab a) = cast (Hab ⬝ Hbc) a :=
+  heq.to_eq (calc 
+    cast Hbc (cast Hab a)  == cast Hab a         : eq_rec_heq Hbc (cast Hab a)
+                       ... == a                  : eq_rec_heq Hab a
+                       ... == cast (Hab ⬝ Hbc) a : heq.symm (eq_rec_heq (Hab ⬝ Hbc) a))
 
-theorem cast_pull {A : Type} {B B' : A → Type} (H : B = B') (f : Π x, B x) (a : A) :
-                  cast (pi_eq H) f a = cast (congr_fun H a) (f a) :=
-heq.to_eq (calc cast (pi_eq H) f a == f a                        : cast_app' H f a
-                             ...   == cast (congr_fun H a) (f a) : heq.symm (cast_heq (congr_fun H a) (f a)))
+  theorem pi_eq (H : P = P') : (Π x, P x) = (Π x, P' x) :=
+  H ▸ (eq.refl (Π x, P x))
 
-theorem hcongr_fun' {A : Type} {B B' : A → Type} {f : Π x, B x} {f' : Π x, B' x} (a : A)
-    (H₁ : f == f') (H₂ : B = B')
-  : f a == f' a :=
-heq.elim H₁ (λ (Ht : (Π x, B x) = (Π x, B' x)) (Hw : cast Ht f = f'),
-  calc f a == cast (pi_eq H₂) f a  : heq.symm (cast_app' H₂ f a)
-       ... =  cast Ht f a          : eq.refl (cast Ht f a)
-       ... =  f' a                 : congr_fun Hw a)
+  theorem hcongr_arg (f : Πx, P x) {a b : A} (H : a = b) : f a == f b :=
+  have e1 : ∀ (H : P a = P a), cast H (f a) = f a, from
+    assume H, cast_eq H (f a),
+  have e2 : ∀ (H : P a = P b), cast H (f a) = f b, from
+    H ▸ e1,
+  have e3 : cast (congr_arg P H) (f a) = f b, from
+    e2 (congr_arg P H),
+  eq_rec_to_heq e3
+
+  -- TODO: generalize to eq_rec
+  theorem cast_app' (H : P = P') (f : Π x, P x) (a : A) :
+    cast (pi_eq H) f a == f a :=
+  have H₁ : ∀ (H : (Π x, P x) = (Π x, P x)), cast H f a == f a, from
+    assume H, heq.from_eq (congr_fun (cast_eq H f) a),
+  have H₂ : ∀ (H : (Π x, P x) = (Π x, P' x)), cast H f a == f a, from
+    H ▸ H₁,
+  H₂ (pi_eq H)
+
+  -- TODO: generalize to eq_rec
+  theorem cast_pull (H : P = P') (f : Π x, P x) (a : A) :
+                    cast (pi_eq H) f a = cast (congr_fun H a) (f a) :=
+  heq.to_eq (calc 
+    cast (pi_eq H) f a == f a                        : cast_app' H f a
+                 ...   == cast (congr_fun H a) (f a) : heq.symm (eq_rec_heq (congr_fun H a) (f a)))
+
+  theorem hcongr_fun' {f : Π x, P x} {f' : Π x, P' x} (a : A)
+      (H₁ : f == f') (H₂ : P = P') : f a == f' a :=
+  heq.elim H₁ (λ (Ht : (Π x, P x) = (Π x, P' x)) (Hw : cast Ht f = f'),
+    calc f a == cast (pi_eq H₂) f a  : heq.symm (cast_app' H₂ f a)
+         ... =  cast Ht f a          : eq.refl (cast Ht f a)
+         ... =  f' a                 : congr_fun Hw a)
+
+  theorem hcongr' {P' : A' → Type} {f : Π a, P a} {f' : Π a', P' a'} {a : A} {a' : A'}
+      (Hf : f == f') (HP : P == P') (Ha : a == a') : f a == f' a' :=
+  have H1 : ∀ (B P' : A → Type) (f : Π x, P x) (f' : Π x, P' x), f == f' → (λx, P x) == (λx, P' x) 
+              → f a == f' a, from
+    take P P' f f' Hf HB, hcongr_fun' a Hf (heq.to_eq HB),
+  have H2 : ∀ (B : A → Type) (P' : A' → Type) (f : Π x, P x) (f' : Π x, P' x),
+      f == f' → (λx, P x) == (λx, P' x) → f a == f' a', from heq.subst Ha H1,
+  H2 P P' f f' Hf HP
+end
+
+
+section
+  variables {A : 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} {F : Type}
+  variables {a a' : A}
+            {b : B a} {b' : B a'}
+            {c : C a b} {c' : C a' b'}
+            {d : D a b c} {d' : D a' b' c'}
+
+  theorem hcongr_arg2 (f : Πa b, C a b) (Ha : a = a') (Hb : b == b') : f a b == f a' b' :=
+  hcongr' (hcongr_arg f Ha) (hcongr_arg C Ha) Hb
+
+  theorem hcongr_arg3 (f : Πa b c, D a b c) (Ha : a = a') (Hb : b == b') (Hc : c == c') 
+      : f a b c == f a' b' c' :=
+  hcongr' (hcongr_arg2 f Ha Hb) (hcongr_arg2 D Ha Hb) Hc
+
+  theorem hcongr_arg4 (f : Πa b c d, E a b c d) 
+    (Ha : a = a') (Hb : b == b') (Hc : c == c') (Hd : d == d') : f a b c d == f a' b' c' d' :=
+  hcongr' (hcongr_arg3 f Ha Hb Hc) (hcongr_arg3 E Ha Hb Hc) Hd
+
+  theorem dcongr_arg2 (f : Πa, B a → F) (Ha : a = a') (Hb : eq.rec_on Ha b = b')
+      : f a b = f a' b' :=
+  heq.to_eq (hcongr_arg2 f Ha (eq_rec_to_heq Hb))
+
+  theorem dcongr_arg3 (f : Πa b, C a b → F) (Ha : a = a') (Hb : eq.rec_on Ha b = b')
+      (Hc : cast (dcongr_arg2 C Ha Hb) c = c') : f a b c = f a' b' c' :=
+  heq.to_eq (hcongr_arg3 f Ha (eq_rec_to_heq Hb) (eq_rec_to_heq Hc))
+
+  theorem dcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : eq.rec_on Ha b = b')
+      (Hc : cast (dcongr_arg2 C Ha Hb) c = c') 
+      (Hd : cast (dcongr_arg3 D Ha Hb Hc) d = d') : f a b c d = f a' b' c' d' :=
+  heq.to_eq (hcongr_arg4 f Ha (eq_rec_to_heq Hb) (eq_rec_to_heq Hc) (eq_rec_to_heq Hd))
+
+  --mixed versions (we want them for example if C a' b' is a subsingleton, like a proposition. Then proving eq is easier than proving heq)
+  theorem hdcongr_arg3 (f : Πa b, C a b → F) (Ha : a = a') (Hb : b == b')
+      (Hc : cast (heq.to_eq (hcongr_arg2 C Ha Hb)) c = c') 
+        : f a b c = f a' b' c' :=
+  heq.to_eq (hcongr_arg3 f Ha Hb (eq_rec_to_heq Hc))
+
+  theorem hhdcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : b == b')
+      (Hc : c == c') 
+      (Hd : cast (dcongr_arg3 D Ha (!eq.rec_on_irrel_arg ⬝ heq.to_cast_eq Hb) 
+                                   (!eq.rec_on_irrel_arg ⬝ heq.to_cast_eq Hc)) d = d') 
+        : f a b c d = f a' b' c' d' :=
+  heq.to_eq (hcongr_arg4 f Ha Hb Hc (eq_rec_to_heq Hd))
+
+  theorem hddcongr_arg4 (f : Πa b c, D a b c → F) (Ha : a = a') (Hb : b == b')
+      (Hc : cast (heq.to_eq (hcongr_arg2 C Ha Hb)) c = c') 
+      (Hd : cast (hdcongr_arg3 D Ha Hb Hc) d = d') 
+        : f a b c d = f a' b' c' d' :=
+  heq.to_eq (hcongr_arg4 f Ha Hb (eq_rec_to_heq Hc) (eq_rec_to_heq Hd))
+
+  --Is a reasonable version of "hcongr2" provable without pi_ext and funext? 
+  --It looks like you need some ugly extra conditions
+
+  -- theorem hcongr2' {A A' : Type} {B : A → Type} {B' : A' → Type} {C : Πa, B a → Type} {C' : Πa, B' a  → Type}
+  --     {f : Π a b, C a b} {f' : Π a' b', C' a' b'} {a : A} {a' : A'} {b : B a} {b' : B' a'} 
+  --     (HBB' : B == B') (HCC' : C == C') 
+  --     (Hff' : f == f') (Haa' : a == a') (Hbb' : b == b') : f a b == f' a' b' :=
+  -- hcongr' (hcongr' Hff' (sorry) Haa') (hcongr' HCC' (sorry) Haa') Hbb'
+
+end
diff --git a/library/logic/decidable.lean b/library/logic/decidable.lean
index e34402bd6..e3a6c3a22 100644
--- a/library/logic/decidable.lean
+++ b/library/logic/decidable.lean
@@ -38,14 +38,14 @@ namespace decidable
         d2)
       d1)
 
-  theorem em (p : Prop) [H : decidable p] : p ∨ ¬p :=
-  induction_on H (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp)
-
   definition by_cases {q : Type} [C : decidable p] (Hpq : p → q) (Hnpq : ¬p → q) : q :=
   rec_on C (assume Hp, Hpq Hp) (assume Hnp, Hnpq Hnp)
 
+  theorem em (p : Prop) [H : decidable p] : p ∨ ¬p :=
+  by_cases (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp)
+
   theorem by_contradiction [Hp : decidable p] (H : ¬p → false) : p :=
-  or.elim (em p)
+  by_cases
     (assume H1 : p, H1)
     (assume H1 : ¬p, false_elim (H H1))
 
@@ -91,10 +91,10 @@ namespace decidable
   rec_on H (λh, H3 h) (λh, H4 h) --this can be proven using dependent version of "by_cases"
 end decidable
 
-definition decidable_rel  {A : Type} (R : A     → Prop) := Π (a   : A), decidable (R a)
+definition decidable_rel  {A : Type} (R : A   →   Prop) := Π (a   : A), decidable (R a)
 definition decidable_rel2 {A : Type} (R : A → A → Prop) := Π (a b : A), decidable (R a b)
 definition decidable_eq (A : Type) := decidable_rel2 (@eq A)
 
---empty cannot depend on decidable
+--empty cannot depend on decidable, so we prove this here
 protected definition empty.has_decidable_eq [instance] : decidable_eq empty :=
 take (a b : empty), decidable.inl (!empty.elim a)
diff --git a/library/logic/eq.lean b/library/logic/eq.lean
index 33f7b41f9..73af42bbc 100644
--- a/library/logic/eq.lean
+++ b/library/logic/eq.lean
@@ -54,30 +54,65 @@ calc_symm  eq.symm
 open eq.ops
 
 namespace eq
-  definition drec_on {A : Type} {a a' : A} {B : Πa' : A, a = a' → Type} (H₁ : a = a') (H₂ : B a (refl a)) : B a' H₁ :=
+  variables {A B : Type} {a a' a₁ a₂ a₃ a₄ : A}
+  definition drec_on {B : Πa' : A, a = a' → Type} (H₁ : a = a') (H₂ : B a (refl a)) : B a' H₁ :=
   eq.rec (λH₁ : a = a, show B a H₁, from H₂) H₁ H₁
 
-  theorem rec_on_id {A : Type} {a : A} {B : Πa' : A, a = a' → Type} (H : a = a) (b : B a H) : drec_on H b = b :=
+--can we remove the theorems about drec_on and only have the rec_on versions?
+  -- theorem drec_on_id {B : Πa' : A, a = a' → Type} (H : a = a) (b : B a H) : drec_on H b = b :=
+  -- rfl
+
+  -- theorem drec_on_constant (H : a = a') {B : Type} (b : B) : drec_on H b = b :=
+  -- drec_on H rfl
+
+  -- theorem drec_on_constant2 (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : drec_on H₁ b = drec_on H₂ b :=
+  -- drec_on_constant H₁ b ⬝ (drec_on_constant H₂ b)⁻¹
+
+  
+  -- theorem drec_on_irrel_arg {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') 
+  --     (b : D (f a)) : drec_on H b = drec_on H' b :=
+  -- drec_on H (λ(H' : f a = f a), !drec_on_id⁻¹) H'
+
+  -- theorem drec_on_irrel {D : A → Type} (H H' : a = a') (b : D a) : 
+  --     drec_on H b = drec_on H' b :=
+  -- !drec_on_irrel_arg
+
+  -- theorem drec_on_compose {a b c : A} {P : A → Type} (H₁ : a = b) (H₂ : b = c)
+  --         (u : P a) : drec_on H₂ (drec_on H₁ u) = drec_on (trans H₁ H₂) u :=
+  --   (show ∀ H₂ : b = c, drec_on H₂ (drec_on H₁ u) = drec_on (trans H₁ H₂) u,
+  --     from drec_on H₂ (take (H₂ : b = b), drec_on_id H₂ _))
+  --   H₂
+
+  theorem rec_on_id {B : A → Type} (H : a = a) (b : B a) : rec_on H b = b :=
   rfl
 
-  theorem rec_on_constant {A : Type} {a a' : A} {B : Type} (H : a = a') (b : B) : drec_on H b = b :=
-  drec_on H (λ(H' : a = a), rec_on_id H' b) H
+  theorem rec_on_constant (H : a = a') {B : Type} (b : B) : rec_on H b = b :=
+  drec_on H rfl
 
-  theorem rec_on_constant2 {A : Type} {a₁ a₂ a₃ a₄ : A} {B : Type} (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) :
-                           drec_on H₁ b = drec_on H₂ b :=
+  theorem rec_on_constant2 (H₁ : a₁ = a₂) (H₂ : a₃ = a₄) (b : B) : rec_on H₁ b = rec_on H₂ b :=
   rec_on_constant H₁ b ⬝ (rec_on_constant H₂ b)⁻¹
 
-  theorem rec_on_irrel {A B : Type} {a a' : A} {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) :
-                       drec_on H b = drec_on H' b :=
-  drec_on H (λ(H : a = a) (H' : f a = f a), rec_on_id H b ⬝ rec_on_id H' b⁻¹) H H'
+  theorem rec_on_irrel_arg {f : A → B} {D : B → Type} (H : a = a') (H' : f a = f a') (b : D (f a)) :
+                       rec_on H b = rec_on H' b :=
+  drec_on H (λ(H' : f a = f a), !rec_on_id⁻¹) H'
 
-  theorem rec_id {A : Type} {a : A} {B : A → Type} (H : a = a) (b : B a) : rec b H = b :=
-  rfl
+  theorem rec_on_irrel {a a' : A} {D : A → Type} (H H' : a = a') (b : D a) : 
+      drec_on H b = drec_on H' b :=
+  !rec_on_irrel_arg
 
-  theorem rec_on_compose {A : Type} {a b c : A} {P : A → Type} (H₁ : a = b) (H₂ : b = c)
-          (u : P a) :
-    drec_on H₂ (drec_on H₁ u) = drec_on (trans H₁ H₂) u :=
-    (show ∀ H₂ : b = c, drec_on H₂ (drec_on H₁ u) = drec_on (trans H₁ H₂) u,
+  --do we need the following?
+  -- theorem rec_on_irrel_fun {B : A → Type} {a : A} {f f' : Π x, B x} {D : Π a, B a → Type} (H : f = f') (H' : f a = f' a) (b : D a (f a)) :
+  --                      rec_on H b = rec_on H' b :=
+  -- sorry
+
+  -- the
+  -- theorem rec_on_comm_ap {B : A → Type} {C : Πa, B a → Type} {a a' : A} {f : Π x, C a x} 
+  --   (H : a = a') (H' : a = a') (b : B a) : rec_on H f b = rec_on H' (f b) :=
+  -- sorry
+
+  theorem rec_on_compose {a b c : A} {P : A → Type} (H₁ : a = b) (H₂ : b = c)
+          (u : P a) : rec_on H₂ (rec_on H₁ u) = rec_on (trans H₁ H₂) u :=
+    (show ∀ H₂ : b = c, rec_on H₂ (rec_on H₁ u) = rec_on (trans H₁ H₂) u,
       from drec_on H₂ (take (H₂ : b = b), rec_on_id H₂ _))
     H₂
 end eq
@@ -86,7 +121,7 @@ open eq
 
 section
   variables {A B C D E F : Type}
-  variables {a a' : A} {b b' : B} {c c' : C} {d d' : D} {e e' : E} {f f' : F}
+  variables {a a' : A} {b b' : B} {c c' : C} {d d' : D} {e e' : E}
 
   theorem congr_fun {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a :=
   H ▸ rfl
@@ -100,76 +135,37 @@ section
   theorem congr_arg2 (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' :=
   congr (congr_arg f Ha) Hb
 
-  theorem congr_arg3 (f : A → B → C → D) (Ha : a = a') (Hb : b = b') (Hc : c = c') : f a b c = f a' b' c' :=
+  theorem congr_arg3 (f : A → B → C → D) (Ha : a = a') (Hb : b = b') (Hc : c = c') 
+      : f a b c = f a' b' c' :=
   congr (congr_arg2 f Ha Hb) Hc
 
-  theorem congr_arg4 (f : A → B → C → D → E) (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') : f a b c d = f a' b' c' d' :=
+  theorem congr_arg4 (f : A → B → C → D → E) (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d')
+      : f a b c d = f a' b' c' d' :=
   congr (congr_arg3 f Ha Hb Hc) Hd
 
-  theorem congr_arg5 (f : A → B → C → D → E → F) (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') (He : e = e')
-                     : f a b c d e = f a' b' c' d' e' :=
+  theorem congr_arg5 (f : A → B → C → D → E → F) 
+      (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') (He : e = e') 
+        : f a b c d e = f a' b' c' d' e' :=
   congr (congr_arg4 f Ha Hb Hc Hd) He
 
   theorem congr2 (f f' : A → B → C) (Hf : f = f') (Ha : a = a') (Hb : b = b') : f a b = f' a' b' :=
   Hf ▸ congr_arg2 f Ha Hb
 
-  theorem congr3 (f f' : A → B → C → D) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') : f a b c = f' a' b' c' :=
+  theorem congr3 (f f' : A → B → C → D) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') 
+      : f a b c = f' a' b' c' :=
   Hf ▸ congr_arg3 f Ha Hb Hc
 
-  theorem congr4 (f f' : A → B → C → D → E) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d')
-                 : f a b c d = f' a' b' c' d' :=
+  theorem congr4 (f f' : A → B → C → D → E) 
+      (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d')
+        : f a b c d = f' a' b' c' d' :=
   Hf ▸ congr_arg4 f Ha Hb Hc Hd
 
-  theorem congr5 (f f' : A → B → C → D → E → F) (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') (He : e = e')
-                 : f a b c d e = f' a' b' c' d' e' :=
+  theorem congr5 (f f' : A → B → C → D → E → F) 
+      (Hf : f = f') (Ha : a = a') (Hb : b = b') (Hc : c = c') (Hd : d = d') (He : e = e')
+        : f a b c d e = f' a' b' c' d' e' :=
   Hf ▸ congr_arg5 f Ha Hb Hc Hd He
 end
 
-section
-  variables {A : Type} {B : A → Type} {C : Πa, B a → Type} {D : Πa b, C a b → Type} {R : Type}
-  variables {a₁ a₂ : A}
-            {b₁ : B a₁} {b₂ : B a₂}
-            {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
-            {d₁ : D a₁ b₁ c₁} {d₂ : D a₂ b₂ c₂}
-
-  theorem congr_arg2_dep (f : Πa, B a → R) (H₁ : a₁ = a₂) (H₂ : eq.drec_on H₁ b₁ = b₂)
-      : f a₁ b₁ = f a₂ b₂ :=
-  eq.drec_on H₁
-    (λ (b₂ : B a₁) (H₁ : a₁ = a₁) (H₂ : eq.drec_on H₁ b₁ = b₂),
-      calc
-        f a₁ b₁ = f a₁ (eq.drec_on H₁ b₁) : {(eq.rec_on_id H₁ b₁)⁻¹}
-            ... = f a₁ b₂                : {H₂})
-    b₂ H₁ H₂
-
-  theorem congr_arg3_dep (f : Πa b, C a b → R) (H₁ : a₁ = a₂) (H₂ : eq.drec_on H₁ b₁ = b₂)
-      (H₃ : eq.drec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂) : f a₁ b₁ c₁ = f a₂ b₂ c₂ :=
-  eq.drec_on H₁
-    (λ (b₂ : B a₁) (H₂ : b₁ = b₂) (c₂ : C a₁ b₂)
-      (H₃ : (drec_on (congr_arg2_dep C (refl a₁) H₂) c₁) = c₂),
-      have H₃' : eq.drec_on H₂ c₁ = c₂, from rec_on_irrel H₂ _ c₁ ⬝ H₃,
-      congr_arg2_dep (f a₁) H₂ H₃')
-    b₂ H₂ c₂ H₃
-
-  -- for the moment the following theorem is commented out, because it takes long to prove
-  -- theorem congr_arg4_dep (f : Πa b c, D a b c → R) (H₁ : a₁ = a₂) (H₂ : eq.rec_on H₁ b₁ = b₂)
-  --     (H₃ : eq.rec_on (congr_arg2_dep C H₁ H₂) c₁ = c₂)
-  --     (H₄ : eq.rec_on (congr_arg3_dep D H₁ H₂ H₃) d₁ = d₂) : f a₁ b₁ c₁ d₁ = f a₂ b₂ c₂ d₂ :=
-  -- eq.rec_on H₁
-  --   (λ b₂ H₂ c₂ H₃ d₂ (H₄ : _),
-  --     have H₃' [visible] : eq.rec_on H₂ c₁ = c₂, from rec_on_irrel H₂ _ c₁ ⬝ H₃,
-  --     have H₄' : rec_on (congr_arg2_dep (D a₁) H₂ H₃') d₁ = d₂, from rec_on_irrel _ _ d₁ ⬝ H₄,
-  --     congr_arg3_dep (f a₁) H₂ H₃' H₄')
-  --   b₂ H₂ c₂ H₃ d₂ H₄
-end
-
-section
-  variables {A B : Type} {C : A → B → Type} {R : Type}
-  variables {a₁ a₂ : A} {b₁ b₂ : B} {c₁ : C a₁ b₁} {c₂ : C a₂ b₂}
-  theorem congr_arg3_ndep_dep (f : Πa b, C a b → R) (H₁ : a₁ = a₂) (H₂ : b₁ = b₂) (H₃ : eq.drec_on (congr_arg2 C H₁ H₂) c₁ = c₂) :
-                              f a₁ b₁ c₁ = f a₂ b₂ c₂ :=
-  congr_arg3_dep f H₁ (rec_on_constant H₁ b₁ ⬝ H₂) H₃
-end
-
 theorem equal_f {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) : ∀x, f x = g x :=
 take x, congr_fun H x
 
@@ -255,8 +251,7 @@ inductive subsingleton [class] (A : Type) : Prop :=
 intro : (∀ a b : A, a = b) -> subsingleton A
 
 namespace subsingleton
-definition elim {A : Type} (H : subsingleton A) : ∀(a b : A), a = b :=
-rec (fun p, p) H
+definition elim {A : Type} {H : subsingleton A} : ∀(a b : A), a = b := rec (fun p, p) H
 end subsingleton
 
 protected definition prop.subsingleton [instance] (P : Prop) : subsingleton P :=