diff --git a/hott/algebra/category/adjoint.hlean b/hott/algebra/category/adjoint.hlean
index 5b19ee3fa..4a92ff589 100644
--- a/hott/algebra/category/adjoint.hlean
+++ b/hott/algebra/category/adjoint.hlean
@@ -20,8 +20,8 @@ namespace category
     (G : D ⇒ C)
     (η : 1 ⟹ G ∘f F)
     (ε : F ∘f G ⟹ 1)
-    (H : Π(c : C), (ε (F c)) ∘ (F (η c)) = ID (F c))
-    (K : Π(d : D), (G (ε d)) ∘ (η (G d)) = ID (G d))
+    (H : Π(c : C), ε (F c) ∘ F (η c) = ID (F c))
+    (K : Π(d : D), G (ε d) ∘ η (G d) = ID (G d))
 
   abbreviation right_adjoint := @is_left_adjoint.G
   abbreviation unit          := @is_left_adjoint.η
@@ -88,7 +88,7 @@ namespace category
     [H : fully_faithful F] (c c' : C) : (c ≅ c') ≃ (F c ≅ F c') :=
   begin
     fapply equiv.MK,
-    { exact preserve_iso F},
+    { exact to_fun_iso F},
     { apply iso_of_F_iso_F},
     { exact abstract begin
       intro f, induction f with f F', induction F' with g p q, apply iso_eq,
@@ -119,18 +119,18 @@ namespace category
                     to_fun_hom G' (natural_map ε d) ∘
                     natural_map η' (to_fun_ob G d) = id,
     { intro d, esimp,
-      rewrite [category.assoc],
+      rewrite [assoc],
       rewrite [-assoc (G (ε' d))],
       esimp, rewrite [nf_fn_eq_fn_nf_pt' G' ε η d],
-      esimp, rewrite [category.assoc],
-      esimp, rewrite [-category.assoc],
+      esimp, rewrite [assoc],
+      esimp, rewrite [-assoc],
       rewrite [↑functor.compose, -respect_comp G],
       rewrite [nf_fn_eq_fn_nf_pt ε ε' d,nf_fn_eq_fn_nf_pt η' η (G d),▸*],
       rewrite [respect_comp G],
-      rewrite [category.assoc,▸*,-category.assoc (G (ε d))],
+      rewrite [assoc,▸*,-assoc (G (ε d))],
       rewrite [↑functor.compose, -respect_comp G],
       rewrite [H' (G d)],
-      rewrite [respect_id,▸*,category.id_right],
+      rewrite [respect_id,▸*,id_right],
       apply K},
     assert lem₃ : Π (d : carrier D),
                     (to_fun_hom G' (natural_map ε d) ∘
@@ -138,17 +138,17 @@ namespace category
                     to_fun_hom G (natural_map ε' d) ∘
                     natural_map η (to_fun_ob G' d) = id,
     { intro d, esimp,
-      rewrite [category.assoc, -assoc (G' (ε d))],
+      rewrite [assoc, -assoc (G' (ε d))],
       esimp, rewrite [nf_fn_eq_fn_nf_pt' G ε' η' d],
-      esimp, rewrite [category.assoc], esimp, rewrite [-category.assoc],
+      esimp, rewrite [assoc], esimp, rewrite [-assoc],
       rewrite [↑functor.compose, -respect_comp G'],
       rewrite [nf_fn_eq_fn_nf_pt ε' ε d,nf_fn_eq_fn_nf_pt η η' (G' d)],
       esimp,
       rewrite [respect_comp G'],
-      rewrite [category.assoc,▸*,-category.assoc (G' (ε' d))],
+      rewrite [assoc,▸*,-assoc (G' (ε' d))],
       rewrite [↑functor.compose, -respect_comp G'],
       rewrite [H (G' d)],
-      rewrite [respect_id,▸*,category.id_right],
+      rewrite [respect_id,▸*,id_right],
       apply K'},
     fapply lem₁,
     { fapply functor.eq_of_pointwise_iso,
@@ -165,7 +165,7 @@ namespace category
       rewrite functor.hom_of_eq_eq_of_pointwise_iso,
       apply nat_trans_eq, intro c, esimp,
       refine !assoc⁻¹ ⬝ ap (λx, _ ∘ x) (nf_fn_eq_fn_nf_pt η η' c) ⬝ !assoc ⬝ _,
-      esimp, rewrite [-respect_comp G',H c,respect_id G',▸*,category.id_left]},
+      esimp, rewrite [-respect_comp G',H c,respect_id G',▸*,id_left]},
    { clear lem₁, refine transport_hom_of_eq_left _ ε ⬝ _,
      krewrite inv_of_eq_compose_left,
      rewrite functor.inv_of_eq_eq_of_pointwise_iso,
@@ -175,7 +175,7 @@ namespace category
    end
 
   definition full_of_fully_faithful (H : fully_faithful F) : full F :=
-  λc c', is_surjective.mk (λg, tr (fiber.mk ((@(to_fun_hom F) c c')⁻¹ᶠ g) !right_inv))
+  λc c' g, tr (fiber.mk ((@(to_fun_hom F) c c')⁻¹ᶠ g) !right_inv)
 
   definition faithful_of_fully_faithful (H : fully_faithful F) : faithful F :=
   λc c' f f' p, is_injective_of_is_embedding p
@@ -198,6 +198,36 @@ namespace category
   end
 
 /-
+  section
+    variables (η : Πc, G (F c) ≅ c) (ε : Πd, F (G d) ≅ d) -- we need some kind of naturality
+    include η ε
+    --definition inverse_of_unit_counit
+
+     private definition adj_η (c : C) : G (F c) ≅ c :=
+     to_fun_iso G (to_fun_iso F (η c)⁻¹ⁱ) ⬝i to_fun_iso G (ε (F c)) ⬝i η c
+     open iso
+
+     private theorem adjointify_adjH (c : C) :
+       to_hom (ε (F c)) ∘ F (to_hom (adj_η η ε c)⁻¹ⁱ) = id  :=
+     begin
+       exact sorry
+     end
+
+     private theorem adjointify_adjK (d : D) :
+       G (to_hom (ε d)) ∘ to_hom (adj_η η ε (G d))⁻¹ⁱ = id :=
+     begin
+       exact sorry
+     end
+
+    variables (F G)
+    definition is_equivalence.mk : is_equivalence F :=
+    begin
+      fconstructor,
+      { exact G},
+      { }
+    end
+
+  end
 
   definition fully_faithful_of_is_equivalence (F : C ⇒ D) [H : is_equivalence F]
     : fully_faithful F :=
@@ -212,19 +242,6 @@ namespace category
     { exact sorry},
   end
 
-  section
-    variables (F G)
-    variables (η : G ∘f F ≅ 1) (ε : F ∘f G ≅ 1)
-    include η ε
-    --definition inverse_of_unit_counit
-
-    definition is_equivalence.mk : is_equivalence F :=
-    begin
-      exact sorry
-    end
-
-  end
-
   definition fully_faithful_equiv (F : C ⇒ D) : fully_faithful F ≃ (faithful F × full F) :=
   sorry
 
diff --git a/hott/algebra/category/category.hlean b/hott/algebra/category/category.hlean
index f19a47652..b58fa4090 100644
--- a/hott/algebra/category/category.hlean
+++ b/hott/algebra/category/category.hlean
@@ -68,7 +68,6 @@ namespace category
     (struct : category carrier)
 
   attribute Category.struct [instance] [coercion]
-  attribute Category.to.precategory category.to_precategory [constructor]
 
   definition Category.to_Precategory [constructor] [coercion] [reducible] (C : Category)
     : Precategory :=
diff --git a/hott/algebra/category/functor.hlean b/hott/algebra/category/functor.hlean
index 03534abe3..2ac7ca60b 100644
--- a/hott/algebra/category/functor.hlean
+++ b/hott/algebra/category/functor.hlean
@@ -84,30 +84,41 @@ namespace functor
     fapply @is_iso.mk, apply (F (f⁻¹)),
     repeat (apply concat ; symmetry ;  apply (respect_comp F) ;
       apply concat ; apply (ap (λ x, to_fun_hom F x)) ;
-      (apply left_inverse | apply right_inverse);
+      (apply iso.left_inverse | apply iso.right_inverse);
       apply (respect_id F) ),
   end
 
-  definition respect_inv (F : C ⇒ D) {a b : C} (f : hom a b) [H : is_iso f] [H' : is_iso (F f)] :
+  theorem respect_inv (F : C ⇒ D) {a b : C} (f : hom a b) [H : is_iso f] [H' : is_iso (F f)] :
     F (f⁻¹) = (F f)⁻¹ :=
   begin
     fapply @left_inverse_eq_right_inverse, apply (F f),
       transitivity to_fun_hom F (f⁻¹ ∘ f),
         {symmetry, apply (respect_comp F)},
         {transitivity to_fun_hom F category.id,
-          {congruence, apply left_inverse},
+          {congruence, apply iso.left_inverse},
           {apply respect_id}},
-      apply right_inverse
+      apply iso.right_inverse
   end
 
   attribute preserve_is_iso [instance] [priority 100]
 
-  definition preserve_iso [constructor] (F : C ⇒ D) {a b : C} (f : a ≅ b) : F a ≅ F b :=
+  definition to_fun_iso [constructor] (F : C ⇒ D) {a b : C} (f : a ≅ b) : F a ≅ F b :=
   iso.mk (F f)
 
-  definition respect_inv' (F : C ⇒ D) {a b : C} (f : hom a b) {H : is_iso f} : F (f⁻¹) = (F f)⁻¹ :=
+  theorem respect_inv' (F : C ⇒ D) {a b : C} (f : hom a b) {H : is_iso f} : F (f⁻¹) = (F f)⁻¹ :=
   respect_inv F f
 
+  theorem respect_refl (F : C ⇒ D) (a : C) : to_fun_iso F (iso.refl a) = iso.refl (F a) :=
+  iso_eq !respect_id
+
+  theorem respect_symm (F : C ⇒ D) {a b : C} (f : a ≅ b)
+    : to_fun_iso F f⁻¹ⁱ = (to_fun_iso F f)⁻¹ⁱ :=
+  iso_eq !respect_inv
+
+  theorem respect_trans (F : C ⇒ D) {a b c : C} (f : a ≅ b) (g : b ≅ c)
+    : to_fun_iso F (f ⬝i g) = to_fun_iso F f ⬝i to_fun_iso F g :=
+  iso_eq !respect_comp
+
   protected definition assoc (H : C ⇒ D) (G : B ⇒ C) (F : A ⇒ B) :
       H ∘f (G ∘f F) = (H ∘f G) ∘f F :=
   !functor_mk_eq_constant (λa b f, idp)
diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean
index 80129c515..9407aee23 100644
--- a/hott/algebra/category/iso.hlean
+++ b/hott/algebra/category/iso.hlean
@@ -160,6 +160,9 @@ 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
+  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')
       : iso.mk f = iso.mk f' :=
   apd011 iso.mk p !is_hprop.elim
diff --git a/hott/algebra/category/yoneda.hlean b/hott/algebra/category/yoneda.hlean
index fd47f6787..227eef201 100644
--- a/hott/algebra/category/yoneda.hlean
+++ b/hott/algebra/category/yoneda.hlean
@@ -199,6 +199,14 @@ open functor
 
 namespace yoneda
   open category.set nat_trans lift
+
+  /-
+    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
+    in a Category to category.category.comp g f
+  -/
+  local attribute Category.to.precategory category.to_precategory [constructor]
+
   -- should this be defined as "yoneda_embedding Cᵒᵖ"?
   definition contravariant_yoneda_embedding (C : Precategory) : Cᵒᵖ ⇒ set ^c C :=
   functor_curry !hom_functor
@@ -270,10 +278,10 @@ namespace yoneda
   definition embedding_on_objects_yoneda_embedding (C : Category) :
     is_embedding (ɏ : C → Cᵒᵖ ⇒ set) :=
   begin
-    apply is_embedding.mk, intro c c', fapply is_equiv_of_equiv_of_homotopy,
+    intro c c', fapply is_equiv_of_equiv_of_homotopy,
     { exact !eq_equiv_iso ⬝e !iso_equiv_F_iso_F ⬝e !eq_equiv_iso⁻¹ᵉ},
     { intro p, induction p, esimp [equiv.trans, equiv.symm],
-      esimp [preserve_iso],
+      esimp [to_fun_iso],
       rewrite -eq_of_iso_refl,
       apply ap eq_of_iso, apply iso_eq, esimp,
       apply nat_trans_eq, intro c',
diff --git a/hott/algebra/e_closure.hlean b/hott/algebra/e_closure.hlean
index 97b2365db..d511d0f0f 100644
--- a/hott/algebra/e_closure.hlean
+++ b/hott/algebra/e_closure.hlean
@@ -31,9 +31,9 @@ section
              (R : A → A → Type)
   local abbreviation T := e_closure R
 
-  variables ⦃a a' : A⦄ {s : R a a'} {r : T a a}
+  variables ⦃a a' a'' : A⦄ {s : R a a'} {r : T a a} {B C : Type}
   parameter {R}
-  protected definition e_closure.elim [unfold 8] {B : Type} {f : A → B}
+  protected definition e_closure.elim [unfold 8] {f : A → B}
     (e : Π⦃a a' : A⦄, R a a' → f a = f a') (t : T a a') : f a = f a' :=
   begin
     induction t,
@@ -115,5 +115,52 @@ section
       intro a a' a'' t t', exact t ⬝r t',
   end
 
+  definition e_closure.transport_left {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a')
+    (t : e_closure R a a') (p : a = a'')
+    : e_closure.elim e (p ▸ t) = (ap f p)⁻¹ ⬝ e_closure.elim e t :=
+  by induction p; exact !idp_con⁻¹
+
+  definition e_closure.transport_right {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a')
+    (t : e_closure R a a') (p : a' = a'')
+    : e_closure.elim e (p ▸ t) = e_closure.elim e t ⬝ (ap f p) :=
+  by induction p; reflexivity
+
+  definition e_closure.transport_lr {f : A → B} (e : Π⦃a a' : A⦄, R a a' → f a = f a')
+    (t : e_closure R a a) (p : a = a')
+    : e_closure.elim e (p ▸ t) = (ap f p)⁻¹ ⬝ e_closure.elim e t ⬝ (ap f p) :=
+  by induction p; esimp; exact !idp_con⁻¹
+
+  --dependent elimination:
+
+  variables {P : B → Type} {Q : C → Type} {f : A → B} {g : B → C} {f' : Π(a : A), P (f a)}
+  protected definition e_closure.elimo [unfold 6]
+    (p : Π⦃a a' : A⦄, R a a' → f a = f a')
+    (po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a')
+    (t : T a a') : f' a =[e_closure.elim p t] f' a' :=
+  begin
+    induction t,
+      exact po r,
+      constructor,
+      exact v_0⁻¹ᵒ,
+      exact v_0 ⬝o v_1
+  end
+
+  definition ap_e_closure_elimo_h [unfold 12]  {g' : Πb, Q (g b)}
+    (p : Π⦃a a' : A⦄, R a a' → f a = f a')
+    --(po : Π⦃a a' : A⦄ (s : R a a'), f' a =[p s] f' a')
+    (po : Π⦃a a' : A⦄ (s : R a a'), g' (f a) =[p s] g' (f a'))
+    (q : Π⦃a a' : A⦄ (s : R a a'), apdo g' (p s) = po s)
+    (t : T a a') : apdo g' (e_closure.elim p t) = e_closure.elimo p po t :=
+  begin
+    induction t,
+      apply q,
+      reflexivity,
+      esimp [e_closure.elim],
+      exact apdo_inv g' (e_closure.elim p r) ⬝ v_0⁻²ᵒ,
+      exact apdo_con g' (e_closure.elim p r) (e_closure.elim p r') ⬝ (v_0 ◾o v_1)
+  end
+
+
+
 end
 end relation
diff --git a/hott/book.md b/hott/book.md
index 015bf9b4d..693da6119 100644
--- a/hott/book.md
+++ b/hott/book.md
@@ -19,7 +19,7 @@ The rows indicate the chapters, the columns the sections.
 | Ch 2  | + | + | + | + | . | + | + | + | + | +  | +  | +  | +  | +  | +  |
 | Ch 3  | + | + | + | + | ½ | + | + | - | + | .  | +  |    |    |    |    |
 | Ch 4  | - | + | - | + | . | + | - | - | + |    |    |    |    |    |    |
-| Ch 5  | - | . | - | - | - | . | . | ½ |   |    |    |    |    |    |    |
+| Ch 5  | - | . | ½ | - | - | . | . | ½ |   |    |    |    |    |    |    |
 | Ch 6  | . | + | + | + | + | ½ | ½ | ¼ | ¼ | ¼  | ¾  | -  | .  |    |    |
 | Ch 7  | + | + | + | - | - | - | - |   |   |    |    |    |    |    |    |
 | Ch 8  | ¾ | - | - | - | - | - | - | - | - | -  |    |    |    |    |    |
@@ -27,7 +27,7 @@ The rows indicate the chapters, the columns the sections.
 | Ch 10 | - | - | - | - | - |   |   |   |   |    |    |    |    |    |    |
 | Ch 11 | - | - | - | - | - | - |   |   |   |    |    |    |    |    |    |
 
-Things not in the book:
+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).
 
@@ -99,7 +99,7 @@ Chapter 5: Induction
 
 - 5.1 (Introduction to inductive types): not formalized
 - 5.2 (Uniqueness of inductive types): no formalizable content
-- 5.3 (W-types): related: [types.W](types/W.hlean)
+- 5.3 (W-types): [types.W](types/W.hlean) defines W-types.
 - 5.4 (Inductive types are initial algebras): not formalized
 - 5.5 (Homotopy-inductive types): not formalized
 - 5.6 (The general syntax of inductive definitions): no formalizable content
diff --git a/hott/cubical/square.hlean b/hott/cubical/square.hlean
index 0b4d24e11..8b023ea9e 100644
--- a/hott/cubical/square.hlean
+++ b/hott/cubical/square.hlean
@@ -64,7 +64,7 @@ namespace eq
     square p p₁₂ p₀₁ p₂₁ :=
   by induction r; exact s₁₁
 
-  definition vconcat_eq [unfold 11] {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) :
+  definition vconcat_eq [unfold 12] {p : a₀₂ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₁₂ = p) :
     square p₁₀ p p₀₁ p₂₁ :=
   by induction r; exact s₁₁
 
@@ -72,11 +72,10 @@ namespace eq
     square p₁₀ p₁₂ p p₂₁ :=
   by induction r; exact s₁₁
 
-  definition hconcat_eq [unfold 11] {p : a₂₀ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p) :
+  definition hconcat_eq [unfold 12] {p : a₂₀ = a₂₂} (s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁) (r : p₂₁ = p) :
     square p₁₀ p₁₂ p₀₁ p :=
   by induction r; exact s₁₁
 
-
   infix `⬝h`:75 := hconcat
   infix `⬝v`:75 := vconcat
   infix `⬝hp`:75 := hconcat_eq
diff --git a/hott/cubical/squareover.hlean b/hott/cubical/squareover.hlean
index 21cefa212..41b51adc1 100644
--- a/hott/cubical/squareover.hlean
+++ b/hott/cubical/squareover.hlean
@@ -32,7 +32,9 @@ namespace eq
             /-a₀₂-/ {p₁₂ : a₀₂ = a₂₂} /-a₂₂-/ {p₃₂ : a₂₂ = a₄₂} /-a₄₂-/
        {p₀₃ : a₀₂ = a₀₄} /-s₁₃-/ {p₂₃ : a₂₂ = a₂₄} /-s₃₃-/ {p₄₃ : a₄₂ = a₄₄}
             /-a₀₄-/ {p₁₄ : a₀₄ = a₂₄} /-a₂₄-/ {p₃₄ : a₂₄ = a₄₄} /-a₄₄-/
-            {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁}
+            {s₁₁ : square p₁₀ p₁₂ p₀₁ p₂₁} {s₃₁ : square p₃₀ p₃₂ p₂₁ p₄₁}
+            {s₁₃ : square p₁₂ p₁₄ p₀₃ p₂₃} {s₃₃ : square p₃₂ p₃₄ p₂₃ p₄₃}
+
             {b₀₀ : B a₀₀} {b₂₀ : B a₂₀} {b₄₀ : B a₄₀}
             {b₀₂ : B a₀₂} {b₂₂ : B a₂₂} {b₄₂ : B a₄₂}
             {b₀₄ : B a₀₄} {b₂₄ : B a₂₄} {b₄₄ : B a₄₄}
@@ -58,12 +60,66 @@ namespace eq
 
   definition vdeg_squareover {q₁₀' : b₀₀ =[p₁₀] b₂₀} (r : q₁₀ = q₁₀')
     : squareover B vrfl q₁₀ q₁₀' idpo idpo :=
-  by induction r;exact vrflo
+  by induction r; exact vrflo
 
   definition hdeg_squareover {q₀₁' : b₀₀ =[p₀₁] b₀₂} (r : q₀₁ = q₀₁')
     : squareover B hrfl idpo idpo q₀₁ q₀₁' :=
   by induction r; exact hrflo
 
+  definition hconcato
+    (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) (t₃₁ : squareover B s₃₁ q₃₀ q₃₂ q₂₁ q₄₁)
+    : squareover B (hconcat s₁₁ s₃₁) (q₁₀ ⬝o q₃₀) (q₁₂ ⬝o q₃₂) q₀₁ q₄₁ :=
+  by induction t₃₁; exact t₁₁
+
+  definition vconcato
+    (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) (t₁₃ : squareover B s₁₃ q₁₂ q₁₄ q₀₃ q₂₃)
+    : squareover B (vconcat s₁₁ s₁₃) q₁₀ q₁₄ (q₀₁ ⬝o q₀₃) (q₂₁ ⬝o q₂₃) :=
+  by induction t₁₃; exact t₁₁
+
+  definition hinverseo (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁)
+    : squareover B (hinverse s₁₁) q₁₀⁻¹ᵒ q₁₂⁻¹ᵒ q₂₁ q₀₁ :=
+  by induction t₁₁; constructor
+
+  definition vinverseo (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁)
+    : squareover B (vinverse s₁₁) q₁₂ q₁₀ q₀₁⁻¹ᵒ q₂₁⁻¹ᵒ :=
+  by induction t₁₁; constructor
+
+  definition eq_vconcato {q : b₀₀ =[p₁₀] b₂₀}
+    (r : q = q₁₀) (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) : squareover B s₁₁ q q₁₂ q₀₁ q₂₁ :=
+  by induction r; exact t₁₁
+
+  definition vconcato_eq {q : b₀₂ =[p₁₂] b₂₂}
+    (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) (r : q₁₂ = q) : squareover B s₁₁ q₁₀ q q₀₁ q₂₁ :=
+  by induction r; exact t₁₁
+
+  definition eq_hconcato {q : b₀₀ =[p₀₁] b₀₂}
+    (r : q = q₀₁) (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) : squareover B s₁₁ q₁₀ q₁₂ q q₂₁ :=
+  by induction r; exact t₁₁
+
+  definition hconcato_eq {q : b₂₀ =[p₂₁] b₂₂}
+    (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) (r : q₂₁ = q) : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q :=
+  by induction r; exact t₁₁
+
+  definition pathover_vconcato {p : a₀₀ = a₂₀} {sp : p = p₁₀} {q : b₀₀ =[p] b₂₀}
+    (r : change_path sp q = q₁₀) (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁)
+    : squareover B (sp ⬝pv s₁₁) q q₁₂ q₀₁ q₂₁ :=
+  by induction sp; induction r; exact t₁₁
+
+  definition vconcato_pathover {p : a₀₂ = a₂₂} {sp : p₁₂ = p} {q : b₀₂ =[p] b₂₂}
+    (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) (r : change_path sp q₁₂ = q)
+    : squareover B (s₁₁ ⬝vp sp) q₁₀ q q₀₁ q₂₁ :=
+  by induction sp; induction r; exact t₁₁
+
+  definition pathover_hconcato {p : a₀₀ = a₀₂} {sp : p = p₀₁} {q : b₀₀ =[p] b₀₂}
+    (r : change_path sp q = q₀₁) (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) :
+    squareover B (sp ⬝ph s₁₁) q₁₀ q₁₂ q q₂₁ :=
+  by induction sp; induction r; exact t₁₁
+
+  definition hconcato_pathover {p : a₂₀ = a₂₂} {sp : p₂₁ = p} {q : b₂₀ =[p] b₂₂}
+    (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) (r : change_path sp q₂₁ = q) :
+    squareover B (s₁₁ ⬝hp sp) q₁₀ q₁₂ q₀₁ q :=
+  by induction sp; induction r; exact t₁₁
+
   -- relating squareovers to squares
   definition square_of_squareover (t₁₁ : squareover B s₁₁ q₁₀ q₁₂ q₀₁ q₂₁) :
     square (!con_tr ⬝ ap (λa, p₂₁ ▸ a) (tr_eq_of_pathover q₁₀))
diff --git a/hott/eq2.hlean b/hott/eq2.hlean
index 33906e227..1942e40cc 100644
--- a/hott/eq2.hlean
+++ b/hott/eq2.hlean
@@ -12,8 +12,8 @@ open function
 namespace eq
   variables {A B C : Type} {f : A → B} {a a' a₁ a₂ a₃ a₄ : A} {b b' : B}
 
-  theorem ap_weakly_constant_eq (p : Πx, f x = b) (q : a = a') :
-      ap_weakly_constant p q =
+  theorem ap_is_constant_eq (p : Πx, f x = b) (q : a = a') :
+      ap_is_constant p q =
       eq_con_inv_of_con_eq ((eq_of_square (square_of_pathover (apdo p q)))⁻¹ ⬝
       whisker_left (p a) (ap_constant q b)) :=
   begin
@@ -48,10 +48,10 @@ namespace eq
            idp :=
   by cases p;apply vrefl
 
-  theorem ap_ap_weakly_constant {A B C : Type} (g : B → C) {f : A → B} {b : B}
+  theorem ap_ap_is_constant {A B C : Type} (g : B → C) {f : A → B} {b : B}
     (p : Πx, f x = b) {x y : A} (q : x = y) :
-    square (ap (ap g) (ap_weakly_constant p q))
-           (ap_weakly_constant (λa, ap g (p a)) q)
+    square (ap (ap g) (ap_is_constant p q))
+           (ap_is_constant (λa, ap g (p a)) q)
            (ap_compose g f q)⁻¹
            (!ap_con ⬝ whisker_left _ !ap_inv) :=
   begin
diff --git a/hott/function.hlean b/hott/function.hlean
index da8d06fa9..fc2de6aa2 100644
--- a/hott/function.hlean
+++ b/hott/function.hlean
@@ -7,39 +7,48 @@ Ported from Coq HoTT
 Theorems about embeddings and surjections
 -/
 
-import hit.trunc types.equiv
+import hit.trunc types.equiv cubical.square
 
 open equiv sigma sigma.ops eq trunc is_trunc pi is_equiv fiber prod
 
-variables {A B : Type} {f : A → B} {b : B}
+variables {A B : Type} (f : A → B) {b : B}
 
-structure is_embedding [class] (f : A → B) :=
-(elim : Π(a a' : A), is_equiv (ap f : a = a' → f a = f a'))
+definition is_embedding [class] (f : A → B) := Π(a a' : A), is_equiv (ap f : a = a' → f a = f a')
 
-structure is_surjective [class] (f : A → B) :=
-(elim : Π(b : B), ∥ fiber f b ∥)
+definition is_surjective [class] (f : A → B) := Π(b : B), ∥ fiber f b ∥
 
-structure is_split_surjective [class] (f : A → B) :=
-(elim : Π(b : B), fiber f b)
+definition is_split_surjective [class] (f : A → B) := Π(b : B), fiber f b
 
 structure is_retraction [class] (f : A → B) :=
   (sect : B → A)
   (right_inverse : Π(b : B), f (sect b) = b)
 
-definition is_weakly_constant [class] (f : A → B) (a a' : A) := f a = f a'
+structure is_section [class] (f : A → B) :=
+  (retr : B → A)
+  (left_inverse : Π(a : A), retr (f a) = a)
+
+definition is_weakly_constant [class] (f : A → B) := Π(a a' : A), f a = f a'
 
 structure is_constant [class] (f : A → B) :=
   (pt : B)
   (eq : Π(a : A), f a = pt)
 
-structure conditionally_constant [class] (f : A → B) :=
+structure is_conditionally_constant [class] (f : A → B) :=
   (g : ∥A∥ → B)
   (eq : Π(a : A), f a = g (tr a))
 
 namespace function
 
-  attribute is_embedding.elim [instance]
+  abbreviation sect          [unfold 4] := @is_retraction.sect
+  abbreviation right_inverse [unfold 4] := @is_retraction.right_inverse
+  abbreviation retr          [unfold 4] := @is_section.retr
+  abbreviation left_inverse  [unfold 4] := @is_section.left_inverse
 
+  definition is_equiv_ap_of_embedding [instance] [H : is_embedding f] (a a' : A)
+    : is_equiv (ap f : a = a' → f a = f a') :=
+  H a a'
+
+  variable {f}
   definition is_injective_of_is_embedding [reducible] [H : is_embedding f] {a a' : A}
     : f a = f a' → a = a' :=
   (ap f)⁻¹
@@ -47,29 +56,18 @@ namespace function
   definition is_embedding_of_is_injective [HA : is_hset A] [HB : is_hset B]
     (H : Π(a a' : A), f a = f a' → a = a') : is_embedding f :=
   begin
-  fapply is_embedding.mk,
   intro a a',
   fapply adjointify,
     {exact (H a a')},
     {intro p, apply is_hset.elim},
     {intro p, apply is_hset.elim}
   end
+  variable (f)
 
-  definition is_hprop_is_embedding [instance] (f : A → B) : is_hprop (is_embedding f) :=
-  begin
-    have H : (Π(a a' : A), is_equiv (@ap A B f a a')) ≃ is_embedding f,
-    begin
-      fapply equiv.MK,
-        {exact is_embedding.mk},
-        {intro h, cases h, exact elim},
-        {intro h, cases h, apply idp},
-        {intro p, apply idp},
-    end,
-    apply is_trunc_equiv_closed,
-    exact H,
-  end
+  definition is_hprop_is_embedding [instance] : is_hprop (is_embedding f) :=
+  by unfold is_embedding; exact _
 
-  definition is_hprop_fiber_of_is_embedding (f : A → B) [H : is_embedding f] (b : B) :
+  definition is_hprop_fiber_of_is_embedding [H : is_embedding f] (b : B) :
     is_hprop (fiber f b) :=
   begin
     apply is_hprop.mk, intro v w,
@@ -79,65 +77,72 @@ namespace function
     { esimp [is_injective_of_is_embedding], symmetry, apply right_inv}
   end
 
+  variable {f}
   definition is_surjective_rec_on {P : Type} (H : is_surjective f) (b : B) [Pt : is_hprop P]
     (IH : fiber f b → P) : P :=
-  trunc.rec_on (is_surjective.elim f b) IH
+  trunc.rec_on (H b) IH
+  variable (f)
 
   definition is_surjective_of_is_split_surjective [instance] [H : is_split_surjective f]
     : is_surjective f :=
-  is_surjective.mk (λb, tr (is_split_surjective.elim f b))
+  λb, tr (H b)
 
-  definition is_hprop_is_surjective [instance] (f : A → B) : is_hprop (is_surjective f) :=
+  definition is_hprop_is_surjective [instance] : is_hprop (is_surjective f) :=
+  by unfold is_surjective; exact _
+
+  definition is_weakly_constant_ap [instance] [H : is_weakly_constant f] (a a' : A) :
+    is_weakly_constant (ap f : a = a' → f a = f a') :=
+  take p q : a = a',
+  have Π{b c : A} {r : b = c}, (H a b)⁻¹ ⬝ H a c = ap f r, from
+    (λb c r, eq.rec_on r !con.left_inv),
+  this⁻¹ ⬝ this
+
+  definition is_constant_ap [unfold 4] [instance] [H : is_constant f] (a a' : A)
+    : is_constant (ap f : a = a' → f a = f a') :=
   begin
-    have H : (Π(b : B), merely (fiber f b)) ≃ is_surjective f,
-    begin
-      fapply equiv.MK,
-        {exact is_surjective.mk},
-        {intro h, cases h, exact elim},
-        {intro h, cases h, apply idp},
-        {intro p, apply idp},
-    end,
-    apply is_trunc_equiv_closed,
-    exact H,
+    induction H with b q,
+    fapply is_constant.mk,
+    { exact q a ⬝ (q a')⁻¹},
+    { intro p, induction p, exact !con.right_inv⁻¹}
   end
 
-  -- definition is_hprop_is_split_surjective [instance] (f : A → B) : is_hprop (is_split_surjective f) :=
-  -- begin
-  --   have H : (Π(b : B), fiber f b) ≃ is_split_surjective f,
-  --   begin
-  --     fapply equiv.MK,
-  --       {exact is_split_surjective.mk},
-  --       {intro h, cases h, exact elim},
-  --       {intro h, cases h, apply idp},
-  --       {intro p, apply idp},
-  --   end,
-  --   apply is_trunc_equiv_closed,
-  --   exact H,
-  --   apply is_trunc_pi, intro b,
-  --   apply is_trunc_equiv_closed_rev,
-  --   apply fiber.sigma_char,
-  -- end
+  definition is_contr_is_retraction [instance] [H : is_equiv f] : is_contr (is_retraction f) :=
+  begin
+    have H2 : (Σ(g : B → A), Πb, f (g b) = b) ≃ is_retraction f,
+    begin
+      fapply equiv.MK,
+        {intro x, induction x with g p, constructor, exact p},
+        {intro h, induction h, apply sigma.mk, assumption},
+        {intro h, induction h, reflexivity},
+        {intro x, induction x, reflexivity},
+    end,
+    apply is_trunc_equiv_closed, exact H2,
+    apply is_equiv.is_contr_right_inverse
+  end
 
-  -- definition is_hprop_is_retraction [instance] (f : A → B) : is_hprop (is_retraction f) :=
-  -- begin
-  --   have H : (Σ(g : B → A), Πb, f (g b) = b) ≃ is_retraction f,
-  --   begin
-  --     fapply equiv.MK,
-  --       {intro x, induction x with g p, constructor, exact p},
-  --       {intro h, induction h, apply sigma.mk, assumption},
-  --       {intro h, induction h, reflexivity},
-  --       {intro x, induction x, reflexivity},
-  --   end,
-  --   apply is_trunc_equiv_closed,
-  --   exact H,
-  --   apply is_trunc_of_imp_is_trunc, intro x, induction x with g p,
-  --   apply is_contr_right_inverse
-  -- end
+  definition is_contr_is_section [instance] [H : is_equiv f] : is_contr (is_section f) :=
+  begin
+    have H2 : (Σ(g : B → A), Πa, g (f a) = a) ≃ is_section f,
+    begin
+      fapply equiv.MK,
+        {intro x, induction x with g p, constructor, exact p},
+        {intro h, induction h, apply sigma.mk, assumption},
+        {intro h, induction h, reflexivity},
+        {intro x, induction x, reflexivity},
+    end,
+    apply is_trunc_equiv_closed, exact H2,
+    fapply is_trunc_equiv_closed,
+      {apply sigma_equiv_sigma_id, intro g, apply eq_equiv_homotopy},
+    fapply is_trunc_equiv_closed,
+      {apply fiber.sigma_char},
+    fapply is_contr_fiber_of_is_equiv,
+    exact to_is_equiv (arrow_equiv_arrow_left_rev A (equiv.mk f H)),
+  end
 
-  definition is_embedding_of_is_equiv [instance] (f : A → B) [H : is_equiv f] : is_embedding f :=
-  is_embedding.mk _
+  definition is_embedding_of_is_equiv [instance] [H : is_equiv f] : is_embedding f :=
+  λa a', _
 
-  definition is_equiv_of_is_surjective_of_is_embedding (f : A → B)
+  definition is_equiv_of_is_surjective_of_is_embedding
     [H : is_embedding f] [H' : is_surjective f] : is_equiv f :=
   @is_equiv_of_is_contr_fun _ _ _
     (λb, is_surjective_rec_on H' b
@@ -146,4 +151,92 @@ namespace function
           fiber_eq ((ap f)⁻¹ ((point_eq a) ⬝ (point_eq a')⁻¹))
                    (by rewrite (right_inv (ap f)); rewrite inv_con_cancel_right))))
 
+  definition is_split_surjective_of_is_retraction [H : is_retraction f] : is_split_surjective f :=
+  λb, fiber.mk (sect f b) (right_inverse f b)
+
+  definition is_constant_compose_point [constructor] [instance] (b : B)
+    : is_constant (f ∘ point : fiber f b → B) :=
+  is_constant.mk b (λv, by induction v with a p;exact p)
+
+  definition is_embedding_of_is_hprop_fiber [H : Π(b : B), is_hprop (fiber f b)] : is_embedding f :=
+  begin
+    intro a a',
+    fapply adjointify,
+    { intro p, exact ap point (is_hprop.elim (fiber.mk a p) (fiber.mk a' idp))},
+    { exact abstract begin
+      intro p, rewrite [-ap_compose],
+      apply @is_constant.eq _ _ _ (is_constant_ap (f ∘ point) (fiber.mk a p) (fiber.mk a' idp))
+      end end },
+    { intro p, induction p, rewrite [▸*,is_hprop_elim_self]},
+  end
+
+  -- definition is_embedding_of_is_section_inv' [H : is_section f] {a : A} {b : B} (p : f a = b) :
+  --   a = retr f b :=
+  -- (left_inverse f a)⁻¹ ⬝ ap (retr f) p
+
+  -- definition is_embedding_of_is_section_inv [H : is_section f] {a a' : A} (p : f a = f a') :
+  --   a = a' :=
+  -- is_embedding_of_is_section_inv' f p ⬝ left_inverse f a'
+
+  -- definition is_embedding_of_is_section [constructor] [instance] [H : is_section f]
+  --   : is_embedding f :=
+  -- begin
+  --   intro a a',
+  --   fapply adjointify,
+  --   { exact is_embedding_of_is_section_inv f},
+  --   { exact abstract begin
+  --     assert H2 : Π {b : B} (p : f a = b), ap f (is_embedding_of_is_section_inv' f p) = p ⬝ _,
+  --     { }
+  --           -- intro p, rewrite [+ap_con,-ap_compose],
+  --           -- check_expr natural_square (left_inverse f),
+  --           -- induction H with g q, esimp,
+  --           end end },
+  --   { intro p, induction p, esimp, apply con.left_inv},
+  -- end
+
+  definition is_retraction_of_is_equiv [instance] [H : is_equiv f] : is_retraction f :=
+  is_retraction.mk f⁻¹ (right_inv f)
+
+  definition is_section_of_is_equiv [instance] [H : is_equiv f] : is_section f :=
+  is_section.mk f⁻¹ (left_inv f)
+
+  definition is_equiv_of_is_section_of_is_retraction [H1 : is_retraction f] [H2 : is_section f]
+    : is_equiv f :=
+  let g := sect f in let h := retr f in
+  adjointify f
+             (g)
+             (right_inverse f)
+             (λa, calc
+                    g (f a) = h (f (g (f a))) : left_inverse
+                    ... = h (f a) : right_inverse f
+                    ... = a : left_inverse)
+
+  section
+    local attribute is_equiv_of_is_section_of_is_retraction [instance]
+    variable (f)
+    definition is_hprop_is_retraction_prod_is_section : is_hprop (is_retraction f × is_section f) :=
+    begin
+      apply is_hprop_of_imp_is_contr, intro H, induction H with H1 H2,
+      exact _,
+    end
+  end
+
+  variable {f}
+
+  local attribute is_hprop_is_retraction_prod_is_section [instance]
+  definition is_retraction_prod_is_section_equiv_is_equiv
+    : (is_retraction f × is_section f) ≃ is_equiv f :=
+  begin
+    apply equiv_of_is_hprop,
+    intro H, induction H, apply is_equiv_of_is_section_of_is_retraction,
+    intro H, split, repeat exact _
+  end
+
+  /-
+    The definitions
+      is_surjective_of_is_equiv
+      is_equiv_equiv_is_embedding_times_is_surjective
+    are in types.trunc
+  -/
+
 end function
diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean
index f7c810600..724cb4670 100644
--- a/hott/hit/two_quotient.hlean
+++ b/hott/hit/two_quotient.hlean
@@ -9,6 +9,26 @@ import hit.circle eq2 algebra.e_closure cubical.cube
 
 open quotient eq circle sum sigma equiv function relation
 
+  /-
+    This files defines a general class of nonrecursive HITs using just quotients.
+    We can define any HIT X which has
+    - a single 0-constructor
+       f : A → X (for some type A)
+    - a single 1-constructor
+       e : Π{a a' : A}, R a a' → a = a' (for some (type-valued) relation R on A)
+    and furthermore has 2-constructors which are all of the form
+    p = p'
+    where p, p' are of the form
+    - refl (f a), for some a : A;
+    - e r, for some r : R a a';
+    - ap f q, where q : a = a';
+    - inverses of such paths;
+    - concatenations of such paths.
+
+    so an example 2-constructor could be (as long as it typechecks):
+      ap f q' ⬝ ((e r)⁻¹ ⬝ ap f q)⁻¹ ⬝ e r' = idp
+  -/
+
 namespace simple_two_quotient
 
   section
@@ -73,7 +93,8 @@ namespace simple_two_quotient
   ap_e_closure_elim_h e (elim_e Pj Pa Pe) t
 
   inductive simple_two_quotient_rel : C → C → Type :=
-  | Rmk {} : Π{a : A} {r : T a a} (q : Q r) (x : circle), simple_two_quotient_rel (f q x) (pre_aux q)
+  | Rmk {} : Π{a : A} {r : T a a} (q : Q r) (x : circle),
+               simple_two_quotient_rel (f q x) (pre_aux q)
 
   open simple_two_quotient_rel
   definition simple_two_quotient := quotient simple_two_quotient_rel
@@ -84,7 +105,7 @@ namespace simple_two_quotient
   definition incl1 (s : R a a') : incl0 a = incl0 a' := ap i (e s)
   definition inclt (t : T a a') : incl0 a = incl0 a' := e_closure.elim incl1 t
   -- "wrong" version inclt, which is ap i (p ⬝ q) instead of ap i p ⬝ ap i q
-  -- it is used in the proof, because inclt is easier to work with
+  -- it is used in the proof, because incltw is easier to work with
   protected definition incltw (t : T a a') : incl0 a = incl0 a' := ap i (et t)
 
   protected definition inclt_eq_incltw (t : T a a') : inclt t = incltw t :=
@@ -96,7 +117,7 @@ namespace simple_two_quotient
   protected definition incl2w (q : Q r) : incltw r = idp :=
   (ap02 i (elim_loop (j a) (et r))⁻¹) ⬝
   (ap_compose i (f q) loop)⁻¹ ⬝
-  ap_weakly_constant (incl2' q) loop ⬝
+  ap_is_constant (incl2' q) loop ⬝
   !con.right_inv
 
   definition incl2 (q : Q r) : inclt r = idp :=
@@ -187,11 +208,11 @@ namespace simple_two_quotient
     xrewrite [eq_top_of_square
                ((ap_compose_natural (elim P0 P1 P2) i (elim_loop (j a) (et r)))⁻¹ʰ⁻¹ᵛ ⬝h
                (ap_ap_compose (elim P0 P1 P2) i (f q) loop)⁻¹ʰ⁻¹ᵛ ⬝h
-               ap_ap_weakly_constant (elim P0 P1 P2) (incl2' q) loop ⬝h
+               ap_ap_is_constant (elim P0 P1 P2) (incl2' q) loop ⬝h
                ap_con_right_inv_sq (elim P0 P1 P2) (incl2' q base)),
                ↑[elim_incltw]],
     apply whisker_tl,
-    rewrite [ap_weakly_constant_eq],
+    rewrite [ap_is_constant_eq],
     xrewrite [naturality_apdo_eq (λx, !elim_eq_of_rel) loop],
     rewrite [↑elim_2,rec_loop,square_of_pathover_concato_eq,square_of_pathover_eq_concato,
             eq_of_square_vconcat_eq,eq_of_square_eq_vconcat],
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index aceafdf58..37a7a755b 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -72,7 +72,7 @@ namespace is_equiv
   private abbreviation adjointify_left_inv' (a : A) : g (f a) = a :=
   ap g (ap f (inverse (sec a))) ⬝ ap g (ret (f a)) ⬝ sec a
 
-  private definition adjointify_adj' (a : A) : ret (f a) = ap f (adjointify_left_inv' a) :=
+  private theorem adjointify_adj' (a : A) : ret (f a) = ap f (adjointify_left_inv' a) :=
   let fgretrfa := ap f (ap g (ret (f a))) in
   let fgfinvsect := ap f (ap g (ap f (sec a)⁻¹)) in
   let fgfa := f (g (f a)) in
diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean
index ace75b6ca..72b1ce5a8 100644
--- a/hott/init/pathover.hlean
+++ b/hott/init/pathover.hlean
@@ -9,9 +9,9 @@ Basic theorems about pathovers
 prelude
 import .path .equiv
 
-open equiv is_equiv equiv.ops
+open equiv is_equiv equiv.ops function
 
-variables {A A' : Type} {B B' : A → Type} {C : Π⦃a⦄, B a → Type}
+variables {A A' : Type} {B B' : A → Type} {B'' : A' → Type} {C : Π⦃a⦄, B a → Type}
           {a a₂ a₃ a₄ : A} {p p' : a = a₂} {p₂ : a₂ = a₃} {p₃ : a₃ = a₄}
           {b b' : B a} {b₂ b₂' : B a₂} {b₃ : B a₃} {b₄ : B a₄}
           {c : C b} {c₂ : C b₂}
@@ -27,16 +27,16 @@ namespace eq
 
   /- equivalences with equality using transport -/
   definition pathover_of_tr_eq [unfold 5 8] (r : p ▸ b = b₂) : b =[p] b₂ :=
-  by cases p; cases r; exact idpo
+  by cases p; cases r; constructor
 
   definition pathover_of_eq_tr [unfold 5 8] (r : b = p⁻¹ ▸ b₂) : b =[p] b₂ :=
-  by cases p; cases r; exact idpo
+  by cases p; cases r; constructor
 
   definition tr_eq_of_pathover [unfold 8] (r : b =[p] b₂) : p ▸ b = b₂ :=
-  by cases r; exact idp
+  by cases r; reflexivity
 
   definition eq_tr_of_pathover [unfold 8] (r : b =[p] b₂) : b = p⁻¹ ▸ b₂ :=
-  by cases r; exact idp
+  by cases r; reflexivity
 
   definition pathover_equiv_tr_eq [constructor] (p : a = a₂) (b : B a) (b₂ : B a₂)
     : (b =[p] b₂) ≃ (p ▸ b = b₂) :=
@@ -59,10 +59,10 @@ namespace eq
   end
 
   definition pathover_tr [unfold 5] (p : a = a₂) (b : B a) : b =[p] p ▸ b :=
-  by cases p;exact idpo
+  by cases p;constructor
 
   definition tr_pathover [unfold 5] (p : a = a₂) (b : B a₂) : p⁻¹ ▸ b =[p] b :=
-  by cases p;exact idpo
+  by cases p;constructor
 
   definition concato [unfold 12] (r : b =[p] b₂) (r₂ : b₂ =[p₂] b₃) : b =[p ⬝ p₂] b₃ :=
   pathover.rec_on r₂ r
@@ -73,9 +73,6 @@ namespace eq
   definition apdo [unfold 6] (f : Πa, B a) (p : a = a₂) : f a =[p] f a₂ :=
   eq.rec_on p idpo
 
-  definition oap [unfold 6] {C : A → Type} (f : Πa, B a → C a) (p : a = a₂) : f a =[p] f a₂ :=
-  eq.rec_on p idpo
-
   definition concato_eq [unfold 10] (r : b =[p] b₂) (q : b₂ = b₂') : b =[p] b₂' :=
   eq.rec_on q r
 
@@ -115,15 +112,15 @@ namespace eq
   by cases q;reflexivity
 
   definition pathover_of_eq {a' a₂' : A'} (q : a' = a₂') : a' =[p] a₂' :=
-  by cases p;cases q;exact idpo
+  by cases p;cases q;constructor
 
   definition pathover_constant [constructor] (p : a = a₂) (a' a₂' : A') : a' =[p] a₂' ≃ a' = a₂' :=
   begin
     fapply equiv.MK,
     { exact eq_of_pathover},
     { exact pathover_of_eq},
-    { intro r, cases p, cases r, exact idp},
-    { intro r, cases r, exact idp},
+    { intro r, cases p, cases r, reflexivity},
+    { intro r, cases r, reflexivity},
   end
 
   definition eq_of_pathover_idp [unfold 6] {b' : B a} (q : b =[idpath a] b') : b = b' :=
@@ -166,7 +163,7 @@ namespace eq
   --pathover with fibration B' ∘ f
   definition pathover_ap [unfold 10] (B' : A' → Type) (f : A → A') {p : a = a₂}
     {b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[p] b₂) : b =[ap f p] b₂ :=
-  by cases q; exact idpo
+  by cases q; constructor
 
   definition pathover_of_pathover_ap (B' : A' → Type) (f : A → A') {p : a = a₂}
     {b : B' (f a)} {b₂ : B' (f a₂)} (q : b =[ap f p] b₂) : b =[p] b₂ :=
@@ -179,15 +176,15 @@ namespace eq
     { apply pathover_ap},
     { apply pathover_of_pathover_ap},
     { intro q, cases p, esimp, apply (idp_rec_on q), apply idp},
-    { intro q, cases q, exact idp},
+    { intro q, cases q, reflexivity},
   end
 
   definition apdo_con (f : Πa, B a) (p : a = a₂) (q : a₂ = a₃)
     : apdo f (p ⬝ q) = apdo f p ⬝o apdo f q :=
-  by cases p; cases q; exact idp
+  by cases p; cases q; reflexivity
 
   definition apdo_inv (f : Πa, B a) (p : a = a₂) : apdo f p⁻¹ = (apdo f p)⁻¹ᵒ :=
-  by cases p; exact idp
+  by cases p; reflexivity
 
   definition apdo_eq_pathover_of_eq_ap (f : A → A') (p : a = a₂) :
     apdo f p = pathover_of_eq (ap f p) :=
@@ -215,13 +212,13 @@ namespace eq
   by induction q;reflexivity
   variable {C}
 
-  definition apo (f : Πa, B a → B' a) {Ha : a = a₂} (Hb : b =[Ha] b₂)
-      : f a b =[Ha] f a₂ b₂ :=
-  by induction Hb; exact idpo
+  definition apo {f : A → A'} (g : Πa, B a → B'' (f a))
+    (q : b =[p] b₂) : g a b =[p] g a₂ b₂ :=
+  by induction q; constructor
 
   definition apo011 (f : Πa, B a → A') (Ha : a = a₂) (Hb : b =[Ha] b₂)
       : f a b = f a₂ b₂ :=
-  by cases Hb; exact idp
+  by cases Hb; reflexivity
 
   definition apo0111 (f : Πa b, C b → A') (Ha : a = a₂) (Hb : b =[Ha] b₂)
     (Hc : c =[apo011 C Ha Hb] c₂) : f a b c = f a₂ b₂ c₂ :=
@@ -229,15 +226,23 @@ namespace eq
 
   definition apo11 {f : Πb, C b} {g : Πb₂, C b₂} (r : f =[p] g)
     {b : B a} {b₂ : B a₂} (q : b =[p] b₂) : f b =[apo011 C p q] g b₂ :=
-  by cases r; apply (idp_rec_on q); exact idpo
+  by cases r; apply (idp_rec_on q); constructor
 
   definition apdo10 {f : Πb, C b} {g : Πb₂, C b₂} (r : f =[p] g)
     (b : B a) : f b =[apo011 C p !pathover_tr] g (p ▸ b) :=
-  by cases r; exact idpo
+  by cases r; constructor
 
   definition apo10 {f : B a → B' a} {g : B a₂ → B' a₂} (r : f =[p] g)
     (b : B a) : f b =[p] g (p ▸ b) :=
-  by cases r; exact idpo
+  by cases r; constructor
+
+  definition apdo_compose1 (g : Πa, B a → B' a) (f : Πa, B a) (p : a = a₂)
+    : apdo (g ∘' f) p = apo g (apdo f p) :=
+  by induction p; reflexivity
+
+  definition apdo_compose2 (g : Πa', B'' a') (f : A → A') (p : a = a₂)
+    : apdo (λa, g (f a)) p = pathover_of_pathover_ap B'' f (apdo g (ap f p)) :=
+  by induction p; reflexivity
 
   definition cono.right_inv_eq (q : b = b')
     : concato_eq (pathover_idp_of_eq q) q⁻¹ = (idpo : b =[refl a] b) :=
@@ -263,4 +268,33 @@ namespace eq
 
   definition change_path_equiv' (f : Π{a}, B a ≃ B' a) (r : f b =[p] f b₂) : b =[p] b₂ :=
   (left_inv f b)⁻¹ ⬝po change_path_equiv (λa, f⁻¹ᵉ) r ⬝op left_inv f b₂
+
+  definition change_path_of_pathover (s : p = p') (r : b =[p] b₂) (r' : b =[p'] b₂)
+    (q : r =[s] r') : change_path s r = r' :=
+  by induction s; eapply idp_rec_on q; reflexivity
+
+  definition pathover_of_change_path (s : p = p') (r : b =[p] b₂) (r' : b =[p'] b₂)
+    (q : change_path s r = r') : r =[s] r' :=
+  by induction s; induction q; constructor
+
+  definition pathover_pathover_path [constructor] (s : p = p') (r : b =[p] b₂) (r' : b =[p'] b₂) :
+    (r =[s] r') ≃ change_path s r = r' :=
+  begin
+    fapply equiv.MK,
+    { apply change_path_of_pathover},
+    { apply pathover_of_change_path},
+    { intro q, induction s, induction q, reflexivity},
+    { intro q, induction s, eapply idp_rec_on q, reflexivity},
+  end
+
+  definition inverseo2 [unfold 10] {r r' : b =[p] b₂} (s : r = r') : r⁻¹ᵒ = r'⁻¹ᵒ :=
+  by induction s; reflexivity
+
+  definition concato2 [unfold 15 16] {r r' : b =[p] b₂} {r₂ r₂' : b₂ =[p₂] b₃}
+    (s : r = r') (s₂ : r₂ = r₂') : r ⬝o r₂ = r' ⬝o r₂' :=
+  by induction s; induction s₂; reflexivity
+
+  infixl `◾o`:75 := concato2
+  postfix [parsing-only] `⁻²ᵒ`:(max+10) := inverseo2 --this notation is abusive, should we use it?
+
 end eq
diff --git a/hott/types/arrow.hlean b/hott/types/arrow.hlean
index 0f1743e14..33034235a 100644
--- a/hott/types/arrow.hlean
+++ b/hott/types/arrow.hlean
@@ -21,30 +21,34 @@ namespace pi
   /- Functorial action -/
   variables (f0 : A' → A) (f1 : B → B')
 
-  definition arrow_functor : (A → B) → (A' → B') := pi_functor f0 (λa, f1)
+  definition arrow_functor [unfold-full] : (A → B) → (A' → B') := pi_functor f0 (λa, f1)
 
   /- Equivalences -/
 
-  definition is_equiv_arrow_functor
+  definition is_equiv_arrow_functor [constructor]
     [H0 : is_equiv f0] [H1 : is_equiv f1] : is_equiv (arrow_functor f0 f1) :=
   is_equiv_pi_functor f0 (λa, f1)
 
-  definition arrow_equiv_arrow_rev (f0 : A' ≃ A) (f1 : B ≃ B') : (A → B) ≃ (A' → B') :=
+  definition arrow_equiv_arrow_rev [constructor] (f0 : A' ≃ A) (f1 : B ≃ B')
+    : (A → B) ≃ (A' → B') :=
   equiv.mk _ (is_equiv_arrow_functor f0 f1)
 
-  definition arrow_equiv_arrow (f0 : A ≃ A') (f1 : B ≃ B') : (A → B) ≃ (A' → B') :=
+  definition arrow_equiv_arrow [constructor] (f0 : A ≃ A') (f1 : B ≃ B') : (A → B) ≃ (A' → B') :=
   arrow_equiv_arrow_rev (equiv.symm f0) f1
 
-  definition arrow_equiv_arrow_right (f1 : B ≃ B') : (A → B) ≃ (A → B') :=
+  variable (A)
+  definition arrow_equiv_arrow_right [constructor] (f1 : B ≃ B') : (A → B) ≃ (A → B') :=
   arrow_equiv_arrow_rev equiv.refl f1
 
-  definition arrow_equiv_arrow_left_rev (f0 : A' ≃ A) : (A → B) ≃ (A' → B) :=
+  variables {A} (B)
+  definition arrow_equiv_arrow_left_rev [constructor] (f0 : A' ≃ A) : (A → B) ≃ (A' → B) :=
   arrow_equiv_arrow_rev f0 equiv.refl
 
-  definition arrow_equiv_arrow_left (f0 : A ≃ A') : (A → B) ≃ (A' → B) :=
+  definition arrow_equiv_arrow_left [constructor] (f0 : A ≃ A') : (A → B) ≃ (A' → B) :=
   arrow_equiv_arrow f0 equiv.refl
 
-  definition arrow_equiv_arrow_right' (f1 : A → (B ≃ B')) : (A → B) ≃ (A → B') :=
+  variables {B}
+  definition arrow_equiv_arrow_right' [constructor] (f1 : A → (B ≃ B')) : (A → B) ≃ (A → B') :=
   pi_equiv_pi_id f1
 
   /- Transport -/
diff --git a/hott/types/eq.hlean b/hott/types/eq.hlean
index 9b3738250..578193fc5 100644
--- a/hott/types/eq.hlean
+++ b/hott/types/eq.hlean
@@ -91,7 +91,7 @@ namespace eq
   theorem idp_con_idp {p : a = a} (q : p = idp) : idp_con p ⬝ q = ap (λp, idp ⬝ p) q :=
   by cases q;reflexivity
 
-  definition ap_weakly_constant [unfold 8] {A B : Type} {f : A → B} {b : B} (p : Πx, f x = b)
+  definition ap_is_constant [unfold 8] {A B : Type} {f : A → B} {b : B} (p : Πx, f x = b)
     {x y : A} (q : x = y) : ap f q = p x ⬝ (p y)⁻¹ :=
   by induction q;exact !con.right_inv⁻¹
 
diff --git a/hott/types/equiv.hlean b/hott/types/equiv.hlean
index 0e7324cb8..cbbb87070 100644
--- a/hott/types/equiv.hlean
+++ b/hott/types/equiv.hlean
@@ -36,7 +36,7 @@ namespace is_equiv
     fapply is_trunc_equiv_closed,
       {apply fiber.sigma_char},
     fapply is_contr_fiber_of_is_equiv,
-    apply (to_is_equiv (arrow_equiv_arrow_right (equiv.mk f H))),
+    apply (to_is_equiv (arrow_equiv_arrow_right B (equiv.mk f H))),
   end
 
   definition is_contr_right_coherence (u : Σ(g : B → A), f ∘ g ~ id)
diff --git a/hott/types/lift.hlean b/hott/types/lift.hlean
index 147df4507..8d332bc8d 100644
--- a/hott/types/lift.hlean
+++ b/hott/types/lift.hlean
@@ -129,7 +129,7 @@ namespace lift
 
   definition is_embedding_lift [instance] : is_embedding lift :=
   begin
-    apply is_embedding.mk, intro A A', fapply is_equiv.homotopy_closed,
+    intro A A', fapply is_equiv.homotopy_closed,
       exact to_inv !lift_eq_lift_equiv,
       exact _,
     { intro p, induction p,
diff --git a/hott/types/pi.hlean b/hott/types/pi.hlean
index 2d08232e0..2e1b82a31 100644
--- a/hott/types/pi.hlean
+++ b/hott/types/pi.hlean
@@ -170,7 +170,7 @@ namespace pi
 
   /- Equivalences -/
 
-  definition is_equiv_pi_functor [instance] [H0 : is_equiv f0]
+  definition is_equiv_pi_functor [instance] [constructor] [H0 : is_equiv f0]
     [H1 : Πa', is_equiv (f1 a')] : is_equiv (pi_functor f0 f1) :=
   begin
     apply (adjointify (pi_functor f0 f1) (pi_functor f0⁻¹
@@ -187,15 +187,16 @@ namespace pi
     end
   end
 
-  definition pi_equiv_pi_of_is_equiv [H : is_equiv f0]
+  definition pi_equiv_pi_of_is_equiv [constructor] [H : is_equiv f0]
     [H1 : Πa', is_equiv (f1 a')] : (Πa, B a) ≃ (Πa', B' a') :=
   equiv.mk (pi_functor f0 f1) _
 
-  definition pi_equiv_pi (f0 : A' ≃ A) (f1 : Πa', (B (to_fun f0 a') ≃ B' a'))
+  definition pi_equiv_pi [constructor] (f0 : A' ≃ A) (f1 : Πa', (B (to_fun f0 a') ≃ B' a'))
     : (Πa, B a) ≃ (Πa', B' a') :=
   pi_equiv_pi_of_is_equiv (to_fun f0) (λa', to_fun (f1 a'))
 
-  definition pi_equiv_pi_id {P Q : A → Type} (g : Πa, P a ≃ Q a) : (Πa, P a) ≃ (Πa, Q a) :=
+  definition pi_equiv_pi_id [constructor] {P Q : A → Type} (g : Πa, P a ≃ Q a)
+    : (Πa, P a) ≃ (Πa, Q a) :=
   pi_equiv_pi equiv.refl g
 
   /- Truncatedness: any dependent product of n-types is an n-type -/
diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean
index f35de985d..4def247fd 100644
--- a/hott/types/trunc.hlean
+++ b/hott/types/trunc.hlean
@@ -65,7 +65,7 @@ namespace is_trunc
   end
 
   definition is_embedding_to_fun (A B : Type) : is_embedding (@to_fun A B)  :=
-  is_embedding.mk (λf f', !is_equiv_ap_to_fun)
+  λf f', !is_equiv_ap_to_fun
 
   definition is_trunc_trunctype [instance] (n : trunc_index) : is_trunc n.+1 (n-Type) :=
   begin
@@ -241,7 +241,7 @@ end trunc open trunc
 namespace function
   variables {A B : Type}
   definition is_surjective_of_is_equiv [instance] (f : A → B) [H : is_equiv f] : is_surjective f :=
-  is_surjective.mk (λb, !center)
+  λb, !center
 
   definition is_equiv_equiv_is_embedding_times_is_surjective (f : A → B)
     : is_equiv f ≃ (is_embedding f × is_surjective f) :=
diff --git a/src/emacs/lean-input.el b/src/emacs/lean-input.el
index 8bf2fe091..bd46a8890 100644
--- a/src/emacs/lean-input.el
+++ b/src/emacs/lean-input.el
@@ -341,12 +341,14 @@ order for the change to take effect."
   ("-1f"       . ("⁻¹ᶠ"))
   ("-1g"       . ("⁻¹ᵍ"))
   ("-1h"       . ("⁻¹ʰ"))
+  ("-1i"       . ("⁻¹ⁱ"))
   ("-1m"       . ("⁻¹ᵐ"))
   ("-1o"       . ("⁻¹ᵒ"))
   ("-1r"       . ("⁻¹ʳ"))
   ("-1p"       . ("⁻¹ᵖ"))
   ("-1v"       . ("⁻¹ᵛ"))
   ("-2"        . ("⁻²"))
+  ("-2o"       . ("⁻²ᵒ"))
   ("-3"        . ("⁻³"))
   ("qed"       . ("∎"))
   ("x"         . ("×"))