diff --git a/hott/algebra/e_closure.hlean b/hott/algebra/e_closure.hlean
index 46b5c3cb7..3048e6938 100644
--- a/hott/algebra/e_closure.hlean
+++ b/hott/algebra/e_closure.hlean
@@ -171,15 +171,15 @@ section
   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'), 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 :=
+    (q : Π⦃a a' : A⦄ (s : R a a'), apd g' (p s) = po s)
+    (t : T a a') : apd g' (e_closure.elim p t) = e_closure.elimo p po t :=
   begin
     induction t with a a' r a a' pp a a' r IH a a' a'' r r' IH₁ IH₂,
       apply q,
       induction pp, reflexivity,
       esimp [e_closure.elim],
-      exact apdo_inv g' (e_closure.elim p r) ⬝ IH⁻²ᵒ,
-      exact apdo_con g' (e_closure.elim p r) (e_closure.elim p r') ⬝ (IH₁ ◾o IH₂)
+      exact apd_inv g' (e_closure.elim p r) ⬝ IH⁻²ᵒ,
+      exact apd_con g' (e_closure.elim p r) (e_closure.elim p r') ⬝ (IH₁ ◾o IH₂)
   end
 
   theorem e_closure_elimo_ap {g' : Π(a : A), Q (g (f a))}
diff --git a/hott/cubical/pathover2.hlean b/hott/cubical/pathover2.hlean
index 193ac69c7..e0a41b123 100644
--- a/hott/cubical/pathover2.hlean
+++ b/hott/cubical/pathover2.hlean
@@ -37,8 +37,8 @@ namespace eq
     : pathover_of_tr_eq r = pathover_tr p b ⬝o pathover_idp_of_eq r :=
   by induction r; induction p; reflexivity
 
-  definition apo011_eq_apo11_apdo (f : Πa, B a → A') (p : a = a₂) (q : b =[p] b₂)
-      : apo011 f p q = eq_of_pathover (apo11 (apdo f p) q) :=
+  definition apo011_eq_apo11_apd (f : Πa, B a → A') (p : a = a₂) (q : b =[p] b₂)
+      : apo011 f p q = eq_of_pathover (apo11 (apd f p) q) :=
   by induction q; reflexivity
 
   definition change_path_con (q : p = p') (q' : p' = p'') (r : b =[p] b₂) :
@@ -92,23 +92,23 @@ namespace eq
     { intro r, induction q, reflexivity},
   end
 
-  definition apdo_ap {B : A' → Type} (g : Πb, B b) (f : A → A') (p : a = a₂)
-    :  apdo g (ap f p) = pathover_ap B f (apdo (λx, g (f x)) p)  :=
+  definition apd_ap {B : A' → Type} (g : Πb, B b) (f : A → A') (p : a = a₂)
+    :  apd g (ap f p) = pathover_ap B f (apd (λx, g (f x)) p)  :=
   by induction p; reflexivity
 
-  definition apdo_eq_apdo_ap {B : A' → Type} (g : Πb, B b) (f : A → A') (p : a = a₂)
-    : apdo (λx, g (f x)) p = pathover_of_pathover_ap B f (apdo g (ap f p)) :=
+  definition apd_eq_apd_ap {B : A' → Type} (g : Πb, B b) (f : A → A') (p : a = a₂)
+    : apd (λx, g (f x)) p = pathover_of_pathover_ap B f (apd g (ap f p)) :=
   by induction p; reflexivity
 
   definition ap_compose_ap02_constant {A B C : Type} {a a' : A} (p : a = a') (b : B) (c : C) :
   ap_compose (λc, b) (λa, c) p ⬝ ap02 (λc, b) (ap_constant p c) = ap_constant p b :=
   by induction p; reflexivity
 
-  theorem apdo_constant (b : B'' a') (p : a = a) :
-    pathover_ap B'' (λa, a') (apdo (λa, b) p) = change_path (ap_constant p a')⁻¹ idpo :=
+  theorem apd_constant (b : B'' a') (p : a = a) :
+    pathover_ap B'' (λa, a') (apd (λa, b) p) = change_path (ap_constant p a')⁻¹ idpo :=
   begin
-    rewrite [apdo_eq_apdo_ap _ _ p],
-    let y := !change_path_of_pathover (apdo (apdo id) (ap_constant p b))⁻¹ᵒ,
+    rewrite [apd_eq_apd_ap _ _ p],
+    let y := !change_path_of_pathover (apd (apd id) (ap_constant p b))⁻¹ᵒ,
     rewrite -y, esimp,
     refine !pathover_ap_pathover_of_pathover_ap ⬝ _,
     rewrite pathover_ap_change_path,
@@ -117,8 +117,8 @@ namespace eq
     apply ap_compose_ap02_constant
   end
 
-  definition apdo_change_path {B : A → Type} {a a₂ : A} (f : Πa, B a) {p p' : a = a₂} (s : p = p')
-    : apdo f p' = change_path s (apdo f p) :=
+  definition apd_change_path {B : A → Type} {a a₂ : A} (f : Πa, B a) {p p' : a = a₂} (s : p = p')
+    : apd f p' = change_path s (apd f p) :=
   by induction s; reflexivity
 
   definition cono_invo_eq_idpo {q q' : b =[p] b₂} (r : q = q')
diff --git a/hott/cubical/squareover.hlean b/hott/cubical/squareover.hlean
index e3d048487..8abf3f3ff 100644
--- a/hott/cubical/squareover.hlean
+++ b/hott/cubical/squareover.hlean
@@ -49,7 +49,7 @@ namespace eq
   definition idso      [reducible] [constructor]               := @squareover.idsquareo A B a₀₀ b₀₀
 
   definition apds (f : Πa, B a) (s : square p₁₀ p₁₂ p₀₁ p₂₁)
-    : squareover B s (apdo f p₁₀) (apdo f p₁₂) (apdo f p₀₁) (apdo f p₂₁) :=
+    : squareover B s (apd f p₁₀) (apd f p₁₂) (apd f p₀₁) (apd f p₂₁) :=
   square.rec_on s idso
 
   definition vrflo : squareover B vrfl q₁₀ q₁₀ idpo idpo :=
@@ -244,7 +244,7 @@ namespace eq
   /- A version of eq_pathover where the type of the equality also varies -/
   definition eq_pathover_dep {f g : Πa, B a} {p : a = a'} {q : f a = g a}
     {r : f a' = g a'} (s : squareover B hrfl (pathover_idp_of_eq q) (pathover_idp_of_eq r)
-                                             (apdo f p) (apdo g p)) : q =[p] r :=
+                                             (apd f p) (apd g p)) : q =[p] r :=
   begin
     induction p, apply pathover_idp_of_eq, apply eq_of_vdeg_square, exact square_of_squareover_ids s
   end
@@ -256,7 +256,7 @@ namespace eq
     (r : pathover B (b a') (q a') (b₂ a'))
     (r₂ : pathover B (b a₂') (q a₂') (b₂ a₂'))
     (s : squareover B (natural_square_tr q p) r r₂
-                      (pathover_ap B f (apdo b p)) (pathover_ap B g (apdo b₂ p)))
+                      (pathover_ap B f (apd b p)) (pathover_ap B g (apd b₂ p)))
     : pathover (λa, pathover B (b a) (q a) (b₂ a)) r p r₂ :=
   begin
     induction p, esimp at s, apply pathover_idp_of_eq, apply eq_of_vdeg_squareover, exact s
diff --git a/hott/eq2.hlean b/hott/eq2.hlean
index 493ab7d79..556398361 100644
--- a/hott/eq2.hlean
+++ b/hott/eq2.hlean
@@ -14,7 +14,7 @@ namespace eq
 
   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)))⁻¹ ⬝
+      eq_con_inv_of_con_eq ((eq_of_square (square_of_pathover (apd p q)))⁻¹ ⬝
       whisker_left (p a) (ap_constant q b)) :=
   begin
     induction q, esimp, generalize (p a), intro p, cases p, apply idpath idp
@@ -105,9 +105,9 @@ namespace eq
   : eq_of_con_inv_eq_idp (r ◾ inverse2 s ⬝ t) = r ⬝ eq_of_con_inv_eq_idp t ⬝ s⁻¹ :=
   by induction s;induction r;induction q;reflexivity
 
-  definition naturality_apdo_eq {A : Type} {B : A → Type} {a a₂ : A} {f g : Πa, B a}
+  definition naturality_apd_eq {A : Type} {B : A → Type} {a a₂ : A} {f g : Πa, B a}
     (H : f ~ g) (p : a = a₂)
-    : apdo f p = concato_eq (eq_concato (H a) (apdo g p)) (H a₂)⁻¹ :=
+    : apd f p = concato_eq (eq_concato (H a) (apd g p)) (H a₂)⁻¹ :=
   begin
     induction p, esimp,
     generalizes [H a, g a], intro ga Ha, induction Ha,
diff --git a/hott/hit/coeq.hlean b/hott/hit/coeq.hlean
index d10da154c..d88138c9a 100644
--- a/hott/hit/coeq.hlean
+++ b/hott/hit/coeq.hlean
@@ -44,7 +44,7 @@ parameters {A B : Type.{u}} (f g : A → B)
 
   theorem rec_cp {P : coeq → Type} (P_i : Π(x : B), P (coeq_i x))
     (Pcp : Π(x : A), P_i (f x) =[cp x] P_i (g x))
-      (x : A) : apdo (rec P_i Pcp) (cp x) = Pcp x :=
+      (x : A) : apd (rec P_i Pcp) (cp x) = Pcp x :=
   !rec_eq_of_rel
 
   protected definition elim {P : Type} (P_i : B → P)
@@ -59,7 +59,7 @@ parameters {A B : Type.{u}} (f g : A → B)
     (x : A) : ap (elim P_i Pcp) (cp x) = Pcp x :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant (cp x)),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_cp],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_cp],
   end
 
   protected definition elim_type (P_i : B → Type)
diff --git a/hott/hit/colimit.hlean b/hott/hit/colimit.hlean
index f877f4a96..a9d2fd38e 100644
--- a/hott/hit/colimit.hlean
+++ b/hott/hit/colimit.hlean
@@ -50,7 +50,7 @@ section
   theorem rec_cglue {P : colimit → Type}
     (Pincl : Π⦃i : I⦄ (x : A i), P (ι x))
     (Pglue : Π(j : J) (x : A (dom j)), Pincl (f j x) =[cglue j x] Pincl x)
-      {j : J} (x : A (dom j)) : apdo (rec Pincl Pglue) (cglue j x) = Pglue j x :=
+      {j : J} (x : A (dom j)) : apd (rec Pincl Pglue) (cglue j x) = Pglue j x :=
   !rec_eq_of_rel
 
   protected definition elim {P : Type} (Pincl : Π⦃i : I⦄ (x : A i), P)
@@ -68,7 +68,7 @@ section
       {j : J} (x : A (dom j)) : ap (elim Pincl Pglue) (cglue j x) = Pglue j x :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant (cglue j x)),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_cglue],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_cglue],
   end
 
   protected definition elim_type (Pincl : Π⦃i : I⦄ (x : A i), Type)
