diff --git a/HoTT-Agda/core/lib/PathOver.agda b/HoTT-Agda/core/lib/PathOver.agda
index 52ea716..cd8c74f 100644
--- a/HoTT-Agda/core/lib/PathOver.agda
+++ b/HoTT-Agda/core/lib/PathOver.agda
@@ -320,14 +320,12 @@ module _ {i j} {A : Type i} where
 
 -- apd-tr conversion
 
-  from-transp-g : (B : A → Type j) {a a' : A} (p : a == a')
-    {u : B a} {v : B a'}
-    → (transport B p u == v)
-    → (u == v [ B ↓ p ])
+  from-transp-g : (B : A → Type j) {a a' : A} (p : a == a') {u : B a} {v : B a'}
+    → transport B p u == v → u == v [ B ↓ p ]
   from-transp-g B idp h = h
 
-  apd-to-tr : (B : A → Type j) (f : (a : A) → B a) {x y : A} (p : x == y)
-    (s : transport B p (f x) == f y)
+  apd-to-tr : (B : A → Type j) (f : (a : A) → B a) {x y : A}
+    (p : x == y) (s : transport B p (f x) == f y)
     → apd f p == from-transp-g B p s → apd-tr f p == s
   apd-to-tr B f idp s h = h
 
@@ -341,8 +339,7 @@ module _ {i j} {A : Type i} {B : Type j} (f g : A → B) where
 
   module _ (K : (z : A) → f z == g z) where
 
-    apd-to-hnat : {x y : A} (p : x == y)
-      (m : ap f p == K x ∙ ap g p  ∙' ! (K y))
+    apd-to-hnat : {x y : A} (p : x == y) (m : ap f p == K x ∙ ap g p  ∙' ! (K y))
       → apd K p == from-hmpty-nat p m → hmpty-nat-∙'-r K p == m
     apd-to-hnat {x} idp m q = lemma (K x) m q
       where
@@ -354,13 +351,14 @@ module _ {i j} {A : Type i} {B : Type j} (f g : A → B) where
     apd-to-hnat-∙ : {x y z : A} (p₁ : x == y) (p₂ : y == z)
       {m₁ : ap f p₁ == K x ∙ ap g p₁  ∙' ! (K y)} {m₂ : ap f p₂ == K y ∙ ap g p₂  ∙' ! (K z)}
       (τ₁ : hmpty-nat-∙'-r K p₁ == m₁) (τ₂ : hmpty-nat-∙'-r K p₂ == m₂)
-      → hmpty-nat-∙'-r K (p₁ ∙ p₂)
+      →
+      hmpty-nat-∙'-r K (p₁ ∙ p₂)
         ==
-        ↯ (ap-∙ f p₁ p₂ ◃∙
-        ap (λ p → p ∙ ap f p₂) m₁ ◃∙
-        ap (λ p → (K x ∙ ap g p₁ ∙' ! (K y)) ∙ p) m₂ ◃∙
-        assoc-tri-!-mid (K x) (ap g p₁) (K y) (ap g p₂) (! (K z)) ◃∙
-        ap (λ p → K x ∙ p ∙' ! (K z)) (! (ap-∙ g p₁ p₂)) ◃∎)
+      ↯ (ap-∙ f p₁ p₂ ◃∙
+      ap (λ p → p ∙ ap f p₂) m₁ ◃∙
+      ap (λ p → (K x ∙ ap g p₁ ∙' ! (K y)) ∙ p) m₂ ◃∙
+      assoc-tri-!-mid (K x) (ap g p₁) (K y) (ap g p₂) (! (K z)) ◃∙
+      ap (λ p → K x ∙ p ∙' ! (K z)) (! (ap-∙ g p₁ p₂)) ◃∎)
     apd-to-hnat-∙ {x} idp idp idp idp = assoc-tri-!-coher (K x)
 
     apd-to-hnat-! : {x y : A} (p : x == y)
@@ -370,7 +368,9 @@ module _ {i j} {A : Type i} {B : Type j} (f g : A → B) where
 
     apd-to-hnat-ap! : ∀ {l} {C : Type l} (h : B → C) {x y : A} (p : x == y)
       {m : ap f p == K x ∙ ap g p  ∙' ! (K y)} (τ : hmpty-nat-∙'-r K p == m)
-      → hmpty-nat-∙'-r (λ z → ap h (! (K z))) p ==
+      →
+      hmpty-nat-∙'-r (λ z → ap h (! (K z))) p
+        ==
       ap-∘-long h g f K p ∙
       ! (ap (λ q → ap h (! (K x)) ∙ ap h q ∙' ! (ap h (! (K y)))) m) ∙
       ! (ap (λ q → ap h (! (K x)) ∙ q ∙' ! (ap h (! (K y)))) (ap-∘ h f p))