Resolve naming conflicts

Author: Madeleine Sydney Ślaga

Cubical/Data/Containers/ContainerExtensionProofs.agda

@@ -61,11 +61,11 @@ module _ {C : Category ℓ ℓ'} where
           (funExt₂ λ X (s , h) → sym (funExt⁻ (nat h) (s , C .id)) ∙
                                  cong (λ Z → mors X (s , Z)) (C .⋆IdL h))
 
-        ret : ∀ X→Y → fib (⟦ X→Y ⟧-mor) ≡ X→Y
-        ret (u ◁ f) i = u ◁ λ s → C .⋆IdR (f s) i
+        ret' : ∀ X→Y → fib (⟦ X→Y ⟧-mor) ≡ X→Y
+        ret' (u ◁ f) i = u ◁ λ s → C .⋆IdR (f s) i
 
         unique : (y : fiber (⟦_⟧-mor) (natTrans mors nat)) → (fib (natTrans mors nat) , fib-pf) ≡ y
-        unique (m , m-eq) = Σ≡Prop (λ _ → isSetNatTrans _ _) (cong fib (sym m-eq) ∙ ret m)
+        unique (m , m-eq) = Σ≡Prop (λ _ → isSetNatTrans _ _) (cong fib (sym m-eq) ∙ ret' m)
 
     -- Proof 2 that the functor ⟦_⟧ is full and faithful
     -- Uses the Yoneda lemma

Cubical/HITs/Pushout/PushoutProduct.agda

@@ -57,8 +57,6 @@ module _
       fam : A → Type _
       fam a = Σ[ k ∈ ((b : B) → P (a , b) .fst) ] ((y : Y) → k (g y) ≡ sec (inr (a , y)))
 
-      open Iso
-
       fiberEquiv : (a : A)
         → fam a ≃ fiber (λ(s : (b : B) → P (a , b) .fst) → s ∘ g) (λ y → sec (inr (a , y)))
       fiberEquiv a =  isoToEquiv
@@ -76,8 +74,8 @@ module _
 
       map-iso = elim.isIsoPrecompose f _ (λ a → fam a , is-m-trunc-fam a) connf
 
-      k = map-iso .inv sec-fam
-      ϕ = map-iso .sec sec-fam
+      k = map-iso .Iso.inv sec-fam
+      ϕ = map-iso .Iso.sec sec-fam
 
     ext : (x : A × B) → P x .fst
     ext (a , b) = k a .fst b

Cubical/HITs/SequentialColimit/Properties.agda

@@ -190,31 +190,31 @@ module _
       (Y : SeqColim X → TypeOfHLevel ℓ' d) where
 
       module _
-        (sec : (x : X .obj n) → Y (incl (X .map x)) .fst) where
+        (sec' : (x : X .obj n) → Y (incl (X .map x)) .fst) where
 
         lift-iso = elim.isIsoPrecompose _ d (Y ∘ incl) conn
 
         liftSec' : (x : X .obj (1 + n)) → Y (incl x) .fst
-        liftSec' = lift-iso .inv sec
+        liftSec' = lift-iso .inv sec'
 
-        liftSecPath' : (x : X .obj n) → sec x ≡ liftSec' (X .map x)
-        liftSecPath' x i = lift-iso .sec sec (~ i) x
+        liftSecPath' : (x : X .obj n) → sec' x ≡ liftSec' (X .map x)
+        liftSecPath' x i = lift-iso .sec sec' (~ i) x
 
       module _
-        (sec : (x : X .obj n) → Y (incl x) .fst) where
+        (sec' : (x : X .obj n) → Y (incl x) .fst) where
 
         liftSec : (x : X .obj (1 + n)) → Y (incl x) .fst
-        liftSec = liftSec' (transpSec n (λ x → Y x .fst) sec)
+        liftSec = liftSec' (transpSec n (λ x → Y x .fst) sec')
 
         liftSecPath :
           (x : X .obj n)
-          → PathP (λ i → Y (push x i) .fst) (sec x) (liftSec (X .map x))
+          → PathP (λ i → Y (push x i) .fst) (sec' x) (liftSec (X .map x))
         liftSecPath x i =
           hcomp (λ j → λ
-            { (i = i0) → sec x
+            { (i = i0) → sec' x
             ; (i = i1) → liftSecPath'
-                (transpSec n (λ x → Y x .fst) sec) x j })
-            (transport-filler (λ i → Y (push x i) .fst) (sec x) i)
+                (transpSec n (λ x → Y x .fst) sec') x j })
+            (transport-filler (λ i → Y (push x i) .fst) (sec' x) i)
 
   module _
     (d : ℕ)(n : ℕ)

Cubical/Homotopy/Group/Base.agda

@@ -324,13 +324,13 @@ isEquiv-Ω→SphereMap zero {A = A} =
                           , λ i j → snd f (~ i ∨ j)))
             λ _ → refl))
 isEquiv-Ω→SphereMap (suc zero) {A = A} =
-  isoToIsEquiv (iso _ invFun sec λ p → sym (rUnit p))
+  isoToIsEquiv (iso _ invFun sec' λ p → sym (rUnit p))
   where
   invFun : S₊∙ 1 →∙ A → typ (Ω A)
   invFun (f , p) = sym p ∙∙ cong f loop ∙∙ p
 
-  sec : section (Ω→SphereMap 1) invFun
-  sec (f , p) =
+  sec' : section (Ω→SphereMap 1) invFun
+  sec' (f , p) =
     ΣPathP ((funExt (λ { base → sym p
                        ; (loop i) j → doubleCompPath-filler
                                         (sym p) (cong f loop) p (~ j) i}))

Cubical/Homotopy/Group/Join.agda

@@ -221,13 +221,13 @@ private
       λ g → cong ∣_∣₂
         (cong (fun (Iso-JoinMap-SphereMap n m)) (sym (·Π≡+* f g))
         ∙ ∘∙-assoc _ _ _
-        ∙ cong (∙Π f g ∘∙_) ret
+        ∙ cong (∙Π f g ∘∙_) ret'
         ∙ ∘∙-idˡ (∙Π f g)
         ∙ cong₂ ∙Π
-              ((sym (∘∙-idˡ f) ∙ cong (f ∘∙_) (sym ret)) ∙ sym (∘∙-assoc _ _ _))
-              (sym (∘∙-idˡ g) ∙ cong (g ∘∙_) (sym ret) ∙ sym (∘∙-assoc _ _ _))))
+              ((sym (∘∙-idˡ f) ∙ cong (f ∘∙_) (sym ret')) ∙ sym (∘∙-assoc _ _ _))
+              (sym (∘∙-idˡ g) ∙ cong (g ∘∙_) (sym ret') ∙ sym (∘∙-assoc _ _ _))))
   where
-  ret = ≃∙→ret/sec∙ {B = _ , ptSn (suc (n + m))}
+  ret' = ≃∙→ret/sec∙ {B = _ , ptSn (suc (n + m))}
           (joinSphereEquiv∙ n m) .snd
 
 -π*≡-π' : ∀ {ℓ} {A : Pointed ℓ} {n m : ℕ}
@@ -241,11 +241,11 @@ private
       (cong (_∘∙ (≃∙map (invEquiv∙ (joinSphereEquiv∙ n m))))
             (sym (-Π≡-* f))
     ∙ ∘∙-assoc _ _ _
-    ∙ cong (-Π f ∘∙_) ret
+    ∙ cong (-Π f ∘∙_) ret'
     ∙ ∘∙-idˡ (-Π f)
-    ∙ cong -Π (sym (∘∙-assoc _ _ _ ∙ cong (f ∘∙_) ret ∙ ∘∙-idˡ f))))
+    ∙ cong -Π (sym (∘∙-assoc _ _ _ ∙ cong (f ∘∙_) ret' ∙ ∘∙-idˡ f))))
   where
-  ret = ≃∙→ret/sec∙ {B = _ , ptSn (suc (n + m))}
+  ret' = ≃∙→ret/sec∙ {B = _ , ptSn (suc (n + m))}
           (joinSphereEquiv∙ n m) .snd
 
 -- Homotopy groups in terms of joins