@@ -141,7 +141,7 @@ section
 
   theorem rec_glue {P : seq_colim → Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P (sι a))
     (Pglue : Π⦃n : ℕ⦄ (a : A n), Pincl (f a) =[glue a] Pincl a) {n : ℕ} (a : A n)
-      : apdo (rec Pincl Pglue) (glue a) = Pglue a :=
+      : apd (rec Pincl Pglue) (glue a) = Pglue a :=
   !rec_eq_of_rel
 
   protected definition elim {P : Type} (Pincl : Π⦃n : ℕ⦄ (a : A n), P)
@@ -158,7 +158,7 @@ section
       : ap (elim Pincl Pglue) (glue a) = Pglue a :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant (glue a)),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_glue],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_glue],
   end
 
   protected definition elim_type (Pincl : Π⦃n : ℕ⦄ (a : A n), Type)
diff --git a/hott/hit/pushout.hlean b/hott/hit/pushout.hlean
index f9fd7d51e..4efe06248 100644
--- a/hott/hit/pushout.hlean
+++ b/hott/hit/pushout.hlean
@@ -51,7 +51,7 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
 
   theorem rec_glue {P : pushout → Type} (Pinl : Π(x : BL), P (inl x))
     (Pinr : Π(x : TR), P (inr x)) (Pglue : Π(x : TL), Pinl (f x) =[glue x] Pinr (g x))
