diff --git a/hott/algebra/binary.hlean b/hott/algebra/binary.hlean
index a58114540..f6b4327b5 100644
--- a/hott/algebra/binary.hlean
+++ b/hott/algebra/binary.hlean
@@ -47,7 +47,7 @@ namespace binary
     variable {f : A → A → A}
     variable H_comm : commutative f
     variable H_assoc : associative f
-    local infixl `*` := f
+    local infixl * := f
     theorem left_comm : left_commutative f :=
     take a b c, calc
       a*(b*c) = (a*b)*c  : H_assoc
@@ -71,7 +71,7 @@ namespace binary
     variable {A : Type}
     variable {f : A → A → A}
     variable H_assoc : associative f
-    local infixl `*` := f
+    local infixl * := f
     theorem assoc4helper (a b c d) : (a*b)*(c*d) = a*((b*c)*d) :=
     calc
       (a*b)*(c*d) = a*(b*(c*d)) : H_assoc
diff --git a/hott/algebra/category/adjoint.hlean b/hott/algebra/category/adjoint.hlean
index 831b9ed72..20ffa0a86 100644
--- a/hott/algebra/category/adjoint.hlean
+++ b/hott/algebra/category/adjoint.hlean
@@ -33,7 +33,7 @@ namespace category
     (is_iso_counit : is_iso ε)
 
   abbreviation inverse := @is_equivalence.G
-  postfix `⁻¹` := inverse
+  postfix ⁻¹ := inverse
   --a second notation for the inverse, which is not overloaded
   postfix [parsing-only] `⁻¹F`:std.prec.max_plus := inverse
 
@@ -55,8 +55,8 @@ namespace category
     (struct : is_isomorphism to_functor)
   --   infix `⊣`:55 := adjoint
 
-  infix `⋍`:25 := equivalence -- \backsimeq or \equiv
-  infix `≌`:25 := isomorphism -- \backcong or \iso
+  infix ` ⋍ `:25 := equivalence -- \backsimeq or \equiv
+  infix ` ≌ `:25 := isomorphism -- \backcong or \iso
 
   definition is_equiv_of_fully_faithful [instance] [reducible] (F : C ⇒ D) [H : fully_faithful F]
     (c c' : C) : is_equiv (@(to_fun_hom F) c c') :=
