diff --git a/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md b/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md
index fa50fc60b7..c0226e3916 100644
--- a/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md
+++ b/src/foundation/universal-property-family-of-fibers-of-maps.lagda.md
@@ -101,10 +101,10 @@ module _
   where
 
   dependent-universal-property-family-of-fibers :
-    {f : A → B} (F : B → UU l3) (δ : lift-family-of-elements f F) → UUω
+    {f : A → B} (F : B → UU l3) (δ : lift-family-of-elements F f) → UUω
   dependent-universal-property-family-of-fibers F δ =
     {l : Level} (X : (b : B) → F b → UU l) →
-    is-equiv (ev-double-lift-family-of-elements {B = F} δ {X})
+    is-equiv (ev-double-lift-family-of-elements {B = F} {X} δ)
 ```
 
 ### The universal property of the family of fibers of a map
@@ -127,10 +127,10 @@ module _
   where
 
   universal-property-family-of-fibers :
-    {f : A → B} (F : B → UU l3) (δ : lift-family-of-elements f F) → UUω
+    {f : A → B} (F : B → UU l3) (δ : lift-family-of-elements F f) → UUω
   universal-property-family-of-fibers F δ =
     {l : Level} (X : B → UU l) →
-    is-equiv (ev-double-lift-family-of-elements {B = F} δ {λ b _ → X b})
+    is-equiv (ev-double-lift-family-of-elements {B = F} {λ b _ → X b} δ)
 ```
 
 ### The lift of any map to its family of fibers
@@ -140,7 +140,7 @@ module _
   {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B)
   where
 
-  lift-family-of-elements-fiber : lift-family-of-elements f (fiber f)
+  lift-family-of-elements-fiber : lift-family-of-elements (fiber f) f
   pr1 (lift-family-of-elements-fiber a) = a
   pr2 (lift-family-of-elements-fiber a) = refl
 ```
@@ -240,7 +240,7 @@ module _
 
   equiv-universal-property-family-of-fibers :
     {l3 : Level} (C : B → UU l3) →
-    ((y : B) → fiber f y → C y) ≃ lift-family-of-elements f C
+    ((y : B) → fiber f y → C y) ≃ lift-family-of-elements C f
   equiv-universal-property-family-of-fibers C =
     equiv-dependent-universal-property-family-of-fibers f (λ y _ → C y)
 ```
@@ -256,7 +256,7 @@ module _
   where
 
   inv-equiv-universal-property-family-of-fibers :