-      (x : TL) : apdo (rec Pinl Pinr Pglue) (glue x) = Pglue x :=
+      (x : TL) : apd (rec Pinl Pinr Pglue) (glue x) = Pglue x :=
   !rec_eq_of_rel
 
   protected definition elim {P : Type} (Pinl : BL → P) (Pinr : TR → P)
@@ -67,7 +67,7 @@ parameters {TL BL TR : Type} (f : TL → BL) (g : TL → TR)
     : ap (elim Pinl Pinr Pglue) (glue x) = Pglue x :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant (glue x)),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑pushout.elim,rec_glue],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑pushout.elim,rec_glue],
   end
 
   protected definition elim_type (Pinl : BL → Type) (Pinr : TR → Type)
diff --git a/hott/hit/quotient.hlean b/hott/hit/quotient.hlean
index 1663af705..94968740c 100644
--- a/hott/hit/quotient.hlean
+++ b/hott/hit/quotient.hlean
@@ -35,7 +35,7 @@ namespace quotient
     : ap (quotient.elim Pc Pp) (eq_of_rel R H) = Pp H :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant (eq_of_rel R H)),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑quotient.elim,rec_eq_of_rel],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑quotient.elim,rec_eq_of_rel],
   end
 
   protected definition rec_prop {A : Type} {R : A → A → Type} {P : quotient R → Type}
@@ -89,7 +89,7 @@ namespace quotient
       (Σ(f : Π(a : A), C (class_of R a)),  Π⦃a a' : A⦄ (H : R a a'), f a =[eq_of_rel R H] f a') :=
     begin
       fapply equiv.MK,