diff --git a/hott/algebra/category/category.md b/hott/algebra/category/category.md
index f7e28b1f5..221bac14b 100644
--- a/hott/algebra/category/category.md
+++ b/hott/algebra/category/category.md
@@ -11,5 +11,7 @@ Development of Category Theory. The following files are in this folder (sorted s
 * [nat_trans](nat_trans.hlean) : Natural transformations
 * [strict](strict.hlean) : Strict categories
 * [constructions](constructions/constructions.md) (subfolder) : basic constructions on categories and examples of categories
-* [adjoint](adjoint.hlean) : Adjoint functors and Equivalences (TODO)
-* [yoneda](yoneda.hlean) : Yoneda Embedding (TODO)
+* [adjoint](adjoint.hlean) : Adjoint functors and Equivalences (WIP)
+* [yoneda](yoneda.hlean) : Yoneda Embedding (WIP)
+* [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
\ No newline at end of file
diff --git a/hott/algebra/category/constructions/constructions.md b/hott/algebra/category/constructions/constructions.md
index ababcc055..e70b79903 100644
--- a/hott/algebra/category/constructions/constructions.md
+++ b/hott/algebra/category/constructions/constructions.md
@@ -3,7 +3,19 @@ algebra.category.constructions
 
 Common categories and constructions on categories. The following files are in this folder.
 
-* [opposite](opposite.hlean) : Opposite category
-* [product](product.hlean) : Product category
-* [hset](hset.hlean) : Category of sets
 * [functor](functor.hlean) : Functor category
+* [opposite](opposite.hlean) : Opposite category
+* [hset](hset.hlean) : Category of sets
+* [sum](sum.hlean) : Sum category
+* [product](product.hlean) : Product category
+* [comma](comma.hlean) : Comma category
+* [cone](cone.hlean) : Cone category
+
+
+Discrete, indiscrete or finite categories:
+
+* [finite_cats](finite_cats.hlean) : Some finite categories, which are diagrams of common limits (the diagram for the pullback or the equalizer). Also contains a general construction of categories where you give some generators for the morphisms, with the condition that you cannot compose two of thosex
+* [discrete](discrete.hlean)
+* [indiscrete](indiscrete.hlean)
+* [terminal](terminal.hlean)
+* [initial](initial.hlean)
diff --git a/hott/algebra/category/constructions/functor.hlean b/hott/algebra/category/constructions/functor.hlean
index 2ca6883b5..2b5dd3c54 100644
--- a/hott/algebra/category/constructions/functor.hlean
+++ b/hott/algebra/category/constructions/functor.hlean
@@ -24,7 +24,7 @@ namespace category
   definition Precategory_functor [reducible] [constructor] (D C : Precategory) : Precategory :=
   precategory.Mk (precategory_functor D C)
 
-  infixr `^c`:35 := Precategory_functor
+  infixr ` ^c `:35 := Precategory_functor
 
   section
   /- we prove that if a natural transformation is pointwise an iso, then it is an iso -/
@@ -229,7 +229,7 @@ namespace category
   Category_functor D C
 
   namespace ops
-    infixr `^c2`:35 := Category_functor
+    infixr ` ^c2 `:35 := Category_functor
   end ops
 
   namespace functor
diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean
index c3e5c1a40..649b69b63 100644
--- a/hott/algebra/category/functor.hlean
+++ b/hott/algebra/category/functor.hlean
@@ -18,7 +18,7 @@ structure functor (C D : Precategory) : Type :=
 
 namespace functor
 
-  infixl `⇒`:25 := functor
+  infixl ` ⇒ `:25 := functor
   variables {A B C D E : Precategory}
 
   attribute to_fun_ob [coercion]
@@ -38,7 +38,7 @@ namespace functor
       G (F (g ∘ f)) = G (F g ∘ F f)     : by rewrite respect_comp
                 ... = G (F g) ∘ G (F f) : by rewrite respect_comp end)
 
-  infixr `∘f`:60 := functor.compose
+  infixr ` ∘f `:60 := functor.compose
 
   protected definition id [reducible] [constructor] {C : Precategory} : functor C C :=
   mk (λa, a) (λ a b f, f) (λ a, idp) (λ a b c f g, idp)
diff --git a/hott/algebra/category/groupoid.hlean b/hott/algebra/category/groupoid.hlean
index 13da43a5a..18153d38a 100644
--- a/hott/algebra/category/groupoid.hlean
+++ b/hott/algebra/category/groupoid.hlean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2014 Jakob von Raumer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Jakob von Raumer
+Authors: Jakob von Raumer, Floris van Doorn
 
 Ported from Coq HoTT
 -/
diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean
index 64b4be25e..247e0fc6d 100644
--- a/hott/algebra/category/iso.hlean
+++ b/hott/algebra/category/iso.hlean
@@ -31,7 +31,7 @@ namespace iso
   abbreviation inverse [unfold 6] := @is_iso.inverse
   abbreviation left_inverse [unfold 6] := @is_iso.left_inverse
   abbreviation right_inverse [unfold 6] := @is_iso.right_inverse
-  postfix `⁻¹` := inverse
+  postfix ⁻¹ := inverse
   --a second notation for the inverse, which is not overloaded
   postfix [parsing-only] `⁻¹ʰ`:std.prec.max_plus := inverse -- input using \-1h
 
@@ -131,7 +131,7 @@ structure iso {ob : Type} [C : precategory ob] (a b : ob) :=
   (to_hom : hom a b)
   [struct : is_iso to_hom]
 
-  infix `≅`:50 := iso
+  infix ` ≅ `:50 := iso
   attribute iso.struct [instance] [priority 4000]
 
 namespace iso
@@ -162,7 +162,7 @@ namespace iso
   protected definition trans [constructor] ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c :=
   mk (to_hom H2 ∘ to_hom H1)
 
-  infixl `⬝i`:75 := iso.trans
+  infixl ` ⬝i `:75 := iso.trans
   postfix [parsing-only] `⁻¹ⁱ`:(max + 1) := iso.symm
 
   definition iso_mk_eq {f f' : a ⟶ b} [H : is_iso f] [H' : is_iso f'] (p : f = f')
diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean
index 5c9337ed4..9a67bbeee 100644
--- a/hott/algebra/category/nat_trans.hlean
+++ b/hott/algebra/category/nat_trans.hlean
@@ -13,7 +13,7 @@ structure nat_trans {C : Precategory} {D : Precategory} (F G : C ⇒ D)
 
 namespace nat_trans
 
-  infixl `⟹`:25 := nat_trans -- \==>
+  infixl ` ⟹ `:25 := nat_trans -- \==>
   variables {B C D E : Precategory} {F G H I : C ⇒ D} {F' G' : D ⇒ E} {F'' G'' : E ⇒ B} {J : C ⇒ C}
 
   attribute natural_map [coercion]
@@ -30,7 +30,7 @@ namespace nat_trans
                       ... = (η b ∘ θ b) ∘ F f : by rewrite assoc
       end)
 
