diff --git a/hott/algebra/category/colimits.hlean b/hott/algebra/category/colimits.hlean
new file mode 100644
index 000000000..b6a33f1d8
--- /dev/null
+++ b/hott/algebra/category/colimits.hlean
@@ -0,0 +1,311 @@
+/-
+Copyright (c) 2015 Floris van Doorn. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Floris van Doorn
+
+Colimits in a category
+-/
+
+import .limits .constructions.opposite
+
+open is_trunc functor nat_trans eq
+
+-- we define colimits to be the dual of a limit
+
+namespace category
+
+  variables {ob : Type} [C : precategory ob] {c c' : ob} (D I : Precategory)
+  include C
+
+  definition is_initial [reducible] (c : ob) := @is_terminal _ (opposite C) c
+
+  definition is_contr_of_is_initial [instance] (c d : ob) [H : is_initial d]
+    : is_contr (d ⟶ c) :=
+  H c
+
+  definition initial_morphism (c c' : ob) [H : is_initial c'] : c' ⟶ c :=
+  !center
+
+  definition hom_initial_eq [H : is_initial c'] (f f' : c' ⟶ c) : f = f' :=
+  !is_hprop.elim
+
+  definition eq_initial_morphism [H : is_initial c'] (f : c' ⟶ c) : f = initial_morphism c c' :=
+  !is_hprop.elim
+
+  definition initial_iso_initial {c c' : ob} (H : is_initial c) (K : is_initial c') : c ≅ c' :=
+  iso_of_opposite_iso (@terminal_iso_terminal _ (opposite C) _ _ H K)
+
+  theorem is_hprop_is_initial [instance] : is_hprop (is_initial c) := _
+
+  omit C
+
+  definition has_initial_object [reducible] : Type := has_terminal_object Dᵒᵖ
+
+  definition initial_object [unfold 2] [reducible] [H : has_initial_object D] : D :=
+  has_terminal_object.d Dᵒᵖ
+
+  definition has_initial_object.is_initial [H : has_initial_object D]
+    : is_initial (initial_object D) :=
+  @has_terminal_object.is_terminal (Opposite D) H
+
+  variable {D}
+  definition initial_object_iso_initial_object (H₁ H₂ : has_initial_object D)
+    : @initial_object D H₁ ≅ @initial_object D H₂ :=
+  initial_iso_initial (@has_initial_object.is_initial D H₁) (@has_initial_object.is_initial D H₂)
+
+  set_option pp.coercions true
+  theorem is_hprop_has_initial_object [instance] (D : Category)
+    : is_hprop (has_initial_object D) :=
+  is_hprop_has_terminal_object (Category_opposite D)
+
+  variable (D)
+  definition has_colimits_of_shape [reducible] := has_limits_of_shape Dᵒᵖ Iᵒᵖ
+
+  /-
+    The next definitions states that a category is cocomplete with respect to diagrams
+    in a certain universe. "is_cocomplete.{o₁ h₁ o₂ h₂}" means that D is cocomplete
+    with respect to diagrams of type Precategory.{o₂ h₂}
+  -/
+
+  definition is_cocomplete [reducible] (D : Precategory) := is_complete Dᵒᵖ
+
+  definition has_colimits_of_shape_of_is_cocomplete [instance] [H : is_cocomplete D]
+    (I : Precategory) : has_colimits_of_shape D I := H Iᵒᵖ
+
+  section
+    open pi
+    theorem is_hprop_has_colimits_of_shape [instance] (D : Category) (I : Precategory)
+      : is_hprop (has_colimits_of_shape D I) :=
+    is_hprop_has_limits_of_shape (Category_opposite D) _
+
+    theorem is_hprop_is_cocomplete [instance] (D : Category) : is_hprop (is_cocomplete D) :=
+    is_hprop_is_complete (Category_opposite D)
+  end
+
+  variables {D I} (F : I ⇒ D) [H : has_colimits_of_shape D I] {i j : I}
+  include H
+
+  definition cocone [reducible] := (cone Fᵒᵖ)ᵒᵖ
+
+  definition has_initial_object_cocone [H : has_colimits_of_shape D I]
+    (F : I ⇒ D) : has_initial_object (cocone F) :=
+  begin
+    unfold [has_colimits_of_shape,has_limits_of_shape] at H,
+    exact H Fᵒᵖ
+  end
+  local attribute has_initial_object_cocone [instance]
+
+  definition colimit_cocone : cocone F := limit_cone Fᵒᵖ
+
+  definition is_initial_colimit_cocone [instance] : is_initial (colimit_cocone F) :=
+  is_terminal_limit_cone Fᵒᵖ
+
+  definition colimit_object : D :=
+  limit_object Fᵒᵖ
+
+  definition colimit_nat_trans : constant_functor Iᵒᵖ (colimit_object F) ⟹ Fᵒᵖ :=
+  limit_nat_trans Fᵒᵖ
+
+  definition colimit_morphism (i : I) : F i ⟶ colimit_object F :=
+  limit_morphism Fᵒᵖ i
+
+  variable {H}
+  theorem colimit_commute {i j : I} (f : i ⟶ j)
+    : colimit_morphism F j ∘ to_fun_hom F f = colimit_morphism F i :=
+  by rexact limit_commute Fᵒᵖ f
+
+  variable [H]
+  definition colimit_cone_obj [constructor] {d : D} {η : Πi, F i ⟶ d}
+    (p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) : cone_obj Fᵒᵖ :=
+  limit_cone_obj Fᵒᵖ proof p qed
+
+  variable {H}
+  definition colimit_hom {d : D} (η : Πi, F i ⟶ d)
+    (p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) : colimit_object F ⟶ d :=
+  hom_limit Fᵒᵖ η proof p qed
+
+  theorem colimit_hom_commute {d : D} (η : Πi, F i ⟶ d)
+    (p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) (i : I)
+    : colimit_hom F η p ∘ colimit_morphism F i = η i :=
+  by rexact hom_limit_commute Fᵒᵖ η proof p qed i
+
+  definition colimit_cone_hom [constructor] {d : D} {η : Πi, F i ⟶ d}
+    (p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) {h : colimit_object F ⟶ d}
+    (q : Πi, h ∘ colimit_morphism F i = η i)
+    : cone_hom (colimit_cone_obj F p) (colimit_cocone F) :=
+  by rexact limit_cone_hom Fᵒᵖ proof p qed proof q qed
+
+  variable {F}
+  theorem eq_colimit_hom {d : D} {η : Πi, F i ⟶ d}
+    (p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i) {h : colimit_object F ⟶ d}
+    (q : Πi, h ∘ colimit_morphism F i = η i) : h = colimit_hom F η p :=
+  by rexact @eq_hom_limit _ _ Fᵒᵖ _ _ _ proof p qed _ proof q qed
+
+  theorem colimit_cocone_unique {d : D} {η : Πi, F i ⟶ d}
+    (p : Π⦃j i : I⦄ (f : i ⟶ j), η j ∘ to_fun_hom F f = η i)
+    {h₁ : colimit_object F ⟶ d} (q₁ : Πi, h₁ ∘ colimit_morphism F i = η i)
+    {h₂ : colimit_object F ⟶ d} (q₂ : Πi, h₂ ∘ colimit_morphism F i = η i) : h₁ = h₂ :=
+  @limit_cone_unique _ _ Fᵒᵖ _ _ _ proof p qed _ proof q₁ qed _ proof q₂ qed
+
+  omit H
+
+  variable (F)
+  definition colimit_object_iso_colimit_object [constructor] (H₁ H₂ : has_colimits_of_shape D I) :
+    @(colimit_object F) H₁ ≅ @(colimit_object F) H₂ :=
+  iso_of_opposite_iso (limit_object_iso_limit_object Fᵒᵖ H₁ H₂)
+
+  section bin_coproducts
+  open bool prod.ops
+  definition has_binary_coproducts [reducible] (D : Precategory) := has_colimits_of_shape D c2
+  variables [K : has_binary_coproducts D] (d d' : D)
+  include K
+
+  definition coproduct_object : D :=
+  colimit_object (c2_functor D d d')
+
+  infixr + := coproduct_object
+
+  definition inl : d ⟶ d + d' :=
+  colimit_morphism (c2_functor D d d') ff
+
+  definition inr : d' ⟶ d + d' :=
+  colimit_morphism (c2_functor D d d') tt
+
+  variables {d d'}
+  definition coproduct_hom {x : D} (f : d ⟶ x) (g : d' ⟶ x) : d + d' ⟶ x :=
+  colimit_hom (c2_functor D d d') (bool.rec f g)
+    (by intro b₁ b₂ f; induction b₁: induction b₂: esimp at *; try contradiction: apply id_right)
+
+  theorem coproduct_hom_inl {x : D} (f : d ⟶ x) (g : d' ⟶ x) : coproduct_hom f g ∘ !inl = f :=
+  colimit_hom_commute (c2_functor D d d') (bool.rec f g) _ ff
+
+  theorem coproduct_hom_inr {x : D} (f : d ⟶ x) (g : d' ⟶ x) : coproduct_hom f g ∘ !inr = g :=
+  colimit_hom_commute (c2_functor D d d') (bool.rec f g) _ tt
+
+  theorem eq_coproduct_hom {x : D} {f : d ⟶ x} {g : d' ⟶ x} {h : d + d' ⟶ x}
+    (p : h ∘ !inl = f) (q : h ∘ !inr = g) : h = coproduct_hom f g :=
+  eq_colimit_hom _ (bool.rec p q)
+
+  theorem coproduct_cocone_unique {x : D} {f : d ⟶ x} {g : d' ⟶ x}
+    {h₁ : d + d' ⟶ x} (p₁ : h₁ ∘ !inl = f) (q₁ : h₁ ∘ !inr = g)
+    {h₂ : d + d' ⟶ x} (p₂ : h₂ ∘ !inl = f) (q₂ : h₂ ∘ !inr = g) : h₁ = h₂ :=
+  eq_coproduct_hom p₁ q₁ ⬝ (eq_coproduct_hom p₂ q₂)⁻¹
+
+  variable (D)
+  definition coproduct_functor [constructor] : D ×c D ⇒ D :=
+  functor.mk
+    (λx, coproduct_object x.1 x.2)
+    (λx y f, coproduct_hom (!inl ∘ f.1) (!inr ∘ f.2))
+    abstract begin intro x, symmetry, apply eq_coproduct_hom: apply id_comp_eq_comp_id end end
+    abstract begin intro x y z g f, symmetry, apply eq_coproduct_hom,
+                   rewrite [-assoc,coproduct_hom_inl,assoc,coproduct_hom_inl,-assoc],
+                   rewrite [-assoc,coproduct_hom_inr,assoc,coproduct_hom_inr,-assoc] end end
+  omit K
+  variables {D} (d d')
+
+  definition coproduct_object_iso_coproduct_object [constructor] (H₁ H₂ : has_binary_coproducts D) :
+    @coproduct_object D H₁ d d' ≅ @coproduct_object D H₂ d d' :=
+  colimit_object_iso_colimit_object _ H₁ H₂
+
+  end bin_coproducts
+
+  /-
+    intentionally we define coproducts in terms of colimits,
+    but coequalizers in terms of equalizers, to see which characterization is more useful
+  -/
+
+  section coequalizers
+  open bool prod.ops sum equalizer_category_hom
+
+  definition has_coequalizers [reducible] (D : Precategory) := has_equalizers Dᵒᵖ
+  variables [K : has_coequalizers D]
+  include K
+
+  variables {d d' x : D} (f g : d ⟶ d')
+  definition coequalizer_object : D :=
+  !(@equalizer_object Dᵒᵖ) f g
+
+  definition coequalizer : d' ⟶ coequalizer_object f g :=
+  !(@equalizer Dᵒᵖ)
+
+  theorem coequalizes : coequalizer f g ∘ f = coequalizer f g ∘ g :=
+  by rexact !(@equalizes Dᵒᵖ)
+
+  variables {f g}
+  definition coequalizer_hom (h : d' ⟶ x) (p : h ∘ f = h ∘ g) : coequalizer_object f g ⟶ x :=
+  !(@hom_equalizer Dᵒᵖ) proof p qed
+
+  theorem coequalizer_hom_coequalizer (h : d' ⟶ x) (p : h ∘ f = h ∘ g)
+    : coequalizer_hom h p ∘ coequalizer f g = h :=
+  by rexact !(@equalizer_hom_equalizer Dᵒᵖ)
+
+  theorem eq_coequalizer_hom {h : d' ⟶ x} (p : h ∘ f = h ∘ g) {i : coequalizer_object f g ⟶ x}
+    (q : i ∘ coequalizer f g = h) : i = coequalizer_hom h p :=
+  by rexact !(@eq_hom_equalizer Dᵒᵖ) proof q qed
+
+  theorem coequalizer_cocone_unique {h : d' ⟶ x} (p : h ∘ f = h ∘ g)
+    {i₁ : coequalizer_object f g ⟶ x} (q₁ : i₁ ∘ coequalizer f g = h)
+    {i₂ : coequalizer_object f g ⟶ x} (q₂ : i₂ ∘ coequalizer f g = h) : i₁ = i₂ :=
+  !(@equalizer_cone_unique Dᵒᵖ) proof p qed proof q₁ qed proof q₂ qed
+
+  omit K
+  variables (f g)
+  definition coequalizer_object_iso_coequalizer_object [constructor] (H₁ H₂ : has_coequalizers D) :
+    @coequalizer_object D H₁ _ _ f g ≅ @coequalizer_object D H₂ _ _ f g :=
+  iso_of_opposite_iso !(@equalizer_object_iso_equalizer_object Dᵒᵖ)
+
+  end coequalizers
+
+  section pushouts
+  open bool prod.ops sum pullback_category_hom
+
+  definition has_pushouts [reducible] (D : Precategory) := has_pullbacks Dᵒᵖ
+  variables [K : has_pushouts D]
+  include K
+
+  variables {d₁ d₂ d₃ x : D} (f : d₁ ⟶ d₂) (g : d₁ ⟶ d₃)
+  definition pushout_object : D :=
+  !(@pullback_object Dᵒᵖ) f g
+
+  definition pushout : d₃ ⟶ pushout_object f g :=
+  !(@pullback Dᵒᵖ)
+
+  definition pushout_rev : d₂ ⟶ pushout_object f g :=
+  !(@pullback_rev Dᵒᵖ)
+
+  theorem pushout_commutes : pushout_rev f g ∘ f = pushout f g ∘ g :=
+  by rexact !(@pullback_commutes Dᵒᵖ)
+
+  variables {f g}
+  definition pushout_hom (h₁ : d₂ ⟶ x) (h₂ : d₃ ⟶ x) (p : h₁ ∘ f = h₂ ∘ g)
+    : pushout_object f g ⟶ x :=
+  !(@hom_pullback Dᵒᵖ) proof p qed
+
+  theorem pushout_hom_pushout (h₁ : d₂ ⟶ x) (h₂ : d₃ ⟶ x) (p : h₁ ∘ f = h₂ ∘ g)
+    : pushout_hom h₁ h₂ p ∘ pushout f g = h₂ :=
+  by rexact !(@pullback_hom_pullback Dᵒᵖ)
+
+  theorem pushout_hom_pushout_rev (h₁ : d₂ ⟶ x) (h₂ : d₃ ⟶ x) (p : h₁ ∘ f = h₂ ∘ g)
+    : pushout_hom h₁ h₂ p ∘ pushout_rev f g = h₁ :=
+  by rexact !(@pullback_rev_hom_pullback Dᵒᵖ)
+
+  theorem eq_pushout_hom {h₁ : d₂ ⟶ x} {h₂ : d₃ ⟶ x} (p : h₁ ∘ f = h₂ ∘ g)
+    {i : pushout_object f g ⟶ x} (q : i ∘ pushout f g = h₂) (r : i ∘ pushout_rev f g = h₁)
+    : i = pushout_hom h₁ h₂ p :=
+  by rexact !(@eq_hom_pullback Dᵒᵖ) proof q qed proof r qed
+
+  theorem pushout_cocone_unique {h₁ : d₂ ⟶ x} {h₂ : d₃ ⟶ x} (p : h₁ ∘ f = h₂ ∘ g)
+    {i₁ : pushout_object f g ⟶ x} (q₁ : i₁ ∘ pushout f g = h₂) (r₁ : i₁ ∘ pushout_rev f g = h₁)
+    {i₂ : pushout_object f g ⟶ x} (q₂ : i₂ ∘ pushout f g = h₂) (r₂ : i₂ ∘ pushout_rev f g = h₁)
+    : i₁ = i₂ :=
+  !(@pullback_cone_unique Dᵒᵖ) proof p qed proof q₁ qed proof r₁ qed proof q₂ qed proof r₂ qed
+
+  omit K
+  variables (f g)
+  definition pushout_object_iso_pushout_object [constructor] (H₁ H₂ : has_pushouts D) :
+    @pushout_object D H₁ _ _ _ f g ≅ @pushout_object D H₂ _ _ _ f g :=
+  iso_of_opposite_iso !(@pullback_object_iso_pullback_object (Opposite D))
+
+  end pushouts
+
+end category
diff --git a/hott/algebra/category/constructions/finite_cats.hlean b/hott/algebra/category/constructions/finite_cats.hlean
index b83270f0f..b89a9ce4e 100644
--- a/hott/algebra/category/constructions/finite_cats.hlean
+++ b/hott/algebra/category/constructions/finite_cats.hlean
@@ -18,8 +18,8 @@ namespace category
 
   include H HR HA
 
-  -- we call a diagram (or category) sparse if you cannot compose two morphism, except the ones which come from equality
-  definition sparse_diagram' [constructor] : precategory A :=
+  -- we call a category sparse if you cannot compose two morphism, except the ones which come from equality
+  definition sparse_category' [constructor] : precategory A :=
   precategory.mk
     (λa b, R a b ⊎ a = b)
     begin
@@ -38,11 +38,11 @@ namespace category
     abstract by intros a b f; induction f with rf pf: reflexivity end
     abstract by intros a b f; (induction f with rf pf: esimp); rewrite idp_con end
 
-  definition sparse_diagram [constructor] : Precategory :=
-  precategory.Mk (sparse_diagram' R @H)
+  definition sparse_category [constructor] : Precategory :=
+  precategory.Mk (sparse_category' R @H)
 
-  definition sparse_diagram_functor [constructor] (C : Precategory) (f : A → C)
-    (g : Π{a b} (r : R a b), f a ⟶ f b) : sparse_diagram R H ⇒ C :=
+  definition sparse_category_functor [constructor] (C : Precategory) (f : A → C)
+    (g : Π{a b} (r : R a b), f a ⟶ f b) : sparse_category R H ⇒ C :=
   functor.mk f
              (λa b, sum.rec g (eq.rec id))
              (λa, idp)
@@ -58,14 +58,14 @@ namespace category
   omit H HR HA
 
   section equalizer
-  inductive equalizer_diagram_hom : bool → bool → Type :=
-  | f1 : equalizer_diagram_hom ff tt
-  | f2 : equalizer_diagram_hom ff tt
+  inductive equalizer_category_hom : bool → bool → Type :=
+  | f1 : equalizer_category_hom ff tt
+  | f2 : equalizer_category_hom ff tt
 
-  open equalizer_diagram_hom
-  theorem is_hset_equalizer_diagram_hom (b₁ b₂ : bool) : is_hset (equalizer_diagram_hom b₁ b₂) :=
+  open equalizer_category_hom
+  theorem is_hset_equalizer_category_hom (b₁ b₂ : bool) : is_hset (equalizer_category_hom b₁ b₂) :=
   begin
-    assert H : Πb b', equalizer_diagram_hom b b' ≃ bool.rec (bool.rec empty bool) (λb, empty) b b',
+    assert H : Πb b', equalizer_category_hom b b' ≃ bool.rec (bool.rec empty bool) (λb, empty) b b',
     { intro b b', fapply equiv.MK,
       { intro x, induction x, exact ff, exact tt},
       { intro v, induction b: induction b': induction v, exact f1, exact f2},
@@ -75,44 +75,44 @@ namespace category
     induction b₁: induction b₂: exact _
   end
 
-  local attribute is_hset_equalizer_diagram_hom [instance]
-  definition equalizer_diagram [constructor] : Precategory :=
-  sparse_diagram
-    equalizer_diagram_hom
+  local attribute is_hset_equalizer_category_hom [instance]
+  definition equalizer_category [constructor] : Precategory :=
+  sparse_category
+    equalizer_category_hom
     begin intro a b c g f; cases g: cases f end
 
-  definition equalizer_diagram_functor [constructor] (C : Precategory) {x y : C} (f g : x ⟶ y)
-    : equalizer_diagram ⇒ C :=
-  sparse_diagram_functor _ _ C
+  definition equalizer_category_functor [constructor] (C : Precategory) {x y : C} (f g : x ⟶ y)
+    : equalizer_category ⇒ C :=
+  sparse_category_functor _ _ C
     (bool.rec x y)
     begin intro a b h; induction h, exact f, exact g end
   end equalizer
 
   section pullback
-  inductive pullback_diagram_ob : Type :=
-  | TR : pullback_diagram_ob
-  | BL : pullback_diagram_ob
-  | BR : pullback_diagram_ob
+  inductive pullback_category_ob : Type :=
+  | TR : pullback_category_ob
+  | BL : pullback_category_ob
+  | BR : pullback_category_ob
 
-  theorem pullback_diagram_ob_decidable_equality : decidable_eq pullback_diagram_ob :=
+  theorem pullback_category_ob_decidable_equality : decidable_eq pullback_category_ob :=
   begin
     intro x y; induction x: induction y:
       try exact decidable.inl idp:
       apply decidable.inr; contradiction
   end
 
-  open pullback_diagram_ob
-  inductive pullback_diagram_hom : pullback_diagram_ob → pullback_diagram_ob → Type :=
-  | f1 : pullback_diagram_hom TR BR
-  | f2 : pullback_diagram_hom BL BR
+  open pullback_category_ob
+  inductive pullback_category_hom : pullback_category_ob → pullback_category_ob → Type :=
+  | f1 : pullback_category_hom TR BR
+  | f2 : pullback_category_hom BL BR
 
-  open pullback_diagram_hom
-  theorem is_hset_pullback_diagram_hom (b₁ b₂ : pullback_diagram_ob)
-    : is_hset (pullback_diagram_hom b₁ b₂) :=
+  open pullback_category_hom
+  theorem is_hset_pullback_category_hom (b₁ b₂ : pullback_category_ob)
+    : is_hset (pullback_category_hom b₁ b₂) :=
   begin
-    assert H : Πb b', pullback_diagram_hom b b' ≃
-      pullback_diagram_ob.rec (λb, empty) (λb, empty)
-                              (pullback_diagram_ob.rec unit unit empty) b' b,
+    assert H : Πb b', pullback_category_hom b b' ≃
+      pullback_category_ob.rec (λb, empty) (λb, empty)
+                              (pullback_category_ob.rec unit unit empty) b' b,
     { intro b b', fapply equiv.MK,
       { intro x, induction x: exact star},
       { intro v, induction b: induction b': induction v, exact f1, exact f2},
@@ -122,16 +122,16 @@ namespace category
     induction b₁: induction b₂: exact _
   end
 
-  local attribute is_hset_pullback_diagram_hom pullback_diagram_ob_decidable_equality [instance]
-  definition pullback_diagram [constructor] : Precategory :=
-  sparse_diagram
-    pullback_diagram_hom
+  local attribute is_hset_pullback_category_hom pullback_category_ob_decidable_equality [instance]
+  definition pullback_category [constructor] : Precategory :=
+  sparse_category
+    pullback_category_hom
     begin intro a b c g f; cases g: cases f end
 
-  definition pullback_diagram_functor [constructor] (C : Precategory) {x y z : C}
-    (f : x ⟶ z) (g : y ⟶ z) : pullback_diagram ⇒ C :=
-  sparse_diagram_functor _ _ C
-    (pullback_diagram_ob.rec x y z)
+  definition pullback_category_functor [constructor] (C : Precategory) {x y z : C}
+    (f : x ⟶ z) (g : y ⟶ z) : pullback_category ⇒ C :=
+  sparse_category_functor _ _ C
+    (pullback_category_ob.rec x y z)
     begin intro a b h; induction h, exact f, exact g end
   end pullback
 
diff --git a/hott/algebra/category/constructions/hset.hlean b/hott/algebra/category/constructions/hset.hlean
index 16d9ba077..27bdef664 100644
--- a/hott/algebra/category/constructions/hset.hlean
+++ b/hott/algebra/category/constructions/hset.hlean
@@ -117,7 +117,7 @@ namespace category
       esimp, apply p}}
   end
 
-  definition is_complete_set.{u v w} : is_complete.{(max u v w)+1 (max u v w) v w} set :=
+  definition is_complete_set.{u v w} [instance] : is_complete.{(max u v w)+1 (max u v w) v w} set :=
   begin
     intro I F, fapply has_terminal_object.mk,
     { exact is_complete_set_cone.{u v w} I F},
@@ -137,4 +137,5 @@ namespace category
           apply is_trunc_pi, intro f,
           apply is_trunc_eq}}}
   end
+
 end category
diff --git a/hott/algebra/category/limits.hlean b/hott/algebra/category/limits.hlean
index 8efa171cc..a8d02104c 100644
--- a/hott/algebra/category/limits.hlean
+++ b/hott/algebra/category/limits.hlean
@@ -67,7 +67,7 @@ namespace category
   /-
     The next definitions states that a category is complete with respect to diagrams
     in a certain universe. "is_complete.{o₁ h₁ o₂ h₂}" means that D is complete
-    with respect to diagrams of type Precategory.{o₂ h₂}
+    with respect to diagrams with shape in Precategory.{o₂ h₂}
   -/
 
   definition is_complete.{o₁ h₁ o₂ h₂} [class] (D : Precategory.{o₁ h₁}) :=
@@ -86,7 +86,7 @@ namespace category
     theorem is_hprop_is_complete [instance] (D : Category) : is_hprop (is_complete D) := _
   end
 
-  variables {I D}
+  variables {D I}
   definition has_terminal_object_cone [H : has_limits_of_shape D I]
     (F : I ⇒ D) : has_terminal_object (cone F) := H F
   local attribute has_terminal_object_cone [instance]
@@ -123,7 +123,7 @@ namespace category
     (p : Π⦃i j : I⦄ (f : i ⟶ j), to_fun_hom F f ∘ η i = η j) : d ⟶ limit_object F :=
   cone_hom.f (@(terminal_morphism (limit_cone_obj F p) _) (is_terminal_limit_cone _))
 
-  definition hom_limit_commute {d : D} (η : Πi, d ⟶ F i)
+  theorem hom_limit_commute {d : D} (η : Πi, d ⟶ F i)
     (p : Π⦃i j : I⦄ (f : i ⟶ j), to_fun_hom F f ∘ η i = η j) (i : I)
     : limit_morphism F i ∘ hom_limit F η p = η i :=
   cone_hom.p (@(terminal_morphism (limit_cone_obj F p) _) (is_terminal_limit_cone _)) i
@@ -189,10 +189,10 @@ namespace category
   hom_limit (c2_functor D d d') (bool.rec f g)
     (by intro b₁ b₂ f; induction b₁: induction b₂: esimp at *; try contradiction: apply id_left)
 
-  definition pr1_hom_product {x : D} (f : x ⟶ d) (g : x ⟶ d') : !pr1 ∘ hom_product f g = f :=
+  theorem pr1_hom_product {x : D} (f : x ⟶ d) (g : x ⟶ d') : !pr1 ∘ hom_product f g = f :=
   hom_limit_commute (c2_functor D d d') (bool.rec f g) _ ff
 
-  definition pr2_hom_product {x : D} (f : x ⟶ d) (g : x ⟶ d') : !pr2 ∘ hom_product f g = g :=
+  theorem pr2_hom_product {x : D} (f : x ⟶ d) (g : x ⟶ d') : !pr2 ∘ hom_product f g = g :=
   hom_limit_commute (c2_functor D d d') (bool.rec f g) _ tt
 
   theorem eq_hom_product {x : D} {f : x ⟶ d} {g : x ⟶ d'} {h : x ⟶ d × d'}
@@ -201,8 +201,7 @@ namespace category
 
   theorem product_cone_unique {x : D} {f : x ⟶ d} {g : x ⟶ d'}
     {h₁ : x ⟶ d × d'} (p₁ : !pr1 ∘ h₁ = f) (q₁ : !pr2 ∘ h₁ = g)
-    {h₂ : x ⟶ d × d'} (p₂ : !pr1 ∘ h₂ = f) (q₂ : !pr2 ∘ h₂ = g)
-      : h₁ = h₂ :=
+    {h₂ : x ⟶ d × d'} (p₂ : !pr1 ∘ h₂ = f) (q₂ : !pr2 ∘ h₂ = g) : h₁ = h₂ :=
   eq_hom_product p₁ q₁ ⬝ (eq_hom_product p₂ q₂)⁻¹
 
   variable (D)
@@ -224,25 +223,25 @@ namespace category
   end bin_products
 
   section equalizers
-  open bool prod.ops sum equalizer_diagram_hom
-  definition has_equalizers [reducible] (D : Precategory) := has_limits_of_shape D equalizer_diagram
+  open bool prod.ops sum equalizer_category_hom
+  definition has_equalizers [reducible] (D : Precategory) := has_limits_of_shape D equalizer_category
   variables [K : has_equalizers D]
   include K
 
   variables {d d' x : D} (f g : d ⟶ d')
   definition equalizer_object : D :=
-  limit_object (equalizer_diagram_functor D f g)
+  limit_object (equalizer_category_functor D f g)
 
   definition equalizer : equalizer_object f g ⟶ d :=
-  limit_morphism (equalizer_diagram_functor D f g) ff
+  limit_morphism (equalizer_category_functor D f g) ff
 
   theorem equalizes : f ∘ equalizer f g = g ∘ equalizer f g :=
-   limit_commute (equalizer_diagram_functor D f g) (inl f1) ⬝
-  (limit_commute (equalizer_diagram_functor D f g) (inl f2))⁻¹
+   limit_commute (equalizer_category_functor D f g) (inl f1) ⬝
+  (limit_commute (equalizer_category_functor D f g) (inl f2))⁻¹
 
   variables {f g}
   definition hom_equalizer (h : x ⟶ d) (p : f ∘ h = g ∘ h) : x ⟶ equalizer_object f g :=
-  hom_limit (equalizer_diagram_functor D f g)
+  hom_limit (equalizer_category_functor D f g)
             (bool.rec h (g ∘ h))
             begin
               intro b₁ b₂ i; induction i with j j: induction j,
@@ -250,15 +249,15 @@ namespace category
               exact p, reflexivity, apply id_left
             end
 
-  definition equalizer_hom_equalizer (h : x ⟶ d) (p : f ∘ h = g ∘ h)
+  theorem equalizer_hom_equalizer (h : x ⟶ d) (p : f ∘ h = g ∘ h)
     : equalizer f g ∘ hom_equalizer h p = h :=
-  hom_limit_commute (equalizer_diagram_functor D f g) (bool.rec h (g ∘ h)) _ ff
+  hom_limit_commute (equalizer_category_functor D f g) (bool.rec h (g ∘ h)) _ ff
 
   theorem eq_hom_equalizer {h : x ⟶ d} (p : f ∘ h = g ∘ h) {i : x ⟶ equalizer_object f g}
     (q : equalizer f g ∘ i = h) : i = hom_equalizer h p :=
   eq_hom_limit _ (bool.rec q
     begin
-      refine ap (λx, x ∘ i) (limit_commute (equalizer_diagram_functor D f g) (inl f2))⁻¹ ⬝ _,
+      refine ap (λx, x ∘ i) (limit_commute (equalizer_category_functor D f g) (inl f2))⁻¹ ⬝ _,
       refine !assoc⁻¹ ⬝ _,
       exact ap (λx, _ ∘ x) q
     end)
@@ -268,6 +267,7 @@ namespace category
     {i₂ : x ⟶ equalizer_object f g} (q₂ : equalizer f g ∘ i₂ = h) : i₁ = i₂ :=
   eq_hom_equalizer p q₁ ⬝ (eq_hom_equalizer p q₂)⁻¹
 
+  omit K
   variables (f g)
   definition equalizer_object_iso_equalizer_object [constructor] (H₁ H₂ : has_equalizers D) :
     @equalizer_object D H₁ _ _ f g ≅ @equalizer_object D H₂ _ _ f g :=
@@ -276,56 +276,56 @@ namespace category
   end equalizers
 
   section pullbacks
-  open sum prod.ops pullback_diagram_ob pullback_diagram_hom
-  definition has_pullbacks [reducible] (D : Precategory) := has_limits_of_shape D pullback_diagram
+  open sum prod.ops pullback_category_ob pullback_category_hom
+  definition has_pullbacks [reducible] (D : Precategory) := has_limits_of_shape D pullback_category
   variables [K : has_pullbacks D]
   include K
 
   variables {d₁ d₂ d₃ x : D} (f : d₁ ⟶ d₃) (g : d₂ ⟶ d₃)
   definition pullback_object : D :=
-  limit_object (pullback_diagram_functor D f g)
+  limit_object (pullback_category_functor D f g)
 
-  definition pullback : pullback_object f g ⟶ d₁ :=
-  limit_morphism (pullback_diagram_functor D f g) TR
+  definition pullback : pullback_object f g ⟶ d₂ :=
+  limit_morphism (pullback_category_functor D f g) BL
 
-  definition pullback_rev : pullback_object f g ⟶ d₂ :=
-  limit_morphism (pullback_diagram_functor D f g) BL
+  definition pullback_rev : pullback_object f g ⟶ d₁ :=
+  limit_morphism (pullback_category_functor D f g) TR
 
-  theorem pullback_commutes : f ∘ pullback f g = g ∘ pullback_rev f g :=
-   limit_commute (pullback_diagram_functor D f g) (inl f1) ⬝
-  (limit_commute (pullback_diagram_functor D f g) (inl f2))⁻¹
+  theorem pullback_commutes : f ∘ pullback_rev f g = g ∘ pullback f g :=
+   limit_commute (pullback_category_functor D f g) (inl f1) ⬝
+  (limit_commute (pullback_category_functor D f g) (inl f2))⁻¹
 
   variables {f g}
   definition hom_pullback (h₁ : x ⟶ d₁) (h₂ : x ⟶ d₂) (p : f ∘ h₁ = g ∘ h₂)
     : x ⟶ pullback_object f g :=
-  hom_limit (pullback_diagram_functor D f g)
-            (pullback_diagram_ob.rec h₁ h₂ (g ∘ h₂))
+  hom_limit (pullback_category_functor D f g)
+            (pullback_category_ob.rec h₁ h₂ (g ∘ h₂))
             begin
               intro i₁ i₂ k; induction k with j j: induction j,
               exact p, reflexivity, apply id_left
             end
 
-  definition pullback_hom_pullback (h₁ : x ⟶ d₁) (h₂ : x ⟶ d₂) (p : f ∘ h₁ = g ∘ h₂)
-    : pullback f g ∘ hom_pullback h₁ h₂ p = h₁ :=
-  hom_limit_commute (pullback_diagram_functor D f g) (pullback_diagram_ob.rec h₁ h₂ (g ∘ h₂)) _ TR
+  theorem pullback_hom_pullback (h₁ : x ⟶ d₁) (h₂ : x ⟶ d₂) (p : f ∘ h₁ = g ∘ h₂)
+    : pullback f g ∘ hom_pullback h₁ h₂ p = h₂ :=
+  hom_limit_commute (pullback_category_functor D f g) (pullback_category_ob.rec h₁ h₂ (g ∘ h₂)) _ BL
 
-  definition pullback_rev_hom_pullback (h₁ : x ⟶ d₁) (h₂ : x ⟶ d₂) (p : f ∘ h₁ = g ∘ h₂)
-    : pullback_rev f g ∘ hom_pullback h₁ h₂ p = h₂ :=
-  hom_limit_commute (pullback_diagram_functor D f g) (pullback_diagram_ob.rec h₁ h₂ (g ∘ h₂)) _ BL
+  theorem pullback_rev_hom_pullback (h₁ : x ⟶ d₁) (h₂ : x ⟶ d₂) (p : f ∘ h₁ = g ∘ h₂)
+    : pullback_rev f g ∘ hom_pullback h₁ h₂ p = h₁ :=
+  hom_limit_commute (pullback_category_functor D f g) (pullback_category_ob.rec h₁ h₂ (g ∘ h₂)) _ TR
 
   theorem eq_hom_pullback {h₁ : x ⟶ d₁} {h₂ : x ⟶ d₂} (p : f ∘ h₁ = g ∘ h₂)
-    {k : x ⟶ pullback_object f g} (q : pullback f g ∘ k = h₁) (r : pullback_rev f g ∘ k = h₂)
+    {k : x ⟶ pullback_object f g} (q : pullback f g ∘ k = h₂) (r : pullback_rev f g ∘ k = h₁)
     : k = hom_pullback h₁ h₂ p :=
-  eq_hom_limit _ (pullback_diagram_ob.rec q r
+  eq_hom_limit _ (pullback_category_ob.rec r q
     begin
-      refine ap (λx, x ∘ k) (limit_commute (pullback_diagram_functor D f g) (inl f2))⁻¹ ⬝ _,
+      refine ap (λx, x ∘ k) (limit_commute (pullback_category_functor D f g) (inl f2))⁻¹ ⬝ _,
       refine !assoc⁻¹ ⬝ _,
-      exact ap (λx, _ ∘ x) r
+      exact ap (λx, _ ∘ x) q
     end)
 
   theorem pullback_cone_unique {h₁ : x ⟶ d₁} {h₂ : x ⟶ d₂} (p : f ∘ h₁ = g ∘ h₂)
-    {k₁ : x ⟶ pullback_object f g} (q₁ : pullback f g ∘ k₁ = h₁) (r₁ : pullback_rev f g ∘ k₁ = h₂)
-    {k₂ : x ⟶ pullback_object f g} (q₂ : pullback f g ∘ k₂ = h₁) (r₂ : pullback_rev f g ∘ k₂ = h₂)
+    {k₁ : x ⟶ pullback_object f g} (q₁ : pullback f g ∘ k₁ = h₂) (r₁ : pullback_rev f g ∘ k₁ = h₁)
+    {k₂ : x ⟶ pullback_object f g} (q₂ : pullback f g ∘ k₂ = h₂) (r₂ : pullback_rev f g ∘ k₂ = h₁)
     : k₁ = k₂ :=
   (eq_hom_pullback p q₁ r₁) ⬝ (eq_hom_pullback p q₂ r₂)⁻¹