-      { intro f, exact ⟨λa, f (class_of R a), λa a' H, apdo f (eq_of_rel R H)⟩},
+      { intro f, exact ⟨λa, f (class_of R a), λa a' H, apd f (eq_of_rel R H)⟩},
       { intro v x, induction v with i p, induction x,
           exact (i a),
           exact (p H)},
@@ -166,7 +166,7 @@ namespace quotient
       (c : C a) : ap (elim @Qpt Qeq) (Peq r c) = Qeq r c :=
     begin
       refine !ap_dpair_eq_dpair ⬝ _,
-      rewrite [apo011_eq_apo11_apdo, rec_eq_of_rel, ▸*, apo011_arrow_pathover_constant_right,
+      rewrite [apo011_eq_apo11_apd, rec_eq_of_rel, ▸*, apo011_arrow_pathover_constant_right,
                ↑elim_type_eq_of_rel', to_right_inv !pathover_equiv_tr_eq, ap_inv],
       apply inv_con_cancel_right
     end
diff --git a/hott/hit/refl_quotient.hlean b/hott/hit/refl_quotient.hlean
index 3f5cc05e1..010a30705 100644
--- a/hott/hit/refl_quotient.hlean
+++ b/hott/hit/refl_quotient.hlean
@@ -47,7 +47,7 @@ section
   definition rec_req_of_rel {P : Type} {P : refl_quotient → Type} (Pc : Π(a : A), P (rclass_of a))
     (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[req_of_rel H] Pc a')
     (Pr : Π(a : A), change_path (pρ a) (Pp (ρ a)) = idpo) ⦃a a' : A⦄ (r : R a a')
-    : apdo (rec Pc Pp Pr) (req_of_rel r) = Pp r :=
+    : apd (rec Pc Pp Pr) (req_of_rel r) = Pp r :=
   !rec_incl1
 
   protected definition elim {P : Type} (Pc : Π(a : A), P)
diff --git a/hott/hit/set_quotient.hlean b/hott/hit/set_quotient.hlean
index 9b75b648e..5b0574174 100644
--- a/hott/hit/set_quotient.hlean
+++ b/hott/hit/set_quotient.hlean
@@ -44,7 +44,7 @@ section
 
   theorem rec_eq_of_rel {P : set_quotient → Type} [Pt : Πaa, is_set (P aa)]
     (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel H] Pc a')
-    {a a' : A} (H : R a a') : apdo (rec Pc Pp) (eq_of_rel H) = Pp H :=
+    {a a' : A} (H : R a a') : apd (rec Pc Pp) (eq_of_rel H) = Pp H :=
   !is_set.elimo
 
   protected definition elim {P : Type} [Pt : is_set P] (Pc : A → P)
@@ -60,7 +60,7 @@ section
     : ap (elim Pc Pp) (eq_of_rel H) = Pp H :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant (eq_of_rel H)),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_eq_of_rel],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_eq_of_rel],
   end
 
   protected definition rec_prop {P : set_quotient → Type} [Pt : Πaa, is_prop (P aa)]
diff --git a/hott/hit/two_quotient.hlean b/hott/hit/two_quotient.hlean
index e96e346da..baafed5b9 100644
--- a/hott/hit/two_quotient.hlean
+++ b/hott/hit/two_quotient.hlean
@@ -76,7 +76,7 @@ namespace simple_two_quotient
   protected theorem rec_e {P : C → Type}
     (Pj : Πa, P (j a)) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), P (pre_aux q))
     (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a =[e s] Pj a') ⦃a a' : A⦄ (s : R a a')
-    : apdo (pre_rec Pj Pa Pe) (e s) = Pe s :=
+    : apd (pre_rec Pj Pa Pe) (e s) = Pe s :=
   !rec_eq_of_rel
 
   protected theorem elim_e {P : Type} (Pj : A → P) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄, Q r → P)
@@ -84,7 +84,7 @@ namespace simple_two_quotient
     : ap (pre_elim Pj Pa Pe) (e s) = Pe s :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant (e s)),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑pre_elim,rec_e],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑pre_elim,rec_e],
   end
 
   protected definition elim_et {P : Type} (Pj : A → P) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄, Q r → P)