-  infixr `∘n`:60 := nat_trans.compose
+  infixr ` ∘n `:60 := nat_trans.compose
 
   protected definition id [reducible] [constructor] {F : C ⇒ D} : nat_trans F F :=
   mk (λa, id) (λa b f, !id_right ⬝ !id_left⁻¹)
@@ -130,12 +130,12 @@ namespace nat_trans
         ... = F (η b ∘ f)               : by rewrite (naturality η f)
         ... = F (η b) ∘ F f             : by rewrite respect_comp)
 
-  infixr `∘nf`:62 := nat_trans_functor_compose
-  infixr `∘fn`:62 := functor_nat_trans_compose
-  infixr `∘n1f`:62 := nat_trans_id_functor_compose
-  infixr `∘1nf`:62 := id_nat_trans_functor_compose
-  infixr `∘f1n`:62 := functor_id_nat_trans_compose
-  infixr `∘fn1`:62 := functor_nat_trans_id_compose
+  infixr ` ∘nf ` :62 := nat_trans_functor_compose
+  infixr ` ∘fn ` :62 := functor_nat_trans_compose
+  infixr ` ∘n1f `:62 := nat_trans_id_functor_compose
+  infixr ` ∘1nf `:62 := id_nat_trans_functor_compose
+  infixr ` ∘f1n `:62 := functor_id_nat_trans_compose
+  infixr ` ∘fn1 `:62 := functor_nat_trans_id_compose
 
   definition nf_fn_eq_fn_nf_pt (η : F ⟹ G) (θ : F' ⟹ G') (c : C)
     : (θ (G c)) ∘ (F' (η c)) = (G' (η c)) ∘ (θ (F c)) :=
diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean
index 5e9366a80..490b7a8ed 100644
--- a/hott/algebra/category/precategory.hlean
+++ b/hott/algebra/category/precategory.hlean
@@ -33,11 +33,11 @@ namespace category
   attribute precategory [multiple-instances]
   attribute precategory.is_hset_hom [instance]
 
-  infixr `∘` := precategory.comp
+  infixr ∘ := precategory.comp
   -- input ⟶ using \--> (this is a different arrow than \-> (→))
-  infixl [parsing-only] `⟶`:25 := precategory.hom
+  infixl [parsing-only] ` ⟶ `:25 := precategory.hom
   namespace hom
-    infixl `⟶`:25 := precategory.hom -- if you open this namespace, hom a b is printed as a ⟶ b
+    infixl ` ⟶ `:25 := precategory.hom -- if you open this namespace, hom a b is printed as a ⟶ b
   end hom
 
   abbreviation hom         [unfold 2] := @precategory.hom
@@ -85,8 +85,8 @@ namespace category
   end basic_lemmas
   section squares
     parameters {ob : Type} [C : precategory ob]
-    local infixl `⟶`:25 := @precategory.hom ob C
-    local infixr `∘`    := @precategory.comp ob C _ _ _
+    local infixl ` ⟶ `:25 := @precategory.hom ob C
+    local infixr ∘    := @precategory.comp ob C _ _ _
     definition compose_squares {xa xb xc ya yb yc : ob}
       {xg : xb ⟶ xc} {xf : xa ⟶ xb} {yg : yb ⟶ yc} {yf : ya ⟶ yb}
       {wa : xa ⟶ ya} {wb : xb ⟶ yb} {wc : xc ⟶ yc}
@@ -149,10 +149,9 @@ namespace category
   attribute Precategory.struct [instance] [priority 10000] [coercion]
   -- definition precategory.carrier [coercion] [reducible] := Precategory.carrier
   -- definition precategory.struct [instance] [coercion] [reducible] := Precategory.struct
