diff --git a/hott/algebra/category/basic.hlean b/hott/algebra/category/basic.hlean
index 7a7842fecc..657ad5608f 100644
--- a/hott/algebra/category/basic.hlean
+++ b/hott/algebra/category/basic.hlean
@@ -16,14 +16,14 @@ open morphism is_equiv eq is_trunc
 namespace category
 
   structure category [class] (ob : Type) extends parent : precategory ob :=
-    (iso_of_path_equiv : Π (a b : ob), is_equiv (@iso_of_path ob parent a b))
+    (iso_of_path_equiv : Π (a b : ob), is_equiv (@iso_of_eq ob parent a b))
 
   attribute category [multiple-instances]
 
   abbreviation iso_of_path_equiv := @category.iso_of_path_equiv
 
   definition category.mk' [reducible] (ob : Type) (C : precategory ob)
-    (H : Π (a b : ob), is_equiv (@iso_of_path ob C a b)) : category ob :=
+    (H : Π (a b : ob), is_equiv (@iso_of_eq ob C a b)) : category ob :=
   precategory.rec_on C category.mk H
 
   section basic
@@ -34,18 +34,18 @@ namespace category
   -- TODO: Unsafe class instance?
   attribute iso_of_path_equiv [instance]
 
-  definition path_of_iso (a b : ob) : a ≅ b → a = b :=
-  iso_of_path⁻¹
+  definition eq_of_iso (a b : ob) : a ≅ b → a = b :=
+  iso_of_eq⁻¹ᵉ
 
   set_option apply.class_instance false -- disable class instance resolution in the apply tactic
 
-  definition ob_1_type : is_trunc 1 ob :=
+  definition is_trunc_1_ob : is_trunc 1 ob :=
   begin
     apply is_trunc_succ_intro, intros (a, b),
     fapply is_trunc_is_equiv_closed,
-          exact (@path_of_iso _ _ a b),
+          exact (@eq_of_iso _ _ a b),
         apply is_equiv_inv,
-    apply is_hset_iso,
+    apply is_hset_isomorphic,
   end
   end basic
 
@@ -64,7 +64,7 @@ namespace category
 
   definition category.Mk [reducible] := Category.mk
   definition category.MK [reducible] (C : Precategory)
-    (H : Π (a b : C), is_equiv (@iso_of_path C C a b)) : Category :=
+    (H : Π (a b : C), is_equiv (@iso_of_eq C C a b)) : Category :=
   Category.mk C (category.mk' C C H)
 
   definition Category.eta (C : Category) : Category.mk C C = C :=
diff --git a/hott/algebra/category/constructions.hlean b/hott/algebra/category/constructions.hlean
index 7d5060fc28..8712f63b89 100644
--- a/hott/algebra/category/constructions.hlean
+++ b/hott/algebra/category/constructions.hlean
@@ -13,11 +13,11 @@ open eq prod eq eq.ops equiv is_trunc funext pi category.ops morphism category
 namespace category
 
   section hset
-  definition is_category_hset (a b : Precategory_hset) : is_equiv (@iso_of_path _ _ a b) :=
+  definition is_univalent_hset (a b : Precategory_hset) : is_equiv (@iso_of_eq _ _ a b) :=
   sorry
 
   definition category_hset [reducible] [instance] : category hset :=
-  category.mk' hset precategory_hset is_category_hset
+  category.mk' hset precategory_hset is_univalent_hset
 
   definition Category_hset [reducible] : Category :=
   Category.mk hset category_hset
diff --git a/hott/algebra/groupoid.hlean b/hott/algebra/groupoid.hlean
index 6464626e70..35fbf6e49f 100644
--- a/hott/algebra/groupoid.hlean
+++ b/hott/algebra/groupoid.hlean
@@ -35,7 +35,7 @@ namespace category
     (λ (a b : A) (p : a = b), con_idp p)
     (λ (a b : A) (p : a = b), idp_con p)
     (λ (a b : A) (p : a = b), @is_iso.mk A _ a b p p⁻¹
-      !con.left_inv !con.right_inv)
+      !con.right_inv !con.left_inv)
 
   -- A groupoid with a contractible carrier is a group
   definition group_of_is_contr_groupoid {ob : Type} [H : is_contr ob]
@@ -49,10 +49,10 @@ namespace category
       intro f, apply id_left,
       intro f, apply id_right,
       intro f, exact (morphism.inverse f),
-      intro f, exact (morphism.inverse_compose f),
+      intro f, exact (morphism.inverse_comp f),
   end
 
-  definition group_of_unit_groupoid [G : groupoid unit] : group (hom ⋆ ⋆) :=
+  definition group_of_groupoid_unit [G : groupoid unit] : group (hom ⋆ ⋆) :=
   begin
     fapply group.mk,
       intros (f, g), apply (comp f g),
@@ -62,11 +62,11 @@ namespace category
       intro f, apply id_left,
       intro f, apply id_right,
       intro f, exact (morphism.inverse f),
-      intro f, exact (morphism.inverse_compose f),
+      intro f, exact (morphism.inverse_comp f),
   end
 
   -- Conversely we can turn each group into a groupoid on the unit type
-  definition of_group.{l} (A : Type.{l}) [G : group A] : groupoid.{l l} unit :=
+  definition groupoid_of_group.{l} (A : Type.{l}) [G : group A] : groupoid.{l l} unit :=
   begin
     fapply groupoid.mk,
       intros, exact A,
@@ -92,7 +92,7 @@ namespace category
       intro f, apply id_left,
       intro f, apply id_right,
       intro f, exact (morphism.inverse f),
-      intro f, exact (morphism.inverse_compose f),
+      intro f, exact (morphism.inverse_comp f),
   end
 
   -- Bundled version of categories
diff --git a/hott/algebra/precategory/basic.hlean b/hott/algebra/precategory/basic.hlean
index 41f86243c5..583771b98c 100644
--- a/hott/algebra/precategory/basic.hlean
+++ b/hott/algebra/precategory/basic.hlean
@@ -45,7 +45,7 @@ namespace category
 
     definition id [reducible] := ID a
 
-    definition id_compose (a : ob) : ID a ∘ ID a = ID a := !id_left
+    definition id_comp (a : ob) : ID a ∘ ID a = ID a := !id_left
 
     definition left_id_unique (H : Π{b} {f : hom b a}, i ∘ f = f) : i = id :=
     calc i = i ∘ id : id_right
diff --git a/hott/algebra/precategory/constructions.hlean b/hott/algebra/precategory/constructions.hlean
index c54a9e8f00..c74cbcd965 100644
--- a/hott/algebra/precategory/constructions.hlean
+++ b/hott/algebra/precategory/constructions.hlean
@@ -39,7 +39,7 @@ namespace category
   --       take the trick they use in Coq-HoTT, and introduce a further
   --       axiom in the definition of precategories that provides thee
   --       symmetric associativity proof.