@@ -95,7 +95,7 @@ namespace simple_two_quotient
   protected definition rec_et {P : C → Type}
     (Pj : Πa, P (j a)) (Pa : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r), P (pre_aux q))
     (Pe : Π⦃a a' : A⦄ (s : R a a'), Pj a =[e s] Pj a') ⦃a a' : A⦄ (t : T a a')
-    : apdo (pre_rec Pj Pa Pe) (et t) = e_closure.elimo e Pe t :=
+    : apd (pre_rec Pj Pa Pe) (et t) = e_closure.elimo e Pe t :=
   ap_e_closure_elimo_h e Pe (rec_e Pj Pa Pe) t
 
   inductive simple_two_quotient_rel : C → C → Type :=
@@ -151,9 +151,9 @@ namespace simple_two_quotient
         refine eq_hconcato _ _, apply _,
         { transitivity _,
           { apply ap (pathover_ap _ _),
-            transitivity _, apply apdo_compose2 (pre_rec P0 _ _) (f q) loop,
+            transitivity _, apply apd_compose2 (pre_rec P0 _ _) (f q) loop,
             apply ap (pathover_of_pathover_ap _ _),
-            transitivity _, apply apdo_change_path, exact !elim_loop⁻¹,
+            transitivity _, apply apd_change_path, exact !elim_loop⁻¹,
             transitivity _,
               apply ap (change_path _),
               transitivity _, apply rec_et,
@@ -171,7 +171,7 @@ namespace simple_two_quotient
           rewrite [↑incl2, con_inv], transitivity _, exact !con.assoc⁻¹,
           rewrite [inv_con_cancel_right, ↑incl2w, ↑ap02, +con_inv, +ap_inv, +inv_inv, -+con.assoc,
             +con_inv_cancel_right], reflexivity},
-        rewrite [change_path_con, apdo_constant],
+        rewrite [change_path_con, apd_constant],
         apply squareover_change_path_left, apply squareover_change_path_right',
         apply squareover_change_path_left,
         refine change_square _ vrflo,
@@ -189,9 +189,9 @@ namespace simple_two_quotient
     (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
     (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r),
       change_path (incl2 q) (e_closure.elimo incl1 P1 r) = idpo) ⦃a a' : A⦄ (s : R a a')
-    : apdo (rec P0 P1 P2) (incl1 s) = P1 s :=
+    : apd (rec P0 P1 P2) (incl1 s) = P1 s :=
   begin
-    unfold [rec, incl1], refine !apdo_ap ⬝ _, esimp, rewrite rec_e,
+    unfold [rec, incl1], refine !apd_ap ⬝ _, esimp, rewrite rec_e,
     apply to_right_inv !pathover_compose
   end
 
@@ -199,7 +199,7 @@ namespace simple_two_quotient
     (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
     (P2 : Π⦃a : A⦄ ⦃r : T a a⦄ (q : Q r),
       change_path (incl2 q) (e_closure.elimo incl1 P1 r) = idpo) ⦃a a' : A⦄ (t : T a a')
-    : apdo (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t :=
+    : apd (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t :=
   ap_e_closure_elimo_h incl1 P1 (rec_incl1 P0 P1 P2) t
 
   protected definition elim {P : Type} (P0 : A → P)
@@ -288,7 +288,7 @@ namespace simple_two_quotient
                ↑[elim_incltw]],
     apply whisker_tl,
     rewrite [ap_is_constant_eq],
-    xrewrite [naturality_apdo_eq (λx, !elim_eq_of_rel) loop],
+    xrewrite [naturality_apd_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],
     apply eq_vconcat,
@@ -390,14 +390,14 @@ namespace two_quotient
     (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
     (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
       change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t')
-    ⦃a a' : A⦄ (s : R a a') : apdo (rec P0 P1 P2) (incl1 s) = P1 s :=
+    ⦃a a' : A⦄ (s : R a a') : apd (rec P0 P1 P2) (incl1 s) = P1 s :=
   rec_incl1 _ _ _ s
 
   theorem rec_inclt {P : two_quotient → Type} (P0 : Π(a : A), P (incl0 a))
     (P1 : Π⦃a a' : A⦄ (s : R a a'), P0 a =[incl1 s] P0 a')
     (P2 : Π⦃a a' : A⦄ ⦃t t' : T a a'⦄ (q : Q t t'),
       change_path (incl2 q) (e_closure.elimo incl1 P1 t) = e_closure.elimo incl1 P1 t')
-    ⦃a a' : A⦄ (t : T a a') : apdo (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t :=
+    ⦃a a' : A⦄ (t : T a a') : apd (rec P0 P1 P2) (inclt t) = e_closure.elimo incl1 P1 t :=
   rec_inclt _ _ _ t
 
   protected definition elim {P : Type} (P0 : A → P)
diff --git a/hott/homotopy/circle.hlean b/hott/homotopy/circle.hlean
index 8c810a98a..e257d97be 100644
--- a/hott/homotopy/circle.hlean
+++ b/hott/homotopy/circle.hlean
@@ -42,12 +42,12 @@ namespace circle
 
   theorem rec2_seg1 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
     (Ps1 : Pb1 =[seg1] Pb2) (Ps2 : Pb1 =[seg2] Pb2)
-      : apdo (rec2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 :=
+      : apd (rec2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 :=
   !rec_merid
 
   theorem rec2_seg2 {P : circle → Type} (Pb1 : P base1) (Pb2 : P base2)
     (Ps1 : Pb1 =[seg1] Pb2) (Ps2 : Pb1 =[seg2] Pb2)
-      : apdo (rec2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
+      : apd (rec2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
   !rec_merid
 
   definition elim2 {P : Type} (Pb1 Pb2 : P) (Ps1 Ps2 : Pb1 = Pb2) (x : circle) : P :=
@@ -61,14 +61,14 @@ namespace circle
     : ap (elim2 Pb1 Pb2 Ps1 Ps2) seg1 = Ps1 :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant seg1),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim2,rec2_seg1],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim2,rec2_seg1],
   end
 
   theorem elim2_seg2 {P : Type} (Pb1 Pb2 : P) (Ps1 : Pb1 = Pb2) (Ps2 : Pb1 = Pb2)
     : ap (elim2 Pb1 Pb2 Ps1 Ps2) seg2 = Ps2 :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant seg2),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim2,rec2_seg2],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim2,rec2_seg2],
   end
 
   definition elim2_type (Pb1 Pb2 : Type) (Ps1 Ps2 : Pb1 ≃ Pb2) (x : circle) : Type :=
@@ -109,9 +109,9 @@ namespace circle
   eq.rec_on p idp
 
   theorem rec_loop {P : circle → Type} (Pbase : P base) (Ploop : Pbase =[loop] Pbase) :
-    apdo (circle.rec Pbase Ploop) loop = Ploop :=
+    apd (circle.rec Pbase Ploop) loop = Ploop :=
   begin
-    rewrite [↑loop,apdo_con,↑circle.rec,↑circle.rec2_on,↑base,rec2_seg2,apdo_inv,rec2_seg1],
+    rewrite [↑loop,apd_con,↑circle.rec,↑circle.rec2_on,↑base,rec2_seg2,apd_inv,rec2_seg1],
     apply rec_loop_helper
   end
 