-    (lift-family-of-elements f C) ≃ ((y : B) → fiber f y → C y)
+    (lift-family-of-elements C f) ≃ ((y : B) → fiber f y → C y)
   inv-equiv-universal-property-family-of-fibers =
     inv-equiv-dependent-universal-property-family-of-fibers f (λ y _ → C y)
 ```
@@ -274,7 +274,7 @@ module _
   abstract
     uniqueness-extension-universal-property-family-of-fibers :
       is-contr
-        ( extension-double-lift-family-of-elements δ (λ y (_ : F y) → G y) γ)
+        ( extension-double-lift-family-of-elements (λ y (_ : F y) → G y) δ γ)
     uniqueness-extension-universal-property-family-of-fibers =
       is-contr-equiv
         ( fiber (ev-double-lift-family-of-elements δ) γ)
@@ -283,7 +283,7 @@ module _
 
   abstract
     extension-universal-property-family-of-fibers :
-      extension-double-lift-family-of-elements δ (λ y (_ : F y) → G y) γ
+      extension-double-lift-family-of-elements (λ y (_ : F y) → G y) δ γ
     extension-universal-property-family-of-fibers =
       center uniqueness-extension-universal-property-family-of-fibers
 
@@ -294,8 +294,9 @@ module _
       extension-universal-property-family-of-fibers
 
   is-extension-fiberwise-map-universal-property-family-of-fibers :
-    is-extension-double-lift-family-of-elements δ
+    is-extension-double-lift-family-of-elements
       ( λ y _ → G y)
+      ( δ)
       ( γ)
       ( fiberwise-map-universal-property-family-of-fibers)
   is-extension-fiberwise-map-universal-property-family-of-fibers =
@@ -392,8 +393,9 @@ module _
     pr1 extension-by-fiberwise-equiv-universal-property-family-of-fibers
 
   is-extension-fiberwise-equiv-universal-property-of-fibers :
-    is-extension-double-lift-family-of-elements δ
+    is-extension-double-lift-family-of-elements
       ( λ y _ → G y)
+      ( δ)
       ( γ)
       ( map-fiberwise-equiv
         ( fiberwise-equiv-universal-property-of-fibers))
diff --git a/src/orthogonal-factorization-systems/double-lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/double-lifts-families-of-elements.lagda.md
index 032f76b87d..acd8dc3b2d 100644
--- a/src/orthogonal-factorization-systems/double-lifts-families-of-elements.lagda.md
+++ b/src/orthogonal-factorization-systems/double-lifts-families-of-elements.lagda.md
@@ -63,27 +63,28 @@ The type of double lifts plays a role in the
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {a : (i : I) → A i}
-  {B : (i : I) → A i → UU l3} (b : dependent-lift-family-of-elements a B)
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {B : (i : I) → A i → UU l3}
   (C : (i : I) (x : A i) → B i x → UU l4)
+  {a : (i : I) → A i} (b : dependent-lift-family-of-elements B a)
   where
 
   dependent-double-lift-family-of-elements : UU (l1 ⊔ l4)
   dependent-double-lift-family-of-elements =
-    dependent-lift-family-of-elements b (λ i → C i (a i))
+    dependent-lift-family-of-elements (λ i → C i (a i)) b
 ```
 
 ### Double lifts of families of elements
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} {a : I → A}
-  {B : A → UU l3} (b : lift-family-of-elements a B) (C : (x : A) → B x → UU l4)
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} {B : A → UU l3}
+  (C : (x : A) → B x → UU l4)
+  {a : I → A} (b : lift-family-of-elements B a)
   where
 
   double-lift-family-of-elements : UU (l1 ⊔ l4)
   double-lift-family-of-elements =
-    dependent-lift-family-of-elements b (λ i → C (a i))
+    dependent-lift-family-of-elements (λ i → C (a i)) b
 ```
 
 ## See also
diff --git a/src/orthogonal-factorization-systems/extensions-double-lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/extensions-double-lifts-families-of-elements.lagda.md
index 5a617ec37c..63ba294492 100644
--- a/src/orthogonal-factorization-systems/extensions-double-lifts-families-of-elements.lagda.md
+++ b/src/orthogonal-factorization-systems/extensions-double-lifts-families-of-elements.lagda.md
@@ -61,14 +61,14 @@ given by `c ↦ (λ i → c i (a i) (b i))`.
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {a : (i : I) → A i}
-  {B : (i : I) → A i → UU l3} (b : dependent-lift-family-of-elements a B)
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {B : (i : I) → A i → UU l3}
   {C : (i : I) (x : A i) → B i x → UU l4}
+  {a : (i : I) → A i} (b : dependent-lift-family-of-elements B a)
   where
 
   ev-dependent-double-lift-family-of-elements :
     ((i : I) (x : A i) (y : B i x) → C i x y) →
-    dependent-double-lift-family-of-elements b C
+    dependent-double-lift-family-of-elements C b
   ev-dependent-double-lift-family-of-elements h i = h i (a i) (b i)
 ```
 
@@ -85,13 +85,13 @@ given by `c ↦ (λ i → c (a i) (b i))`.
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} {a : I → A}
-  {B : A → UU l3} (b : lift-family-of-elements a B)
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} {B : A → UU l3}
   {C : (x : A) → B x → UU l4}
+  {a : I → A} (b : lift-family-of-elements B a)
   where
 
   ev-double-lift-family-of-elements :