-  notation g `∘[`:60 C:0 `]`:0 f:60 :=
+  notation g ` ∘[`:60 C:0 `] `:0 f:60 :=
   @comp (Precategory.carrier C) (Precategory.struct C) _ _ _ g f
   -- TODO: make this left associative
-  -- TODO: change this notation?
 
   definition Precategory.eta (C : Precategory) : Precategory.mk C C = C :=
   Precategory.rec (λob c, idp) C
diff --git a/hott/algebra/e_closure.hlean b/hott/algebra/e_closure.hlean
index d511d0f0f..9bcda26ef 100644
--- a/hott/algebra/e_closure.hlean
+++ b/hott/algebra/e_closure.hlean
@@ -18,7 +18,7 @@ inductive e_closure {A : Type} (R : A → A → Type) : A → A → Type :=
 | trans : Π{a a' a''} (r : e_closure R a a') (r' : e_closure R a' a''), e_closure R a a''
 
 namespace e_closure
-  infix `⬝r`:75 := e_closure.trans
+  infix ` ⬝r `:75 := e_closure.trans
   postfix `⁻¹ʳ`:(max+10) := e_closure.symm
   notation `[`:max a `]`:0 := e_closure.of_rel a
   abbreviation rfl {A : Type} {R : A → A → Type} {a : A} := refl R a
diff --git a/hott/algebra/field.hlean b/hott/algebra/field.hlean
index 39751c302..6bb21b744 100644
--- a/hott/algebra/field.hlean
+++ b/hott/algebra/field.hlean
@@ -26,7 +26,7 @@ section division_ring
   include s
 
   definition divide (a b : A) : A := a * b⁻¹
-  infix `/` := divide
+  infix / := divide
 
   -- only in this file
   local attribute divide [reducible]
diff --git a/hott/algebra/group.hlean b/hott/algebra/group.hlean
index 4c1b44bab..c6cb4a665 100644
--- a/hott/algebra/group.hlean
+++ b/hott/algebra/group.hlean
@@ -34,12 +34,12 @@ structure has_inv [class] (A : Type) :=
 structure has_neg [class] (A : Type) :=
 (neg : A → A)
 
-infixl `*`   := has_mul.mul
-infixl `+`   := has_add.add
-postfix `⁻¹` := has_inv.inv
-prefix `-`   := has_neg.neg
-notation 1   := !has_one.one
-notation 0   := !has_zero.zero
+infixl   * := has_mul.mul
+infixl   + := has_add.add
+postfix ⁻¹ := has_inv.inv
+prefix   - := has_neg.neg
+notation 1 := !has_one.one
+notation 0 := !has_zero.zero
 
 --a second notation for the inverse, which is not overloaded
 postfix [parsing-only] `⁻¹ᵍ`:std.prec.max_plus := has_inv.inv
@@ -387,7 +387,7 @@ section add_group
   -- TODO: derive corresponding facts for div in a field
   definition sub [reducible] (a b : A) : A := a + -b
 
-  infix `-` := sub
+  infix - := sub
 
   theorem sub_eq_add_neg (a b : A) : a - b = a + -b := rfl
 
diff --git a/hott/algebra/order.hlean b/hott/algebra/order.hlean
index d9c2c2f13..1f4dd97ea 100644
--- a/hott/algebra/order.hlean
+++ b/hott/algebra/order.hlean
@@ -29,9 +29,9 @@ structure has_le.{l} [class] (A : Type.{l}) : Type.{l+1} :=
 structure has_lt [class] (A : Type) :=
 (lt : A → A → Type₀)
 
-infixl `<=`   := has_le.le
-infixl `≤`   := has_le.le
-infixl `<`   := has_lt.lt
+infixl <=  := has_le.le
+infixl ≤   := has_le.le
+infixl <   := has_lt.lt
 
 definition has_le.ge [reducible] {A : Type} [s : has_le A] (a b : A) := b ≤ a
 notation a ≥ b := has_le.ge a b
diff --git a/hott/init/bool.hlean b/hott/init/bool.hlean
index 545183412..462f10f99 100644
--- a/hott/init/bool.hlean
+++ b/hott/init/bool.hlean
@@ -16,12 +16,12 @@ namespace bool
   definition bor (a b : bool) :=
   bool.rec_on a (bool.rec_on b ff tt) tt
 