@@ -127,14 +127,14 @@ namespace circle
     ap (circle.elim Pbase Ploop) loop = Ploop :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant loop),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑circle.elim,rec_loop],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑circle.elim,rec_loop],
   end
 
   theorem elim_seg1 {P : Type} (Pbase : P) (Ploop : Pbase = Pbase)
     : ap (circle.elim Pbase Ploop) seg1 = (tr_constant seg1 Pbase)⁻¹ :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant seg1),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑circle.elim,↑circle.rec],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑circle.elim,↑circle.rec],
     rewrite [↑circle.rec2_on,rec2_seg1], apply inverse,
     apply pathover_of_eq_tr_constant_inv
   end
@@ -143,7 +143,7 @@ namespace circle
     : ap (circle.elim Pbase Ploop) seg2 = Ploop ⬝ (tr_constant seg1 Pbase)⁻¹ :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant seg2),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑circle.elim,↑circle.rec],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑circle.elim,↑circle.rec],
     rewrite [↑circle.rec2_on,rec2_seg2],
     assert l : Π(A B : Type)(a a₂ a₂' : A)(b b' : B)(p : a = a₂)(p' : a₂' = a₂)
                    (q : b = b'),
@@ -188,7 +188,7 @@ namespace circle
     : (Π(x : S¹), P x) ≃ Σ(p : P base), p =[loop] p :=
   begin
     fapply equiv.MK,
-    { intro f, exact ⟨f base, apdo f loop⟩},
+    { intro f, exact ⟨f base, apd f loop⟩},
     { intro v x, induction v with p q, induction x,
       { exact p},
       { exact q}},
diff --git a/hott/homotopy/cylinder.hlean b/hott/homotopy/cylinder.hlean
index 62f661c67..410da225f 100644
--- a/hott/homotopy/cylinder.hlean
+++ b/hott/homotopy/cylinder.hlean
@@ -52,7 +52,7 @@ parameters {A B : Type.{u}} (f : A → B)
   theorem rec_seg {P : cylinder → Type}
     (Pbase : Π(b : B), P (base b)) (Ptop : Π(a : A), P (top a))
     (Pseg : Π(a : A), Pbase (f a) =[seg a] Ptop a)
-      (a : A) : apdo (rec Pbase Ptop Pseg) (seg a) = Pseg a :=
+      (a : A) : apd (rec Pbase Ptop Pseg) (seg a) = Pseg a :=
   !rec_eq_of_rel
 
   protected definition elim {P : Type} (Pbase : B → P) (Ptop : A → P)
@@ -68,7 +68,7 @@ parameters {A B : Type.{u}} (f : A → B)
     (a : A) : ap (elim Pbase Ptop Pseg) (seg a) = Pseg a :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant (seg a)),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_seg],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_seg],
   end
 
   protected definition elim_type (Pbase : B → Type) (Ptop : A → Type)
diff --git a/hott/homotopy/interval.hlean b/hott/homotopy/interval.hlean
index 154511c4e..c25e103f3 100644
--- a/hott/homotopy/interval.hlean
+++ b/hott/homotopy/interval.hlean
@@ -31,7 +31,7 @@ namespace interval
   interval.rec P0 P1 Ps x
 
   theorem rec_seg {P : interval → Type} (P0 : P zero) (P1 : P one) (Ps : P0 =[seg] P1)
-      : apdo (interval.rec P0 P1 Ps) seg = Ps :=
+      : apd (interval.rec P0 P1 Ps) seg = Ps :=
   !rec_merid
 
   protected definition elim {P : Type} (P0 P1 : P) (Ps : P0 = P1) (x : interval) : P :=
@@ -45,7 +45,7 @@ namespace interval
     : ap (interval.elim P0 P1 Ps) seg = Ps :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant seg),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑interval.elim,rec_seg],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑interval.elim,rec_seg],
   end
 
   protected definition elim_type (P0 P1 : Type) (Ps : P0 ≃ P1) (x : interval) : Type :=
diff --git a/hott/homotopy/join.hlean b/hott/homotopy/join.hlean
index b6025afcb..22c817ed5 100644
--- a/hott/homotopy/join.hlean
+++ b/hott/homotopy/join.hlean
@@ -34,7 +34,7 @@ namespace join
     (Pinr : Π(y : B), P (inr y))
     (Pglue : Π(x : A)(y : B), Pinl x =[glue x y] Pinr y)
     (x : A) (y : B)
-    : apdo (join.rec Pinl Pinr Pglue) (glue x y) = Pglue x y :=
+    : apd (join.rec Pinl Pinr Pglue) (glue x y) = Pglue x y :=
   !quotient.rec_eq_of_rel
 
   protected definition elim {P : Type} (Pinl : A → P) (Pinr : B → P)
@@ -46,7 +46,7 @@ namespace join
     : ap (join.elim Pinl Pinr Pglue) (glue x y) = Pglue x y :=
   begin
     apply equiv.eq_of_fn_eq_fn_inv !(pathover_constant (glue x y)),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑join.elim],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑join.elim],
     apply join.rec_glue
   end
 
