Swap order of arguments for lifts of families of elements (#981)

Makes the arguments to definitions about lifts of elements start with
type families, and continue with the families of elements that we're
lifting. This makes sense conceptually, because e.g.
`lift-family-of-elements B` is now a function which takes a family of
elements to its type of lifts, so we can talk about concepts such as
"transport in the family of lifts" by writing `tr
(lift-family-of-elements 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))

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

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,24 +85,24 @@ 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)
 ```
 
 ### Dependent extensions of double lifts of 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} (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,18 +154,19 @@ 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 :
     (x : A) (y : B x) → C x y
   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 =