-  notation a || b := bor a b
+  infix || := bor
 
   definition band (a b : bool) :=
   bool.rec_on a ff (bool.rec_on b ff tt)
 
-  notation a && b := band a b
+  infix && := band
 
   definition bnot (a : bool) :=
   bool.rec_on a tt ff
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index 37a7a755b..b29987fbb 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -30,7 +30,7 @@ structure equiv (A B : Type) :=
 
 namespace is_equiv
   /- Some instances and closure properties of equivalences -/
-  postfix `⁻¹` := inv
+  postfix ⁻¹ := inv
   /- a second notation for the inverse, which is not overloaded -/
   postfix [parsing-only] `⁻¹ᶠ`:std.prec.max_plus := inv
 
@@ -261,7 +261,7 @@ namespace equiv
   open equiv.ops
   attribute to_is_equiv [instance]
 
-  infix `≃`:25 := equiv
+  infix ` ≃ `:25 := equiv
 
   section
   variables {A B C : Type}
@@ -358,7 +358,7 @@ namespace equiv
 
 
   namespace ops
-    postfix `⁻¹` := equiv.symm -- overloaded notation for inverse
+    postfix ⁻¹ := equiv.symm -- overloaded notation for inverse
   end ops
 end equiv
 
diff --git a/hott/init/function.hlean b/hott/init/function.hlean
index 6f1e4eeb3..cb6e9075f 100644
--- a/hott/init/function.hlean
+++ b/hott/init/function.hlean
@@ -53,15 +53,11 @@ definition curry [reducible] [unfold-full] : (A × B → C) → A → B → C :=
 definition uncurry [reducible] [unfold 5] : (A → B → C) → (A × B → C) :=
 λ f p, match p with (a, b) := f a b end
 
-precedence `∘'`:60
-precedence `on`:1
-precedence `$`:1
 
-
-infixr  ∘                    := compose
-infixr  ∘'                   := dcompose
-infixl  on                   := on_fun
-infixr  $                    := app
+infixr  ` ∘ `            := compose
+infixr  ` ∘' `:60        := dcompose
+infixl  ` on `:1         := on_fun
+infixr  ` $ `:1          := app
 notation f ` -[` op `]- ` g  := combine f op g
 
 end function
diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
index ef7b48ca3..8a0d4902d 100644
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@@ -10,7 +10,7 @@ import init.reserved_notation
 /- not -/
 
 definition not [reducible] (a : Type) := a → empty
-prefix `¬` := not
+prefix ¬ := not
 
 definition absurd {a b : Type} (H₁ : a) (H₂ : ¬a) : b :=
 empty.rec (λ e, b) (H₂ H₁)
@@ -36,7 +36,7 @@ assume Hb : b, absurd (assume Ha : a, Hb) H
 
 /- eq -/
 
-notation a = b := eq a b
+infix = := eq
 definition rfl {A : Type} {a : A} := eq.refl a
 
 namespace eq
@@ -52,9 +52,9 @@ namespace eq
   subst H (refl a)
 
   namespace ops
-    notation H `⁻¹` := symm H --input with \sy or \-1 or \inv
-    notation H1 ⬝ H2 := trans H1 H2
-    notation H1 ▸ H2 := subst H1 H2
+    postfix ⁻¹ := symm --input with \sy or \-1 or \inv
+    infixl ⬝ := trans
+    infixr ▸ := subst
   end ops
 end eq
 
@@ -94,7 +94,7 @@ end lift
 /- ne -/
 
 definition ne {A : Type} (a b : A) := ¬(a = b)
-notation a ≠ b := ne a b
+infix ≠ := ne
 
 namespace ne
   open eq.ops
@@ -132,8 +132,8 @@ end
 
 definition iff (a b : Type) := prod (a → b) (b → a)
 
-notation a <-> b := iff a b
-notation a ↔ b := iff a b
+infix <-> := iff
+infix ↔ := iff
 
 namespace iff
   variables {a b c : Type}
diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 18180e0f7..25071735c 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -559,7 +559,7 @@ namespace eq
   definition inverse2 [unfold 6] {p q : x = y} (h : p = q) : p⁻¹ = q⁻¹ :=
   eq.rec_on h idp
 