-  definition op_op' {ob : Type} (C : precategory ob) : opposite (opposite C) = C :=
+  definition opposite_opposite' {ob : Type} (C : precategory ob) : opposite (opposite C) = C :=
   begin
     apply (precategory.rec_on C), intros (hom', homH', comp', ID', assoc', id_left', id_right'),
     apply (ap (λassoc'', precategory.mk hom' @homH' comp' ID' assoc'' id_left' id_right')),
@@ -48,8 +48,8 @@ namespace category
     apply (@is_hset.elim), apply !homH',
   end
 
-  definition op_op : Opposite (Opposite C) = C :=
-  (ap (Precategory.mk C) (op_op' C)) ⬝ !Precategory.eta
+  definition opposite_opposite : Opposite (Opposite C) = C :=
+  (ap (Precategory.mk C) (opposite_opposite' C)) ⬝ !Precategory.eta
 
   end opposite
 
@@ -91,7 +91,7 @@ namespace category
   section
   open prod is_trunc
 
-  definition prod_precategory [reducible] {obC obD : Type} (C : precategory obC) (D : precategory obD)
+  definition precategory_prod [reducible] {obC obD : Type} (C : precategory obC) (D : precategory obD)
       : precategory (obC × obD) :=
   precategory.mk (λ a b, hom (pr1 a) (pr1 b) × hom (pr2 a) (pr2 b))
                  (λ a b, !is_trunc_prod)
@@ -101,8 +101,8 @@ namespace category
                  (λ a b f,         prod_eq  !id_left  !id_left )
                  (λ a b f,         prod_eq  !id_right !id_right)
 
-  definition Prod_precategory [reducible] (C D : Precategory) : Precategory :=
-  precategory.Mk (prod_precategory C D)
+  definition Precategory_prod [reducible] (C D : Precategory) : Precategory :=
+  precategory.Mk (precategory_prod C D)
 
   end
   end product
@@ -111,7 +111,7 @@ namespace category
     --notation 1 := Category_one
     --notation 2 := Category_two
     postfix `ᵒᵖ`:max := opposite.Opposite
-    infixr `×c`:30 := product.Prod_precategory
+    infixr `×c`:30 := product.Precategory_prod
     --instance [persistent] type_category category_one
     --                      category_two product.prod_category
   end ops
@@ -169,7 +169,7 @@ namespace category
     -- definition Precategory_functor_rev [reducible] (C D : Precategory) : Precategory :=
     -- Precategory_functor D C
 
-    /- we prove that if a natural transformation is pointwise an iso, then it is an iso -/
+    /- we prove that if a natural transformation is pointwise an to_fun, then it is an to_fun -/
     variables {C D : Precategory} {F G : C ⇒ D} (η : F ⟹ G) [iso : Π(a : C), is_iso (η a)]
     include iso
     definition nat_trans_inverse : G ⟹ F :=
@@ -177,16 +177,16 @@ namespace category
       (λc, (η c)⁻¹)
       (λc d f,
       begin
-        apply iso.con_inv_eq_of_eq_con,
+        apply to_fun.comp_inverse_eq_of_eq_comp,
         apply concat, rotate_left 1, apply assoc,
-        apply iso.eq_inv_con_of_con_eq,
+        apply to_fun.eq_inverse_comp_of_comp_eq,
         apply inverse,
         apply naturality,
       end)
     definition nat_trans_left_inverse : nat_trans_inverse η ∘n η = nat_trans.id :=
     begin
     fapply (apD011 nat_trans.mk),
-      apply eq_of_homotopy, intro c, apply inverse_compose,
+      apply eq_of_homotopy, intro c, apply inverse_comp,
     apply eq_of_homotopy, intros, apply eq_of_homotopy, intros, apply eq_of_homotopy, intros,
     apply is_hset.elim
     end
@@ -194,7 +194,7 @@ namespace category
     definition nat_trans_right_inverse : η ∘n nat_trans_inverse η = nat_trans.id :=
     begin
     fapply (apD011 nat_trans.mk),
-      apply eq_of_homotopy, intro c, apply compose_inverse,
+      apply eq_of_homotopy, intro c, apply comp_inverse,
     apply eq_of_homotopy, intros, apply eq_of_homotopy, intros, apply eq_of_homotopy, intros,
     apply is_hset.elim
     end
diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean
index 2c4e429312..88d0d4546e 100644
--- a/hott/algebra/precategory/functor.hlean
+++ b/hott/algebra/precategory/functor.hlean
@@ -12,19 +12,19 @@ open function category eq prod equiv is_equiv sigma sigma.ops is_trunc funext
 open pi
 
 structure functor (C D : Precategory) : Type :=
-  (obF : C → D)
-  (homF : Π ⦃a b : C⦄, hom a b → hom (obF a) (obF b))
-  (respect_id : Π (a : C), homF (ID a) = ID (obF a))
+  (to_fun_ob : C → D)
+  (to_fun_hom : Π ⦃a b : C⦄, hom a b → hom (to_fun_ob a) (to_fun_ob b))
+  (respect_id : Π (a : C), to_fun_hom (ID a) = ID (to_fun_ob a))
   (respect_comp : Π {a b c : C} (g : hom b c) (f : hom a b),
-    homF (g ∘ f) = homF g ∘ homF f)
+    to_fun_hom (g ∘ f) = to_fun_hom g ∘ to_fun_hom f)
 
 namespace functor
 
   infixl `⇒`:25 := functor
   variables {C D E : Precategory}
 
-  attribute obF [coercion]
-  attribute homF [coercion]
+  attribute to_fun_ob [coercion]
+  attribute to_fun_hom [coercion]
 
   -- The following lemmas will later be used to prove that the type of
   -- precategories forms a precategory itself
@@ -78,7 +78,7 @@ namespace functor
   functor_eq_mk'' id₁ id₂ comp₁ comp₂ idp
                   (eq_of_homotopy (λc, eq_of_homotopy (λc', eq_of_homotopy (pH c c'))))
 
-  definition functor_eq_mk {F₁ F₂ : C ⇒ D} : Π(p : obF F₁ ∼ obF F₂),
+  definition functor_eq_mk {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ ∼ to_fun_ob F₂),
     (Π(a b : C) (f : hom a b), transport (λF, hom (F a) (F b)) (eq_of_homotopy p) (F₁ f) = F₂ f)
       → F₁ = F₂ :=
   functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_eq_mk'))
@@ -97,11 +97,11 @@ namespace functor
   -- "functor C D" is equivalent to a certain sigma type
   set_option unifier.max_steps 38500
   protected definition sigma_char :
-    (Σ (obF : C → D)
-    (homF : Π ⦃a b : C⦄, hom a b → hom (obF a) (obF b)),
-    (Π (a : C), homF (ID a) = ID (obF a)) ×
+    (Σ (to_fun_ob : C → D)
+    (to_fun_hom : Π ⦃a b : C⦄, hom a b → hom (to_fun_ob a) (to_fun_ob b)),
+    (Π (a : C), to_fun_hom (ID a) = ID (to_fun_ob a)) ×
     (Π {a b c : C} (g : hom b c) (f : hom a b),
-      homF (g ∘ f) = homF g ∘ homF f)) ≃ (functor C D) :=
+      to_fun_hom (g ∘ f) = to_fun_hom g ∘ to_fun_hom f)) ≃ (functor C D) :=
   begin
     fapply equiv.MK,
       {intro S, fapply functor.mk,
@@ -120,7 +120,7 @@ namespace functor
         apply idp},
   end
 
-  protected definition strict_cat_has_functor_hset
+  protected definition is_hset_functor
     [HD : is_hset D] : is_hset (functor C D) :=
   begin
     apply is_trunc_is_equiv_closed, apply equiv.to_is_equiv,
@@ -143,21 +143,21 @@ namespace category
   open functor
 
   --TODO: make this a structure
-  definition precat_of_strict_precats : precategory (Σ (C : Precategory), is_hset C) :=
+  definition precat_strict_precat : precategory (Σ (C : Precategory), is_hset C) :=
   precategory.mk (λ a b, functor a.1 b.1)
-     (λ a b, @functor.strict_cat_has_functor_hset a.1 b.1 b.2)
+     (λ a b, @functor.is_hset_functor a.1 b.1 b.2)
      (λ a b c g f, functor.compose g f)
      (λ a, functor.id)
      (λ a b c d h g f, !functor.assoc)
      (λ a b f, !functor.id_left)
      (λ a b f, !functor.id_right)
 
-  definition Precat_of_strict_cats := precategory.Mk precat_of_strict_precats
+  definition Precat_of_strict_cats := precategory.Mk precat_strict_precat
 
   namespace ops
 
     abbreviation SPreCat := Precat_of_strict_cats
-    --attribute precat_of_strict_precats [instance]
+    --attribute precat_strict_precat [instance]
 
   end ops
 
diff --git a/hott/algebra/precategory/iso.hlean b/hott/algebra/precategory/iso.hlean
index 75f6e61843..0412ae999e 100644
--- a/hott/algebra/precategory/iso.hlean
+++ b/hott/algebra/precategory/iso.hlean
@@ -2,7 +2,7 @@
 Copyright (c) 2014 Jakob von Raumer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Module: algebra.precategory.iso
+Module: algebra.precategory.to_fun
 Authors: Floris van Doorn, Jakob von Raumer
 -/
 
@@ -32,7 +32,7 @@ namespace morphism
 
   -- The structure for isomorphism can be characterized up to equivalence
   -- by a sigma type.
-  definition sigma_is_iso_equiv ⦃a b : ob⦄ : (Σ (f : hom a b), is_iso f) ≃ (a ≅ b) :=
+  definition isomorphic.sigma_char ⦃a b : ob⦄ : (Σ (f : hom a b), is_iso f) ≃ (a ≅ b) :=
   begin
     fapply (equiv.mk),
       {intro S, apply isomorphic.mk, apply (S.2)},
@@ -45,7 +45,7 @@ namespace morphism
   set_option apply.class_instance false -- disable class instance resolution in the apply tactic
 
   -- The statement "f is an isomorphism" is a mere proposition
-  definition is_hprop_of_is_iso : is_hset (is_iso f) :=
+  definition is_hset_iso : is_hset (is_iso f) :=
   begin
     apply is_trunc_is_equiv_closed,
       apply (equiv.to_is_equiv (!sigma_char)),
@@ -56,17 +56,17 @@ namespace morphism
   end
 
   -- The type of isomorphisms between two objects is a set
-  definition is_hset_iso : is_hset (a ≅ b) :=
+  definition is_hset_isomorphic : is_hset (a ≅ b) :=
   begin
     apply is_trunc_is_equiv_closed,
-      apply (equiv.to_is_equiv (!sigma_is_iso_equiv)),
+      apply (equiv.to_is_equiv (!isomorphic.sigma_char)),
       apply is_trunc_sigma,
        apply homH,
-       {intro f, apply is_hprop_of_is_iso},
+       {intro f, apply is_hset_iso},
   end
 
   -- In a precategory, equal objects are isomorphic
-  definition iso_of_path (p : a = b) : a ≅ b :=
+  definition iso_of_eq (p : a = b) : a ≅ b :=
   eq.rec_on p (isomorphic.mk id)
 
 end morphism
diff --git a/hott/algebra/precategory/morphism.hlean b/hott/algebra/precategory/morphism.hlean
index 9101f22c8e..c53dcf275e 100644
--- a/hott/algebra/precategory/morphism.hlean
+++ b/hott/algebra/precategory/morphism.hlean
@@ -11,26 +11,26 @@ import algebra.precategory.basic
 open eq category sigma sigma.ops equiv is_equiv is_trunc
 
 namespace morphism
-  structure is_section [class] {ob : Type} [C : precategory ob] {a b : ob} (f : a ⟶ b) :=
+  structure split_mono [class] {ob : Type} [C : precategory ob] {a b : ob} (f : a ⟶ b) :=
     {retraction_of : b ⟶ a}
-    (retraction_compose : retraction_of ∘ f = id)
-  structure is_retraction [class] {ob : Type} [C : precategory ob] {a b : ob} (f : a ⟶ b) :=
+    (retraction_comp : retraction_of ∘ f = id)
+  structure split_epi [class] {ob : Type} [C : precategory ob] {a b : ob} (f : a ⟶ b) :=
     {section_of : b ⟶ a}
-    (compose_section : f ∘ section_of = id)
+    (comp_section : f ∘ section_of = id)
   structure is_iso [class] {ob : Type} [C : precategory ob] {a b : ob} (f : a ⟶ b) :=
     {inverse : b ⟶ a}
-    (inverse_compose : inverse ∘ f = id)
-    (compose_inverse : f ∘ inverse = id)
+    (inverse_comp : inverse ∘ f = id)
+    (comp_inverse : f ∘ inverse = id)
 
   attribute is_iso [multiple-instances]
-  open is_section is_retraction is_iso
-  definition retraction_of [reducible] := @is_section.retraction_of
-  definition retraction_compose [reducible] := @is_section.retraction_compose
-  definition section_of [reducible] := @is_retraction.section_of
-  definition compose_section [reducible] := @is_retraction.compose_section
+  open split_mono split_epi is_iso
+  definition retraction_of [reducible] := @split_mono.retraction_of
+  definition retraction_comp [reducible] := @split_mono.retraction_comp
+  definition section_of [reducible] := @split_epi.section_of
+  definition comp_section [reducible] := @split_epi.comp_section
   definition inverse [reducible] := @is_iso.inverse
-  definition inverse_compose [reducible] := @is_iso.inverse_compose
-  definition compose_inverse [reducible] := @is_iso.compose_inverse
+  definition inverse_comp [reducible] := @is_iso.inverse_comp
+  definition comp_inverse [reducible] := @is_iso.comp_inverse
   postfix `⁻¹` := inverse
   --a second notation for the inverse, which is not overloaded
   postfix [parsing-only] `⁻¹ʰ`:std.prec.max_plus := inverse
@@ -40,77 +40,77 @@ namespace morphism
   include C
 
   definition iso_imp_retraction [instance] [priority 300] [reducible]
-    (f : a ⟶ b) [H : is_iso f] : is_section f :=
-  is_section.mk !inverse_compose
+    (f : a ⟶ b) [H : is_iso f] : split_mono f :=
+  split_mono.mk !inverse_comp
 
   definition iso_imp_section [instance] [priority 300] [reducible]
-    (f : a ⟶ b) [H : is_iso f] : is_retraction f :=
-  is_retraction.mk !compose_inverse
+    (f : a ⟶ b) [H : is_iso f] : split_epi f :=
+  split_epi.mk !comp_inverse
 
   definition is_iso_id [instance] [priority 500] (a : ob) : is_iso (ID a) :=
-  is_iso.mk !id_compose !id_compose
+  is_iso.mk !id_comp !id_comp
 
   definition is_iso_inverse [instance] [priority 200] (f : a ⟶ b) [H : is_iso f] : is_iso f⁻¹ :=
-  is_iso.mk !compose_inverse !inverse_compose
+  is_iso.mk !comp_inverse !inverse_comp
 
   definition left_inverse_eq_right_inverse {f : a ⟶ b} {g g' : hom b a}
       (Hl : g ∘ f = id) (Hr : f ∘ g' = id) : g = g' :=
   by rewrite [-(id_right g), -Hr, assoc, Hl, id_left]
 
-  definition retraction_eq_intro [H : is_section f] (H2 : f ∘ h = id) : retraction_of f = h :=
-  left_inverse_eq_right_inverse !retraction_compose H2
+  definition retraction_eq [H : split_mono f] (H2 : f ∘ h = id) : retraction_of f = h :=
+  left_inverse_eq_right_inverse !retraction_comp H2
 
-  definition section_eq_intro [H : is_retraction f] (H2 : h ∘ f = id) : section_of f = h :=
-  (left_inverse_eq_right_inverse H2 !compose_section)⁻¹
+  definition section_eq [H : split_epi f] (H2 : h ∘ f = id) : section_of f = h :=
+  (left_inverse_eq_right_inverse H2 !comp_section)⁻¹
 
-  definition inverse_eq_intro_right [H : is_iso f] (H2 : f ∘ h = id) : f⁻¹ = h :=
-  left_inverse_eq_right_inverse !inverse_compose H2
+  definition inverse_eq_right [H : is_iso f] (H2 : f ∘ h = id) : f⁻¹ = h :=
+  left_inverse_eq_right_inverse !inverse_comp H2
 
-  definition inverse_eq_intro_left [H : is_iso f] (H2 : h ∘ f = id) : f⁻¹ = h :=
-  (left_inverse_eq_right_inverse H2 !compose_inverse)⁻¹
+  definition inverse_eq_left [H : is_iso f] (H2 : h ∘ f = id) : f⁻¹ = h :=
+  (left_inverse_eq_right_inverse H2 !comp_inverse)⁻¹
 
-  definition section_eq_retraction (f : a ⟶ b) [Hl : is_section f] [Hr : is_retraction f] :
+  definition retraction_eq_section (f : a ⟶ b) [Hl : split_mono f] [Hr : split_epi f] :
       retraction_of f = section_of f :=
-  retraction_eq_intro !compose_section
+  retraction_eq !comp_section
 
-  definition section_retraction_imp_iso (f : a ⟶ b) [Hl : is_section f] [Hr : is_retraction f]
+  definition iso_of_split_epi_of_split_mono (f : a ⟶ b) [Hl : split_mono f] [Hr : split_epi f]
     : is_iso f :=
-  is_iso.mk ((section_eq_retraction f) ▹ (retraction_compose f)) (compose_section f)
+  is_iso.mk ((retraction_eq_section f) ▹ (retraction_comp f)) (comp_section f)
 
   definition inverse_unique (H H' : is_iso f) : @inverse _ _ _ _ f H = @inverse _ _ _ _ f H' :=
-  inverse_eq_intro_left !inverse_compose
+  inverse_eq_left !inverse_comp
 
   definition inverse_involutive (f : a ⟶ b) [H : is_iso f] : (f⁻¹)⁻¹ = f :=
-  inverse_eq_intro_right !inverse_compose
+  inverse_eq_right !inverse_comp
 
-  definition retraction_of_id (a : ob) : retraction_of (ID a) = id :=
-  retraction_eq_intro !id_compose
+  definition retraction_id (a : ob) : retraction_of (ID a) = id :=
+  retraction_eq !id_comp
 
-  definition section_of_id (a : ob) : section_of (ID a) = id :=
-  section_eq_intro !id_compose
+  definition section_id (a : ob) : section_of (ID a) = id :=
+  section_eq !id_comp
 
-  definition iso_of_id (a : ob) [H : is_iso (ID a)] : (ID a)⁻¹ = id :=
-  inverse_eq_intro_left !id_compose
+  definition id_inverse (a : ob) [H : is_iso (ID a)] : (ID a)⁻¹ = id :=
+  inverse_eq_left !id_comp
 
-  definition composition_is_section [instance] [priority 150] (g : b ⟶ c) (f : a ⟶ b)
-    [Hf : is_section f] [Hg : is_section g] : is_section (g ∘ f) :=
-  is_section.mk
+  definition split_mono_comp [instance] [priority 150] (g : b ⟶ c) (f : a ⟶ b)
+    [Hf : split_mono f] [Hg : split_mono g] : split_mono (g ∘ f) :=
+  split_mono.mk
     (show (retraction_of f ∘ retraction_of g) ∘ g ∘ f = id,
-     by rewrite [-assoc, assoc _ g f, retraction_compose, id_left, retraction_compose])
+     by rewrite [-assoc, assoc _ g f, retraction_comp, id_left, retraction_comp])
 
-  definition composition_is_retraction [instance] [priority 150] (g : b ⟶ c) (f : a ⟶ b)
-    [Hf : is_retraction f] [Hg : is_retraction g] : is_retraction (g ∘ f) :=
-  is_retraction.mk
+  definition split_epi_comp [instance] [priority 150] (g : b ⟶ c) (f : a ⟶ b)
+    [Hf : split_epi f] [Hg : split_epi g] : split_epi (g ∘ f) :=
+  split_epi.mk
     (show (g ∘ f) ∘ section_of f ∘ section_of g = id,
-     by rewrite [-assoc, {f ∘ _}assoc, compose_section, id_left, compose_section])
+     by rewrite [-assoc, {f ∘ _}assoc, comp_section, id_left, comp_section])
 
-  definition composition_is_inverse [instance] [priority 150] (g : b ⟶ c) (f : a ⟶ b)
+  definition iso_comp [instance] [priority 150] (g : b ⟶ c) (f : a ⟶ b)
     [Hf : is_iso f] [Hg : is_iso g] : is_iso (g ∘ f) :=
-  !section_retraction_imp_iso
+  !iso_of_split_epi_of_split_mono
 
   structure isomorphic (a b : ob) :=
-    (iso : hom a b)
-    [struct : is_iso iso]
+    (to_fun : hom a b)
+    [struct : is_iso to_fun]
 
   infix `≅`:50 := morphism.isomorphic
   attribute isomorphic.struct [instance] [priority 400]
@@ -122,57 +122,57 @@ namespace morphism
     mk (ID a)
 
     protected definition symm ⦃a b : ob⦄ (H : a ≅ b) : b ≅ a :=
-    mk (iso H)⁻¹
+    mk (to_fun H)⁻¹
 
     protected definition trans ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c :=
-    mk (iso H2 ∘ iso H1)
+    mk (to_fun H2 ∘ to_fun H1)
 
   end isomorphic
 
-  structure is_mono [class] (f : a ⟶ b) :=
+  structure mono [class] (f : a ⟶ b) :=
     (elim : ∀c (g h : hom c a), f ∘ g = f ∘ h → g = h)
-  structure is_epi  [class] (f : a ⟶ b) :=
+  structure epi  [class] (f : a ⟶ b) :=
     (elim : ∀c (g h : hom b c), g ∘ f = h ∘ f → g = h)
 
-  definition is_mono_of_is_section [instance] (f : a ⟶ b) [H : is_section f] : is_mono f :=
-  is_mono.mk
+  definition mono_of_split_mono [instance] (f : a ⟶ b) [H : split_mono f] : mono f :=
+  mono.mk
     (λ c g h H,
       calc
         g = id ∘ g                    : by rewrite id_left
-      ... = (retraction_of f ∘ f) ∘ g : by rewrite -retraction_compose
+      ... = (retraction_of f ∘ f) ∘ g : by rewrite -retraction_comp
       ... = (retraction_of f ∘ f) ∘ h : by rewrite [-assoc, H, -assoc]
-      ... = id ∘ h                    : by rewrite retraction_compose
+      ... = id ∘ h                    : by rewrite retraction_comp
       ... = h                         : by rewrite id_left)
 
-  definition is_epi_of_is_retraction [instance] (f : a ⟶ b) [H : is_retraction f] : is_epi f :=
-  is_epi.mk
+  definition epi_of_split_epi [instance] (f : a ⟶ b) [H : split_epi f] : epi f :=
+  epi.mk
     (λ c g h H,
       calc
         g = g ∘ id                 : by rewrite id_right
-      ... = g ∘ f ∘ section_of f   : by rewrite -compose_section
+      ... = g ∘ f ∘ section_of f   : by rewrite -comp_section
       ... = h ∘ f ∘ section_of f   : by rewrite [assoc, H, -assoc]
-      ... = h ∘ id                 : by rewrite compose_section
+      ... = h ∘ id                 : by rewrite comp_section
       ... = h                      : by rewrite id_right)
 
-  definition is_mono_comp [instance] (g : b ⟶ c) (f : a ⟶ b) [Hf : is_mono f] [Hg : is_mono g]
-    : is_mono (g ∘ f) :=
-  is_mono.mk
+  definition mono_comp [instance] (g : b ⟶ c) (f : a ⟶ b) [Hf : mono f] [Hg : mono g]
+    : mono (g ∘ f) :=
+  mono.mk
     (λ d h₁ h₂ H,
     have H2 : g ∘ (f ∘ h₁) = g ∘ (f ∘ h₂),
     begin
       rewrite *assoc, exact H
     end,
-    !is_mono.elim (!is_mono.elim H2))
+    !mono.elim (!mono.elim H2))
 
-  definition is_epi_comp  [instance] (g : b ⟶ c) (f : a ⟶ b) [Hf : is_epi f] [Hg : is_epi g]
-    : is_epi  (g ∘ f) :=
-  is_epi.mk
+  definition epi_comp  [instance] (g : b ⟶ c) (f : a ⟶ b) [Hf : epi f] [Hg : epi g]
+    : epi  (g ∘ f) :=
+  epi.mk
     (λ d h₁ h₂ H,
     have H2 : (h₁ ∘ g) ∘ f = (h₂ ∘ g) ∘ f,
     begin
       rewrite -*assoc, exact H
     end,
-    !is_epi.elim (!is_epi.elim H2))
+    !epi.elim (!epi.elim H2))
 
 end morphism
 
@@ -181,37 +181,37 @@ namespace morphism
   rewrite lemmas for inverses, modified from
   https://github.com/JasonGross/HoTT-categories/blob/master/theories/Categories/Category/Morphisms.v
   -/
-  namespace iso
+  namespace to_fun
   section
   variables {ob : Type} [C : precategory ob] include C
   variables {a b c d : ob}                         (f : b ⟶ a)
                            (r : c ⟶ d) (q : b ⟶ c) (p : a ⟶ b)
                            (g : d ⟶ c)
   variable [Hq : is_iso q] include Hq
-  definition compose_pV : q ∘ q⁻¹ = id := !compose_inverse
-  definition compose_Vp : q⁻¹ ∘ q = id := !inverse_compose
-  definition compose_V_pp : q⁻¹ ∘ (q ∘ p) = p :=
-   by rewrite [assoc, inverse_compose, id_left]
-  definition compose_p_Vp : q ∘ (q⁻¹ ∘ g) = g :=
-   by rewrite [assoc, compose_inverse, id_left]
-  definition compose_pp_V : (r ∘ q) ∘ q⁻¹ = r :=
-  by rewrite [-assoc, compose_inverse, id_right]
-  definition compose_pV_p : (f ∘ q⁻¹) ∘ q = f :=
-  by rewrite [-assoc, inverse_compose, id_right]
+  definition comp.right_inverse : q ∘ q⁻¹ = id := !comp_inverse
+  definition comp.left_inverse : q⁻¹ ∘ q = id := !inverse_comp
+  definition inverse_comp_cancel_left : q⁻¹ ∘ (q ∘ p) = p :=
+   by rewrite [assoc, inverse_comp, id_left]
+  definition comp_inverse_cancel_left : q ∘ (q⁻¹ ∘ g) = g :=
+   by rewrite [assoc, comp_inverse, id_left]
+  definition comp_inverse_cancel_right : (r ∘ q) ∘ q⁻¹ = r :=
+  by rewrite [-assoc, comp_inverse, id_right]
+  definition inverse_comp_cancel_right : (f ∘ q⁻¹) ∘ q = f :=
+  by rewrite [-assoc, inverse_comp, id_right]
 
-  definition con_inv [Hp : is_iso p] [Hpq : is_iso (q ∘ p)] : (q ∘ p)⁻¹ʰ = p⁻¹ʰ ∘ q⁻¹ʰ :=
-  inverse_eq_intro_left
+  definition comp_inverse [Hp : is_iso p] [Hpq : is_iso (q ∘ p)] : (q ∘ p)⁻¹ʰ = p⁻¹ʰ ∘ q⁻¹ʰ :=
+  inverse_eq_left
     (show (p⁻¹ʰ ∘ q⁻¹ʰ) ∘ q ∘ p = id, from
-     by rewrite [-assoc, compose_V_pp, inverse_compose])
+     by rewrite [-assoc, inverse_comp_cancel_left, inverse_comp])
 