-    ((x : A) (y : B x) → C x y) → double-lift-family-of-elements b C
+    ((x : A) (y : B x) → C x y) → double-lift-family-of-elements C b
   ev-double-lift-family-of-elements h i = h (a i) (b i)
 ```
 
@@ -99,10 +99,10 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {a : (i : I) → A i}
-  {B : (i : I) → A i → UU l3} (b : dependent-lift-family-of-elements a B)
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {B : (i : I) → A i → UU l3}
   (C : (i : I) (x : A i) (y : B i x) → UU l4)
-  (c : dependent-double-lift-family-of-elements b C)
+  {a : (i : I) → A i} (b : dependent-lift-family-of-elements B a)
+  (c : dependent-double-lift-family-of-elements C b)
   where
 
   is-extension-dependent-double-lift-family-of-elements :
@@ -116,11 +116,11 @@ module _
       ( is-extension-dependent-double-lift-family-of-elements)
 
 module _
-  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {a : (i : I) → A i}
-  {B : (i : I) → A i → UU l3} {b : dependent-lift-family-of-elements a B}
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {B : (i : I) → A i → UU l3}
   {C : (i : I) (x : A i) (y : B i x) → UU l4}
-  {c : dependent-double-lift-family-of-elements b C}
-  (f : extension-dependent-double-lift-family-of-elements b C c)
+  {a : (i : I) → A i} {b : dependent-lift-family-of-elements B a}
+  {c : dependent-double-lift-family-of-elements C b}
+  (f : extension-dependent-double-lift-family-of-elements C b c)
   where
 
   family-of-elements-extension-dependent-double-lift-family-of-elements :
@@ -129,7 +129,7 @@ module _
     pr1 f
 
   is-extension-extension-dependent-double-lift-family-of-elements :
-    is-extension-dependent-double-lift-family-of-elements b C c
+    is-extension-dependent-double-lift-family-of-elements C b c
       ( family-of-elements-extension-dependent-double-lift-family-of-elements)
   is-extension-extension-dependent-double-lift-family-of-elements = pr2 f
 ```
@@ -138,9 +138,10 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} {a : I → A}
-  {B : A → UU l3} (b : lift-family-of-elements a B)
-  (C : (x : A) (y : B x) → UU l4) (c : double-lift-family-of-elements b C)
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} {B : A → UU l3}
+  (C : (x : A) (y : B x) → UU l4)
+  {a : I → A} (b : lift-family-of-elements B a)
+  (c : double-lift-family-of-elements C b)
   where
 
   is-extension-double-lift-family-of-elements :
@@ -153,10 +154,11 @@ module _
     Σ ((x : A) (y : B x) → C x y) is-extension-double-lift-family-of-elements
 
 module _
-  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} {a : I → A}
-  {B : A → UU l3} {b : lift-family-of-elements a B}
-  {C : (x : A) (y : B x) → UU l4} {c : double-lift-family-of-elements b C}
-  (f : extension-double-lift-family-of-elements b C c)
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} {B : A → UU l3}
+  {C : (x : A) (y : B x) → UU l4}
+  {a : I → A} {b : lift-family-of-elements B a}
+  {c : double-lift-family-of-elements C b}
+  (f : extension-double-lift-family-of-elements C b c)
   where
 
   family-of-elements-extension-double-lift-family-of-elements :
@@ -164,7 +166,7 @@ module _
   family-of-elements-extension-double-lift-family-of-elements = pr1 f
 
   is-extension-extension-double-lift-family-of-elements :
-    is-extension-double-lift-family-of-elements b C c
+    is-extension-double-lift-family-of-elements C b c
       ( family-of-elements-extension-double-lift-family-of-elements)
   is-extension-extension-double-lift-family-of-elements = pr2 f
 ```
@@ -173,12 +175,12 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {a : (i : I) → A i}
-  {B : (i : I) → A i → UU l3} (b : dependent-lift-family-of-elements a B)
+  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : (i : I) → A i → UU l3}
+  {a : (i : I) → A i} (b : dependent-lift-family-of-elements B a)
   where
 
   id-extension-dependent-double-lift-family-of-elements :
-    extension-dependent-double-lift-family-of-elements b (λ i x y → B i x) b
+    extension-dependent-double-lift-family-of-elements (λ i x y → B i x) b b
   pr1 id-extension-dependent-double-lift-family-of-elements i x = id
   pr2 id-extension-dependent-double-lift-family-of-elements = refl-htpy
 ```
@@ -187,12 +189,12 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {I : UU l1} {A : UU l2} {a : I → A}
-  {B : A → UU l3} (b : lift-family-of-elements a B)
+  {l1 l2 l3 : Level} {I : UU l1} {A : UU l2} {B : A → UU l3}
+  {a : I → A} (b : lift-family-of-elements B a)
   where
 
   id-extension-double-lift-family-of-elements :
