diff --git a/hott/algebra/category/category.md b/hott/algebra/category/category.md
index 9006089a5..39d311a54 100644
--- a/hott/algebra/category/category.md
+++ b/hott/algebra/category/category.md
@@ -11,6 +11,4 @@ Development of Category Theory. The following files are in this folder (sorted s
 * [strict](strict.hlean) : Strict categories
 * [nat_trans](nat_trans.hlean) : Natural transformations
 * [constructions](constructions/constructions.md) (subfolder) : basic constructions on categories and examples of categories
-* [limits](limits.hlean) : Limits in a category, defined as terminal object in the cone category
-* [colimits](colimits.hlean) : Colimits in a category, defined as the limit of the opposite functor
-* [yoneda](yoneda.hlean) : Yoneda Embedding (WIP)
+* [limits](limits/limits.md) (subfolder) : Limits and colimits in precategories
diff --git a/hott/algebra/category/constructions/constructions.md b/hott/algebra/category/constructions/constructions.md
index 77df95b45..56c067e6d 100644
--- a/hott/algebra/category/constructions/constructions.md
+++ b/hott/algebra/category/constructions/constructions.md
@@ -5,7 +5,7 @@ Common categories and constructions on categories. The following files are in th
 
 * [functor](functor.hlean) : Functor category
 * [opposite](opposite.hlean) : Opposite category
-* [hset](hset.hlean) : Category of sets. Includes proof that it is complete and cocomplete
+* [set](set.hlean) : Category of sets
 * [sum](sum.hlean) : Sum category
 * [product](product.hlean) : Product category
 * [comma](comma.hlean) : Comma category
@@ -18,6 +18,3 @@ Discrete, indiscrete or finite categories:
 * [indiscrete](indiscrete.hlean)
 * [terminal](terminal.hlean)
 * [initial](initial.hlean)
-
-Non-basic topics:
-* [functor2](functor2.hlean) : showing that the functor category has (co)limits if the codomain has them.
diff --git a/hott/algebra/category/constructions/default.hlean b/hott/algebra/category/constructions/default.hlean
index ec7444404..c8d65bd74 100644
--- a/hott/algebra/category/constructions/default.hlean
+++ b/hott/algebra/category/constructions/default.hlean
@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn
 -/
 
-import .functor .hset .opposite .product .comma
+import .functor .set .opposite .product .comma .sum .discrete .indiscrete .terminal .initial
diff --git a/hott/algebra/category/constructions/product.hlean b/hott/algebra/category/constructions/product.hlean
index 9851e60c0..cef0b9911 100644
--- a/hott/algebra/category/constructions/product.hlean
+++ b/hott/algebra/category/constructions/product.hlean
@@ -123,6 +123,8 @@ namespace category
     { intro c c' f, apply prod_eq: esimp:apply naturality}
   end
 
+  infixr ` ×n `:70 := prod_nat_trans
+
   definition prod_flip_functor [constructor] (C D : Precategory) : C ×c D ⇒ D ×c C :=
   functor.mk (λp, (p.2, p.1))
              (λp p' h, (h.2, h.1))
diff --git a/hott/algebra/category/constructions/set.hlean b/hott/algebra/category/constructions/set.hlean
new file mode 100644
index 000000000..5eaaff5e9
--- /dev/null
+++ b/hott/algebra/category/constructions/set.hlean
@@ -0,0 +1,103 @@
+/-
+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, Jakob von Raumer
+
+Category of sets
+-/
+
+import ..functor.basic ..category types.equiv types.lift
+
+open eq category equiv iso is_equiv is_trunc function sigma
+
+namespace category
+
+  definition precategory_hset.{u} [reducible] [constructor] : precategory hset.{u} :=
+  precategory.mk (λx y : hset, x → y)
+                 (λx y z g f a, g (f a))
+                 (λx a, a)
+                 (λx y z w h g f, eq_of_homotopy (λa, idp))
+                 (λx y f, eq_of_homotopy (λa, idp))
+                 (λx y f, eq_of_homotopy (λa, idp))
+
+  definition Precategory_hset [reducible] [constructor] : Precategory :=
+  Precategory.mk hset precategory_hset
+
+  abbreviation set [constructor] := Precategory_hset
+
+  namespace set
+    local attribute is_equiv_subtype_eq [instance]
+    definition iso_of_equiv [constructor] {A B : set} (f : A ≃ B) : A ≅ B :=
+    iso.MK (to_fun f)
+           (to_inv f)
+           (eq_of_homotopy (left_inv (to_fun f)))
+           (eq_of_homotopy (right_inv (to_fun f)))
+
+    definition equiv_of_iso [constructor] {A B : set} (f : A ≅ B) : A ≃ B :=
+    begin
+      apply equiv.MK (to_hom f) (iso.to_inv f),
+        exact ap10 (to_right_inverse f),
+        exact ap10 (to_left_inverse f)
+    end
+
+    definition is_equiv_iso_of_equiv [constructor] (A B : set)
+      : is_equiv (@iso_of_equiv A B) :=
+    adjointify _ (λf, equiv_of_iso f)
+                 (λf, proof iso_eq idp qed)
+                 (λf, equiv_eq idp)
+
+    local attribute is_equiv_iso_of_equiv [instance]
+
+    definition iso_of_eq_eq_compose (A B : hset) : @iso_of_eq _ _ A B =
+      @iso_of_equiv A B ∘ @equiv_of_eq A B ∘ subtype_eq_inv _ _ ∘
+      @ap _ _ (to_fun (trunctype.sigma_char 0)) A B :=
+    eq_of_homotopy (λp, eq.rec_on p idp)
+
+    definition equiv_equiv_iso (A B : set) : (A ≃ B) ≃ (A ≅ B) :=
+    equiv.MK (λf, iso_of_equiv f)
+             (λf, proof equiv.MK (to_hom f)
+                           (iso.to_inv f)
+                           (ap10 (to_right_inverse f))
+                           (ap10 (to_left_inverse  f)) qed)
+             (λf, proof iso_eq idp qed)
+             (λf, proof equiv_eq idp qed)
+
+    definition equiv_eq_iso (A B : set) : (A ≃ B) = (A ≅ B) :=
+    ua !equiv_equiv_iso
+
+    definition is_univalent_hset (A B : set) : is_equiv (iso_of_eq : A = B → A ≅ B) :=
+    assert H₁ : is_equiv (@iso_of_equiv A B ∘ @equiv_of_eq A B ∘ subtype_eq_inv _ _ ∘
+                  @ap _ _ (to_fun (trunctype.sigma_char 0)) A B), from
+      @is_equiv_compose _ _ _ _ _
+      (@is_equiv_compose _ _ _ _ _
+         (@is_equiv_compose _ _ _ _ _
+           _
+           (@is_equiv_subtype_eq_inv _ _ _ _ _))
+         !univalence)
+       !is_equiv_iso_of_equiv,
+    let H₂ := (iso_of_eq_eq_compose A B)⁻¹ in
+    begin
+      rewrite H₂ at H₁,
+      assumption
+    end
+  end set
+
+  definition category_hset [instance] [constructor] [reducible] : category hset :=
+  category.mk precategory_hset set.is_univalent_hset
+
+  definition Category_hset [reducible] [constructor] : Category :=
+  Category.mk hset category_hset
+
+  abbreviation cset [constructor] := Category_hset
+
+  open functor lift
+  definition lift_functor.{u v} [constructor] : set.{u} ⇒ set.{max u v} :=
+  functor.mk tlift
+             (λa b, lift_functor)
+             (λa, eq_of_homotopy (λx, by induction x; reflexivity))
+             (λa b c g f, eq_of_homotopy (λx, by induction x; reflexivity))
+
+  open pi sigma.ops
+
+
+end category
diff --git a/hott/algebra/category/constructions/sum.hlean b/hott/algebra/category/constructions/sum.hlean
index ee2771dbc..9af9b5130 100644
--- a/hott/algebra/category/constructions/sum.hlean
+++ b/hott/algebra/category/constructions/sum.hlean
@@ -107,6 +107,6 @@ namespace category
     { intro a b f, induction a: induction b: esimp at *; induction f with f; esimp;
       try contradiction: apply naturality}
   end
-
+  infixr ` +n `:65 := sum_nat_trans
 
 end category
diff --git a/hott/algebra/category/functor/adjoint2.hlean b/hott/algebra/category/functor/adjoint2.hlean
index 3c0ff5bf0..1a2e32da6 100644
--- a/hott/algebra/category/functor/adjoint2.hlean
+++ b/hott/algebra/category/functor/adjoint2.hlean
@@ -3,12 +3,12 @@ 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
 
-TODO: move
+TODO: merge with adjoint
 -/
 
-import .adjoint ..yoneda
+import .adjoint .examples
 
-open eq functor nat_trans yoneda iso prod is_trunc
+open eq functor nat_trans iso prod is_trunc
 
 namespace category
 
diff --git a/hott/algebra/category/functor/curry.hlean b/hott/algebra/category/functor/curry.hlean
index 31352df7c..9ada0b4ca 100644
--- a/hott/algebra/category/functor/curry.hlean
+++ b/hott/algebra/category/functor/curry.hlean
@@ -5,173 +5,3 @@ Authors: Floris van Doorn
 
 Definition of currying and uncurrying of functors
 -/
-
-import ..constructions.functor ..constructions.product
-
-open category prod nat_trans eq prod.ops iso equiv
-
-namespace functor
-
-  variables {C D E : Precategory} (F F' : C ×c D ⇒ E) (G G' : C ⇒ E ^c D)
-  definition functor_curry_ob [reducible] [constructor] (c : C) : E ^c D :=
-  functor.mk (λd, F (c,d))
-             (λd d' g, F (id, g))
-             (λd, !respect_id)
-             (λd₁ d₂ d₃ g' g, calc
-               F (id, g' ∘ g) = F (id ∘ id, g' ∘ g) : by rewrite id_id
-                 ... = F ((id,g') ∘ (id, g))        : by esimp
-                 ... = F (id,g') ∘ F (id, g)        : by rewrite respect_comp)
-
-  definition functor_curry_hom [constructor] ⦃c c' : C⦄ (f : c ⟶ c')
-    : functor_curry_ob F c ⟹ functor_curry_ob F c' :=
-  begin
-    fapply nat_trans.mk,
-      {intro d, exact F (f, id)},
-      {intro d d' g, calc
-        F (id, g) ∘ F (f, id) = F (id ∘ f, g ∘ id) : respect_comp F
-                   ... = F (f, g ∘ id)         : by rewrite id_left
-                   ... = F (f, g)              : by rewrite id_right
-                   ... = F (f ∘ id, g)         : by rewrite id_right
-                   ... = F (f ∘ id, id ∘ g)    : by rewrite id_left
-                   ... = F (f, id) ∘ F (id, g) : (respect_comp F (f, id) (id, g))⁻¹ᵖ
-        }
-  end
-  local abbreviation Fhom [constructor] := @functor_curry_hom
-
-  theorem functor_curry_hom_def ⦃c c' : C⦄ (f : c ⟶ c') (d : D) :
-    (Fhom F f) d = to_fun_hom F (f, id) := idp
-
-  theorem functor_curry_id (c : C) : Fhom F (ID c) = nat_trans.id :=
-  nat_trans_eq (λd, respect_id F _)
-
-  theorem functor_curry_comp ⦃c c' c'' : C⦄ (f' : c' ⟶ c'') (f : c ⟶ c')
-    : Fhom F (f' ∘ f) = Fhom F f' ∘n Fhom F f :=
-  begin
-    apply @nat_trans_eq,
-    intro d, calc
-    natural_map (Fhom F (f' ∘ f)) d = F (f' ∘ f, id) : by rewrite functor_curry_hom_def
-      ... = F (f' ∘ f, id ∘ id)                      : by rewrite id_id
-      ... = F ((f',id) ∘ (f, id))                    : by esimp
-      ... = F (f',id) ∘ F (f, id)                    : by rewrite [respect_comp F]
-      ... = natural_map ((Fhom F f') ∘ (Fhom F f)) d : by esimp
-  end
-
-  definition functor_curry [reducible] [constructor] : C ⇒ E ^c D :=
-  functor.mk (functor_curry_ob F)
-             (functor_curry_hom F)
-             (functor_curry_id F)
-             (functor_curry_comp F)
-
-  definition functor_uncurry_ob [reducible] (p : C ×c D) : E :=
-  to_fun_ob (G p.1) p.2
-
-  definition functor_uncurry_hom ⦃p p' : C ×c D⦄ (f : hom p p')
-    : functor_uncurry_ob G p ⟶ functor_uncurry_ob G p'  :=
-  to_fun_hom (to_fun_ob G p'.1) f.2 ∘ natural_map (to_fun_hom G f.1) p.2
-  local abbreviation Ghom := @functor_uncurry_hom
-
-  theorem functor_uncurry_id (p : C ×c D) : Ghom G (ID p) = id :=
-  calc
-    Ghom G (ID p) = to_fun_hom (to_fun_ob G p.1) id ∘ natural_map (to_fun_hom G id) p.2 : by esimp
-      ... = id ∘ natural_map (to_fun_hom G id) p.2 : by rewrite respect_id
-      ... = id ∘ natural_map nat_trans.id p.2      : by rewrite respect_id
-      ... = id                                     : id_id
-
-  theorem functor_uncurry_comp ⦃p p' p'' : C ×c D⦄ (f' : p' ⟶ p'') (f : p ⟶ p')
-    : Ghom G (f' ∘ f) = Ghom G f' ∘ Ghom G f :=
-  calc
-    Ghom G (f' ∘ f)
-          = to_fun_hom (to_fun_ob G p''.1) (f'.2 ∘ f.2) ∘ natural_map (to_fun_hom G (f'.1 ∘ f.1)) p.2 : by esimp
-      ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2)
-              ∘ natural_map (to_fun_hom G (f'.1 ∘ f.1)) p.2                : by rewrite respect_comp
-      ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2)
-              ∘ natural_map (to_fun_hom G f'.1 ∘ to_fun_hom G f.1) p.2     : by rewrite respect_comp
-      ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2)
-             ∘ (natural_map (to_fun_hom G f'.1) p.2 ∘ natural_map (to_fun_hom G f.1) p.2) : by esimp
-      ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ natural_map (to_fun_hom G f'.1) p'.2)
-              ∘ (to_fun_hom (to_fun_ob G p'.1) f.2 ∘ natural_map (to_fun_hom G f.1) p.2) :
-                  by rewrite [square_prepostcompose (!naturality⁻¹ᵖ) _ _]
-      ... = Ghom G f' ∘ Ghom G f : by esimp
-
-  definition functor_uncurry [reducible] [constructor] : C ×c D ⇒ E :=
-  functor.mk (functor_uncurry_ob G)
-             (functor_uncurry_hom G)
-             (functor_uncurry_id G)
-             (functor_uncurry_comp G)
-
-  theorem functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F :=
-  functor_eq (λp, ap (to_fun_ob F) !prod.eta)
-  begin
-    intro cd cd' fg,
-    cases cd with c d, cases cd' with c' d', cases fg with f g,
-    transitivity to_fun_hom (functor_uncurry (functor_curry F)) (f, g),
-    apply id_leftright,
-    show (functor_uncurry (functor_curry F)) (f, g) = F (f,g),
-      from calc
-        (functor_uncurry (functor_curry F)) (f, g) = to_fun_hom F (id, g) ∘ to_fun_hom F (f, id) : by esimp
-          ... = F (id ∘ f, g ∘ id) : by krewrite [-respect_comp F (id,g) (f,id)]
-          ... = F (f, g ∘ id)      : by rewrite id_left
-          ... = F (f,g)            : by rewrite id_right,
-  end
-
-  definition functor_curry_functor_uncurry_ob (c : C)
-    : functor_curry (functor_uncurry G) c = G c :=
-  begin
-  fapply functor_eq,
-   { intro d, reflexivity},
-   { intro d d' g, refine !id_leftright ⬝ _, esimp,
-     rewrite [▸*, ↑functor_uncurry_hom, respect_id, ▸*, id_right]}
-  end
-
-  theorem functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G :=
-  begin
-  fapply functor_eq, exact (functor_curry_functor_uncurry_ob G),
-  intro c c' f,
-  fapply nat_trans_eq,
-  intro d,
-  apply concat,
-    {apply (ap (λx, x ∘ _)),
-      apply concat, apply natural_map_hom_of_eq, apply (ap hom_of_eq), apply ap010_functor_eq},
-  apply concat,
-     {apply (ap (λx, _ ∘ x)), apply (ap (λx, _ ∘ x)),
-       apply concat, apply natural_map_inv_of_eq,
-       apply (ap (λx, hom_of_eq x⁻¹)), apply ap010_functor_eq},
-  apply concat, apply id_leftright,
-  apply concat, apply (ap (λx, x ∘ _)), apply respect_id,
-  apply id_left
-  end
-
-  definition prod_functor_equiv_functor_functor [constructor] (C D E : Precategory)
-    : (C ×c D ⇒ E) ≃ (C ⇒ E ^c D) :=
-  equiv.MK functor_curry
-           functor_uncurry
-           functor_curry_functor_uncurry
-           functor_uncurry_functor_curry
-
-  variables {F F' G G'}
-  definition nat_trans_curry_nat [constructor] (η : F ⟹ F') (c : C)
-    : functor_curry_ob F c ⟹ functor_curry_ob F' c :=
-  begin
-    fapply nat_trans.mk: esimp,
-    { intro d, exact η (c, d)},
-    { intro d d' f, apply naturality}
-  end
-
-  definition nat_trans_curry [constructor] (η : F ⟹ F')
-    : functor_curry F ⟹ functor_curry F' :=
-  begin
-    fapply nat_trans.mk: esimp,
-    { exact nat_trans_curry_nat η},
-    { intro c c' f, apply nat_trans_eq, intro d, esimp, apply naturality}
-  end
-
-  definition nat_trans_uncurry [constructor] (η : G ⟹ G')
-    : functor_uncurry G ⟹ functor_uncurry G' :=
-  begin
-    fapply nat_trans.mk: esimp,
-    { intro v, unfold functor_uncurry_ob, exact (η v.1) v.2},
-    { intro v w f, unfold functor_uncurry_hom,
-      rewrite [-assoc, ap010 natural_map (naturality η f.1) v.2, assoc, naturality, -assoc]}
-  end
-
-end functor
diff --git a/hott/algebra/category/functor/examples.hlean b/hott/algebra/category/functor/examples.hlean
new file mode 100644
index 000000000..abcee40dc
--- /dev/null
+++ b/hott/algebra/category/functor/examples.hlean
@@ -0,0 +1,208 @@
+/-
+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
+
+Definition of functors involving at least two different constructions of categories
+-/
+
+import ..constructions.functor ..constructions.product ..constructions.opposite
+       ..constructions.set
+
+open category nat_trans eq prod prod.ops
+
+namespace functor
+
+  section
+  open iso equiv
+  variables {C D E : Precategory} (F F' : C ×c D ⇒ E) (G G' : C ⇒ E ^c D)
+  /- currying a functor -/
+  definition functor_curry_ob [reducible] [constructor] (c : C) : D ⇒ E :=
+  F ∘f (constant_functor D c ×f 1)
+
+  definition functor_curry_hom [constructor] ⦃c c' : C⦄ (f : c ⟶ c')
+    : functor_curry_ob F c ⟹ functor_curry_ob F c' :=
+  F ∘fn (constant_nat_trans D f ×n 1)
+
+  local abbreviation Fhom [constructor] := @functor_curry_hom
+
+  theorem functor_curry_id (c : C) : Fhom F (ID c) = nat_trans.id :=
+  nat_trans_eq (λd, respect_id F _)
+
+  theorem functor_curry_comp ⦃c c' c'' : C⦄ (f' : c' ⟶ c'') (f : c ⟶ c')
+    : Fhom F (f' ∘ f) = Fhom F f' ∘n Fhom F f :=
+  begin
+    apply @nat_trans_eq,
+    intro d, calc
+    natural_map (Fhom F (f' ∘ f)) d = F (f' ∘ f, id) : by esimp
+      ... = F (f' ∘ f, id ∘ id)                      : by rewrite id_id
+      ... = F ((f',id) ∘ (f, id))                    : by esimp
+      ... = F (f',id) ∘ F (f, id)                    : by rewrite [respect_comp F]
+      ... = natural_map ((Fhom F f') ∘ (Fhom F f)) d : by esimp
+  end
+
+  definition functor_curry [reducible] [constructor] : C ⇒ E ^c D :=
+  functor.mk (functor_curry_ob F)
+             (functor_curry_hom F)
+             (functor_curry_id F)
+             (functor_curry_comp F)
+
+  /- uncurrying a functor -/
+
+  definition functor_uncurry_ob [reducible] (p : C ×c D) : E :=
+  to_fun_ob (G p.1) p.2
+
+  definition functor_uncurry_hom ⦃p p' : C ×c D⦄ (f : hom p p')
+    : functor_uncurry_ob G p ⟶ functor_uncurry_ob G p'  :=
+  to_fun_hom (to_fun_ob G p'.1) f.2 ∘ natural_map (to_fun_hom G f.1) p.2
+  local abbreviation Ghom := @functor_uncurry_hom
+
+  theorem functor_uncurry_id (p : C ×c D) : Ghom G (ID p) = id :=
+  calc
+    Ghom G (ID p) = to_fun_hom (to_fun_ob G p.1) id ∘ natural_map (to_fun_hom G id) p.2 : by esimp
+      ... = id ∘ natural_map (to_fun_hom G id) p.2 : by rewrite respect_id
+      ... = id ∘ natural_map nat_trans.id p.2      : by rewrite respect_id
+      ... = id                                     : id_id
+
+  theorem functor_uncurry_comp ⦃p p' p'' : C ×c D⦄ (f' : p' ⟶ p'') (f : p ⟶ p')
+    : Ghom G (f' ∘ f) = Ghom G f' ∘ Ghom G f :=
+  calc
+    Ghom G (f' ∘ f)
+          = to_fun_hom (to_fun_ob G p''.1) (f'.2 ∘ f.2) ∘ natural_map (to_fun_hom G (f'.1 ∘ f.1)) p.2 : by esimp
+      ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2)
+              ∘ natural_map (to_fun_hom G (f'.1 ∘ f.1)) p.2                : by rewrite respect_comp
+      ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2)
+              ∘ natural_map (to_fun_hom G f'.1 ∘ to_fun_hom G f.1) p.2     : by rewrite respect_comp
+      ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ to_fun_hom (to_fun_ob G p''.1) f.2)
+             ∘ (natural_map (to_fun_hom G f'.1) p.2 ∘ natural_map (to_fun_hom G f.1) p.2) : by esimp
+      ... = (to_fun_hom (to_fun_ob G p''.1) f'.2 ∘ natural_map (to_fun_hom G f'.1) p'.2)
+              ∘ (to_fun_hom (to_fun_ob G p'.1) f.2 ∘ natural_map (to_fun_hom G f.1) p.2) :
+                  by rewrite [square_prepostcompose (!naturality⁻¹ᵖ) _ _]
+      ... = Ghom G f' ∘ Ghom G f : by esimp
+
+  definition functor_uncurry [reducible] [constructor] : C ×c D ⇒ E :=
+  functor.mk (functor_uncurry_ob G)
+             (functor_uncurry_hom G)
+             (functor_uncurry_id G)
+             (functor_uncurry_comp G)
+
+  theorem functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F :=
+  functor_eq (λp, ap (to_fun_ob F) !prod.eta)
+  begin
+    intro cd cd' fg,
+    cases cd with c d, cases cd' with c' d', cases fg with f g,
+    transitivity to_fun_hom (functor_uncurry (functor_curry F)) (f, g),
+    apply id_leftright,
+    show (functor_uncurry (functor_curry F)) (f, g) = F (f,g),
+      from calc
+        (functor_uncurry (functor_curry F)) (f, g) = to_fun_hom F (id, g) ∘ to_fun_hom F (f, id) : by esimp
+          ... = F (id ∘ f, g ∘ id) : by krewrite [-respect_comp F (id,g) (f,id)]
+          ... = F (f, g ∘ id)      : by rewrite id_left
+          ... = F (f,g)            : by rewrite id_right,
+  end
+
+  definition functor_curry_functor_uncurry_ob (c : C)
+    : functor_curry (functor_uncurry G) c = G c :=
+  begin
+    fapply functor_eq,
+     { intro d, reflexivity},
+     { intro d d' g, refine !id_leftright ⬝ _, esimp,
+       rewrite [▸*, ↑functor_uncurry_hom, respect_id, ▸*, id_right]}
+  end
+
+  theorem functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G :=
+  begin
+    fapply functor_eq, exact (functor_curry_functor_uncurry_ob G),
+    intro c c' f,
+    fapply nat_trans_eq,
+    intro d,
+    apply concat,
+      {apply (ap (λx, x ∘ _)),
+        apply concat, apply natural_map_hom_of_eq, apply (ap hom_of_eq), apply ap010_functor_eq},
+    apply concat,
+       {apply (ap (λx, _ ∘ x)), apply (ap (λx, _ ∘ x)),
+         apply concat, apply natural_map_inv_of_eq,
+         apply (ap (λx, hom_of_eq x⁻¹)), apply ap010_functor_eq},
+    apply concat, apply id_leftright,
+    apply concat, apply (ap (λx, x ∘ _)), apply respect_id,
+    apply id_left
+  end
+
+  /-
+     This only states that the carriers of (C ^ D) ^ E and C ^ (E × D) are equivalent.
+     In [exponential laws] we prove that these are in fact isomorphic categories
+  -/
+  definition prod_functor_equiv_functor_functor [constructor] (C D E : Precategory)
+    : (C ×c D ⇒ E) ≃ (C ⇒ E ^c D) :=
+  equiv.MK functor_curry
+           functor_uncurry
+           functor_curry_functor_uncurry
+           functor_uncurry_functor_curry
+
+  variables {F F' G G'}
+  definition nat_trans_curry_nat [constructor] (η : F ⟹ F') (c : C)
+    : functor_curry_ob F c ⟹ functor_curry_ob F' c :=
+  begin
+    fapply nat_trans.mk: esimp,
+    { intro d, exact η (c, d)},
+    { intro d d' f, apply naturality}
+  end
+
+  definition nat_trans_curry [constructor] (η : F ⟹ F')
+    : functor_curry F ⟹ functor_curry F' :=
+  begin
+    fapply nat_trans.mk: esimp,
+    { exact nat_trans_curry_nat η},
+    { intro c c' f, apply nat_trans_eq, intro d, esimp, apply naturality}
+  end
+
+  definition nat_trans_uncurry [constructor] (η : G ⟹ G')
+    : functor_uncurry G ⟹ functor_uncurry G' :=
+  begin
+    fapply nat_trans.mk: esimp,
+    { intro v, unfold functor_uncurry_ob, exact (η v.1) v.2},
+    { intro v w f, unfold functor_uncurry_hom,
+      rewrite [-assoc, ap010 natural_map (naturality η f.1) v.2, assoc, naturality, -assoc]}
+  end
+  end
+
+  section
+  open is_trunc
+
+  /- hom-functors -/
+
+  definition hom_functor_assoc {C : Precategory} {a1 a2 a3 a4 a5 a6 : C}
+    (f1 : hom a5 a6) (f2 : hom a4 a5) (f3 : hom a3 a4) (f4 : hom a2 a3) (f5 : hom a1 a2)
+      : (f1 ∘ f2) ∘ f3 ∘ (f4 ∘ f5) = f1 ∘ (f2 ∘ f3 ∘ f4) ∘ f5 :=
+  calc
+        _ = f1 ∘ f2 ∘ f3 ∘ f4 ∘ f5     : by rewrite -assoc
+      ... = f1 ∘ (f2 ∘ f3) ∘ f4 ∘ f5   : by rewrite -assoc
+      ... = f1 ∘ ((f2 ∘ f3) ∘ f4) ∘ f5 : by rewrite -(assoc (f2 ∘ f3) _ _)
+      ... = _                          : by rewrite (assoc f2 f3 f4)
+
+  -- the functor hom(-,-)
+  definition hom_functor.{u v} [constructor] (C : Precategory.{u v}) : Cᵒᵖ ×c C ⇒ set.{v} :=
+  functor.mk
+    (λ (x : Cᵒᵖ ×c C), @homset (Cᵒᵖ) C x.1 x.2)
+    (λ (x y : Cᵒᵖ ×c C) (f : @category.precategory.hom (Cᵒᵖ ×c C) (Cᵒᵖ ×c C) x y)
+       (h : @homset (Cᵒᵖ) C x.1 x.2), f.2 ∘[C] (h ∘[C] f.1))
+    (λ x, abstract @eq_of_homotopy _ _ _ (ID (@homset Cᵒᵖ C x.1 x.2))
+            (λ h, concat (by apply @id_left) (by apply @id_right)) end)
+    (λ x y z g f, abstract eq_of_homotopy (by intros; apply @hom_functor_assoc) end)
+
+  -- the functor hom(-, c)
+  definition hom_functor_left.{u v} [constructor] (C : Precategory.{u v}) (c : C)
+    : Cᵒᵖ ⇒ set.{v} :=
+  hom_functor C ∘f (1 ×f constant_functor Cᵒᵖ c)
+
+  -- the functor hom(c, -)
+  definition hom_functor_right.{u v} [constructor] (C : Precategory.{u v}) (c : C)
+    : C ⇒ set.{v} :=
+  hom_functor C ∘f (constant_functor C c ×f 1)
+
+
+  end
+
+
+
+end functor
diff --git a/hott/algebra/category/functor/exponential_laws.hlean b/hott/algebra/category/functor/exponential_laws.hlean
index 5023cca12..e64b09e0d 100644
--- a/hott/algebra/category/functor/exponential_laws.hlean
+++ b/hott/algebra/category/functor/exponential_laws.hlean
@@ -6,7 +6,7 @@ Authors: Floris van Doorn, Jakob von Raumer
 Exponential laws
 -/
 
-import .equivalence .curry
+import .equivalence .examples
        ..constructions.terminal ..constructions.initial ..constructions.product ..constructions.sum
        ..constructions.discrete
 
diff --git a/hott/algebra/category/functor/functor.md b/hott/algebra/category/functor/functor.md
index 839e68cf7..7297fcd75 100644
--- a/hott/algebra/category/functor/functor.md
+++ b/hott/algebra/category/functor/functor.md
@@ -1,11 +1,14 @@
 algebra.category.functor
 ========================
 
+Functors, functor attributes, equivalences, isomorphism, adjointness.
+
 * [basic](basic.hlean) : Definition and basic properties of functors
-* [curry](curry.hlean) : Define currying and uncurrying of functors
+* [examples](examples.hlean) : Constructions of functors between categories, involving more than one category in the [constructions](../constructions/constructions.md) folder (functors which only depend on one constructions are in the corresponding file). This includes the currying and uncurrying of functors
 * [attributes](attributes.hlean): Attributes of functors (full, faithful, split essentially surjective, ...)
 * [adjoint](adjoint.hlean) : Adjoint functors and equivalences
 * [equivalence](equivalence.hlean) : Equivalences and Isomorphisms
 * [exponential_laws](exponential_laws.hlean)
+* [yoneda](yoneda.hlean) : the Yoneda Embedding
 
-Note: the functor category is defined in [constructions.functor](../constructions/functor.hlean).
\ No newline at end of file
+Note: the functor category is defined in [constructions.functor](../constructions/functor.hlean). Functors preserving limits is in [limits.functor_preserve](../limits/functor_preserve.hlean).
\ No newline at end of file
diff --git a/hott/algebra/category/yoneda.hlean b/hott/algebra/category/functor/yoneda.hlean
similarity index 82%
rename from hott/algebra/category/yoneda.hlean
rename to hott/algebra/category/functor/yoneda.hlean
index 27bc7747d..e3e51e7f8 100644
--- a/hott/algebra/category/yoneda.hlean
+++ b/hott/algebra/category/functor/yoneda.hlean
@@ -6,30 +6,12 @@ Authors: Floris van Doorn
 Yoneda embedding and Yoneda lemma
 -/
 
-import .functor.curry .constructions.hset .constructions.opposite .functor.attributes
+import .examples .attributes
 
 open category eq functor prod.ops is_trunc iso is_equiv equiv category.set nat_trans lift
 
 namespace yoneda
 
-  definition representable_functor_assoc [C : Precategory] {a1 a2 a3 a4 a5 a6 : C}
-    (f1 : hom a5 a6) (f2 : hom a4 a5) (f3 : hom a3 a4) (f4 : hom a2 a3) (f5 : hom a1 a2)
-      : (f1 ∘ f2) ∘ f3 ∘ (f4 ∘ f5) = f1 ∘ (f2 ∘ f3 ∘ f4) ∘ f5 :=
-  calc
-        _ = f1 ∘ f2 ∘ f3 ∘ f4 ∘ f5     : by rewrite -assoc
-      ... = f1 ∘ (f2 ∘ f3) ∘ f4 ∘ f5   : by rewrite -assoc
-      ... = f1 ∘ ((f2 ∘ f3) ∘ f4) ∘ f5 : by rewrite -(assoc (f2 ∘ f3) _ _)
-      ... = _                          : by rewrite (assoc f2 f3 f4)
-
-  definition hom_functor.{u v} [constructor] (C : Precategory.{u v}) : Cᵒᵖ ×c C ⇒ set.{v} :=
-  functor.mk
-    (λ (x : Cᵒᵖ ×c C), @homset (Cᵒᵖ) C x.1 x.2)
-    (λ (x y : Cᵒᵖ ×c C) (f : @category.precategory.hom (Cᵒᵖ ×c C) (Cᵒᵖ ×c C) x y)
-       (h : @homset (Cᵒᵖ) C x.1 x.2), f.2 ∘[C] (h ∘[C] f.1))
-    (λ x, abstract @eq_of_homotopy _ _ _ (ID (@homset Cᵒᵖ C x.1 x.2))
-            (λ h, concat (by apply @id_left) (by apply @id_right)) end)
-    (λ x y z g f, abstract eq_of_homotopy (by intros; apply @representable_functor_assoc) end)
-
   /-
     These attributes make sure that the fields of the category "set" reduce to the right things
     However, we don't want to have them globally, because that will unfold the composition g ∘ f
@@ -45,6 +27,7 @@ namespace yoneda
   definition yoneda_embedding [constructor] (C : Precategory) : C ⇒ cset ^c Cᵒᵖ :=
   functor_curry (!hom_functor ∘f !prod_flip_functor)
 
+
   notation `ɏ` := yoneda_embedding _
 
   definition yoneda_lemma_hom [constructor] {C : Precategory} (c : C) (F : Cᵒᵖ ⇒ cset)
diff --git a/hott/algebra/category/limits/adjoint.hlean b/hott/algebra/category/limits/adjoint.hlean
index fe36e5546..6fb62dc06 100644
--- a/hott/algebra/category/limits/adjoint.hlean
+++ b/hott/algebra/category/limits/adjoint.hlean
@@ -6,9 +6,9 @@ Authors: Floris van Doorn
 colimit_functor ⊣ Δ ⊣ limit_functor
 -/
 
-import ..colimits ..functor.adjoint2
+import .colimits ..functor.adjoint2
 
-open functor category is_trunc prod yoneda --remove
+open functor category is_trunc prod
 
 namespace category
 
diff --git a/hott/algebra/category/colimits.hlean b/hott/algebra/category/limits/colimits.hlean
similarity index 99%
rename from hott/algebra/category/colimits.hlean
rename to hott/algebra/category/limits/colimits.hlean
index 9c78526c0..4a8faece7 100644
--- a/hott/algebra/category/colimits.hlean
+++ b/hott/algebra/category/limits/colimits.hlean
@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 Colimits in a category
 -/
 
-import .limits .constructions.opposite
+import .limits ..constructions.opposite
 
 open is_trunc functor nat_trans eq
 
diff --git a/hott/algebra/category/limits/default.hlean b/hott/algebra/category/limits/default.hlean
new file mode 100644
index 000000000..e936fa68f
--- /dev/null
+++ b/hott/algebra/category/limits/default.hlean
@@ -0,0 +1,7 @@
+/-
+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
+-/
+
+import .limits .colimits
diff --git a/hott/algebra/category/constructions/functor2.hlean b/hott/algebra/category/limits/functor.hlean
similarity index 99%
rename from hott/algebra/category/constructions/functor2.hlean
rename to hott/algebra/category/limits/functor.hlean
index 7d6b41639..94d3d9a9e 100644
--- a/hott/algebra/category/constructions/functor2.hlean
+++ b/hott/algebra/category/limits/functor.hlean
@@ -6,7 +6,7 @@ Authors: Floris van Doorn, Jakob von Raumer
 Functor category has (co)limits if the codomain has them
 -/
 
-import ..colimits
+import .colimits
 
 open functor nat_trans eq is_trunc
 
diff --git a/hott/algebra/category/limits/functor_preserve.hlean b/hott/algebra/category/limits/functor_preserve.hlean
index af2d92a0c..136c9f739 100644
--- a/hott/algebra/category/limits/functor_preserve.hlean
+++ b/hott/algebra/category/limits/functor_preserve.hlean
@@ -6,7 +6,7 @@ Authors: Floris van Doorn
 Functors preserving limits
 -/
 
-import ..colimits ..yoneda
+import .colimits ..functor.yoneda
 
 open functor yoneda is_trunc nat_trans
 
diff --git a/hott/algebra/category/limits.hlean b/hott/algebra/category/limits/limits.hlean
similarity index 99%
rename from hott/algebra/category/limits.hlean
rename to hott/algebra/category/limits/limits.hlean
index fff03a3f6..95ea5d114 100644
--- a/hott/algebra/category/limits.hlean
+++ b/hott/algebra/category/limits/limits.hlean
@@ -6,8 +6,8 @@ Authors: Floris van Doorn
 Limits in a category
 -/
 
-import .constructions.cone .constructions.discrete .constructions.product
-       .constructions.finite_cats .category .constructions.functor
+import ..constructions.cone ..constructions.discrete ..constructions.product
+       ..constructions.finite_cats ..category ..constructions.functor
 
 open is_trunc functor nat_trans eq
 
diff --git a/hott/algebra/category/limits/limits.md b/hott/algebra/category/limits/limits.md
new file mode 100644
index 000000000..7938b8a73
--- /dev/null
+++ b/hott/algebra/category/limits/limits.md
@@ -0,0 +1,8 @@
+algebra.category.limits
+=======================
+
+* [limits](limits.hlean) : Limits in a category, defined as terminal object in the cone category
+* [colimits](colimits.hlean) : Colimits in a category, defined as the limit of the opposite functor
+* [complete](complete.hlean) : Categories which are (co)complete or constructions which preserve (co)completeness
+* [functor_preserve](functor_preserve.hlean) : Functors which preserve limits and colimits
+* [adjoint](adjoint.hlean) : the (co)limit functor is adjoint to the diagonal map
diff --git a/hott/algebra/category/constructions/hset.hlean b/hott/algebra/category/limits/set.hlean
similarity index 54%
rename from hott/algebra/category/constructions/hset.hlean
rename to hott/algebra/category/limits/set.hlean
index 49977f2b2..ac65e8f52 100644
--- a/hott/algebra/category/constructions/hset.hlean
+++ b/hott/algebra/category/limits/set.hlean
@@ -3,101 +3,14 @@ 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, Jakob von Raumer
 
-Category of hsets
+The category of sets is complete and cocomplete
 -/
 
-import ..category types.equiv types.lift ..colimits hit.set_quotient
+import .colimits ..constructions.set hit.set_quotient
 
-open eq category equiv iso is_equiv is_trunc function sigma set_quotient trunc
+open eq functor is_trunc sigma pi sigma.ops trunc set_quotient
 
 namespace category
-
-  definition precategory_hset.{u} [reducible] [constructor] : precategory hset.{u} :=
-  precategory.mk (λx y : hset, x → y)
-                 (λx y z g f a, g (f a))
-                 (λx a, a)
-                 (λx y z w h g f, eq_of_homotopy (λa, idp))
-                 (λx y f, eq_of_homotopy (λa, idp))
-                 (λx y f, eq_of_homotopy (λa, idp))
-
-  definition Precategory_hset [reducible] [constructor] : Precategory :=
-  Precategory.mk hset precategory_hset
-
-  abbreviation set [constructor] := Precategory_hset
-
-  namespace set
-    local attribute is_equiv_subtype_eq [instance]
-    definition iso_of_equiv [constructor] {A B : set} (f : A ≃ B) : A ≅ B :=
-    iso.MK (to_fun f)
-           (to_inv f)
-           (eq_of_homotopy (left_inv (to_fun f)))
-           (eq_of_homotopy (right_inv (to_fun f)))
-
-    definition equiv_of_iso [constructor] {A B : set} (f : A ≅ B) : A ≃ B :=
-    begin
-      apply equiv.MK (to_hom f) (iso.to_inv f),
-        exact ap10 (to_right_inverse f),
-        exact ap10 (to_left_inverse f)
-    end
-
-    definition is_equiv_iso_of_equiv [constructor] (A B : set)
-      : is_equiv (@iso_of_equiv A B) :=
-    adjointify _ (λf, equiv_of_iso f)
-                 (λf, proof iso_eq idp qed)
-                 (λf, equiv_eq idp)
-
-    local attribute is_equiv_iso_of_equiv [instance]
-
-    definition iso_of_eq_eq_compose (A B : hset) : @iso_of_eq _ _ A B =
-      @iso_of_equiv A B ∘ @equiv_of_eq A B ∘ subtype_eq_inv _ _ ∘
-      @ap _ _ (to_fun (trunctype.sigma_char 0)) A B :=
-    eq_of_homotopy (λp, eq.rec_on p idp)
-
-    definition equiv_equiv_iso (A B : set) : (A ≃ B) ≃ (A ≅ B) :=
-    equiv.MK (λf, iso_of_equiv f)
-             (λf, proof equiv.MK (to_hom f)
-                           (iso.to_inv f)
-                           (ap10 (to_right_inverse f))
-                           (ap10 (to_left_inverse  f)) qed)
-             (λf, proof iso_eq idp qed)
-             (λf, proof equiv_eq idp qed)
-
-    definition equiv_eq_iso (A B : set) : (A ≃ B) = (A ≅ B) :=
-    ua !equiv_equiv_iso
-
-    definition is_univalent_hset (A B : set) : is_equiv (iso_of_eq : A = B → A ≅ B) :=
-    assert H₁ : is_equiv (@iso_of_equiv A B ∘ @equiv_of_eq A B ∘ subtype_eq_inv _ _ ∘
-                  @ap _ _ (to_fun (trunctype.sigma_char 0)) A B), from
-      @is_equiv_compose _ _ _ _ _
-      (@is_equiv_compose _ _ _ _ _
-         (@is_equiv_compose _ _ _ _ _
-           _
-           (@is_equiv_subtype_eq_inv _ _ _ _ _))
-         !univalence)
-       !is_equiv_iso_of_equiv,
-    let H₂ := (iso_of_eq_eq_compose A B)⁻¹ in
-    begin
-      rewrite H₂ at H₁,
-      assumption
-    end
-  end set
-
-  definition category_hset [instance] [constructor] [reducible] : category hset :=
-  category.mk precategory_hset set.is_univalent_hset
-
-  definition Category_hset [reducible] [constructor] : Category :=
-  Category.mk hset category_hset
-
-  abbreviation cset [constructor] := Category_hset
-
-  open functor lift
-  definition lift_functor.{u v} [constructor] : set.{u} ⇒ set.{max u v} :=
-  functor.mk tlift
-             (λa b, lift_functor)
-             (λa, eq_of_homotopy (λx, by induction x; reflexivity))
-             (λa b c g f, eq_of_homotopy (λx, by induction x; reflexivity))
-
-  open pi sigma.ops
   local attribute Category.to.precategory [unfold 1]
   local attribute category.to_precategory [unfold 2]
 
@@ -154,6 +67,7 @@ namespace category
       { exact _}
   end
 
+
   definition is_cocomplete_set_cone.{u v w} [constructor]
     (I : Precategory.{v w}) (F : I ⇒ set.{max u v w}ᵒᵖ) : cone_obj F :=
   begin
@@ -189,6 +103,4 @@ namespace category
         { intro v w r, apply is_hprop.elimo}}},
   end
 
-
-
 end category
diff --git a/hott/book.md b/hott/book.md
index a931e9bef..e9adaeb51 100644
--- a/hott/book.md
+++ b/hott/book.md
@@ -29,7 +29,9 @@ The rows indicate the chapters, the columns the sections.
 
 Theorems and definitions in the library which are not in the book:
 
-* One major difference is that in this library we heavily use pathovers, so we need less theorems about transports, but instead corresponding theorems about pathovers. These are in [init.pathover](init/pathover.hlean). For higher paths there are [squares](cubical/square.hlean), [squareovers](cubical/squareover.hlean), and the rudiments of [cubes](cubical/cube.hlean) and [cubeovers](cubical/cubeover.hlean).
+* A major difference is that in this library we heavily use pathovers [D. Licata, G. Brunerie. A Cubical Approach to Synthetic Homotopy Theory]. This means that we need less theorems about transports, but instead corresponding theorems about pathovers. These are in [init.pathover](init/pathover.hlean). For higher paths there are [squares](cubical/square.hlean), [squareovers](cubical/squareover.hlean), and the rudiments of [cubes](cubical/cube.hlean) and [cubeovers](cubical/cubeover.hlean).
+
+* The category theory library is more extensive than what is presented in the book. For example, we have [limits](algebra/category/limits/limits.md).
 
 Chapter 1: Type theory
 ---------
@@ -159,7 +161,7 @@ Every file is in the folder [algebra.category](algebra/category/category.md)
 - 9.2 (Functors and transformations): [functor.basic](algebra/category/functor/basic.hlean), [nat_trans](algebra/category/nat_trans.hlean), [constructions.functor](algebra/category/constructions/functor.hlean)
 - 9.3 (Adjunctions): [functor.adjoint](algebra/category/functor/adjoint.hlean)
 - 9.4 (Equivalences): [functor.equivalence](algebra/category/functor/equivalence.hlean) and [functor.attributes](algebra/category/functor/attributes.hlean) (partially)
-- 9.5 (The Yoneda lemma): [constructions.opposite](algebra/category/constructions/opposite.hlean), [constructions.product](algebra/category/constructions/product.hlean), [yoneda](algebra/category/yoneda.hlean) (up to Theorem 9.5.9)
+- 9.5 (The Yoneda lemma): [constructions.opposite](algebra/category/constructions/opposite.hlean), [constructions.product](algebra/category/constructions/product.hlean), [functor.yoneda](algebra/category/functor/yoneda.hlean) (up to Theorem 9.5.9)
 - 9.6 (Strict categories): [strict](algebra/category/strict.hlean) (only definition)
 - 9.7 (†-categories): not formalized
 - 9.8 (The structure identity principle): not formalized
diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index 1650b2f2b..3112edc06 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -41,7 +41,7 @@
     "⁻¹ᵉ" "⁻¹ᶠ" "⁻¹ᵍ" "⁻¹ʰ" "⁻¹ⁱ" "⁻¹ᵐ" "⁻¹ᵒ" "⁻¹ᵖ" "⁻¹ʳ" "⁻¹ᵛ" "⁻¹ˢ" "⁻²" "⁻²ᵒ"
     "⬝e" "⬝i" "⬝o" "⬝op" "⬝po" "⬝h" "⬝v" "⬝hp" "⬝vp" "⬝ph" "⬝pv" "⬝r" "◾" "◾o"
     "∘n" "∘f" "∘fi" "∘nf" "∘fn" "∘n1f" "∘1nf" "∘f1n" "∘fn1"
-    "^c" "≃c" "≅c" "×c" "×f" "+c" "+f")
+    "^c" "≃c" "≅c" "×c" "×f" "×n" "+c" "+f" "+n")
   "lean constants")
 (defconst lean-constants-regexp (regexp-opt lean-constants))
 (defconst lean-numerals-regexp