From d8a616fa70351cdace046b83211351bda95cc15b Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Mon, 3 Nov 2014 19:22:30 -0500
Subject: [PATCH] refactor(library): major changes in the library
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

I made some major changes in the library. I wanted to wait with pushing
until I had finished the formalization of the slice functor, but for
some reason that is very hard to formalize, requiring a lot of casts and
manipulation of casts. So I've not finished that yet.

Changes:

- in multiple files make more use of variables

- move dependent congr_arg theorems to logic.cast and proof them using heq (which doesn't involve nested inductions and fewer casts).

- prove some more theorems involving heq, e.g. hcongr_arg3 (which do not
  require piext)

- in theorems where casts are used in the statement use eq.rec_on
  instead of eq.drec_on

- in category split basic into basic, functor and natural_transformation

- change the definition of functor to use fully bundled
categories. @avigad: this means that the file semisimplicial.lean will
also need changes (but I'm quite sure nothing major).  You want to
define the fully bundled category Delta, and use only fully bundled
categories (type and ᵒᵖ are notations for the fully bundled
Type_category and Opposite if you open namespace category.ops). If you
want I can make the changes.

- lots of minor changes
---
 library/algebra/category/adjoint.lean         |  29 +-
 library/algebra/category/basic.lean           | 147 +--------
 library/algebra/category/constructions.lean   | 280 +++++++++++-------
 library/algebra/category/default.lean         |   2 +-
 library/algebra/category/functor.lean         | 145 +++++++++
 library/algebra/category/limit.lean           |   8 +-
 library/algebra/category/morphism.lean        |  94 +++---
 .../category/natural_transformation.lean      |  49 +++
 library/algebra/category/yoneda.lean          |  16 +-
 library/data/quotient/basic.lean              |   8 +-
 library/data/sigma.lean                       |  43 ++-
 library/logic/axioms/funext.lean              |  12 +-
 library/logic/axioms/piext.lean               |   1 +
 library/logic/cast.lean                       | 222 ++++++++++----
 library/logic/decidable.lean                  |  12 +-
 library/logic/eq.lean                         | 139 +++++----
 16 files changed, 704 insertions(+), 503 deletions(-)
 create mode 100644 library/algebra/category/functor.lean
 create mode 100644 library/algebra/category/natural_transformation.lean

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 :=