@@ -404,7 +404,7 @@ section join_switch
 
     private definition switch_inv_cube_aux2 {A B : Type} {b : B} {f : A → B}
       (g : Π a, f a = b) {x y : A} (p : x = y) {sq : square (g x) (g y) (ap f p) idp}
-      (q : apdo g p = eq_pathover (sq ⬝hp !ap_constant⁻¹)) : square_Flr_ap_idp _ _ = sq :=
+      (q : apd g p = eq_pathover (sq ⬝hp !ap_constant⁻¹)) : square_Flr_ap_idp _ _ = sq :=
     begin
       cases p, esimp at *, apply concat, apply inverse, apply vdeg_square_idp,
       apply concat, apply ap vdeg_square, exact ap eq_of_pathover_idp q,
@@ -448,7 +448,7 @@ section join_switch
 
   private definition natural_square_tr_beta {A B : Type} {f₁ f₂ : A → B}
     (p : Π a, f₁ a = f₂ a) {x y : A} (q : x = y) {sq : square (p x) (p y) (ap f₁ q) (ap f₂ q)}
-    (e : apdo p q = eq_pathover sq) :
+    (e : apd p q = eq_pathover sq) :
     natural_square_tr p q = sq :=
   begin
     cases q, esimp at *, apply concat, apply inverse, apply vdeg_square_idp,
diff --git a/hott/homotopy/red_susp.hlean b/hott/homotopy/red_susp.hlean
index a71996e89..b46b65a3d 100644
--- a/hott/homotopy/red_susp.hlean
+++ b/hott/homotopy/red_susp.hlean
@@ -47,7 +47,7 @@ section
 
   -- definition rec_merid {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb)
   --   (Pe : Pm pt =[merid_pt] idpo) (a : A)
-  --   : apdo (rec Pb Pm Pe) (merid a) = Pm a :=
+  --   : apd (rec Pb Pm Pe) (merid a) = Pm a :=
   -- !rec_incl1
 
   -- theorem elim_merid_pt {P : red_susp → Type} (Pb : P base) (Pm : Π(a : A), Pb =[merid a] Pb)
diff --git a/hott/homotopy/susp.hlean b/hott/homotopy/susp.hlean
index aab3ab608..ba6417966 100644
--- a/hott/homotopy/susp.hlean
+++ b/hott/homotopy/susp.hlean
@@ -39,7 +39,7 @@ namespace susp
 
   theorem rec_merid {P : susp A → Type} (PN : P north) (PS : P south)
     (Pm : Π(a : A), PN =[merid a] PS) (a : A)
-      : apdo (susp.rec PN PS Pm) (merid a) = Pm a :=
+      : apd (susp.rec PN PS Pm) (merid a) = Pm a :=
   !rec_glue
 
   protected definition elim {P : Type} (PN : P) (PS : P) (Pm : A → PN = PS)
@@ -54,7 +54,7 @@ namespace susp
     : ap (susp.elim PN PS Pm) (merid a) = Pm a :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant (merid a)),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑susp.elim,rec_merid],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑susp.elim,rec_merid],
   end
 
   protected definition elim_type (PN : Type) (PS : Type) (Pm : A → PN ≃ PS)
@@ -119,7 +119,7 @@ end susp
 
 /- Flattening lemma -/
 namespace susp
-  
+
   open prod prod.ops
   section
     universe variable u