-    extension-double-lift-family-of-elements b (λ x (y : B x) → B x) b
+    extension-double-lift-family-of-elements (λ x (y : B x) → B x) b b
   pr1 id-extension-double-lift-family-of-elements x = id
   pr2 id-extension-double-lift-family-of-elements = refl-htpy
 ```
@@ -202,17 +204,21 @@ module _
 ```agda
 module _
   {l1 l2 l3 l4 l5 : Level} {I : UU l1}
-  {A : I → UU l2} {a : (i : I) → A i}
-  {B : (i : I) → A i → UU l3} {b : dependent-lift-family-of-elements a B}
-  {C : (i : I) → A i → UU l4} {c : dependent-lift-family-of-elements a C}
-  {D : (i : I) → A i → UU l5} {d : dependent-lift-family-of-elements a D}
+  {A : I → UU l2} {B : (i : I) → A i → UU l3} {C : (i : I) → A i → UU l4}
+  {D : (i : I) → A i → UU l5}
+  {a : (i : I) → A i}
+  {b : dependent-lift-family-of-elements B a}
+  {c : dependent-lift-family-of-elements C a}
+  {d : dependent-lift-family-of-elements D a}
   (g :
-    extension-dependent-double-lift-family-of-elements c
+    extension-dependent-double-lift-family-of-elements
       ( λ i x (_ : C i x) → D i x)
+      ( c)
       ( d))
   (f :
-    extension-dependent-double-lift-family-of-elements b
+    extension-dependent-double-lift-family-of-elements
       ( λ i x (_ : B i x) → C i x)
+      ( b)
       ( c))
   where
 
@@ -226,8 +232,9 @@ module _
       f i x
 
   is-extension-comp-extension-dependent-double-lift-family-of-elements :
-    is-extension-dependent-double-lift-family-of-elements b
+    is-extension-dependent-double-lift-family-of-elements
       ( λ i x _ → D i x)
+      ( b)
       ( d)
       ( family-of-elements-comp-extension-dependent-double-lift-family-of-elements)
   is-extension-comp-extension-dependent-double-lift-family-of-elements i =
@@ -238,8 +245,9 @@ module _
     ( is-extension-extension-dependent-double-lift-family-of-elements g i)
 
   comp-extension-dependent-double-lift-family-of-elements :
-    extension-dependent-double-lift-family-of-elements b
+    extension-dependent-double-lift-family-of-elements
       ( λ i x (_ : B i x) → D i x)
+      ( b)
       ( d)
   pr1 comp-extension-dependent-double-lift-family-of-elements =
     family-of-elements-comp-extension-dependent-double-lift-family-of-elements
@@ -251,12 +259,12 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 l4 l5 : Level} {I : UU l1} {A : UU l2} {a : I → A}
-  {B : A → UU l3} {b : lift-family-of-elements a B}
-  {C : A → UU l4} {c : lift-family-of-elements a C}
-  {D : A → UU l5} {d : lift-family-of-elements a D}
-  (g : extension-double-lift-family-of-elements c (λ x (_ : C x) → D x) d)
-  (f : extension-double-lift-family-of-elements b (λ x (_ : B x) → C x) c)
+  {l1 l2 l3 l4 l5 : Level} {I : UU l1} {A : UU l2} {B : A → UU l3}
+  {C : A → UU l4} {D : A → UU l5}
+  {a : I → A} {b : lift-family-of-elements B a}
+  {c : lift-family-of-elements C a} {d : lift-family-of-elements D a}
+  (g : extension-double-lift-family-of-elements (λ x (_ : C x) → D x) c d)
+  (f : extension-double-lift-family-of-elements (λ x (_ : B x) → C x) b c)
   where
 
   family-of-elements-comp-extension-double-lift-family-of-elements :
@@ -266,8 +274,9 @@ module _
     family-of-elements-extension-double-lift-family-of-elements f x
 
   is-extension-comp-extension-double-lift-family-of-elements :
-    is-extension-double-lift-family-of-elements b
+    is-extension-double-lift-family-of-elements
       ( λ x _ → D x)
