diff --git a/hott/algebra/category/constructions/cone.hlean b/hott/algebra/category/constructions/cone.hlean
new file mode 100644
index 000000000..64d7dd96e
--- /dev/null
+++ b/hott/algebra/category/constructions/cone.hlean
@@ -0,0 +1,73 @@
+/-
+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
+
+Cones
+-/
+
+import ..nat_trans
+
+open functor nat_trans eq equiv is_trunc
+
+namespace category
+
+  structure cone_obj {I C : Precategory} (F : I ⇒ C) :=
+  (c : C)
+  (η : constant_functor I c ⟹ F)
+
+  local attribute cone_obj.c [coercion]
+
+  variables {I C : Precategory} {F : I ⇒ C} {x y z : cone_obj F}
+  structure cone_hom (x y : cone_obj F) :=
+  (f : x ⟶ y)
+  (p : Πi, cone_obj.η y i ∘ f = cone_obj.η x i)
+
+  local attribute cone_hom.f [coercion]
+
+  definition cone_id [constructor] (x : cone_obj F) : cone_hom x x :=
+  cone_hom.mk id
+              (λi, !id_right)
+
+  definition cone_comp [constructor] (g : cone_hom y z) (f : cone_hom x y) : cone_hom x z :=
+  cone_hom.mk (cone_hom.f g ∘ cone_hom.f f)
+              abstract λi, by rewrite [assoc, +cone_hom.p] end
+
+  definition is_hprop_hom_eq [instance] [priority 1001] {ob : Type} [C : precategory ob] {x y : ob} (f g : x ⟶ y)
+    : is_hprop (f = g) :=
+  _
+
+  theorem cone_hom_eq (f f' : cone_hom x y) (q : cone_hom.f f = cone_hom.f f') : f = f' :=
+  begin
+    induction f, induction f', esimp at *, induction q, apply ap (cone_hom.mk f),
+    apply @is_hprop.elim, apply pi.is_trunc_pi, intro x, apply is_trunc_eq, -- type class fails
+  end
+
+  variable (F)
+
+  definition precategory_cone [instance] [constructor] : precategory (cone_obj F) :=
+  @precategory.mk _ cone_hom
+                 abstract begin
+                   intro x y,
+                   assert H : cone_hom x y ≃ Σ(f : x ⟶ y), Πi, cone_obj.η y i ∘ f = cone_obj.η x i,
+                   { fapply equiv.MK,
+                     { intro f, induction f, constructor, assumption},
+                     { intro v, induction v, constructor, assumption},
+                     { intro v, induction v, reflexivity},
+                     { intro f, induction f, reflexivity}},
+                   apply is_trunc.is_trunc_equiv_closed_rev, exact H,
+                   fapply sigma.is_trunc_sigma, intros,
+                   apply is_trunc_succ, apply pi.is_trunc_pi, intros, esimp,
+                   /-exact _,-/ -- type class inference fails here
+                   apply is_trunc_eq,
+                 end end
+                 (λx y z, cone_comp)
+                 cone_id
+                 abstract begin intros, apply cone_hom_eq, esimp, apply assoc    end end
+                 abstract begin intros, apply cone_hom_eq, esimp, apply id_left  end end
+                 abstract begin intros, apply cone_hom_eq, esimp, apply id_right end end
+
+  definition cone [constructor] : Precategory :=
+  precategory.Mk (precategory_cone F)
+
+end category
diff --git a/hott/algebra/category/constructions/discrete.hlean b/hott/algebra/category/constructions/discrete.hlean
new file mode 100644
index 000000000..10d5a39eb
--- /dev/null
+++ b/hott/algebra/category/constructions/discrete.hlean
@@ -0,0 +1,58 @@
+/-
+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
+
+Discrete category
+-/
+
+import ..groupoid types.bool ..functor
+
+open eq is_trunc iso bool functor
+
+namespace category
+
+  definition precategory_of_1_type [constructor] (A : Type) [H : is_trunc 1 A] : precategory A :=
+  precategory.mk
+    (λ (a b : A), a = b)
+    (λ (a b c : A) (p : b = c) (q : a = b), q ⬝ p)
+    (λ (a : A), refl a)
+    (λ (a b c d : A) (p : c = d) (q : b = c) (r : a = b), con.assoc r q p)
+    (λ (a b : A) (p : a = b), con_idp p)
+    (λ (a b : A) (p : a = b), idp_con p)
+
+  definition groupoid_of_1_type [constructor] (A : Type) [H : is_trunc 1 A] : groupoid A :=
+  groupoid.mk !precategory_of_1_type
+              (λ (a b : A) (p : a = b), is_iso.mk !con.right_inv !con.left_inv)
+
+  definition Precategory_of_1_type [constructor] (A : Type) [H : is_trunc 1 A] : Precategory :=
+  precategory.Mk (precategory_of_1_type A)
+
+  definition Groupoid_of_1_type [constructor] (A : Type) [H : is_trunc 1 A] : Groupoid :=
+  groupoid.Mk _ (groupoid_of_1_type A)
+
+  definition discrete_precategory [constructor] (A : Type) [H : is_hset A] : precategory A :=
+  precategory_of_1_type A
+
+  definition discrete_groupoid [constructor] (A : Type) [H : is_hset A] : groupoid A :=
+  groupoid_of_1_type A
+
+  definition Discrete_precategory [constructor] (A : Type) [H : is_hset A] : Precategory :=
+  precategory.Mk (discrete_precategory A)
+
+  definition Discrete_groupoid [constructor] (A : Type) [H : is_hset A] : Groupoid :=
+  groupoid.Mk _ (discrete_groupoid A)
+
+  definition c2 [constructor] : Precategory := Discrete_precategory bool
+  definition c1 [constructor] : Precategory := Discrete_precategory unit
+
+  definition c2_functor [constructor] (C : Precategory) (x y : C) : c2 ⇒ C :=
+  functor.mk (bool.rec x y)
+             (bool.rec (bool.rec (λf, id) (by contradiction))
+                       (bool.rec (by contradiction) (λf, id)))
+             abstract (bool.rec idp idp) end
+             abstract begin intro b₁ b₂ b₃ g f, induction b₁: induction b₂: induction b₃:
+                            esimp at *: try contradiction: exact !id_id⁻¹ end end
+
+end category
diff --git a/hott/algebra/category/constructions/finite_cats.hlean b/hott/algebra/category/constructions/finite_cats.hlean
new file mode 100644
index 000000000..b83270f0f
--- /dev/null
+++ b/hott/algebra/category/constructions/finite_cats.hlean
@@ -0,0 +1,138 @@
+/-
+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
+
+Some finite categories which are neither discrete nor indiscrete
+-/
+
+import ..functor types.sum
+
+open bool unit is_trunc sum eq functor equiv
+
+namespace category
+
+  variables {A : Type} (R : A → A → Type) (H : Π⦃a b c⦄, R a b → R b c → empty)
+    [HR : Πa b, is_hset (R a b)] [HA : is_trunc 1 A]
+
+  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 :=
+  precategory.mk
+    (λa b, R a b ⊎ a = b)
+    begin
+      intros a b c g f, induction g with rg pg: induction f with rf pf,
+      { exfalso, exact H rf rg},
+      { exact inl (pf⁻¹ ▸ rg)},
+      { exact inl (pg ▸ rf)},
+      { exact inr (pf ⬝ pg)},
+    end
+    (λa, inr idp)
+    abstract begin
+      intros a b c d h g f, induction h with rh ph: induction g with rg pg: induction f with rf pf:
+      esimp: try induction pf; try induction pg; try induction ph: esimp;
+      try (exfalso; apply H;assumption;assumption)
+    end end
+    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_diagram_functor [constructor] (C : Precategory) (f : A → C)
+    (g : Π{a b} (r : R a b), f a ⟶ f b) : sparse_diagram R H ⇒ C :=
+  functor.mk f
+             (λa b, sum.rec g (eq.rec id))
+             (λa, idp)
+             abstract begin
+               intro a b c g f, induction g with rg pg: induction f with rf pf: esimp:
+               try induction pg: try induction pf: esimp,
+                 exfalso, exact H rf rg,
+                 exact !id_right⁻¹,
+                 exact !id_left⁻¹,
+                 exact !id_id⁻¹
+             end end
+
+  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
+
+  open equalizer_diagram_hom
+  theorem is_hset_equalizer_diagram_hom (b₁ b₂ : bool) : is_hset (equalizer_diagram_hom b₁ b₂) :=
+  begin
+    assert H : Πb b', equalizer_diagram_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},
+      { intro v, induction b: induction b': induction v: reflexivity},
+      { intro x, induction x: reflexivity}},
+    apply is_trunc_equiv_closed_rev, apply H,
+    induction b₁: induction b₂: exact _
+  end
+
+  local attribute is_hset_equalizer_diagram_hom [instance]
+  definition equalizer_diagram [constructor] : Precategory :=
+  sparse_diagram
+    equalizer_diagram_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
+    (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
+
+  theorem pullback_diagram_ob_decidable_equality : decidable_eq pullback_diagram_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_diagram_hom
+  theorem is_hset_pullback_diagram_hom (b₁ b₂ : pullback_diagram_ob)
+    : is_hset (pullback_diagram_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,
+    { intro b b', fapply equiv.MK,
+      { intro x, induction x: exact star},
+      { intro v, induction b: induction b': induction v, exact f1, exact f2},
+      { intro v, induction b: induction b': induction v: reflexivity},
+      { intro x, induction x: reflexivity}},
+    apply is_trunc_equiv_closed_rev, apply H,
+    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
+    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)
+    begin intro a b h; induction h, exact f, exact g end
+  end pullback
+
+end category
diff --git a/hott/algebra/category/constructions/product.hlean b/hott/algebra/category/constructions/product.hlean
index 98eb38a0d..31cfe6c38 100644
--- a/hott/algebra/category/constructions/product.hlean
+++ b/hott/algebra/category/constructions/product.hlean
@@ -6,9 +6,9 @@ Authors: Floris van Doorn, Jakob von Raumer
 Functor product precategory and (TODO) category
 -/
 
-import ..category ..functor
+import ..category ..functor hit.trunc
 
-open eq prod is_trunc functor
+open eq prod is_trunc functor sigma trunc
 
 namespace category
   definition precategory_prod [constructor] [reducible] {obC obD : Type}
@@ -27,12 +27,55 @@ namespace category
 
   infixr `×c`:30 := Precategory_prod
 
-  definition prod_functor [constructor] [reducible] {C C' D D' : Precategory}
+  definition pr1_functor [constructor] {C D : Precategory} : C ×c D ⇒ C :=
+  functor.mk pr1
+             (λa b, pr1)
+             (λa, idp)
+             (λa b c g f, idp)
+
+  definition pr2_functor [constructor] {C D : Precategory} : C ×c D ⇒ D :=
+  functor.mk pr2
+             (λa b, pr2)
+             (λa, idp)
+             (λa b c g f, idp)
+
+  definition functor_prod [constructor] [reducible] {C D X : Precategory}
+    (F : X ⇒ C) (G : X ⇒ D) : X ⇒ C ×c D :=
+  functor.mk (λ a,     pair (F a) (G a))
+             (λ a b f, pair (F f) (G f))
+             (λ a,         abstract pair_eq !respect_id   !respect_id   end)
+             (λ a b c g f, abstract pair_eq !respect_comp !respect_comp end)
+
+  definition pr1_functor_prod {C D X : Precategory} (F : X ⇒ C) (G : X ⇒ D)
+    : pr1_functor ∘f functor_prod F G = F :=
+  functor_eq (λx, idp)
+             (λx y f, !id_leftright)
+
+  definition pr2_functor_prod {C D X : Precategory} (F : X ⇒ C) (G : X ⇒ D)
+    : pr2_functor ∘f functor_prod F G = G :=
+  functor_eq (λx, idp)
+             (λx y f, !id_leftright)
+
+  -- definition universal_property_prod {C D X : Precategory} (F : X ⇒ C) (G : X ⇒ D)
+  --   : is_contr (Σ(H : X ⇒ C ×c D), pr1_functor ∘f H = F × pr2_functor ∘f H = G) :=
+  -- is_contr.mk
+  --   ⟨functor_prod F G, (pr1_functor_prod F G, pr2_functor_prod F G)⟩
+  --   begin
+  --     intro v, induction v with H w, induction w with p q,
+  --     symmetry, fapply sigma_eq: esimp,
+  --     { fapply functor_eq,
+  --       { intro x, apply prod_eq: esimp,
+  --         { exact ap010 to_fun_ob p x},
+  --         { exact ap010 to_fun_ob q x}},
+  --       { intro x y f, apply prod_eq: esimp,
+  --         { exact sorry},
+  --         { exact sorry}}},
+  --     { exact sorry}
+  --   end
+
+  definition prod_functor_prod [constructor] {C C' D D' : Precategory}
     (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)
-             (λ a b c g f, pair_eq !respect_comp !respect_comp)
+  functor_prod (F ∘f pr1_functor) (G ∘f pr2_functor)
 
   infixr `×f`:30 := prod_functor
 
diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean
index 88e78e03f..c3e5c1a40 100644
--- a/hott/algebra/category/functor.hlean
+++ b/hott/algebra/category/functor.hlean
@@ -46,6 +46,12 @@ namespace functor
   protected definition ID [reducible] [constructor] (C : Precategory) : functor C C := @functor.id C
   notation 1 := functor.id
 
+  definition constant_functor [constructor] (C : Precategory) {D : Precategory} (d : D) : C ⇒ D :=
+  functor.mk (λc, d)
+             (λc c' f, id)
+             (λc, idp)
+             (λa b c g f, !id_id⁻¹)
+
   definition functor_mk_eq' {F₁ F₂ : C → D} {H₁ : Π(a b : C), hom a b → hom (F₁ a) (F₁ b)}
     {H₂ : Π(a b : C), hom a b → hom (F₂ a) (F₂ b)} (id₁ id₂ comp₁ comp₂)
     (pF : F₁ = F₂) (pH : pF ▸ H₁ = H₂)
diff --git a/hott/algebra/category/groupoid.hlean b/hott/algebra/category/groupoid.hlean
index 5ee7ff5f3..13da43a5a 100644
--- a/hott/algebra/category/groupoid.hlean
+++ b/hott/algebra/category/groupoid.hlean
@@ -22,50 +22,7 @@ namespace category
     (H : Π (a b : ob) (f : a ⟶ b), is_iso f) : groupoid ob :=
   precategory.rec_on C groupoid.mk' H
 
-  definition precategory_of_1_type.{l} (A : Type.{l})
-      [H : is_trunc 1 A] : precategory.{l l} A :=
-  precategory.mk
-    (λ (a b : A), a = b)
-    (λ (a b c : A) (p : b = c) (q : a = b), q ⬝ p)
-    (λ (a : A), refl a)
-    (λ (a b c d : A) (p : c = d) (q : b = c) (r : a = b), con.assoc r q p)
-    (λ (a b : A) (p : a = b), con_idp p)
-    (λ (a b : A) (p : a = b), idp_con p)
-
-  definition groupoid_of_1_type.{l} (A : Type.{l})
-      [H : is_trunc 1 A] : groupoid.{l l} A :=
-  groupoid.mk !precategory_of_1_type
-              (λ (a b : A) (p : a = b), is_iso.mk !con.right_inv !con.left_inv)
-
-  -- A groupoid with a contractible carrier is a group
-  definition group_of_is_contr_groupoid {ob : Type} [H : is_contr ob]
-    [G : groupoid ob] : group (hom (center ob) (center ob)) :=
-  begin
-    fapply group.mk,
-      intro f g, apply (comp f g),
-      apply is_hset_hom,
-      intro f g h, apply (assoc f g h)⁻¹,
-      apply (ID (center ob)),
-      intro f, apply id_left,
-      intro f, apply id_right,
-      intro f, exact (iso.inverse f),
-      intro f, exact (iso.left_inverse f),
-  end
-
-  definition group_of_groupoid_unit [G : groupoid unit] : group (hom ⋆ ⋆) :=
-  begin
-    fapply group.mk,
-      intro f g, apply (comp f g),
-      apply is_hset_hom,
-      intro f g h, apply (assoc f g h)⁻¹,
-      apply (ID ⋆),
-      intro f, apply id_left,
-      intro f, apply id_right,
-      intro f, exact (iso.inverse f),
-      intro f, exact (iso.left_inverse f),
-  end
-
-  -- Conversely we can turn each group into a groupoid on the unit type
+  -- We can turn each group into a groupoid on the unit type
   definition groupoid_of_group.{l} (A : Type.{l}) [G : group A] : groupoid.{0 l} unit :=
   begin
     fapply groupoid.mk, fapply precategory.mk,
@@ -81,7 +38,7 @@ namespace category
         apply mul.right_inv,
   end
 
-  protected definition hom_group {A : Type} [G : groupoid A] (a : A) :
+  definition hom_group {A : Type} [G : groupoid A] (a : A) :
     group (hom a a) :=
   begin
     fapply group.mk,
@@ -95,6 +52,10 @@ namespace category
       intro f, exact (iso.left_inverse f),
   end
 
+  definition group_of_is_contr_groupoid {ob : Type} [H : is_contr ob]
+    [G : groupoid ob] : group (hom (center ob) (center ob)) := !hom_group
+  definition group_of_groupoid_unit [G : groupoid unit] : group (hom ⋆ ⋆) := !hom_group
+
   -- Bundled version of categories
   -- we don't use Groupoid.carrier explicitly, but rather use Groupoid.carrier (to_Precategory C)
   structure Groupoid : Type :=
diff --git a/hott/algebra/category/limits.hlean b/hott/algebra/category/limits.hlean
new file mode 100644
index 000000000..3ca550e4a
--- /dev/null
+++ b/hott/algebra/category/limits.hlean
@@ -0,0 +1,301 @@
+/-
+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
+
+Limits in a category
+-/
+
+import .constructions.cone .groupoid .constructions.discrete .constructions.product
+       .constructions.finite_cats
+
+open is_trunc functor nat_trans eq
+
+namespace category
+
+  variables {ob : Type} [C : precategory ob] {c c' : ob} (D I : Precategory)
+  include C
+
+  definition is_terminal [class] (c : ob) := Πd, is_contr (d ⟶ c)
+  definition is_contr_of_is_terminal [instance] (c d : ob) [H : is_terminal d]
+    : is_contr (c ⟶ d) :=
+  H c
+
+  definition terminal_morphism (c c' : ob) [H : is_terminal c'] : c ⟶ c' :=
+  !center
+
+  definition hom_terminal_eq [H : is_terminal c'] (f f' : c ⟶ c') : f = f' :=
+  !is_hprop.elim
+
+  definition eq_terminal_morphism [H : is_terminal c'] (f : c ⟶ c') : f = terminal_morphism c c' :=
+  !is_hprop.elim
+
+  definition terminal_iso_terminal {c c' : ob} (H : is_terminal c) (K : is_terminal c') : c ≅ c' :=
+  iso.MK !terminal_morphism !terminal_morphism !hom_terminal_eq !hom_terminal_eq
+
+  omit C
+
+  structure has_terminal_object [class] (D : Precategory) :=
+    (d : D)
+    (is_term : is_terminal d)
+
+  abbreviation terminal_object [constructor] := @has_terminal_object.d
+  attribute has_terminal_object.is_term [instance]
+
+  definition terminal_object_iso_terminal_object (H₁ H₂ : has_terminal_object D)
+    : @terminal_object D H₁ ≅ @terminal_object D H₂ :=
+  terminal_iso_terminal (@has_terminal_object.is_term D H₁) (@has_terminal_object.is_term D H₂)
+
+  definition has_limits_of_shape [class] := Π(F : I ⇒ D), has_terminal_object (cone F)
+
+  variables {I D}
+  definition has_terminal_object_of_has_limits_of_shape [instance] [H : has_limits_of_shape D I]
+    (F : I ⇒ D) : has_terminal_object (cone F) :=
+  H F
+
+  variables (F : I ⇒ D) [H : has_limits_of_shape D I] {i j : I}
+  include H
+
+  definition limit_cone : cone F := !terminal_object
+
+  definition is_terminal_limit_cone [instance] : is_terminal (limit_cone F) :=
+  has_terminal_object.is_term _
+
+  definition limit_object : D :=
+  cone_obj.c (limit_cone F)
+
+  definition limit_nat_trans : constant_functor I (limit_object F) ⟹ F :=
+  cone_obj.η (limit_cone F)
+
+  definition limit_morphism (i : I) : limit_object F ⟶ F i :=
+  limit_nat_trans F i
+
+  variable {H}
+  theorem limit_commute {i j : I} (f : i ⟶ j)
+    : to_fun_hom F f ∘ limit_morphism F i = limit_morphism F j :=
+  naturality (limit_nat_trans F) f ⬝ !id_right
+
+  variable [H]
+  definition limit_cone_obj [constructor] {d : D} {η : Πi, d ⟶ F i}
+    (p : Π⦃i j : I⦄ (f : i ⟶ j), to_fun_hom F f ∘ η i = η j) : cone_obj F :=
+  cone_obj.mk d (nat_trans.mk η (λa b f, p f ⬝ !id_right⁻¹))
+
+  variable {H}
+  definition hom_limit {d : D} (η : Πi, d ⟶ F i)
+    (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)
+    (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
+
+  definition limit_cone_hom [constructor] {d : D} {η : Πi, d ⟶ F i}
+    (p : Π⦃i j : I⦄ (f : i ⟶ j), to_fun_hom F f ∘ η i = η j) {h : d ⟶ limit_object F}
+    (q : Πi, limit_morphism F i ∘ h = η i) : cone_hom (limit_cone_obj F p) (limit_cone F) :=
+  cone_hom.mk h q
+
+  variable {F}
+  theorem eq_hom_limit {d : D} {η : Πi, d ⟶ F i}
+    (p : Π⦃i j : I⦄ (f : i ⟶ j), to_fun_hom F f ∘ η i = η j) {h : d ⟶ limit_object F}
+    (q : Πi, limit_morphism F i ∘ h = η i) : h = hom_limit F η p :=
+  ap cone_hom.f (@eq_terminal_morphism _ _ _ _ (is_terminal_limit_cone _) (limit_cone_hom F p q))
+
+  theorem limit_cone_unique {d : D} {η : Πi, d ⟶ F i}
+    (p : Π⦃i j : I⦄ (f : i ⟶ j), to_fun_hom F f ∘ η i = η j)
+    {h₁ : d ⟶ limit_object F} (q₁ : Πi, limit_morphism F i ∘ h₁ = η i)
+    {h₂ : d ⟶ limit_object F} (q₂ : Πi, limit_morphism F i ∘ h₂ = η i): h₁ = h₂ :=
+  eq_hom_limit p q₁ ⬝ (eq_hom_limit p q₂)⁻¹
+
+  omit H
+
+-- notation `noinstances` t:max := by+ with_options [elaborator.ignore_instances true] (exact t)
+-- definition noinstance (t : tactic) : tactic := with_options [elaborator.ignore_instances true] t
+
+  variable (F)
+  definition limit_object_iso_limit_object [constructor] (H₁ H₂ : has_limits_of_shape D I) :
+    @(limit_object F) H₁ ≅ @(limit_object F) H₂ :=
+  begin
+    fapply iso.MK,
+    { apply hom_limit, apply @(limit_commute F) H₁},
+    { apply @(hom_limit F) H₁, apply limit_commute},
+    { exact abstract begin fapply limit_cone_unique,
+      { apply limit_commute},
+      { intro i, rewrite [assoc, hom_limit_commute], apply hom_limit_commute},
+      { intro i, apply id_right} end end},
+    { exact abstract begin fapply limit_cone_unique,
+      { apply limit_commute},
+      { intro i, rewrite [assoc, hom_limit_commute], apply hom_limit_commute},
+      { intro i, apply id_right} end end}
+  end
+
+  section bin_products
+  open bool prod.ops
+  definition has_binary_products [reducible] (D : Precategory) := has_limits_of_shape D c2
+  variables [K : has_binary_products D] (d d' : D)
+  include K
+
+  definition product_object : D :=
+  limit_object (c2_functor D d d')
+
+  infixr × := product_object
+
+  definition pr1 : d × d' ⟶ d :=
+  limit_morphism (c2_functor D d d') ff
+
+  definition pr2 : d × d' ⟶ d' :=
+  limit_morphism (c2_functor D d d') tt
+
+  variables {d d'}
+  definition hom_product {x : D} (f : x ⟶ d) (g : x ⟶ d') : x ⟶ d × d' :=
+  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 :=
+  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 :=
+  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'}
+    (p : !pr1 ∘ h = f) (q : !pr2 ∘ h = g) : h = hom_product f g :=
+  eq_hom_limit _ (bool.rec p q)
+
+  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₂ :=
+  eq_hom_product p₁ q₁ ⬝ (eq_hom_product p₂ q₂)⁻¹
+
+  variable (D)
+  definition product_functor [constructor] : D ×c D ⇒ D :=
+  functor.mk
+    (λx, product_object x.1 x.2)
+    (λx y f, hom_product (f.1 ∘ !pr1) (f.2 ∘ !pr2))
+    abstract begin intro x, symmetry, apply eq_hom_product: apply comp_id_eq_id_comp end end
+    abstract begin intro x y z g f, symmetry, apply eq_hom_product,
+                   rewrite [assoc,pr1_hom_product,-assoc,pr1_hom_product,assoc],
+                   rewrite [assoc,pr2_hom_product,-assoc,pr2_hom_product,assoc] end end
+  omit K
+  variables {D} (d d')
+
+  definition product_object_iso_product_object [constructor] (H₁ H₂ : has_binary_products D) :
+    @product_object D H₁ d d' ≅ @product_object D H₂ d d' :=
+  limit_object_iso_limit_object _ H₁ H₂
+
+  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
+  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)
+
+  definition equalizer : equalizer_object f g ⟶ d :=
+  limit_morphism (equalizer_diagram_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))⁻¹
+
+  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)
+            (bool.rec h (g ∘ h))
+            begin
+              intro b₁ b₂ i; induction i with j j: induction j,
+              -- report(?) "esimp" is super slow here
+              exact p, reflexivity, apply id_left
+            end
+
+  definition 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
+
+  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 !assoc⁻¹ ⬝ _,
+      exact ap (λx, _ ∘ x) q
+    end)
+
+  theorem equalizer_cone_unique {h : x ⟶ d} (p : f ∘ h = g ∘ h)
+    {i₁ : x ⟶ equalizer_object f g} (q₁ : equalizer f g ∘ i₁ = h)
+    {i₂ : x ⟶ equalizer_object f g} (q₂ : equalizer f g ∘ i₂ = h) : i₁ = i₂ :=
+  eq_hom_equalizer p q₁ ⬝ (eq_hom_equalizer p q₂)⁻¹
+
+  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 :=
+  limit_object_iso_limit_object _ H₁ H₂
+
+  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
+  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)
+
+  definition pullback : pullback_object f g ⟶ d₁ :=
+  limit_morphism (pullback_diagram_functor D f g) TR
+
+  definition pullback_rev : pullback_object f g ⟶ d₂ :=
+  limit_morphism (pullback_diagram_functor D f g) BL
+
+  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))⁻¹
+
+  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₂))
+            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
+
+  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 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 = hom_pullback h₁ h₂ p :=
+  eq_hom_limit _ (pullback_diagram_ob.rec q r
+    begin
+      refine ap (λx, x ∘ k) (limit_commute (pullback_diagram_functor D f g) (inl f2))⁻¹ ⬝ _,
+      refine !assoc⁻¹ ⬝ _,
+      exact ap (λx, _ ∘ x) r
+    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₁ = k₂ :=
+  (eq_hom_pullback p q₁ r₁) ⬝ (eq_hom_pullback p q₂ r₂)⁻¹
+
+  variables (f g)
+  definition pullback_object_iso_pullback_object [constructor] (H₁ H₂ : has_pullbacks D) :
+    @pullback_object D H₁ _ _ _ f g ≅ @pullback_object D H₂ _ _ _ f g :=
+  limit_object_iso_limit_object _ H₁ H₂
+
+  end pullbacks
+
+end category
diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean
index 67a7091e2..8fab27eba 100644
--- a/hott/algebra/category/precategory.hlean
+++ b/hott/algebra/category/precategory.hlean
@@ -71,6 +71,7 @@ namespace category
 
     definition id_leftright       (f : hom a b) : id ∘ f ∘ id = f := !id_left ⬝ !id_right
     definition comp_id_eq_id_comp (f : hom a b) : f ∘ id = id ∘ f := !id_right ⬝ !id_left⁻¹
+    definition id_comp_eq_comp_id (f : hom a b) : id ∘ f = f ∘ id := !id_left ⬝ !id_right⁻¹
 
     definition left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id :=
     calc i = i ∘ id : by rewrite id_right
@@ -142,7 +143,7 @@ namespace category
 
   definition precategory.Mk [reducible] [constructor] {ob} (C) : Precategory := Precategory.mk ob C
   definition precategory.MK [reducible] [constructor] (a b c d e f g h) : Precategory :=
-  Precategory.mk a (@precategory.mk _ b c d e f g h)
+  Precategory.mk a (@precategory.mk a b c d e f g h)
 
   abbreviation carrier := @Precategory.carrier
 
diff --git a/hott/types/bool.hlean b/hott/types/bool.hlean
index 941672e55..1532cf2d9 100644
--- a/hott/types/bool.hlean
+++ b/hott/types/bool.hlean
@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 Theorems about the booleans
 -/
 
-open is_equiv eq equiv function is_trunc option unit
+open is_equiv eq equiv function is_trunc option unit decidable
 
 namespace bool
 
@@ -42,4 +42,11 @@ namespace bool
     { intro u, cases u with u, reflexivity, cases u, reflexivity},
     { intro b, cases b, reflexivity, reflexivity},
   end
+
+  protected definition has_decidable_eq [instance] : ∀ x y : bool, decidable (x = y)
+  | has_decidable_eq ff ff := inl rfl
+  | has_decidable_eq ff tt := inr (by contradiction)
+  | has_decidable_eq tt ff := inr (by contradiction)
+  | has_decidable_eq tt tt := inl rfl
+
 end bool