diff --git a/library/algebra/category.lean b/library/algebra/category.lean
deleted file mode 100644
index a44e2a328e..0000000000
--- a/library/algebra/category.lean
+++ /dev/null
@@ -1,554 +0,0 @@
--- 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
-
--- category
-import logic.eq logic.connectives
-import data.unit data.sigma data.prod
-import algebra.function
-import logic.axioms.funext
-
-open eq eq.ops
-
-inductive category [class] (ob : Type) : Type :=
-mk : Π (mor : ob → ob → Type) (comp : Π⦃A B C : ob⦄, mor B C → mor A B → mor A C)
-           (id : Π {A : ob}, mor A A),
-            (Π ⦃A B C D : ob⦄ {h : mor C D} {g : mor B C} {f : mor A B},
-            comp h (comp g f) = comp (comp h g) f) →
-           (Π ⦃A B : ob⦄ {f : mor A B}, comp id f = f) →
-           (Π ⦃A B : ob⦄ {f : mor A B}, comp f id = f) →
-            category ob
-
-inductive Category : Type :=
-mk : Π (A : Type), category A → Category
-
-namespace category
-
-  section
-  parameters {ob : Type} {Cat : category ob} {A B C D : ob}
-
-  definition mor : ob → ob → Type := rec (λ mor compose id assoc idr idl, mor) Cat
-  definition compose : Π {A B C : ob}, mor B C → mor A B → mor A C :=
-  rec (λ mor compose id assoc idr idl, compose) Cat
-
-  definition id : Π {A : ob}, mor A A :=
-  rec (λ mor compose id assoc idr idl, id) Cat
-  definition ID (A : ob) : mor A A := @id A
-
-  precedence `∘` : 60
-  infixr `∘` := compose
-  infixl `=>`:25 := mor
-
-  theorem assoc : Π {A B C D : ob} {h : mor C D} {g : mor B C} {f : mor A B},
-                h ∘ (g ∘ f) = (h ∘ g) ∘ f :=
-  rec (λ mor comp id assoc idr idl, assoc) Cat
-
-  theorem id_left  : Π {A B : ob} {f : mor A B}, id ∘ f = f :=
-  rec (λ mor comp id assoc idl idr, idl) Cat
-  theorem id_right : Π {A B : ob} {f : mor A B}, f ∘ id = f :=
-  rec (λ mor comp id assoc idl idr, idr) Cat
-
-  theorem id_compose {A : ob} : (ID A) ∘ id = id :=
-  id_left
-
-  theorem left_id_unique (i : mor A A) (H : Π{B} {f : mor B A}, i ∘ f = f) : i = id :=
-  calc
-    i = i ∘ id : symm id_right
-    ... = id : H
-
-  theorem right_id_unique (i : mor A A) (H : Π{B} {f : mor A B}, f ∘ i = f) : i = id :=
-  calc
-    i = id ∘ i : eq.symm id_left
-    ... = id : H
-
-  inductive is_section [class] {A B : ob} (f : mor A B) : Type :=
-  mk : ∀{g}, g ∘ f = id → is_section f
-  inductive is_retraction [class] {A B : ob} (f : mor A B) : Type :=
-  mk : ∀{g}, f ∘ g = id → is_retraction f
-  inductive is_iso [class] {A B : ob} (f : mor A B) : Type :=
-  mk : ∀{g}, g ∘ f = id → f ∘ g = id → is_iso f
-
-  definition retraction_of {A B : ob} (f : mor A B) {H : is_section f} : mor B A :=
-  is_section.rec (λg h, g) H
-  definition section_of {A B : ob} (f : mor A B) {H : is_retraction f} : mor B A :=
-  is_retraction.rec (λg h, g) H
-  definition inverse {A B : ob} (f : mor A B) {H : is_iso f} : mor B A :=
-  is_iso.rec (λg h1 h2, g) H
-
-  postfix `⁻¹` := inverse
-
-  theorem id_is_iso [instance] : is_iso (ID A) :=
-  is_iso.mk id_compose id_compose
-
-  theorem inverse_compose {A B : ob} {f : mor A B} {H : is_iso f} : f⁻¹ ∘ f = id :=
-  is_iso.rec (λg h1 h2, h1) H
-
-  theorem compose_inverse {A B : ob} {f : mor A B} {H : is_iso f} : f ∘ f⁻¹ = id :=
-  is_iso.rec (λg h1 h2, h2) H
-
-  theorem iso_imp_retraction [instance] {A B : ob} (f : mor A B) {H : is_iso f} : is_section f :=
-  is_section.mk inverse_compose
-
-  theorem iso_imp_section [instance] {A B : ob} (f : mor A B) {H : is_iso f} : is_retraction f :=
-  is_retraction.mk compose_inverse
-
-  theorem retraction_compose {A B : ob} {f : mor A B} {H : is_section f} :
-      retraction_of f ∘ f = id :=
-  is_section.rec (λg h, h) H
-
-  theorem compose_section {A B : ob} {f : mor A B} {H : is_retraction f} :
-      f ∘ section_of f = id :=
-  is_retraction.rec (λg h, h) H
-
-  theorem left_inverse_eq_right_inverse {A B : ob} {f : mor A B} {g g' : mor B A}
-      (Hl : g ∘ f = id) (Hr : f ∘ g' = id) : g = g' :=
-  calc
-    g = g ∘ id : symm id_right
-     ... = g ∘ f ∘ g' : {symm Hr}
-     ... = (g ∘ f) ∘ g' : assoc
-     ... = id ∘ g' : {Hl}
-     ... = g' : id_left
-
-  theorem section_eq_retraction {A B : ob} {f : mor A B}
-      (Hl : is_section f) (Hr : is_retraction f) : retraction_of f = section_of f :=
-  left_inverse_eq_right_inverse retraction_compose compose_section
-
-  theorem section_retraction_imp_iso {A B : ob} {f : mor A B}
-      (Hl : is_section f) (Hr : is_retraction f) : is_iso f :=
-  is_iso.mk (subst (section_eq_retraction Hl Hr) retraction_compose) compose_section
-
-  theorem inverse_unique {A B : ob} {f : mor A B} (H H' : is_iso f)
-          : @inverse _ _ f H = @inverse _ _ f H' :=
-  left_inverse_eq_right_inverse inverse_compose compose_inverse
-
-  theorem retraction_of_id {A : ob} : retraction_of (ID A) = id :=
-  left_inverse_eq_right_inverse retraction_compose id_compose
-
-  theorem section_of_id {A : ob} : section_of (ID A) = id :=
-  symm (left_inverse_eq_right_inverse id_compose compose_section)
-
-  theorem iso_of_id {A : ob} : ID A⁻¹ = id :=
-  left_inverse_eq_right_inverse inverse_compose id_compose
-
-  theorem composition_is_section [instance] {f : mor A B} {g : mor B C}
-      (Hf : is_section f) (Hg : is_section g) : is_section (g ∘ f) :=
-  is_section.mk
-    (calc
-      (retraction_of f ∘ retraction_of g) ∘ g ∘ f
-            = retraction_of f ∘ retraction_of g ∘ g ∘ f : symm assoc
-        ... = retraction_of f ∘ (retraction_of g ∘ g) ∘ f : {assoc}
-        ... = retraction_of f ∘ id ∘ f : {retraction_compose}
-        ... = retraction_of f ∘ f : {id_left}
-        ... = id : retraction_compose)
-
-  theorem composition_is_retraction [instance] {f : mor A B} {g : mor B C}
-      (Hf : is_retraction f) (Hg : is_retraction g) : is_retraction (g ∘ f) :=
-  is_retraction.mk
-    (calc
-      (g ∘ f) ∘ section_of f ∘ section_of g = g ∘ f ∘ section_of f ∘ section_of g : symm assoc
-        ... = g ∘ (f ∘ section_of f) ∘ section_of g : {assoc}
-        ... = g ∘ id ∘ section_of g : {compose_section}
-        ... = g ∘ section_of g : {id_left}
-        ... = id : compose_section)
-
-  theorem composition_is_inverse [instance] {f : mor A B} {g : mor B C}
-      (Hf : is_iso f) (Hg : is_iso g) : is_iso (g ∘ f) :=
-  section_retraction_imp_iso _ _
-
-  definition mono {A B : ob} (f : mor A B) : Prop :=
-  ∀⦃C⦄ {g h : mor C A}, f ∘ g = f ∘ h → g = h
-  definition epi  {A B : ob} (f : mor A B) : Prop :=
-  ∀⦃C⦄ {g h : mor B C}, g ∘ f = h ∘ f → g = h
-
-  theorem section_is_mono {f : mor A B} (H : is_section f) : mono f :=
-  λ C g h H,
-  calc
-    g = id ∘ g : symm id_left
-  ... = (retraction_of f ∘ f) ∘ g : {symm retraction_compose}
-  ... = retraction_of f ∘ f ∘ g : symm assoc
-  ... = retraction_of f ∘ f ∘ h : {H}
-  ... = (retraction_of f ∘ f) ∘ h : assoc
-  ... = id ∘ h : {retraction_compose}
-  ... = h : id_left
-
-  theorem retraction_is_epi {f : mor A B} (H : is_retraction f) : epi f :=
-  λ C g h H,
-  calc
-    g = g ∘ id : symm id_right
-  ... = g ∘ f ∘ section_of f : {symm compose_section}
-  ... = (g ∘ f) ∘ section_of f : assoc
-  ... = (h ∘ f) ∘ section_of f : {H}
-  ... = h ∘ f ∘ section_of f : symm assoc
-  ... = h ∘ id : {compose_section}
-  ... = h : id_right
-
-  end
-
-  section
-
-  definition objects [coercion] (C : Category) : Type
-  := Category.rec (fun c s, c) C
-
-  definition category_instance [instance] (C : Category) : category (objects C)
-  := Category.rec (fun c s, s) C
-
-  end
-
-end category
-
-open category
-
-inductive functor {obC obD : Type} (C : category obC) (D : category obD) : Type :=
-mk : Π (obF : obC → obD) (morF : Π⦃A B : obC⦄, mor A B → mor (obF A) (obF B)),
-    (Π ⦃A : obC⦄, morF (ID A) = ID (obF A)) →
-    (Π ⦃A B C : obC⦄ {f : mor A B} {g : mor B C}, morF (g ∘ f) = morF g ∘ morF 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
-  section basic_functor
-  parameters {obC obD : Type} {C : category obC} {D : category obD}
-  definition object [coercion] (F : C ⇒ D) : obC → obD := rec (λ obF morF Hid Hcomp, obF) F
-
-  definition morphism [coercion] (F : C ⇒ D) : Π{A B : obC}, mor A B → mor (F A) (F B) :=
-  rec (λ obF morF Hid Hcomp, morF) F
-
-  theorem respect_id (F : C ⇒ D) : Π {A : obC}, F (ID A) = ID (F A) :=
-  rec (λ obF morF Hid Hcomp, Hid) F
-
-  theorem respect_comp (F : C ⇒ D) : Π {a b c : obC} {f : mor a b} {g : mor b c},
-      F (g ∘ f) = F g ∘ F f :=
-  rec (λ obF morF Hid Hcomp, Hcomp) F
-  end basic_functor
-
-  section category_functor
-
-  protected definition compose {obC obD obE : Type} {C : category obC} {D : category obD} {E : category obE}
-      (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}
-               ... = id   : respect_id G)
-    (λ a b c f g, calc
-      G (F (g ∘ f)) = G (F g ∘ F f)     : {respect_comp F}
-                ... = G (F g) ∘ G (F f) : respect_comp G)
-
-  precedence `∘∘` : 60
-  infixr `∘∘` := 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 ∘∘ (G ∘∘ F) = (H ∘∘ G) ∘∘ 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 {obC obB : Type} {B : category obB} {C : category obC} {F : B ⇒ C}
-      : id ∘∘ F = F :=
-  rec (λ obF morF idF compF, rfl) F
-
-  protected theorem id_right {obC obB : Type} {B : category obB} {C : category obC} {F : B ⇒ C}
-      : F ∘∘ id = F :=
-  rec (λ obF morF idF compF, rfl) F
-
-  end category_functor
-
-  section Functor
---  parameters {C D E : Category} (G : Functor D E) (F : Functor C D)
-  definition Functor_functor {C D : Category} (F : Functor C D) : functor (category_instance C) (category_instance D) :=
-  Functor.rec (λ x, x) F
-
-  protected definition Compose {C D E : Category} (G : Functor D E) (F : Functor C D) : Functor C E :=
-  Functor.mk (compose (Functor_functor G) (Functor_functor F))
-
---  namespace Functor
-  precedence `∘∘` : 60
-  infixr `∘∘` := Compose
---  end Functor
-
-  protected definition Assoc {A B C D : Category} {H : Functor C D} {G : Functor B C} {F : Functor A B}
-    :  H ∘∘ (G ∘∘ F) = (H ∘∘ G) ∘∘ F :=
-  rfl
-
-  protected theorem Id_left {B : Category} {C : Category} {F : Functor B C}
-      : Id ∘∘ F = F :=
-  Functor.rec (λ f, subst id_left rfl) F
-
-  protected theorem Id_right {B : Category} {C : Category} {F : Functor B C}
-      : F ∘∘ Id = F :=
-  Functor.rec (λ f, subst id_right rfl) F
-
-  end Functor
-
-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), mor (object F a) (object G a)), (Π{a b : obC} (f : mor a b), morphism G f ∘ η a = η b ∘ morphism 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
-  section
-  parameters {obC obD : Type} {C : category obC} {D : category obD} {F G : C ⇒ D}
-
-  definition natural_map [coercion] (η : F ==> G) :
-      Π(a : obC), mor (object F a) (object G a) :=
-  rec (λ x y, x) η
-
-  definition naturality (η : F ==> G) :
-      Π{a b : obC} (f : mor a b), morphism G f ∘ η a = η b ∘ morphism F f :=
-  rec (λ x y, y) η
-  end
-
-  section
-  parameters {obC obD : Type} {C : category obC} {D : category obD} {F G H : C ⇒ D}
-  protected definition compose (η : G ==> H) (θ : F ==> G) : F ==> H :=
-  natural_transformation.mk
-    (λ a, η a ∘ θ a)
-    (λ a b f,
-      calc
-        morphism H f ∘ (η a ∘ θ a) = (morphism H f ∘ η a) ∘ θ a : assoc
-          ... = (η b ∘ morphism G f) ∘ θ a : {naturality η f}
-          ... = η b ∘ (morphism G f ∘ θ a) : symm assoc
-          ... = η b ∘ (θ b ∘ morphism F f) : {naturality θ f}
-          ... = (η b ∘ θ b) ∘ morphism F f : assoc)
-  end
-  precedence `∘n` : 60
-  infixr `∘n` := compose
-  section
-  protected theorem assoc {obC obD : Type} {C : category obC} {D : category obD} {F₄ F₃ F₂ F₁ : C ⇒ D} {η₃ : 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 {obC obD : Type} {C : category obC} {D : category obD} {F G : C ⇒ D}
-      {η : F ==> G} : natural_transformation.compose id η = η :=
-  rec (λf H, congr_arg2_dep mk (funext (take x, id_left)) proof_irrel) η
-
-  protected theorem id_right {obC obD : Type} {C : category obC} {D : category obD} {F G : C ⇒ D}
-      {η : F ==> G} : natural_transformation.compose η id = η :=
-  rec (λf H, congr_arg2_dep mk (funext (take x, id_right)) proof_irrel) η
-
-  end
-end natural_transformation
-
--- examples of categories / basic constructions (TODO: move to separate file)
-
-open functor
-namespace category
-  section
-  open unit
-  definition one [instance] : category unit :=
-  category.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
-
-  section
-  parameter {ob : Type}
-  definition opposite (C : category ob) : category ob :=
-  category.mk (λa b, mor 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)
-  precedence `∘op` : 60
-  infixr `∘op` := @compose _ (opposite _) _ _ _
-
-  parameters {C : category ob} {a b c : ob}
-
-  theorem compose_op {f : @mor ob C a b} {g : mor b c} : f ∘op g = g ∘ f :=
-  rfl
-
-  theorem op_op {C : category ob} : opposite (opposite C) = C :=
-  category.rec (λ mor comp id assoc idl idr, refl (mk _ _ _ _ _ _)) C
-  end
-
-  definition Opposite (C : Category) : Category :=
-  Category.mk (objects C) (opposite (category_instance C))
-
-
-  section
-  definition type_category : category Type :=
-  mk (λA B, A → B) (λ a b c, function.compose) (λ a, function.id)
-    (λ 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
-
-  section cat_Cat
-
-  definition Cat : 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_Cat
-
-  section functor_category
-  parameters {obC obD : Type} (C : category obC) (D : category obD)
-  definition functor_category : category (functor C D) :=
-  mk (λa b, natural_transformation a b)
-     (λ a b c g f, natural_transformation.compose g f)
-     (λ a, natural_transformation.id)
-     (λ a b c d h g f, natural_transformation.assoc)
-     (λ a b f, natural_transformation.id_left)
-     (λ a b f, natural_transformation.id_right)
-  end functor_category
-
-
-  section slice
-  open sigma
-
-  definition slice {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), mor b c) :=
-  mk (λa b, Σ(g : mor (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 give proof_irrel instead of rfl, to give the unifier an easier time
-  end slice
-
-  section coslice
-  open sigma
-
-  definition coslice {ob : Type} (C : category ob) (c : ob) : category (Σ(b : ob), mor c b) :=
-  mk (λa b, Σ(g : mor (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
-
-  section product
-  open prod
-  definition product {obC obD : Type} (C : category obC) (D : category obD)
-      : category (obC × obD) :=
-  mk (λa b, mor (pr1 a) (pr1 b) × mor (pr2 a) (pr2 b))
-     (λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f) )
-     (λ a, (id,id))
-     (λ 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)
-
-  end product
-
-  section arrow
-  open sigma eq.ops
-  -- theorem concat_commutative_squares {ob : Type} {C : category ob} {a1 a2 a3 b1 b2 b3 : ob}
-  --     {f1 : a1 => b1} {f2 : a2 => b2} {f3 : a3 => b3} {g2 : a2 => a3} {g1 : a1 => a2}
-  --     {h2 : b2 => b3} {h1 : b1 => b2} (H1 : f2 ∘ g1 = h1 ∘ f1) (H2 : f3 ∘ g2 = h2 ∘ f2)
-  --       : f3 ∘ (g2 ∘ g1) = (h2 ∘ h1) ∘ f1 :=
-  -- calc
-  --   f3 ∘ (g2 ∘ g1) = (f3 ∘ g2) ∘ g1 : assoc
-  --     ... = (h2 ∘ f2) ∘ g1 : {H2}
-  --     ... = h2 ∘ (f2 ∘ g1) : symm assoc
-  --     ... = h2 ∘ (h1 ∘ f1) : {H1}
-  --     ... = (h2 ∘ h1) ∘ f1 : assoc
-
-  -- definition arrow {ob : Type} (C : category ob) : category (Σ(a b : ob), mor a b) :=
-  -- mk (λa b, Σ(g : mor (dpr1 a) (dpr1 b)) (h : mor (dpr2' a) (dpr2' b)),
-  --      dpr3 b ∘ g = h ∘ dpr3 a)
-  --    (λ a b c g f, dpair (dpr1 g ∘ dpr1 f) (dpair (dpr2' g ∘ dpr2' f) (concat_commutative_squares (dpr3 f) (dpr3 g))))
-  --    (λ a, dpair id (dpair id (id_right ⬝ (symm id_left))))
-  --    (λ a b c d h g f, dtrip_eq2   assoc    assoc    proof_irrel)
-  --    (λ a b f,         trip.equal2 id_left  id_left  proof_irrel)
-  --    (λ a b f,         trip.equal2 id_right id_right proof_irrel)
-
-  definition arrow_obs (ob : Type) (C : category ob) :=
-  Σ(a b : ob), mor a b
-
-  definition src {ob : Type} {C : category ob} (a : arrow_obs ob C) : ob :=
-  dpr1 a
-
-  definition dst {ob : Type} {C : category ob} (a : arrow_obs ob C) : ob :=
-  dpr2' a
-
-  definition to_mor {ob : Type} {C : category ob} (a : arrow_obs ob C) : mor (src a) (dst a) :=
-  dpr3 a
-
-  definition arrow_mor (ob : Type) (C : category ob) (a b : arrow_obs ob C) : Type :=
-  Σ (g : mor (src a) (src b)) (h : mor (dst a) (dst b)), to_mor b ∘ g = h ∘ to_mor a
-
-  definition mor_src {ob : Type} {C : category ob} {a b : arrow_obs ob C} (m : arrow_mor ob C a b) : mor (src a) (src b) :=
-  dpr1 m
-
-  definition mor_dst {ob : Type} {C : category ob} {a b : arrow_obs ob C} (m : arrow_mor ob C a b) : mor (dst a) (dst b) :=
-  dpr2' m
-
-  definition commute {ob : Type} {C : category ob} {a b : arrow_obs ob C} (m : arrow_mor ob C a b) :
-       to_mor b ∘ (mor_src m) = (mor_dst m) ∘ to_mor a :=
-  dpr3 m
-
-  definition arrow (ob : Type) (C : category ob) : category (arrow_obs ob C) :=
-  mk (λa b, arrow_mor ob C a b)
-     (λ a b c g f, dpair (mor_src g ∘ mor_src f) (dpair (mor_dst g ∘ mor_dst f)
-        (show to_mor c ∘ (mor_src g ∘ mor_src f) = (mor_dst g ∘ mor_dst f) ∘ to_mor a,
-         proof
-         calc
-         to_mor c ∘ (mor_src g ∘ mor_src f) = (to_mor c ∘ mor_src g) ∘ mor_src f : assoc
-           ... = (mor_dst g ∘ to_mor b) ∘ mor_src f  : {commute g}
-           ... = mor_dst g ∘ (to_mor b ∘ mor_src f)  : symm assoc
-           ... = mor_dst g ∘ (mor_dst f ∘ to_mor a)  : {commute f}
-           ... = (mor_dst g ∘ mor_dst f) ∘ to_mor a  : assoc
-         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)
-
-  end arrow
-
-  -- definition foo
-  --     : category (sorry) :=
-  -- mk (λa b, sorry)
-  --    (λ a b c g f, sorry)
-  --    (λ a, sorry)
-  --    (λ a b c d h g f, sorry)
-  --    (λ a b f, sorry)
-  --    (λ a b f, sorry)
-
-end category
diff --git a/library/algebra/category/basic.lean b/library/algebra/category/basic.lean
new file mode 100644
index 0000000000..f1456195b3
--- /dev/null
+++ b/library/algebra/category/basic.lean
@@ -0,0 +1,223 @@
+-- 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 logic.axioms.funext
+
+open eq eq.ops
+
+inductive category [class] (ob : Type) : Type :=
+mk : Π (hom : ob → ob → Type) 
+       (comp : Π⦃a b c : ob⦄, hom b c → hom a b → hom a c)
+       (id : Π {a : ob}, hom a a),
+       (Π ⦃a b c d : ob⦄ {h : hom c d} {g : hom b c} {f : hom a b},
+           comp h (comp g f) = comp (comp h g) f) →
+       (Π ⦃a b : ob⦄ {f : hom a b}, comp id f = f) →
+       (Π ⦃a b : ob⦄ {f : hom a b}, comp f id = f) →
+         category ob
+
+inductive Category : Type := mk : Π (ob : Type), category ob → Category
+
+namespace category
+  section
+  parameters {ob : Type} {C : category ob} 
+  variables {a b c d : ob} 
+
+  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
+
+  infixr `∘`:60 := compose
+  infixl `⟶`:25 := hom -- input ⟶ using \-->
+
+  variables {h : hom c d} {g : hom b c} {f : hom a b} {i : hom a a}
+
+  theorem assoc : Π ⦃a b c d : ob⦄ (h : hom c d) (g : hom b c) (f : hom a b), 
+      h ∘ (g ∘ f) = (h ∘ g) ∘ f :=
+  rec (λ hom comp id assoc idr idl, assoc) C
+
+  theorem id_left  : Π ⦃a b : ob⦄ (f : hom a b), id ∘ f = f :=
+  rec (λ hom comp id assoc idl idr, idl) C
+  theorem id_right : Π ⦃a b : ob⦄ (f : hom a b), f ∘ id = f :=
+  rec (λ hom comp id assoc idl idr, idr) C
+
+  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 :=
+  calc
+    i = i ∘ id : symm !id_right
+    ... = id : H
+
+  theorem right_id_unique (H : Π{b} {f : hom a b}, f ∘ i = f) : i = id :=
+  calc
+    i = id ∘ i : eq.symm !id_left
+    ... = id : H
+  end
+
+  section
+
+  definition objects [coercion] (C : Category) : Type
+  := Category.rec (fun c s, c) C
+
+  definition category_instance [instance] (C : Category) : category (objects C)
+  := Category.rec (fun c s, s) C
+
+  end
+
+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
+  section basic_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 `∘∘`: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 ∘∘ (G ∘∘ F) = (H ∘∘ G) ∘∘ 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 := rec (λ obF homF idF compF, rfl) F
+  protected theorem id_right (F : C ⇒ D) : F ∘∘ id = F := rec (λ obF homF idF compF, rfl) F
+
+  end basic_functor
+
+  section Functor
+  variables {C₁ C₂ C₃ C₄: Category} --(G : Functor D E) (F : Functor C D)
+  definition Functor_functor {C₁ C₂ : Category} (F : Functor C₁ C₂) : --remove params
+      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))
+
+--  namespace Functor
+  infixr `∘∘`:60 := Compose
+--  end Functor
+
+  protected definition Assoc (H : Functor C₃ C₄) (G : Functor C₂ C₃) (F : Functor C₁ C₂)
+    :  H ∘∘ (G ∘∘ F) = (H ∘∘ G) ∘∘ F :=
+  rfl
+
+  protected theorem Id_left (F : Functor C₁ C₂) : Id ∘∘ F = F := 
+  Functor.rec (λ f, subst !id_left rfl) F
+
+  protected theorem Id_right {F : Functor C₁ C₂} : F ∘∘ Id = F :=
+  Functor.rec (λ f, subst !id_right rfl) F
+  end Functor
+
+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 (object F a) (object G a)), (Π{a b : obC} (f : hom a b), morphism G f ∘ η a = η b ∘ morphism 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
+  section
+  parameters {obC obD : Type} {C : category obC} {D : category obD} {F G : C ⇒ D}
+
+  definition natural_map [coercion] (η : F ⟹ G) :
+      Π(a : obC), hom (object F a) (object G a) :=
+  rec (λ x y, x) η
+
+  definition naturality (η : F ⟹ G) :
+      Π{a b : obC} (f : hom a b), morphism G f ∘ η a = η b ∘ morphism F f :=
+  rec (λ x y, y) η
+  end
+
+  section
+  parameters {obC obD : Type} {C : category obC} {D : category obD} {F G H : C ⇒ D}
+  protected definition compose (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H :=
+  natural_transformation.mk
+    (λ a, η a ∘ θ a)
+    (λ a b f,
+      calc
+        morphism H f ∘ (η a ∘ θ a) = (morphism H f ∘ η a) ∘ θ a : !assoc
+          ... = (η b ∘ morphism G f) ∘ θ a : {naturality η f}
+          ... = η b ∘ (morphism G f ∘ θ a) : symm !assoc
+          ... = η b ∘ (θ b ∘ morphism F f) : {naturality θ f}
+          ... = (η b ∘ θ b) ∘ morphism F f : !assoc)
+  end
+  precedence `∘n` : 60
+  infixr `∘n` := compose
+  section
+  variables {obC obD : Type} {C : category obC} {D : category obD} {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
+end natural_transformation
+
+
diff --git a/library/algebra/category/constructions.lean b/library/algebra/category/constructions.lean
new file mode 100644
index 0000000000..188386baf8
--- /dev/null
+++ b/library/algebra/category/constructions.lean
@@ -0,0 +1,270 @@
+-- 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
+
+-- This file contains basic constructions on categories, including common categories
+
+
+import .basic
+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
+
+  section
+  variables {ob : Type} {C : category ob} {a b c : ob}
+  definition opposite (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
+
+  theorem op_op {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))
+
+  section
+  definition type_category : category Type :=
+  mk (λa b, a → b)
+     (λ a b c, function.compose)
+     (λ a, function.id)
+     (λ 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
+
+  section
+  open decidable unit empty
+  parameters (A : Type) {H : decidable_eq A}
+  private definition set_hom (a b : A) := decidable.rec_on (H a b) (λh, unit) (λh, empty)
+  private theorem set_hom_subsingleton [instance] (a b : A) : subsingleton (set_hom a b) := _
+  private definition set_compose {a b c : A} (g : set_hom b c) (f : set_hom a b) : set_hom a c :=
+  decidable.rec_on
+    (H b c)
+    (λ Hbc g, decidable.rec_on
+      (H a b)
+      (λ Hab f, rec_on_true (trans Hab Hbc) ⋆)
+      (λh f, empty.rec _ f) f)
+    (λh (g : empty), empty.rec _ g) g
+
+  definition set_category : 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 _ _ _)
+  end
+
+  section
+  open bool
+  definition category_two := set_category bool
+  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
+
+  section product
+  open prod
+  definition product_category {obC obD : Type} (C : category obC) (D : category obD)
+      : category (obC × obD) :=
+  mk (λa b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b))
+     (λ a b c g f, (pr1 g ∘ pr1 f , pr2 g ∘ pr2 f) )
+     (λ a, (id,id))
+     (λ 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)
+
+  end product
+
+namespace ops
+  notation `Cat` := category_of_categories
+  notation `type` := type_category
+  notation 1 := category_one
+  postfix `ᵒᵖ`:max := opposite
+  infixr `×` := product_category
+  instance category_of_categories type_category category_one product_category
+end ops
+
+  section functor_category
+  parameters {obC obD : Type} (C : category obC) (D : category obD)
+  definition functor_category : category (functor C D) :=
+  mk (λa b, natural_transformation a b)
+     (λ a b c g f, natural_transformation.compose g f)
+     (λ a, natural_transformation.id)
+     (λ a b c d h g f, !natural_transformation.assoc)
+     (λ a b f, !natural_transformation.id_left)
+     (λ a b f, !natural_transformation.id_right)
+  end functor_category
+
+  section
+  open sigma
+
+  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,
+	 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
+  end --remove
+  namespace slice
+  section --remove
+  open sigma category.ops --remove sigma
+  instance slice_category
+  parameters {ob : Type} (C : category ob)
+  definition forgetful (x : ob) : (slice_category C x) ⇒ C :=
+  functor.mk (λ a, dpr1 a)
+	     (λ a b f, dpr1 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}))
+	     (λ 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
+  --		 !proof_irrel
+  --		 !proof_irrel))
+  --            (λ a b c g f, sorry)
+  end
+  end slice
+
+  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)
+
+  -- 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
+  -- theorem concat_commutative_squares {ob : Type} {C : category ob} {a1 a2 a3 b1 b2 b3 : ob}
+  --     {f1 : a1 => b1} {f2 : a2 => b2} {f3 : a3 => b3} {g2 : a2 => a3} {g1 : a1 => a2}
+  --     {h2 : b2 => b3} {h1 : b1 => b2} (H1 : f2 ∘ g1 = h1 ∘ f1) (H2 : f3 ∘ g2 = h2 ∘ f2)
+  --       : f3 ∘ (g2 ∘ g1) = (h2 ∘ h1) ∘ f1 :=
+  -- calc
+  --   f3 ∘ (g2 ∘ g1) = (f3 ∘ g2) ∘ g1 : assoc
+  --     ... = (h2 ∘ f2) ∘ g1 : {H2}
+  --     ... = h2 ∘ (f2 ∘ g1) : symm assoc
+  --     ... = h2 ∘ (h1 ∘ f1) : {H1}
+  --     ... = (h2 ∘ h1) ∘ f1 : assoc
+
+  -- definition arrow {ob : Type} (C : category ob) : category (Σ(a b : ob), hom a b) :=
+  -- mk (λa b, Σ(g : hom (dpr1 a) (dpr1 b)) (h : hom (dpr2' a) (dpr2' b)),
+  --      dpr3 b ∘ g = h ∘ dpr3 a)
+  --    (λ a b c g f, dpair (dpr1 g ∘ dpr1 f) (dpair (dpr2' g ∘ dpr2' f) (concat_commutative_squares (dpr3 f) (dpr3 g))))
+  --    (λ a, dpair id (dpair id (id_right ⬝ (symm id_left))))
+  --    (λ a b c d h g f, dtrip_eq2   assoc    assoc    !proof_irrel)
+  --    (λ a b f,         trip.equal2 id_left  id_left  !proof_irrel)
+  --    (λ a b f,         trip.equal2 id_right id_right !proof_irrel)
+
+  -- make these definitions private?
+  variables {ob : Type} {C : category ob}
+  protected definition arrow_obs (ob : Type) (C : category ob) := Σ(a b : ob), hom a b
+  variables {a b : arrow_obs ob C}
+  protected definition src    (a : arrow_obs ob C) : ob                  := dpr1 a
+  protected definition dst    (a : arrow_obs ob C) : ob                  := dpr2' a
+  protected definition to_hom (a : arrow_obs ob C) : hom (src a) (dst a) := dpr3 a
+
+  protected definition arrow_hom (a b : arrow_obs ob C) : Type :=
+  Σ (g : hom (src a) (src b)) (h : hom (dst a) (dst b)), to_hom b ∘ g = h ∘ to_hom a
+
+  protected definition hom_src (m : arrow_hom a b) : hom (src a) (src b) := dpr1 m
+  protected definition hom_dst (m : arrow_hom a b) : hom (dst a) (dst b) := dpr2' m
+  protected definition commute (m : arrow_hom a b) : to_hom b ∘ (hom_src m) = (hom_dst m) ∘ to_hom a
+  := dpr3 m
+
+  definition arrow (ob : Type) (C : category ob) : category (arrow_obs ob C) :=
+  mk (λa b, arrow_hom a b)
+     (λ a b c g f, dpair (hom_src g ∘ hom_src f) (dpair (hom_dst g ∘ hom_dst f)
+	(show to_hom c ∘ (hom_src g ∘ hom_src f) = (hom_dst g ∘ hom_dst f) ∘ to_hom a,
+	 proof
+	 calc
+	 to_hom c ∘ (hom_src g ∘ hom_src f) = (to_hom c ∘ hom_src g) ∘ hom_src f : !assoc
+	   ... = (hom_dst g ∘ to_hom b) ∘ hom_src f  : {commute g}
+	   ... = hom_dst g ∘ (to_hom b ∘ hom_src f)  : symm !assoc
+	   ... = hom_dst g ∘ (hom_dst f ∘ to_hom a)  : {commute f}
+	   ... = (hom_dst g ∘ hom_dst f) ∘ to_hom a  : !assoc
+	 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)
+
+  end arrow
+
+end category
+
+  -- definition foo
+  --     : category (sorry) :=
+  -- mk (λa b, sorry)
+  --    (λ a b c g f, sorry)
+  --    (λ a, sorry)
+  --    (λ a b c d h g f, sorry)
+  --    (λ a b f, sorry)
+  --    (λ a b f, sorry)
diff --git a/library/algebra/category/default.lean b/library/algebra/category/default.lean
new file mode 100644
index 0000000000..a5d646e767
--- /dev/null
+++ b/library/algebra/category/default.lean
@@ -0,0 +1,5 @@
+-- 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 .constructions
diff --git a/library/algebra/category/limit.lean b/library/algebra/category/limit.lean
new file mode 100644
index 0000000000..62577cbd49
--- /dev/null
+++ b/library/algebra/category/limit.lean
@@ -0,0 +1,35 @@
+-- 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 data.sigma
+
+open eq eq.ops category functor natural_transformation
+
+namespace limits
+--representable functor
+  section
+  parameters {obI ob : Type} {I : category obI} {C : category ob} {D : I ⇒ C}
+
+  definition constant_diagram (a : ob) : 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_category : category cone :=
+  -- mk (λa b, sorry)
+  --    (λ a b c g f, sorry)
+  --    (λ a, sorry)
+  --    (λ a b c d h g f, sorry)
+  --    (λ a b f, sorry)
+  --    (λ a b f, sorry)
+
+  end
+end limits
+  -- functor.mk (λ a, sorry)
+  --            (λ a b f, sorry)
+  --            (λ a, sorry)
+  --            (λ a b c g f, sorry)
diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean
new file mode 100644
index 0000000000..626454dc7f
--- /dev/null
+++ b/library/algebra/category/morphism.lean
@@ -0,0 +1,278 @@
+-- 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 algebra.relation algebra.binary
+
+open eq eq.ops category
+
+namespace morphism
+  section
+  parameters {ob : Type} {C : category ob} include C
+  variables {a b c d : ob} {h : @hom ob C c d} {g : @hom ob C b c} {f : @hom ob C a b} {i : @hom ob C b a}
+  inductive is_section    [class] (f : @hom ob C a b) : Type
+  := mk : ∀{g}, g ∘ f = id → is_section f
+  inductive is_retraction [class] (f : @hom ob C a b) : Type
+  := mk : ∀{g}, f ∘ g = id → is_retraction f
+  inductive is_iso        [class] (f : @hom ob C 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 :=
+  is_section.rec (λg h, g) H
+  definition section_of    (f : hom 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 :=
+  is_iso.rec (λg h1 h2, g) H
+
+  postfix `⁻¹` := inverse
+
+  theorem inverse_compose (f : hom 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 :=
+  is_iso.rec (λg h1 h2, h2) H
+
+  theorem retraction_compose (f : hom 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 :=
+  is_retraction.rec (λg h, h) H
+
+  theorem iso_imp_retraction [instance] (f : hom 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 :=
+  is_retraction.mk !compose_inverse
+
+  theorem id_is_iso [instance] : is_iso (ID a) :=
+  is_iso.mk !id_compose !id_compose
+
+  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}
+      (Hl : g ∘ f = id) (Hr : f ∘ g' = id) : g = g' :=
+  calc
+    g = g ∘ id : symm !id_right
+     ... = g ∘ f ∘ g' : {symm Hr}
+     ... = (g ∘ f) ∘ g' : !assoc
+     ... = id ∘ g' : {Hl}
+     ... = g' : !id_left
+
+  theorem retraction_eq_intro {H : is_section f} (H2 : f ∘ i = id) : retraction_of f = i
+  := left_inverse_eq_right_inverse !retraction_compose H2
+
+  theorem section_eq_intro {H : is_retraction f} (H2 : i ∘ f = id) : section_of f = i
+  := symm (left_inverse_eq_right_inverse H2 !compose_section)
+
+  theorem inverse_eq_intro_right {H : is_iso f} (H2 : f ∘ i = id) : f⁻¹ = i
+  := left_inverse_eq_right_inverse !inverse_compose H2
+
+  theorem inverse_eq_intro_left {H : is_iso f} (H2 : i ∘ f = id) : f⁻¹ = i
+  := symm (left_inverse_eq_right_inverse H2 !compose_inverse)
+
+  theorem section_eq_retraction (f : a ⟶ b) {Hl : is_section f} {Hr : is_retraction f} :
+      retraction_of f = section_of f :=
+  retraction_eq_intro !compose_section
+
+  theorem section_retraction_imp_iso (f : a ⟶ b) {Hl : is_section f} {Hr : is_retraction f}
+      : is_iso f :=
+  is_iso.mk (subst (section_eq_retraction f) (retraction_compose f)) (compose_section f)
+
+  theorem inverse_unique (H H' : is_iso f) : @inverse _ _ f H = @inverse _ _ f H' :=
+  inverse_eq_intro_left !inverse_compose
+
+  theorem inverse_involutive (f : a ⟶ b) {H : is_iso f} : (f⁻¹)⁻¹ = f :=
+  inverse_eq_intro_right !inverse_compose
+
+  theorem retraction_of_id : retraction_of (ID a) = id :=
+  retraction_eq_intro !id_compose
+
+  theorem section_of_id : section_of (ID a) = id :=
+  section_eq_intro !id_compose
+
+  theorem iso_of_id : ID a⁻¹ = id :=
+  inverse_eq_intro_left !id_compose
+
+  theorem composition_is_section [instance] {Hf : is_section f} {Hg : is_section g}
+      : is_section (g ∘ f) :=
+  is_section.mk
+    (calc
+      (retraction_of f ∘ retraction_of g) ∘ g ∘ f
+	    = retraction_of f ∘ retraction_of g ∘ g ∘ f : symm !assoc
+	... = retraction_of f ∘ (retraction_of g ∘ g) ∘ f : {assoc _ g f}
+	... = retraction_of f ∘ id ∘ f : {!retraction_compose}
+	... = retraction_of f ∘ f : {!id_left}
+	... = id : !retraction_compose)
+
+  theorem composition_is_retraction [instance] (Hf : is_retraction f) (Hg : is_retraction g)
+      : is_retraction (g ∘ f) :=
+  is_retraction.mk
+    (calc
+      (g ∘ f) ∘ section_of f ∘ section_of g = g ∘ f ∘ section_of f ∘ section_of g : symm !assoc
+	... = g ∘ (f ∘ section_of f) ∘ section_of g : {assoc f _ _}
+	... = g ∘ id ∘ section_of g : {!compose_section}
+	... = g ∘ section_of g : {!id_left}
+	... = id : !compose_section)
+
+  theorem composition_is_inverse [instance] (Hf : is_iso f) (Hg : is_iso g) : is_iso (g ∘ f) :=
+  !section_retraction_imp_iso
+
+  inductive isomorphic (a b : ob) : Type := mk : ∀(g : a ⟶ b) {H : is_iso g}, isomorphic a b
+
+  end -- remove
+  namespace isomorphic
+  section --remove
+  parameters {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 :=
+  isomorphic.rec (λg h, g) H
+  theorem is_iso [coercion][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?
+
+  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
+  parameters {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 :=
+  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 :=
+  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
+  := is_mono.rec (λH3, H3 c g h H2) H
+  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 :=
+  is_mono.mk
+    (λ c g h H,
+      calc
+	g = id ∘ g : symm !id_left
+      ... = (retraction_of f ∘ f) ∘ g : {symm (retraction_compose f)}
+      ... = retraction_of f ∘ f ∘ g : symm !assoc
+      ... = retraction_of f ∘ f ∘ h : {H}
+      ... = (retraction_of f ∘ f) ∘ h : !assoc
+      ... = id ∘ h : {retraction_compose f}
+      ... = h : !id_left)
+
+  theorem retraction_is_epi [instance] (f : hom a b) {H : is_retraction f} : is_epi f :=
+  is_epi.mk
+    (λ c g h H,
+      calc
+	g = g ∘ id : symm !id_right
+      ... = g ∘ f ∘ section_of f : {symm (compose_section f)}
+      ... = (g ∘ f) ∘ section_of f : !assoc
+      ... = (h ∘ f) ∘ section_of f : {H}
+      ... = h ∘ f ∘ section_of f : symm !assoc
+      ... = h ∘ id : {compose_section f}
+      ... = h : !id_right)
+
+  --these theorems are now proven automatically using type classes
+  --should they be instances?
+  theorem id_is_mono : is_mono (ID a)
+  theorem id_is_epi  : is_epi  (ID a)
+
+  theorem composition_is_mono [instance] {Hf : is_mono f} {Hg : is_mono g} : is_mono (g ∘ f) :=
+  is_mono.mk
+    (λ d h₁ h₂ H,
+    have H2 : g ∘ (f ∘ h₁) = g ∘ (f ∘ h₂), from symm (assoc g f h₁)  ▸ symm (assoc g f h₂) ▸ H,
+    mono_elim (mono_elim H2))
+
+  theorem composition_is_epi  [instance] {Hf : is_epi f}  {Hg : is_epi g}  : is_epi  (g ∘ f) :=
+  is_epi.mk
+    (λ 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
+
+--rewrite lemmas for inverses, modified from
+--https://github.com/JasonGross/HoTT-categories/blob/master/theories/Categories/Category/Morphisms.v
+
+  namespace iso
+  section
+  parameters {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)
+  variable {Hq : is_iso q} include Hq
+  theorem compose_pV : q ∘ q⁻¹ = id := !compose_inverse
+  theorem compose_Vp : q⁻¹ ∘ q = id := !inverse_compose
+  theorem compose_V_pp : q⁻¹ ∘ (q ∘ p) = p :=
+  calc
+    q⁻¹ ∘ (q ∘ p) = (q⁻¹ ∘ q) ∘ p : assoc (q⁻¹) q p
+      ... = id ∘ p : {inverse_compose q}
+      ... = p : id_left p
+  theorem compose_p_Vp : q ∘ (q⁻¹ ∘ g) = g :=
+  calc
+     q ∘ (q⁻¹ ∘ g)  = (q ∘ q⁻¹) ∘ g : assoc q (q⁻¹) g
+      ... = id ∘ g : {compose_inverse q}
+      ... = g : id_left g
+  theorem compose_pp_V : (r ∘ q) ∘ q⁻¹ = r :=
+  calc
+    (r ∘ q) ∘ q⁻¹ = r ∘ q ∘ q⁻¹ : assoc r q (q⁻¹)⁻¹
+      ... = r ∘ id : {compose_inverse q}
+      ... = r : id_right r
+  theorem compose_pV_p : (f ∘ q⁻¹) ∘ q = f :=
+  calc
+    (f ∘ q⁻¹) ∘ q = f ∘ q⁻¹ ∘ q : assoc f (q⁻¹) q⁻¹
+      ... = f ∘ id : {inverse_compose q}
+      ... = f : id_right f
+
+  theorem inv_pp {H' : is_iso p} : (q ∘ p)⁻¹ = p⁻¹ ∘ q⁻¹ :=
+  have H1 : (p⁻¹ ∘ q⁻¹) ∘ q ∘ p = p⁻¹ ∘ (q⁻¹ ∘ (q ∘ p)), from assoc (p⁻¹) (q⁻¹) (q ∘ p)⁻¹,
+  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)
+  -- inverse_eq_intro_left
+  --   (calc
+  --     (p⁻¹ ∘ (q⁻¹)) ∘ q ∘ p = p⁻¹ ∘ (q⁻¹ ∘ (q ∘ p)) : assoc (p⁻¹) (q⁻¹) (q ∘ p)⁻¹
+  --     ... = (p⁻¹) ∘ p : congr_arg (λx, p⁻¹ ∘ x) (compose_V_pp q p)
+  --     ... = id : inverse_compose p)
+  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
+  parameters {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}
+  variable {Hq : is_iso q} include Hq
+
+  theorem moveR_Mp (H : y = q⁻¹ ∘ g) : q ∘ y = g := H⁻¹ ▸ compose_p_Vp q g
+  theorem moveR_pM (H : w = f ∘ q⁻¹) : w ∘ q = f := H⁻¹ ▸ compose_pV_p f q
+  theorem moveR_Vp (H : z = q ∘ p) : q⁻¹ ∘ z = p := H⁻¹ ▸ compose_V_pp q p
+  theorem moveR_pV (H : x = r ∘ q) : x ∘ q⁻¹ = r := H⁻¹ ▸ compose_pp_V r q
+  theorem moveL_Mp (H : q⁻¹ ∘ g = y) : g = q ∘ y := moveR_Mp (H⁻¹)⁻¹
+  theorem moveL_pM (H : f ∘ q⁻¹ = w) : f = w ∘ q := moveR_pM (H⁻¹)⁻¹
+  theorem moveL_Vp (H : q ∘ p = z) : p = q⁻¹ ∘ z := moveR_Vp (H⁻¹)⁻¹
+  theorem moveL_pV (H : r ∘ q = x) : r = x ∘ q⁻¹ := moveR_pV (H⁻¹)⁻¹
+  theorem moveL_1V (H : h ∘ q = id) : h = q⁻¹ := inverse_eq_intro_left H⁻¹
+  theorem moveL_V1 (H : q ∘ h = id) : h = q⁻¹ := inverse_eq_intro_right H⁻¹
+  theorem moveL_1M (H : i ∘ q⁻¹ = id) : i = q := moveL_1V H ⬝ inverse_involutive q
+  theorem moveL_M1 (H : q⁻¹ ∘ i = id) : i = q := moveL_V1 H ⬝ inverse_involutive q
+  theorem moveR_1M (H : id = i ∘ q⁻¹) : q = i := moveL_1M (H⁻¹)⁻¹
+  theorem moveR_M1 (H : id = q⁻¹ ∘ i) : q = i := moveL_M1 (H⁻¹)⁻¹
+  theorem moveR_1V (H : id = h ∘ q) : q⁻¹ = h := moveL_1V (H⁻¹)⁻¹
+  theorem moveR_V1 (H : id = q ∘ h) : q⁻¹ = h := moveL_V1 (H⁻¹)⁻¹
+  end
+  end iso
+
+end morphism
diff --git a/library/algebra/category/yoneda.lean b/library/algebra/category/yoneda.lean
new file mode 100644
index 0000000000..6f63365fe4
--- /dev/null
+++ b/library/algebra/category/yoneda.lean
@@ -0,0 +1,16 @@
+-- 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 .constructions
+
+open eq eq.ops category functor category.ops
+
+namespace yoneda
+--representable functor
+  section
+  parameters {ob : Type} {C : category ob}
+  -- definition Hom : Cᵒᵖ × C ⇒ type :=
+  -- sorry
+  end
+end yoneda