+      ( b)
       ( d)
       ( family-of-elements-comp-extension-double-lift-family-of-elements)
   is-extension-comp-extension-double-lift-family-of-elements i =
@@ -277,7 +286,7 @@ module _
     ( is-extension-extension-double-lift-family-of-elements g i)
 
   comp-extension-double-lift-family-of-elements :
-    extension-double-lift-family-of-elements b (λ x (_ : B x) → D x) d
+    extension-double-lift-family-of-elements (λ x (_ : B x) → D x) b d
   pr1 comp-extension-double-lift-family-of-elements =
     family-of-elements-comp-extension-double-lift-family-of-elements
   pr2 comp-extension-double-lift-family-of-elements =
diff --git a/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md
index f7998568ba..6d5980be63 100644
--- a/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md
+++ b/src/orthogonal-factorization-systems/extensions-lifts-families-of-elements.lagda.md
@@ -67,20 +67,20 @@ defined by `b ↦ (λ i → b i (a i))`.
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} (a : (i : I) → A i)
-  {B : (i : I) → A i → UU l3}
+  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : (i : I) → A i → UU l3}
+  (a : (i : I) → A i)
   where
 
   ev-dependent-lift-family-of-elements :
-    ((i : I) (x : A i) → B i x) → dependent-lift-family-of-elements a B
+    ((i : I) (x : A i) → B i x) → dependent-lift-family-of-elements B a
   ev-dependent-lift-family-of-elements b i = b i (a i)
 
 module _
-  {l1 l2 l3 : Level} {I : UU l1} {A : UU l2} (a : I → A) {B : A → UU l3}
+  {l1 l2 l3 : Level} {I : UU l1} {A : UU l2} {B : A → UU l3} (a : I → A)
   where
 
   ev-lift-family-of-elements :
-    ((x : A) → B x) → lift-family-of-elements a B
+    ((x : A) → B x) → lift-family-of-elements B a
   ev-lift-family-of-elements b i = b (a i)
 ```
 
@@ -88,8 +88,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} (a : (i : I) → A i)
-  (B : (i : I) → A i → UU l3) (b : dependent-lift-family-of-elements a B)
+  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} (B : (i : I) → A i → UU l3)
+  (a : (i : I) → A i) (b : dependent-lift-family-of-elements B a)
   where
 
   is-extension-dependent-lift-family-of-elements :
@@ -102,9 +102,9 @@ module _
     Σ ((i : I) (x : A i) → B i x) is-extension-dependent-lift-family-of-elements
 
 module _
-  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {a : (i : I) → A i}
-  {B : (i : I) → A i → UU l3} {b : dependent-lift-family-of-elements a B}
-  (f : extension-dependent-lift-family-of-elements a B b)
+  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} {B : (i : I) → A i → UU l3}
+  {a : (i : I) → A i} {b : dependent-lift-family-of-elements B a}
+  (f : extension-dependent-lift-family-of-elements B a b)
   where
 
   family-of-elements-extension-dependent-lift-family-of-elements :
@@ -112,7 +112,7 @@ module _
   family-of-elements-extension-dependent-lift-family-of-elements = pr1 f
 
   is-extension-extension-dependent-lift-family-of-elements :
-    is-extension-dependent-lift-family-of-elements a B b
+    is-extension-dependent-lift-family-of-elements B a b
       ( family-of-elements-extension-dependent-lift-family-of-elements)
   is-extension-extension-dependent-lift-family-of-elements = pr2 f
 ```
@@ -121,8 +121,8 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {I : UU l1} {A : UU l2} (a : I → A)
-  (B : A → UU l3) (b : lift-family-of-elements a B)
+  {l1 l2 l3 : Level} {I : UU l1} {A : UU l2} (B : A → UU l3)
+  (a : I → A) (b : lift-family-of-elements B a)
   where
 
   is-extension-lift-family-of-elements : (f : (x : A) → B x) → UU (l1 ⊔ l3)
@@ -133,16 +133,16 @@ module _
     Σ ((x : A) → B x) is-extension-lift-family-of-elements
 
 module _