-  infixl `◾`:75 := concat2
+  infixl ` ◾ `:75 := concat2
   postfix [parsing-only] `⁻²`:(max+10) := inverse2 --this notation is abusive, should we use it?
 
   /- Whiskering -/
@@ -584,11 +584,11 @@ namespace eq
     whisker_right h idp = h :=
   eq.rec_on h (eq.rec_on p idp)
 
-  definition whisker_right_idp_left (p : x = y) (q : y = z) :
+  definition whisker_right_idp_left [unfold-full] (p : x = y) (q : y = z) :
     whisker_right idp q = idp :> (p ⬝ q = p ⬝ q) :=
   idp
 
-  definition whisker_left_idp_right (p : x = y) (q : y = z) :
+  definition whisker_left_idp_right [unfold-full] (p : x = y) (q : y = z) :
     whisker_left p idp = idp :> (p ⬝ q = p ⬝ q) :=
   idp
 
@@ -596,11 +596,11 @@ namespace eq
     (idp_con p) ⁻¹ ⬝ whisker_left idp h ⬝ idp_con q = h :=
   eq.rec_on h (eq.rec_on p idp)
 
-  definition con2_idp {p q : x = y} (h : p = q) :
+  definition con2_idp [unfold-full] {p q : x = y} (h : p = q) :
     h ◾ idp = whisker_right h idp :> (p ⬝ idp = q ⬝ idp) :=
   idp
 
-  definition idp_con2 {p q : x = y} (h : p = q) :
+  definition idp_con2 [unfold-full] {p q : x = y} (h : p = q) :
     idp ◾ h = whisker_left idp h :> (idp ⬝ p = idp ⬝ q) :=
   idp
 
diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean
index 3a17537bc..5c81c8fab 100644
--- a/hott/init/reserved_notation.hlean
+++ b/hott/init/reserved_notation.hlean
@@ -33,7 +33,7 @@ num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (
 /- Logical operations and relations -/
 
 reserve prefix `¬`:40
-reserve prefix ` ~ `:40
+reserve prefix `~`:40
 reserve infixr ` ∧ `:35
 reserve infixr ` /\ `:35
 reserve infixr ` \/ `:30
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index d13c684af..4d0734091 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -26,8 +26,8 @@ namespace is_trunc
      notation for trunc_index is -2, -1, 0, 1, ...
      from 0 and up this comes from a coercion from num to trunc_index (via nat)
   -/
-  postfix `.+1`:(max+1) := trunc_index.succ
-  postfix `.+2`:(max+1) := λn, (n .+1 .+1)
+  postfix ` .+1`:(max+1) := trunc_index.succ
+  postfix ` .+2`:(max+1) := λn, (n .+1 .+1)
   notation `-2` := trunc_index.minus_two
   notation `-1` := -2.+1 -- ISSUE: -1 gets printed as -2.+1
   export [coercions] nat
@@ -56,7 +56,7 @@ namespace is_trunc
   definition sub_two [reducible] (n : nat) : trunc_index :=
   nat.rec_on n -2 (λ n k, k.+1)
 
-  postfix `.-2`:(max+1) := sub_two
+  postfix ` .-2`:(max+1) := sub_two
 
   /- truncated types -/
 
diff --git a/hott/types/nat/basic.hlean b/hott/types/nat/basic.hlean
index a745067e1..8b80bfbd6 100644
--- a/hott/types/nat/basic.hlean
+++ b/hott/types/nat/basic.hlean
@@ -15,7 +15,7 @@ namespace nat
 
 definition addl (x y : ℕ) : ℕ :=
 nat.rec y (λ n r, succ r) x
-infix `⊕`:65 := addl
+infix ` ⊕ `:65 := addl
 
 definition addl_succ_right (n m : ℕ) : n ⊕ succ m = succ (n ⊕ m) :=
 nat.rec_on n
diff --git a/hott/types/pointed.hlean b/hott/types/pointed.hlean
index c7c2c9f60..c9f535394 100644
--- a/hott/types/pointed.hlean
+++ b/hott/types/pointed.hlean
@@ -74,7 +74,7 @@ namespace pointed
   nat.rec_on n (λA, A) (λn IH A, IH (Loop_space A)) A
 
   prefix `Ω`:(max+5) := Loop_space
-  notation `Ω[`:95 n:0 `]`:0 A:95 := Iterated_loop_space n A
+  notation `Ω[`:95 n:0 `] `:0 A:95 := Iterated_loop_space n A
 
   definition refln [constructor] {A : Type*} {n : ℕ} : Ω[n] A := pt
 
@@ -117,7 +117,7 @@ namespace pointed
 
   abbreviation respect_pt [unfold 3] := @pmap.resp_pt
   notation `map₊` := pmap
-  infix `→*`:30 := pmap
+  infix ` →* `:30 := pmap
   attribute pmap.map [coercion]
   variables {A B C D : Type*} {f g h : A →* B}
 
@@ -137,13 +137,13 @@ namespace pointed
   definition pcompose [constructor] (g : B →* C) (f : A →* B) : A →* C :=
   pmap.mk (λa, g (f a)) (ap g (respect_pt f) ⬝ respect_pt g)
 
-  infixr `∘*`:60 := pcompose
+  infixr ` ∘* `:60 := pcompose
 
   structure phomotopy (f g : A →* B) :=
     (homotopy : f ~ g)
     (homotopy_pt : homotopy pt ⬝ respect_pt g = respect_pt f)
 
-  infix `~*`:50 := phomotopy
+  infix ` ~* `:50 := phomotopy
   abbreviation to_homotopy_pt [unfold 5] := @phomotopy.homotopy_pt
   abbreviation to_homotopy [coercion] [unfold 5] (p : f ~* g) : Πa, f a = g a :=
   phomotopy.homotopy p
@@ -262,7 +262,7 @@ namespace pointed
       induction p', esimp, apply inv_con_cancel_left}
   end
 
-  infix `⬝*`:75 := phomotopy.trans
+  infix ` ⬝* `:75 := phomotopy.trans
   postfix `⁻¹*`:(max+1) := phomotopy.symm
 
   definition eq_of_phomotopy (p : f ~* g) : f = g :=
@@ -295,7 +295,7 @@ namespace pointed
     (to_pmap : A →* B)
     (is_equiv_to_pmap : is_equiv to_pmap)
 
-  infix `≃*`:25 := pequiv
+  infix ` ≃* `:25 := pequiv
   attribute pequiv.to_pmap [coercion]
   attribute pequiv.is_equiv_to_pmap [instance]
 
diff --git a/hott/types/types.md b/hott/types/types.md
index 6fd738289..d774789be 100644
--- a/hott/types/types.md
+++ b/hott/types/types.md
@@ -12,14 +12,16 @@ Types (not necessarily HoTT-related):
 * [sum](sum.hlean)
 * [pi](pi.hlean)
 * [arrow](arrow.hlean)
-* [W](W.hlean): W-types (not loaded by default)
 * [arrow_2](arrow_2.hlean): alternative development of properties of arrows
+* [W](W.hlean): W-types (not loaded by default)
+* [lift](lift.hlean)
 
 HoTT types
 
 * [eq](eq.hlean): show that functions related to the identity type are equivalences
-* [pointed](pointed.hlean)
+* [pointed](pointed.hlean): pointed types, maps, homotopies, and equivalences
 * [fiber](fiber.hlean)
 * [equiv](equiv.hlean)
 * [trunc](trunc.hlean): truncation levels, n-Types, truncation
-
+* [pullback](pullback.hlean)
+* [univ](univ.hlean)
\ No newline at end of file
diff --git a/hott/types/univ.hlean b/hott/types/univ.hlean
index 03ba156df..720e37fad 100644
--- a/hott/types/univ.hlean
+++ b/hott/types/univ.hlean
@@ -47,7 +47,6 @@ namespace univ
   assume H : is_hset Type,
   absurd (is_trunc_is_embedding_closed lift star) not_is_hset_type0
 
-  --set_option pp.notation false
   definition not_double_negation_elimination0 : ¬Π(A : Type₀), ¬¬A → A :=
   begin
     intro f,
diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean
index 62f698afc..41f4ea202 100644
--- a/library/init/reserved_notation.lean
+++ b/library/init/reserved_notation.lean
@@ -33,7 +33,7 @@ num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (
 /- Logical operations and relations -/
 
 reserve prefix `¬`:40
-reserve prefix ` ~ `:40
+reserve prefix `~`:40
 reserve infixr ` ∧ `:35
 reserve infixr ` /\ `:35
 reserve infixr ` \/ `:30