diff --git a/hott/homotopy/torus.hlean b/hott/homotopy/torus.hlean
index 3a1f55cd9..1f9da174c 100644
--- a/hott/homotopy/torus.hlean
+++ b/hott/homotopy/torus.hlean
@@ -51,12 +51,12 @@ namespace torus
 
   theorem rec_loop1 {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
     (Pl2 : Pb =[loop2] Pb) (Ps : squareover P surf Pl1 Pl1 Pl2 Pl2)
-    : apdo (torus.rec Pb Pl1 Pl2 Ps) loop1 = Pl1 :=
+    : apd (torus.rec Pb Pl1 Pl2 Ps) loop1 = Pl1 :=
   !rec_incl1
 
   theorem rec_loop2 {P : torus → Type} (Pb : P base) (Pl1 : Pb =[loop1] Pb)
     (Pl2 : Pb =[loop2] Pb) (Ps : squareover P surf Pl1 Pl1 Pl2 Pl2)
-    : apdo (torus.rec Pb Pl1 Pl2 Ps) loop2 = Pl2 :=
+    : apd (torus.rec Pb Pl1 Pl2 Ps) loop2 = Pl2 :=
   !rec_incl1
 
   protected definition elim {P : Type} (Pb : P) (Pl1 : Pb = Pb) (Pl2 : Pb = Pb)
diff --git a/hott/init/hit.hlean b/hott/init/hit.hlean
index ea3c27526..4a6197c03 100644
--- a/hott/init/hit.hlean
+++ b/hott/init/hit.hlean
@@ -81,7 +81,7 @@ namespace quotient
 
   constant rec_eq_of_rel {A : Type} {R : A → A → Type} {P : quotient R → Type}
     (Pc : Π(a : A), P (class_of R a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), Pc a =[eq_of_rel R H] Pc a')
-    {a a' : A} (H : R a a') : apdo (quotient.rec Pc Pp) (eq_of_rel R H) = Pp H
+    {a a' : A} (H : R a a') : apd (quotient.rec Pc Pp) (eq_of_rel R H) = Pp H
 end quotient
 
 attribute quotient.class_of trunc.tr [constructor]
diff --git a/hott/init/pathover.hlean b/hott/init/pathover.hlean
index bf0262850..1b96d4ebc 100644
--- a/hott/init/pathover.hlean
+++ b/hott/init/pathover.hlean
@@ -70,7 +70,7 @@ namespace eq
   definition inverseo [unfold 8] (r : b =[p] b₂) : b₂ =[p⁻¹] b :=
   pathover.rec_on r idpo
 
-  definition apdo [unfold 6] (f : Πa, B a) (p : a = a₂) : f a =[p] f a₂ :=
+  definition apd [unfold 6] (f : Πa, B 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₂' :=
@@ -198,15 +198,15 @@ namespace eq
     { 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 :=
+  definition apd_con (f : Πa, B a) (p : a = a₂) (q : a₂ = a₃)
+    : apd f (p ⬝ q) = apd f p ⬝o apd f q :=
   by cases p; cases q; reflexivity
 
-  definition apdo_inv (f : Πa, B a) (p : a = a₂) : apdo f p⁻¹ = (apdo f p)⁻¹ᵒ :=
+  definition apd_inv (f : Πa, B a) (p : a = a₂) : apd f p⁻¹ = (apd f p)⁻¹ᵒ :=
   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) :=
+  definition apd_eq_pathover_of_eq_ap (f : A → A') (p : a = a₂) :
+    apd f p = pathover_of_eq (ap f p) :=
   eq.rec_on p idp
 
   definition pathover_of_pathover_tr (q : b =[p ⬝ p₂] p₂ ▸ b₂) : b =[p] b₂ :=
@@ -273,12 +273,12 @@ namespace eq
     (q : b =[p] b₂) : f b =[p] g b₂ :=
   by induction q; exact apo10 r b
 
-  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) :=
+  definition apd_compose1 (g : Πa, B a → B' a) (f : Πa, B a) (p : a = a₂)
+    : apd (g ∘' f) p = apo g (apd 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)) :=
+  definition apd_compose2 (g : Πa', B'' a') (f : A → A') (p : a = a₂)
+    : apd (λa, g (f a)) p = pathover_of_pathover_ap B'' f (apd g (ap f p)) :=
   by induction p; reflexivity
 
   definition cono.right_inv_eq (q : b = b')
diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean
index 47c5b2376..b13912ad5 100644
--- a/hott/types/sigma.hlean
+++ b/hott/types/sigma.hlean
@@ -63,7 +63,7 @@ namespace sigma
   ap eq_pr1 r
 
   definition eq2_pr2 {p q : u = v} (r : p = q) : p..2 =[eq2_pr1 r] q..2 :=
-  !pathover_ap (apdo eq_pr2 r)
+  !pathover_ap (apd eq_pr2 r)
 
   definition tr_pr1_sigma_eq {B' : A → Type} (p : u.1 = v.1) (q : u.2 =[p] v.2)
     : transport (λx, B' x.1) (sigma_eq p q) = transport B' p :=
diff --git a/hott/types/univ.hlean b/hott/types/univ.hlean
index bf396ba67..f60e2fdc0 100644
--- a/hott/types/univ.hlean
+++ b/hott/types/univ.hlean
@@ -51,7 +51,7 @@ namespace univ
   begin
     intro f,
     have u : ¬¬bool, by exact (λg, g tt),
-    let H1 := apdo f eq_bnot,
+    let H1 := apd f eq_bnot,
     note H2 := apo10 H1 u,
     have p : eq_bnot ▸ u = u, from !is_prop.elim,
     rewrite p at H2,
diff --git a/tests/lean/extra/755.hlean b/tests/lean/extra/755.hlean
index 193156c89..2df1b7cd0 100644
--- a/tests/lean/extra/755.hlean
+++ b/tests/lean/extra/755.hlean
@@ -31,7 +31,7 @@ section
 
   theorem rec_tr_eq {P : one_step_tr → Type} (Pt : Π(a : A), P (tr a))
     (Pe : Π(a a' : A), Pt a =[tr_eq a a'] Pt a') (a a' : A)
-    : apdo (rec Pt Pe) (tr_eq a a') = Pe a a' :=
+    : apd (rec Pt Pe) (tr_eq a a') = Pe a a' :=
   !rec_eq_of_rel
 
   theorem elim_tr_eq {P : Type} (Pt : A → P)
@@ -39,7 +39,7 @@ section
     : ap (elim Pt Pe) (tr_eq a a') = Pe a a' :=
   begin
     apply eq_of_fn_eq_fn_inv !(pathover_constant (tr_eq a a')),
-    rewrite [▸*,-apdo_eq_pathover_of_eq_ap,↑elim,rec_tr_eq],
+    rewrite [▸*,-apd_eq_pathover_of_eq_ap,↑elim,rec_tr_eq],
   end
 
 end