-  {l1 l2 l3 : Level} {I : UU l1} {A : UU l2} {a : I → A}
-  {B : A → UU l3} {b : lift-family-of-elements a B}
-  (f : extension-lift-family-of-elements a B b)
+  {l1 l2 l3 : Level} {I : UU l1} {A : UU l2} {B : A → UU l3}
+  {a : I → A} {b : lift-family-of-elements B a}
+  (f : extension-lift-family-of-elements B a b)
   where
 
   family-of-elements-extension-lift-family-of-elements : (x : A) → B x
   family-of-elements-extension-lift-family-of-elements = pr1 f
 
   is-extension-extension-lift-family-of-elements :
-    is-extension-lift-family-of-elements a B b
+    is-extension-lift-family-of-elements B a b
       ( family-of-elements-extension-lift-family-of-elements)
   is-extension-extension-lift-family-of-elements = pr2 f
 ```
@@ -155,7 +155,7 @@ module _
   where
 
   id-extension-dependent-lift-family-of-elements :
-    extension-dependent-lift-family-of-elements a (λ i _ → A i) a
+    extension-dependent-lift-family-of-elements (λ i _ → A i) a a
   pr1 id-extension-dependent-lift-family-of-elements i = id
   pr2 id-extension-dependent-lift-family-of-elements = refl-htpy
 ```
@@ -168,7 +168,7 @@ module _
   where
 
   id-extension-lift-family-of-elements :
-    extension-lift-family-of-elements a (λ _ → A) a
+    extension-lift-family-of-elements (λ _ → A) a a
   pr1 id-extension-lift-family-of-elements = id
   pr2 id-extension-lift-family-of-elements = refl-htpy
 ```
@@ -213,11 +213,10 @@ extensions of `b` along `a` to obtain extensions of `c` along `a`.
 ```agda
 module _
   {l1 l2 l3 l4 : Level} {I : UU l1}
-  {A : I → UU l2} {a : (i : I) → A i}
-  {B : I → UU l3} {b : (i : I) → B i}
-  {C : I → UU l4} {c : (i : I) → C i}
-  (g : extension-dependent-lift-family-of-elements b (λ i _ → C i) c)
-  (f : extension-dependent-lift-family-of-elements a (λ i _ → B i) b)
+  {A : I → UU l2} {B : I → UU l3} {C : I → UU l4}
+  {a : (i : I) → A i} {b : (i : I) → B i} {c : (i : I) → C i}
+  (g : extension-dependent-lift-family-of-elements (λ i _ → C i) b c)
+  (f : extension-dependent-lift-family-of-elements (λ i _ → B i) a b)
   where
 
   family-of-elements-comp-extension-dependent-lift-family-of-elements :
@@ -227,8 +226,9 @@ module _
     family-of-elements-extension-dependent-lift-family-of-elements f i
 
   is-extension-comp-extension-dependent-lift-family-of-elements :
-    is-extension-dependent-lift-family-of-elements a
+    is-extension-dependent-lift-family-of-elements
       ( λ i _ → C i)
+      ( a)
       ( c)
       ( family-of-elements-comp-extension-dependent-lift-family-of-elements)
   is-extension-comp-extension-dependent-lift-family-of-elements i =
@@ -238,7 +238,7 @@ module _
     ( is-extension-extension-dependent-lift-family-of-elements g i)
 
   comp-extension-dependent-lift-family-of-elements :
-    extension-dependent-lift-family-of-elements a (λ i _ → C i) c
+    extension-dependent-lift-family-of-elements (λ i _ → C i) a c
   pr1 comp-extension-dependent-lift-family-of-elements =
     family-of-elements-comp-extension-dependent-lift-family-of-elements
   pr2 comp-extension-dependent-lift-family-of-elements =
@@ -274,11 +274,10 @@ The composite `g ∘ f` is then an extension of `c` along `a.
 ```agda
 module _
   {l1 l2 l3 l4 : Level} {I : UU l1}
-  {A : UU l2} {a : I → A}
-  {B : UU l3} {b : I → B}
-  {C : UU l4} {c : I → C}
-  (g : extension-lift-family-of-elements b (λ _ → C) c)
-  (f : extension-lift-family-of-elements a (λ _ → B) b)
+  {A : UU l2} {B : UU l3} {C : UU l4}
+  {a : I → A} {b : I → B} {c : I → C}
+  (g : extension-lift-family-of-elements (λ _ → C) b c)
+  (f : extension-lift-family-of-elements (λ _ → B) a b)
   where
 
   map-comp-extension-lift-family-of-elements : A → C