-  definition inv_con_inv_left [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q :=
-  inverse_involutive q ▹ con_inv q⁻¹ g
+  definition inverse_comp_inverse_left [H' : is_iso g] : (q⁻¹ ∘ g)⁻¹ = g⁻¹ ∘ q :=
+  inverse_involutive q ▹ comp_inverse q⁻¹ g
 
-  definition inv_con_inv_right [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ :=
-  inverse_involutive f ▹ con_inv q f⁻¹
+  definition inverse_comp_inverse_right [H' : is_iso f] : (q ∘ f⁻¹)⁻¹ = f ∘ q⁻¹ :=
+  inverse_involutive f ▹ comp_inverse q f⁻¹
 
-  definition inv_con_inv_inv [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q :=
-  inverse_involutive r ▹ inv_con_inv_left q r⁻¹
+  definition inverse_comp_inverse_inverse [H' : is_iso r] : (q⁻¹ ∘ r⁻¹)⁻¹ = r ∘ q :=
+  inverse_involutive r ▹ inverse_comp_inverse_left q r⁻¹
   end
 
   section
@@ -224,25 +224,35 @@ namespace morphism
                    {y : d ⟶ b} {w : c ⟶ a}
   variable [Hq : is_iso q] include Hq
 
-  definition con_eq_of_eq_inv_con (H : y = q⁻¹ ∘ g) : q ∘ y = g := H⁻¹ ▹ compose_p_Vp q g
-  definition con_eq_of_eq_con_inv (H : w = f ∘ q⁻¹) : w ∘ q = f := H⁻¹ ▹ compose_pV_p f q
-  definition inv_con_eq_of_eq_con (H : z = q ∘ p) : q⁻¹ ∘ z = p := H⁻¹ ▹ compose_V_pp q p
-  definition con_inv_eq_of_eq_con (H : x = r ∘ q) : x ∘ q⁻¹ = r := H⁻¹ ▹ compose_pp_V r q
-  definition eq_con_of_inv_con_eq (H : q⁻¹ ∘ g = y) : g = q ∘ y := (con_eq_of_eq_inv_con H⁻¹)⁻¹
-  definition eq_con_of_con_inv_eq (H : f ∘ q⁻¹ = w) : f = w ∘ q := (con_eq_of_eq_con_inv H⁻¹)⁻¹
-  definition eq_inv_con_of_con_eq (H : q ∘ p = z) : p = q⁻¹ ∘ z := (inv_con_eq_of_eq_con H⁻¹)⁻¹
-  definition eq_con_inv_of_con_eq (H : r ∘ q = x) : r = x ∘ q⁻¹ := (con_inv_eq_of_eq_con H⁻¹)⁻¹
-  definition eq_inv_of_con_eq_idp' (H : h ∘ q = id) : h = q⁻¹ := (inverse_eq_intro_left H)⁻¹
-  definition eq_inv_of_con_eq_idp (H : q ∘ h = id) : h = q⁻¹ := (inverse_eq_intro_right H)⁻¹
-  definition eq_of_con_inv_eq_idp (H : i ∘ q⁻¹ = id) : i = q :=
-  eq_inv_of_con_eq_idp' H ⬝ inverse_involutive q
-  definition eq_of_inv_con_eq_idp (H : q⁻¹ ∘ i = id) : i = q :=
-  eq_inv_of_con_eq_idp H ⬝ inverse_involutive q
-  definition eq_of_idp_eq_con_inv (H : id = i ∘ q⁻¹) : q = i := (eq_of_con_inv_eq_idp H⁻¹)⁻¹
-  definition eq_of_idp_eq_inv_con (H : id = q⁻¹ ∘ i) : q = i := (eq_of_inv_con_eq_idp H⁻¹)⁻¹
-  definition inv_eq_of_idp_eq_con (H : id = h ∘ q) : q⁻¹ = h := (eq_inv_of_con_eq_idp' H⁻¹)⁻¹
-  definition inv_eq_of_idp_eq_con' (H : id = q ∘ h) : q⁻¹ = h := (eq_inv_of_con_eq_idp H⁻¹)⁻¹
+  definition comp_eq_of_eq_inverse_comp (H : y = q⁻¹ ∘ g) : q ∘ y = g :=
+  H⁻¹ ▹ comp_inverse_cancel_left q g
+  definition comp_eq_of_eq_comp_inverse (H : w = f ∘ q⁻¹) : w ∘ q = f :=
+  H⁻¹ ▹ inverse_comp_cancel_right f q
+  definition inverse_comp_eq_of_eq_comp (H : z = q ∘ p) : q⁻¹ ∘ z = p :=
+  H⁻¹ ▹ inverse_comp_cancel_left q p
+  definition comp_inverse_eq_of_eq_comp (H : x = r ∘ q) : x ∘ q⁻¹ = r :=
+  H⁻¹ ▹ comp_inverse_cancel_right r q
+  definition eq_comp_of_inverse_comp_eq (H : q⁻¹ ∘ g = y) : g = q ∘ y :=
+  (comp_eq_of_eq_inverse_comp H⁻¹)⁻¹
+  definition eq_comp_of_comp_inverse_eq (H : f ∘ q⁻¹ = w) : f = w ∘ q :=
+  (comp_eq_of_eq_comp_inverse H⁻¹)⁻¹
+  definition eq_inverse_comp_of_comp_eq (H : q ∘ p = z) : p = q⁻¹ ∘ z :=
+  (inverse_comp_eq_of_eq_comp H⁻¹)⁻¹
+  definition eq_comp_inverse_of_comp_eq (H : r ∘ q = x) : r = x ∘ q⁻¹ :=
+  (comp_inverse_eq_of_eq_comp H⁻¹)⁻¹
+  definition eq_inverse_of_comp_eq_id' (H : h ∘ q = id) : h = q⁻¹ := (inverse_eq_left H)⁻¹
+  definition eq_inverse_of_comp_eq_id (H : q ∘ h = id) : h = q⁻¹ := (inverse_eq_right H)⁻¹
+  definition eq_of_comp_inverse_eq_id (H : i ∘ q⁻¹ = id) : i = q :=
+  eq_inverse_of_comp_eq_id' H ⬝ inverse_involutive q
+  definition eq_of_inverse_comp_eq_id (H : q⁻¹ ∘ i = id) : i = q :=
+  eq_inverse_of_comp_eq_id H ⬝ inverse_involutive q
+  definition eq_of_id_eq_comp_inverse (H : id = i ∘ q⁻¹) : q = i := (eq_of_comp_inverse_eq_id H⁻¹)⁻¹
+  definition eq_of_id_eq_inverse_comp (H : id = q⁻¹ ∘ i) : q = i := (eq_of_inverse_comp_eq_id H⁻¹)⁻¹
+  definition inverse_eq_of_id_eq_comp (H : id = h ∘ q) : q⁻¹ = h :=
+  (eq_inverse_of_comp_eq_id' H⁻¹)⁻¹
+  definition inverse_eq_of_id_eq_comp' (H : id = q ∘ h) : q⁻¹ = h :=
+  (eq_inverse_of_comp_eq_id H⁻¹)⁻¹
   end
-  end iso
+  end to_fun
 
 end morphism
diff --git a/hott/algebra/precategory/yoneda.hlean b/hott/algebra/precategory/yoneda.hlean
index 1c0bfab50c..24c4bf23f2 100644
--- a/hott/algebra/precategory/yoneda.hlean
+++ b/hott/algebra/precategory/yoneda.hlean
@@ -26,7 +26,7 @@ namespace yoneda
       ... = _ : assoc
 
   --disturbing behaviour: giving the type of f "(x ⟶ y)" explicitly makes the unifier loop
-  definition representable_functor (C : Precategory) : Cᵒᵖ ×c C ⇒ set :=
+  definition hom_functor (C : Precategory) : Cᵒᵖ ×c C ⇒ set :=
   functor.mk (λ(x : Cᵒᵖ ×c C), homset x.1 x.2)
              (λ(x y : Cᵒᵖ ×c C) (f : _) (h : homset x.1 x.2), f.2 ∘⁅ C ⁆ (h ∘⁅ C ⁆ f.1))
              proof (λ(x : Cᵒᵖ ×c C), eq_of_homotopy (λ(h : homset x.1 x.2), !id_left ⬝ !id_right)) qed
@@ -48,7 +48,7 @@ namespace functor
              (λd d' g, F (id, g))
              (λd, !respect_id)
              (λd₁ d₂ d₃ g' g, proof calc
-               F (id, g' ∘ g) = F (id ∘ id, g' ∘ g) : {(id_compose c)⁻¹}
+               F (id, g' ∘ g) = F (id ∘ id, g' ∘ g) : {(id_comp c)⁻¹}
                  ... = F ((id,g') ∘ (id, g)) : idp
                  ... = F (id,g') ∘ F (id, g) : respect_comp F qed)
   local abbreviation Fob := @functor_curry_ob
@@ -66,7 +66,7 @@ namespace functor
   local abbreviation Fhom := @functor_curry_hom
 
   definition functor_curry_hom_def ⦃c c' : C⦄ (f : c ⟶ c') (d : D) :
-    (Fhom F f) d = homF F (f, id) := idp
+    (Fhom F f) d = to_fun_hom F (f, id) := idp
 
   definition functor_curry_id (c : C) : Fhom F (ID c) = nat_trans.id :=
   nat_trans_eq_mk (λd, respect_id F _)
@@ -75,7 +75,7 @@ namespace functor
     : Fhom F (f' ∘ f) = Fhom F f' ∘n Fhom F f :=
   nat_trans_eq_mk (λd, calc
     natural_map (Fhom F (f' ∘ f)) d = F (f' ∘ f, id) : functor_curry_hom_def
-      ... = F (f' ∘ f, id ∘ id) : {(id_compose d)⁻¹}
+      ... = F (f' ∘ f, id ∘ id) : {(id_comp d)⁻¹}
       ... = F ((f',id) ∘ (f, id)) : idp
       ... = F (f',id) ∘ F (f, id) : respect_comp F
       ... = natural_map ((Fhom F f') ∘ (Fhom F f)) d : idp)
@@ -87,35 +87,35 @@ namespace functor
              (functor_curry_comp F)
 
   definition functor_uncurry_ob [reducible] (p : C ×c D) : E :=
-  obF (G p.1) p.2
+  to_fun_ob (G p.1) p.2
   local abbreviation Gob := @functor_uncurry_ob
 
   definition functor_uncurry_hom ⦃p p' : C ×c D⦄ (f : hom p p') : Gob G p ⟶ Gob G p'  :=
-  homF (obF G p'.1) f.2 ∘ natural_map (homF 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
   local abbreviation Ghom := @functor_uncurry_hom
 
   definition functor_uncurry_id (p : C ×c D) : Ghom G (ID p) = id :=
   calc
-    Ghom G (ID p) = homF (obF G p.1) id ∘ natural_map (homF G id) p.2 : idp
-      ... = id ∘ natural_map (homF G id) p.2 : ap (λx, x ∘ _) (respect_id (obF G p.1) p.2)
+    Ghom G (ID p) = to_fun_hom (to_fun_ob G p.1) id ∘ natural_map (to_fun_hom G id) p.2 : idp
+      ... = id ∘ natural_map (to_fun_hom G id) p.2 : ap (λx, x ∘ _) (respect_id (to_fun_ob G p.1) p.2)
       ... = id ∘ natural_map nat_trans.id p.2 : {respect_id G p.1}
-      ... = id : id_compose
+      ... = id : id_comp
 
   definition 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)
-          = homF (obF G p''.1) (f'.2 ∘ f.2) ∘ natural_map (homF G (f'.1 ∘ f.1)) p.2 : idp
-      ... = (homF (obF G p''.1) f'.2 ∘ homF (obF G p''.1) f.2)
-              ∘ natural_map (homF G (f'.1 ∘ f.1)) p.2 : {respect_comp (obF G p''.1) f'.2 f.2}
-      ... = (homF (obF G p''.1) f'.2 ∘ homF (obF G p''.1) f.2)
-              ∘ natural_map (homF G f'.1 ∘ homF G f.1) p.2 : {respect_comp G f'.1 f.1}
-      ... = (homF (obF G p''.1) f'.2 ∘ homF (obF G p''.1) f.2)
-              ∘ (natural_map (homF G f'.1) p.2 ∘ natural_map (homF G f.1) p.2) : idp
-      ... = (homF (obF G p''.1) f'.2 ∘ homF (obF G p''.1) f.2)
-              ∘ (natural_map (homF G f'.1) p.2 ∘ natural_map (homF G f.1) p.2) : idp
-      ... = (homF (obF G p''.1) f'.2 ∘ natural_map (homF G f'.1) p'.2)
-              ∘ (homF (obF G p'.1) f.2 ∘ natural_map (homF G f.1) p.2) :
+          = 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 : idp
+      ... = (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 : {respect_comp (to_fun_ob G p''.1) f'.2 f.2}
+      ... = (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 : {respect_comp G f'.1 f.1}
+      ... = (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) : idp
+      ... = (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) : idp
+      ... = (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) :
                   square_prepostcompose (!naturality⁻¹ᵖ) _ _
       ... = Ghom G f' ∘ Ghom G f : idp
 
@@ -144,20 +144,20 @@ namespace functor
   --      apply idp
   --     end))))
 
-  -- definition functor_eq_mk1 {F₁ F₂ : C ⇒ D} : Π(p : obF F₁ = obF F₂),
+  -- definition functor_eq_mk1 {F₁ F₂ : C ⇒ D} : Π(p : to_fun_ob F₁ = to_fun_ob F₂),
   --   (Π(a b : C) (f : hom a b), transport (λF, hom (F a) (F b)) p (F₁ f) = F₂ f)
   --     → F₁ = F₂ :=
   -- functor.rec_on F₁ (λO₁ H₁ id₁ comp₁, functor.rec_on F₂ (λO₂ H₂ id₂ comp₂ p, !functor_eq_mk'1))
 
   --set_option pp.notation false
   definition functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F :=
-  functor_eq_mk (λp, ap (obF F) !prod.eta)
+  functor_eq_mk (λp, ap (to_fun_ob F) !prod.eta)
   begin
     intros (cd, cd', fg),
     cases cd with (c,d), cases cd' with (c',d'), cases fg with (f,g),
     have H : (functor_uncurry (functor_curry F)) (f, g) = F (f,g),
       from calc
-        (functor_uncurry (functor_curry F)) (f, g) = homF F (id, g) ∘ homF F (f, id) : idp
+        (functor_uncurry (functor_curry F)) (f, g) = to_fun_hom F (id, g) ∘ to_fun_hom F (f, id) : idp
           ... = F (id ∘ f, g ∘ id) : respect_comp F (id,g) (f,id)
           ... = F (f, g ∘ id) : {id_left f}
           ... = F (f,g) : {id_right g},
@@ -172,13 +172,13 @@ namespace functor
       fapply functor_eq_mk,
        {intro d, apply idp},
        {intros (d, d', g),
-        have H : homF (functor_curry (functor_uncurry G) c) g = homF (G c) g,
+        have H : to_fun_hom (functor_curry (functor_uncurry G) c) g = to_fun_hom (G c) g,
         from calc
-          homF (functor_curry (functor_uncurry G) c) g
-                = homF (G c) g ∘ natural_map (homF G (ID c)) d : idp
-            ... = homF (G c) g ∘ natural_map (ID (G c)) d
-                   : ap (λx, homF (G c) g ∘ natural_map x d) (respect_id G c)
-            ... = homF (G c) g : id_right,
+          to_fun_hom (functor_curry (functor_uncurry G) c) g
+                = to_fun_hom (G c) g ∘ natural_map (to_fun_hom G (ID c)) d : idp
+            ... = to_fun_hom (G c) g ∘ natural_map (ID (G c)) d
+                   : ap (λx, to_fun_hom (G c) g ∘ natural_map x d) (respect_id G c)
+            ... = to_fun_hom (G c) g : id_right,
         rewrite H,
 --        esimp {idp},
         apply sorry
@@ -199,7 +199,7 @@ namespace functor
 
 
   definition contravariant_yoneda_embedding : Cᵒᵖ ⇒ set ^c C :=
-  functor_curry !yoneda.representable_functor
+  functor_curry !yoneda.hom_functor
 
 end functor
 
@@ -209,8 +209,8 @@ end functor
 --   --universe levels are given explicitly because Lean uses 6 variables otherwise
 
 --   structure adjoint.{u v} [C D : Precategory.{u v}] (F : C ⇒ D) (G : D ⇒ C) : Type.{max u v} :=
---   (nat_iso : (representable_functor D) ∘f (prod_functor (opposite_functor F) (functor.ID D)) ⟹
---              (representable_functor C) ∘f (prod_functor (functor.ID (Cᵒᵖ)) G))
+--   (nat_iso : (hom_functor D) ∘f (prod_functor (opposite_functor F) (functor.ID D)) ⟹
+--              (hom_functor C) ∘f (prod_functor (functor.ID (Cᵒᵖ)) G))
 --   (is_iso_nat_iso : is_iso nat_iso)
 
 --   infix `⊣`:55 := adjoint
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index 2b8b427044..ee37eb0654 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -109,7 +109,7 @@ namespace is_equiv
       have eq1 : ap f (sec a) = _,
         from calc ap f (sec a)
               = idp ⬝ ap f (sec a) : !idp_con⁻¹
-          ... = (ret (f a) ⬝ (ret (f a))⁻¹) ⬝ ap f (sec a) : {!con.left_inv⁻¹}
+          ... = (ret (f a) ⬝ (ret (f a))⁻¹) ⬝ ap f (sec a) : {!con.right_inv⁻¹}
           ... = ((ret fgfa)⁻¹ ⬝ ap (f ∘ g) (ret (f a))) ⬝ ap f (sec a) : {!con_ap_eq_con⁻¹}
           ... = ((ret fgfa)⁻¹ ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _}
           ... = (ret fgfa)⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)) : !con.assoc,
@@ -180,11 +180,11 @@ namespace is_equiv
           ◾ (inverse (ap_compose f⁻¹ f _))
           ◾ (adj f _)⁻¹)
         ⬝ con_ap_con_eq_con_con (retr f) _ _
-        ⬝ whisker_right !con.right_inv _
+        ⬝ whisker_right !con.left_inv _
         ⬝ !idp_con)
       (λp, whisker_right (whisker_left _ (ap_compose f f⁻¹ _)⁻¹) _
         ⬝ con_ap_con_eq_con_con (sect f) _ _
-        ⬝ whisker_right !con.right_inv _
+        ⬝ whisker_right !con.left_inv _
         ⬝ !idp_con)
 
   -- The function equiv_rect says that given an equivalence f : A → B,
diff --git a/hott/init/path.hlean b/hott/init/path.hlean
index 231d9f8a58..01dc347819 100644
--- a/hott/init/path.hlean
+++ b/hott/init/path.hlean
@@ -66,11 +66,11 @@ namespace eq
   eq.rec_on r (eq.rec_on q idp)
 
   -- The left inverse law.
-  definition con.left_inv (p : x = y) : p ⬝ p⁻¹ = idp :=
+  definition con.right_inv (p : x = y) : p ⬝ p⁻¹ = idp :=
   eq.rec_on p idp
 
   -- The right inverse law.
-  definition con.right_inv (p : x = y) : p⁻¹ ⬝ p = idp :=
+  definition con.left_inv (p : x = y) : p⁻¹ ⬝ p = idp :=
   eq.rec_on p idp
 
   /- Several auxiliary theorems about canceling inverses across associativity. These are somewhat
@@ -408,11 +408,11 @@ namespace eq
 
   definition tr_inv_tr (P : A → Type) {x y : A} (p : x = y) (z : P y) :
     p ▹ p⁻¹ ▹ z = z :=
-  (tr_con P p⁻¹ p z)⁻¹ ⬝ ap (λr, transport P r z) (con.right_inv p)
+  (tr_con P p⁻¹ p z)⁻¹ ⬝ ap (λr, transport P r z) (con.left_inv p)
 
   definition inv_tr_tr (P : A → Type) {x y : A} (p : x = y) (z : P x) :
     p⁻¹ ▹ p ▹ z = z :=
-  (tr_con P p p⁻¹ z)⁻¹ ⬝ ap (λr, transport P r z) (con.left_inv p)
+  (tr_con P p p⁻¹ z)⁻¹ ⬝ ap (λr, transport P r z) (con.right_inv p)
 
   definition tr_con_lemma (P : A → Type)
       {x y z w : A} (p : x = y) (q : y = z) (r : z = w) (u : P x) :
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index b71ff16df5..297d15d9fa 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -105,7 +105,7 @@ namespace is_trunc
   (contr x)⁻¹ ⬝ (contr y)
 
   definition hprop_eq {A : Type} [H : is_contr A] {x y : A} (p q : x = y) : p = q :=
-  have K : ∀ (r : x = y), center_eq x y = r, from (λ r, eq.rec_on r !con.right_inv),
+  have K : ∀ (r : x = y), center_eq x y = r, from (λ r, eq.rec_on r !con.left_inv),
   (K p)⁻¹ ⬝ K q
 
   definition is_contr_eq [instance] {A : Type} [H : is_contr A] (x y : A) : is_contr (x = y)
diff --git a/script/rename.pl b/script/rename.pl
index 6c51a7513f..e1ecc9faf8 100755
--- a/script/rename.pl
+++ b/script/rename.pl
@@ -65,7 +65,7 @@ sub rename_in_file {
 	foreach my $key (keys %renamings) {
 	    # replace instances of key, not preceeded by a letter, and not
 	    # followed by a letter, number, ', or .
-	    s/(?<![a-zA-z])$key(?![w'.])/$renamings{$key}/g;
+	    s/(?<![a-zA-z])$key(?![\w'])/$renamings{$key}/g;
 	}
 	print;
     }