@@ -287,8 +286,9 @@ module _
     family-of-elements-extension-lift-family-of-elements f
 
   is-extension-comp-extension-lift-family-of-elements :
-    is-extension-lift-family-of-elements a
+    is-extension-lift-family-of-elements
       ( λ _ → C)
+      ( a)
       ( c)
       ( map-comp-extension-lift-family-of-elements)
   is-extension-comp-extension-lift-family-of-elements x =
@@ -298,7 +298,7 @@ module _
     ( is-extension-extension-lift-family-of-elements g x)
 
   comp-extension-lift-family-of-elements :
-    extension-lift-family-of-elements a (λ _ → C) c
+    extension-lift-family-of-elements (λ _ → C) a c
   pr1 comp-extension-lift-family-of-elements =
     map-comp-extension-lift-family-of-elements
   pr2 comp-extension-lift-family-of-elements =
diff --git a/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md b/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md
index e3a3aa1f13..6155ddf59e 100644
--- a/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md
+++ b/src/orthogonal-factorization-systems/lifts-families-of-elements.lagda.md
@@ -14,12 +14,14 @@ open import foundation.universe-levels
 
 ## Idea
 
-Consider a family of elements `a : (i : I) → A i` and a type family
+Consider a type family
 
 ```text
-  B : (i : I) → A i → 𝒰.
+  B : (i : I) → A i → 𝒰
 ```
 
+and a family of elements `a : (i : I) → A i`.
+
 A {{#concept "dependent lift" Disambiguation="family of elements"}} of the
 family of elements `a` to the type family `B` is a family of elements
 
@@ -42,8 +44,8 @@ elements `a` is a family of elements
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} (a : (i : I) → A i)
-  (B : (i : I) → A i → UU l3)
+  {l1 l2 l3 : Level} {I : UU l1} {A : I → UU l2} (B : (i : I) → A i → UU l3)
+  (a : (i : I) → A i)
   where
 
   dependent-lift-family-of-elements : UU (l1 ⊔ l3)
@@ -54,37 +56,37 @@ module _
 
 ```agda
 module _
-  {l1 l2 l3 : Level} {I : UU l1} {A : UU l2} (a : I → A) (B : A → UU l3)
+  {l1 l2 l3 : Level} {I : UU l1} {A : UU l2} (B : A → UU l3) (a : I → A)
   where
 
   lift-family-of-elements : UU (l1 ⊔ l3)
-  lift-family-of-elements = dependent-lift-family-of-elements a (λ _ → B)
+  lift-family-of-elements = dependent-lift-family-of-elements (λ _ → B) a
 ```
 
 ### Dependent lifts of binary families of elements
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} (a : (i : I) → A i)
-  {B : (i : I) → A i → UU l3} (C : (i : I) (x : A i) → B i x → UU l4)
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : I → UU l2} {B : (i : I) → A i → UU l3}
+  (C : (i : I) (x : A i) → B i x → UU l4) (a : (i : I) → A i)
   where
 
   dependent-lift-binary-family-of-elements : UU (l1 ⊔ l3 ⊔ l4)
   dependent-lift-binary-family-of-elements =
-    dependent-lift-family-of-elements a (λ i x → (y : B i x) → C i x y)
+    dependent-lift-family-of-elements (λ i x → (y : B i x) → C i x y) a
 ```
 
 ### Lifts of binary families of elements
 
 ```agda
 module _
-  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} (a : I → A)
-  {B : A → UU l3} {C : (x : A) → B x → UU l4}
+  {l1 l2 l3 l4 : Level} {I : UU l1} {A : UU l2} {B : A → UU l3}
+  {C : (x : A) → B x → UU l4} (a : I → A)
   where
 
   lift-binary-family-of-elements : UU (l1 ⊔ l3 ⊔ l4)
   lift-binary-family-of-elements =
-    dependent-lift-binary-family-of-elements a (λ _ → C)
+    dependent-lift-binary-family-of-elements (λ _ → C) a
 ```
 
 ## See also