From dc6b4150bc6c1d9fe69e919b4c83a5072b61e476 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 15 Feb 2024 13:37:12 +0100
Subject: [PATCH 1/3] generalize equalizerLemma

---
 .../Localisation/InvertingElements.agda       | 22 +++-----
 .../Algebra/CommRing/Localisation/Limit.agda  | 56 +++++++++----------
 2 files changed, 36 insertions(+), 42 deletions(-)

diff --git a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda
index b190c9cc72..1a10d2e56b 100644
--- a/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda
+++ b/Cubical/Algebra/CommRing/Localisation/InvertingElements.agda
@@ -175,26 +175,22 @@ module InvertingElementsBase (R' : CommRing ℓ) where
               1r · s · g ^ l ∎
 
 
- invElPropElimN : (n : ℕ) (f : FinVec R (suc n)) (P : ((i : Fin (suc n)) → R[1/ (f i) ]) → Type ℓ')
+ invElPropElimN : (n : ℕ) (f : FinVec R n) (P : ((i : Fin n) → R[1/ (f i) ]) → Type ℓ')
           → (∀ x → isProp (P x))
-          → (∀ (r : FinVec R (suc n)) (m : ℕ) → P (λ i → [ r i , (f i ^ m) , PT.∣ m , refl ∣₁ ]))
+          → (∀ (r : FinVec R n) (m : ℕ) → P (λ i → [ r i , (f i ^ m) , PT.∣ m , refl ∣₁ ]))
           -------------------------------------------------------------------------------------
           → ∀ x → P x
  invElPropElimN zero f P isPropP baseCase x =
-              subst P (funExt (λ { zero → refl })) (invElPropElim {P = P'} (λ _ → isPropP _)
-     (λ r n → subst P (funExt (λ { zero → refl })) (baseCase (λ {zero → r}) n)) (x zero))
-   where
-   P' : R[1/ (f zero) ] → Type _
-   P' x = P (λ {zero → x})
+   subst P (funExt (λ ())) (baseCase (λ ()) zero)
 
  invElPropElimN (suc n) f P isPropP baseCase x =
    subst P (funExt (λ { zero → refl ; (suc i) → refl }))
            (invElPropElimN n (f ∘ suc) P' (λ _ → isPropP _) baseCase' (x ∘ suc))
    where
-   P' : ((i : Fin (suc n)) → R[1/ (f (suc i)) ]) → Type _
+   P' : ((i : Fin n) → R[1/ (f (suc i)) ]) → Type _
    P' y = P (λ { zero → x zero ; (suc i) → y i })
 
-   baseCase' : ∀ (rₛ : FinVec R (suc n)) (m : ℕ)
+   baseCase' : ∀ (rₛ : FinVec R n) (m : ℕ)
              → P' (λ i → [ rₛ i , f (suc i) ^ m , ∣ m , refl ∣₁ ])
    baseCase' rₛ m =
      subst P (funExt (λ { zero → refl ; (suc i) → refl }))
@@ -209,15 +205,15 @@ module InvertingElementsBase (R' : CommRing ℓ) where
       where
       l = max m k
 
-      newEnumVec : FinVec R (suc (suc n))
+      newEnumVec : FinVec R (suc n)
       newEnumVec zero = r₀ · (f zero) ^ (l ∸ k)
       newEnumVec (suc i) = rₛ i · (f (suc i)) ^ (l ∸ m)
 
-      oldBaseVec : (i : Fin (suc (suc n))) → R[1/ (f i) ]
+      oldBaseVec : (i : Fin (suc n)) → R[1/ (f i) ]
       oldBaseVec = λ { zero → [ r₀ , f zero ^ k , ∣ k , refl ∣₁ ]
                      ; (suc i) → [ rₛ i , f (suc i) ^ m , ∣ m , (λ _ → f (suc i) ^ m) ∣₁ ] }
 
-      newBaseVec : (i : Fin (suc (suc n))) → R[1/ (f i) ]
+      newBaseVec : (i : Fin (suc n)) → R[1/ (f i) ]
       newBaseVec zero = [ r₀ · (f zero) ^ (l ∸ k) , (f zero) ^ l , ∣ l , refl ∣₁ ]
       newBaseVec (suc i) = [ rₛ i · (f (suc i)) ^ (l ∸ m) , (f (suc i)) ^ l , ∣ l , refl ∣₁ ]
 
@@ -292,8 +288,6 @@ module _ {A B : CommRing ℓ} (φ : CommRingHom A B) (f : fst A) where
                      (fst χ) ∘ (fst AU./1AsCommRingHom) ≡ (fst φ/1)
   uniqInvElemHom = AU.invElemUniversalProp _ φ/1 (BU.S/1⊆S⁻¹Rˣ _ ∣ 1 , sym (·IdR _) ∣₁)
 
-
-
 module _ (R : CommRing ℓ) (f : fst R) where
  open CommRingTheory R
  open RingTheory (CommRing→Ring R)
diff --git a/Cubical/Algebra/CommRing/Localisation/Limit.agda b/Cubical/Algebra/CommRing/Localisation/Limit.agda
index b8e3dc24c3..afd060cb27 100644
--- a/Cubical/Algebra/CommRing/Localisation/Limit.agda
+++ b/Cubical/Algebra/CommRing/Localisation/Limit.agda
@@ -59,7 +59,7 @@ private
 
 -- were not dealing with case 0 here
 -- but then R = 0 = lim {} (limit of the empty diagram)
-module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
+module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') n) where
  open isMultClosedSubset
  open CommRingTheory R'
  open RingTheory (CommRing→Ring R')
@@ -84,13 +84,13 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
   module UP i j = S⁻¹RUniversalProp R' [ f i · f j ⁿ|n≥0] (powersFormMultClosedSubset (f i · f j))
 
   -- some syntax to make things readable
-  0at : (i : Fin (suc n)) →  R[1/ (f i) ]
+  0at : (i : Fin n) →  R[1/ (f i) ]
   0at i = R[1/ (f i) ]AsCommRing .snd .CommRingStr.0r
 
-  _/1ˢ : R → {i : Fin (suc n)} →  R[1/ (f i) ]
+  _/1ˢ : R → {i : Fin n} →  R[1/ (f i) ]
   (r /1ˢ) {i = i} = U._/1 i r
 
-  _/1ᵖ : R → {i j : Fin (suc n)} →  R[1/ (f i) · (f j) ]
+  _/1ᵖ : R → {i j : Fin n} →  R[1/ (f i) · (f j) ]
   (r /1ᵖ) {i = i} {j = j} = UP._/1 i j r
 
 
@@ -108,7 +108,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
                     → x ≡ 0r
   annihilatorHelper ann = recFin (is-set _ _) exponentHelper uIsPower
     where
-    u : FinVec R (suc n)
+    u : FinVec R n
     u i = ann i .fst .fst
 
     uIsPower : ∀ i → u i ∈ₚ [ (f i) ⁿ|n≥0]
@@ -121,7 +121,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
                    → x ≡ 0r
     exponentHelper pows = PT.rec (is-set _ _) Σhelper (GeneratingPowers.thm R' l _ _ 1∈⟨f₀,⋯,fₙ⟩)
       where
-      m : FinVec ℕ (suc n)
+      m : FinVec ℕ n
       m i = pows i .fst
 
       u≡fᵐ : ∀ i → u i ≡ f i ^ m i
@@ -129,7 +129,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
 
       l = Max m
 
-      fˡ : FinVec R (suc n)
+      fˡ : FinVec R n
       fˡ i = f i ^ l
 
       fˡx≡0 : ∀ i → f i ^ l · x ≡ 0r
@@ -145,7 +145,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
         0r ∎
 
 
-      Σhelper : Σ[ α ∈ FinVec R (suc n) ] 1r ≡ ∑ (λ i → α i · f i ^ l)
+      Σhelper : Σ[ α ∈ FinVec R n ] 1r ≡ ∑ (λ i → α i · f i ^ l)
               → x ≡ 0r
       Σhelper (α , 1≡∑αfˡ) =
         x                                   ≡⟨ sym (·IdL _) ⟩
@@ -155,13 +155,13 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
                                                                   (f i ^ l) x)) ⟩
         ∑ (λ i → α i · (f i ^ l · x))       ≡⟨ ∑Ext (λ i → cong (α i ·_) (fˡx≡0 i)) ⟩
         ∑ (λ i → α i · 0r)                  ≡⟨ ∑Ext (λ i → 0RightAnnihilates (α i)) ⟩
-        ∑ (replicateFinVec (suc n) 0r)      ≡⟨ ∑0r (suc n) ⟩
+        ∑ (replicateFinVec n 0r)      ≡⟨ ∑0r n ⟩
         0r ∎
 
 
  -- the morphisms into localisations of products from the left/right
  -- we need to define them by hand as using RadicalLemma wouldn't compute later
- χˡUnique : (i j : Fin (suc n))
+ χˡUnique : (i j : Fin n)
           → ∃![ χ ∈ CommRingHom R[1/ f i ]AsCommRing R[1/ f i · f j ]AsCommRing ]
                 (fst χ) ∘ (U._/1 i) ≡ (UP._/1 i j)
  χˡUnique i j = U.S⁻¹RHasUniversalProp i _ (UP./1AsCommRingHom i j) unitHelper
@@ -175,10 +175,10 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
      path : (n : ℕ) → 1r · (f i ^ n · f j ^ n) · 1r ≡ (1r · 1r) · (1r · ((f i · f j) ^ n))
      path n = solve! R' ∙ sym (^-ldist-· (f i) (f j) n) ∙ solve! R'
 
- χˡ : (i j : Fin (suc n)) → CommRingHom R[1/ f i ]AsCommRing R[1/ f i · f j ]AsCommRing
+ χˡ : (i j : Fin n) → CommRingHom R[1/ f i ]AsCommRing R[1/ f i · f j ]AsCommRing
  χˡ i j = χˡUnique i j .fst .fst
 
- χʳUnique : (i j : Fin (suc n))
+ χʳUnique : (i j : Fin n)
           →  ∃![ χ ∈ CommRingHom R[1/ f j ]AsCommRing R[1/ f i · f j ]AsCommRing ]
                 (fst χ) ∘ (U._/1 j) ≡ (UP._/1 i j)
  χʳUnique i j = U.S⁻¹RHasUniversalProp j _ (UP./1AsCommRingHom i j) unitHelper
@@ -192,14 +192,14 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
      path : (n : ℕ) → 1r · (f j ^ n · f i ^ n) · 1r ≡ (1r · 1r) · (1r · ((f i · f j) ^ n))
      path n = solve! R' ∙ sym (^-ldist-· (f i) (f j) n) ∙ solve! R'
 
- χʳ : (i j : Fin (suc n)) → CommRingHom R[1/ f j ]AsCommRing R[1/ f i · f j ]AsCommRing
+ χʳ : (i j : Fin n) → CommRingHom R[1/ f j ]AsCommRing R[1/ f i · f j ]AsCommRing
  χʳ i j = χʳUnique i j .fst .fst
 
 
 
  -- super technical stuff, please don't look at it
  private
-  χ≡Elim<Only : (x  : (i : Fin (suc n)) → R[1/ f i ])
+  χ≡Elim<Only : (x  : (i : Fin n) → R[1/ f i ])
           → (∀ i j → i < j → χˡ i j .fst (x i) ≡ χʳ i j .fst (x j))
           → ∀ i j → χˡ i j .fst (x i) ≡ χʳ i j .fst (x j)
   χ≡Elim<Only x <hyp i j = aux (i ≟ j) -- doesn't type check in reasonable time using with syntax
@@ -218,14 +218,14 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
       χˡsubst i j (x j) ≡⟨ sym (χSwapR→L i j (x j)) ⟩
       χʳ i j .fst (x j) ∎
       where
-      χʳsubst : (i j : Fin (suc n)) → R[1/ f i ] → R[1/ f i · f j ]
+      χʳsubst : (i j : Fin n) → R[1/ f i ] → R[1/ f i · f j ]
       χʳsubst i j x = subst (λ r → R[1/ r ]) (·Comm (f j) (f i)) (χʳ j i .fst x)
 
       χSwapL→R : ∀ i j x → χˡ i j .fst x ≡ χʳsubst i j x
       χSwapL→R i j = invElPropElim (λ _ → squash/ _ _)
              λ r m → cong [_] (ΣPathP (sym (transportRefl _) , Σ≡Prop (∈-isProp _)
                       (sym (transportRefl _ ∙ cong (λ x → 1r · transport refl (x ^ m)) (·Comm _ _)))))
-      χˡsubst : (i j : Fin (suc n)) → R[1/ f j ] → R[1/ f i · f j ]
+      χˡsubst : (i j : Fin n) → R[1/ f j ] → R[1/ f i · f j ]
       χˡsubst i j x = subst (λ r → R[1/ r ]) (·Comm (f j) (f i)) (χˡ j i .fst x)
 
       χSwapR→L : ∀ i j x → χʳ i j .fst x ≡ χˡsubst i j x
@@ -233,17 +233,17 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
              λ r m → cong [_] (ΣPathP (sym (transportRefl _) , Σ≡Prop (∈-isProp _)
                       (sym (transportRefl _ ∙ cong (λ x → 1r · transport refl (x ^ m)) (·Comm _ _)))))
 
- χ≡PropElim : {B : ((i : Fin (suc n)) → R[1/ f i ]) → Type ℓ''} (isPropB : ∀ {x} → isProp (B x))
-            → (∀ (r : FinVec R (suc n)) (m l : ℕ)
+ χ≡PropElim : {B : ((i : Fin n) → R[1/ f i ]) → Type ℓ''} (isPropB : ∀ {x} → isProp (B x))
+            → (∀ (r : FinVec R n) (m l : ℕ)
                   → (∀ i j → r i · f j ^ m · (f i · f j) ^ l ≡ r j · f i ^ m · (f i · f j) ^ l)
                   → B (λ i → [ r i , f i ^ m , ∣ m , refl ∣₁ ]))
           -------------------------------------------------------------------------------------
-           → (x : (i : Fin (suc n)) → R[1/ f i ])
+           → (x : (i : Fin n) → R[1/ f i ])
            → (∀ i j → χˡ i j .fst (x i) ≡ χʳ i j .fst (x j))
            → B x
  χ≡PropElim {B = B} isPropB baseHyp = invElPropElimN n f _ (λ _ → isProp→ isPropB) baseCase
    where
-   baseCase : ∀ (r : FinVec R (suc n)) (m : ℕ)
+   baseCase : ∀ (r : FinVec R n) (m : ℕ)
             → (∀ i j → χˡ i j .fst ([ r i , f i ^ m , ∣ m , refl ∣₁ ])
                      ≡ χʳ i j .fst ([ r j , f j ^ m , ∣ m , refl ∣₁ ]))
             → B (λ i → [ r i , f i ^ m , ∣ m , refl ∣₁ ])
@@ -269,7 +269,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
      annihilatorHelper anns = recFin2 isPropB exponentHelper sIsPow
        where
        -- notation
-       s : (i j : Fin (suc n)) → R
+       s : (i j : Fin n) → R
        s i j = anns i j .fst .fst
 
        sIsPow : ∀ i j → s i j ∈ₚ [ (f i · f j) ⁿ|n≥0]
@@ -305,7 +305,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
        exponentHelper pows = baseHyp r m (m +ℕ k) paths
          where
          -- sᵢⱼ = fᵢfⱼ ^ lᵢⱼ, so need to take max over all of these...
-         l : (i j : Fin (suc n)) → ℕ
+         l : (i j : Fin n) → ℕ
          l i j = pows i j .fst
 
          k = Max (λ i → Max (l i))
@@ -400,12 +400,12 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
 
  -- this will do all the heavy lifting
  equalizerLemma : 1r ∈ ⟨f₀,⋯,fₙ⟩
-                → ∀ (x : (i : Fin (suc n)) → R[1/ f i ]) -- s.t.
+                → ∀ (x : (i : Fin n) → R[1/ f i ]) -- s.t.
                 → (∀ i j → χˡ i j .fst (x i) ≡ χʳ i j .fst (x j))
                 → ∃![ y ∈ R ] (∀ i → y /1ˢ ≡ x i)
  equalizerLemma 1∈⟨f₀,⋯,fₙ⟩ = χ≡PropElim isProp∃! baseCase
    where
-   baseCase : ∀ (r : FinVec R (suc n)) (m l : ℕ)
+   baseCase : ∀ (r : FinVec R n) (m l : ℕ)
             → (∀ i j → r i · f j ^ m · (f i · f j) ^ l ≡ r j · f i ^ m · (f i · f j) ^ l)
             → ∃![ y ∈ R ] (∀ i → y /1ˢ ≡ [ r i , f i ^ m , ∣ m , refl ∣₁ ])
    baseCase r m l <Paths = PT.rec isProp∃! Σhelper (GeneratingPowers.thm R' 2m+l _ _ 1∈⟨f₀,⋯,fₙ⟩)
@@ -413,10 +413,10 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
      -- critical exponent
      2m+l = m +ℕ (m +ℕ l)
 
-     f²ᵐ⁺ˡ : FinVec R (suc n)
+     f²ᵐ⁺ˡ : FinVec R n
      f²ᵐ⁺ˡ i = f i ^ 2m+l
 
-     Σhelper : Σ[ α ∈ FinVec R (suc n) ] 1r ≡ linearCombination R' α f²ᵐ⁺ˡ
+     Σhelper : Σ[ α ∈ FinVec R n ] 1r ≡ linearCombination R' α f²ᵐ⁺ˡ
              → ∃![ y ∈ R ] (∀ i → y /1ˢ ≡ [ r i , f i ^ m , ∣ m , refl ∣₁ ])
      Σhelper (α , linCombi) = (z , z≡r/fᵐ)
                             , λ y' → Σ≡Prop (λ _ → isPropΠ (λ _ → squash/ _ _)) (unique _ (y' .snd))
@@ -524,7 +524,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
  open Cone
  open Functor
 
- locDiagram : Functor (DLShfDiag (suc n) ℓ) CommRingsCategory
+ locDiagram : Functor (DLShfDiag n ℓ) CommRingsCategory
  F-ob locDiagram (sing i) = R[1/ f i ]AsCommRing
  F-ob locDiagram (pair i j _) = R[1/ f i · f j ]AsCommRing
  F-hom locDiagram idAr = idCommRingHom _
@@ -549,7 +549,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') (suc n)) where
    instance
     _ = snd A'
 
-   φ : (i : Fin (suc n)) → CommRingHom A' R[1/ f i ]AsCommRing
+   φ : (i : Fin n) → CommRingHom A' R[1/ f i ]AsCommRing
    φ i = cᴬ .coneOut (sing i)
 
    applyEqualizerLemma : ∀ a → ∃![ r ∈ R ] ∀ i → r /1ˢ ≡ φ i .fst a

From fb89c7cc1a5ae7a2efe33c8012076b35dbccd986 Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 15 Feb 2024 13:50:18 +0100
Subject: [PATCH 2/3] also simplify ZariskiLattice.StructureSheaf a bit

---
 .../ZariskiLattice/StructureSheaf.agda        | 35 +++++--------------
 1 file changed, 8 insertions(+), 27 deletions(-)

diff --git a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda b/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda
index 78f2aca287..ac8798946b 100644
--- a/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda
+++ b/Cubical/Algebra/ZariskiLattice/StructureSheaf.agda
@@ -211,28 +211,9 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
  private instance _ = snd ZariskiLattice
 
  isSheaf𝓞ᴮ : isDLBasisSheaf 𝓞ᴮ
- isSheaf𝓞ᴮ {n = zero} α isBO⋁α A cᴬ = uniqueExists
-   (isTerminal𝓞ᴮ[0] A .fst)
-     (λ {(sing ()) ; (pair () _ _) }) -- the unique morphism is a cone morphism
-       (isPropIsConeMor _ _)
-         λ φ _ → isTerminal𝓞ᴮ[0] A .snd φ
-   where
-   -- D(0) is not 0 of the Zariski  lattice by refl!
-   p : 𝓞ᴮ .F-ob (0l , isBO⋁α) ≡ R[1/ 0r ]AsCommRing
-   p = 𝓞ᴮ .F-ob (0l , isBO⋁α)
-     ≡⟨ cong (𝓞ᴮ .F-ob) (Σ≡Prop (λ _ → ∈ₚ-isProp _ _)
-             (eq/ _ _ ((λ ()) , λ {zero → ∣ 1 , ∣ (λ ()) , 0LeftAnnihilates _ ∣₁ ∣₁ }))) ⟩
-       𝓞ᴮ .F-ob (D 0r , ∣ 0r , refl ∣₁)
-     ≡⟨ 𝓞ᴮOb≡ 0r ⟩
-       R[1/ 0r ]AsCommRing ∎
-
-   isTerminal𝓞ᴮ[0] : isTerminal CommRingsCategory (𝓞ᴮ .F-ob (0l , isBO⋁α))
-   isTerminal𝓞ᴮ[0] = subst (isTerminal CommRingsCategory)
-                           (sym (p ∙ R[1/0]≡0)) (TerminalCommRing .snd)
-
- isSheaf𝓞ᴮ {n = suc n} α = curriedHelper (fst ∘ α) (snd ∘ α)
+ isSheaf𝓞ᴮ {n = n} α = curriedHelper (fst ∘ α) (snd ∘ α)
   where
-  curriedHelper : (𝔞 : FinVec ZL (suc n)) (𝔞∈BO : ∀ i → 𝔞 i ∈ₚ BasicOpens)
+  curriedHelper : (𝔞 : FinVec ZL n) (𝔞∈BO : ∀ i → 𝔞 i ∈ₚ BasicOpens)
                   (⋁𝔞∈BO : ⋁ 𝔞 ∈ₚ BasicOpens)
                 → isLimCone _ _ (F-cone 𝓞ᴮ
                                 (condCone.B⋁Cone (λ i → 𝔞 i , 𝔞∈BO i) ⋁𝔞∈BO))
@@ -254,7 +235,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
       open condCone (λ i → 𝔞 i , ∣ f i , Df≡𝔞 i ∣₁)
       theSheafCone = B⋁Cone ∣ h , Dh≡⋁𝔞 ∣₁
 
-      DHelper : D h ≡ [ suc n , f ] --⋁ (D ∘ f)
+      DHelper : D h ≡ [ n , f ] --⋁ (D ∘ f)
       DHelper = Dh≡⋁𝔞 ∙ ⋁Ext (λ i → sym (Df≡𝔞 i)) ∙ ⋁D≡ f
 
       open Exponentiation R'
@@ -279,7 +260,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
       ff∈√⟨h⟩ : ∀ i j → f i · f j ∈ √ ⟨ h ⟩ₛ
       ff∈√⟨h⟩ i j = √ ⟨ h ⟩ₛ .snd .·Closed (f i) (f∈√⟨h⟩ j)
 
-      f/1 : FinVec (R[1/ h ]) (suc n)
+      f/1 : FinVec (R[1/ h ]) n
       f/1 i = (f i) /1
 
       1∈⟨f/1⟩ : 1r ∈ₕ ⟨ f/1 ⟩[ R[1/ h ]AsCommRing ]
@@ -291,9 +272,9 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
         helper1 : (m : ℕ) → h ^ m ∈ ⟨ f ⟩[ R' ] → 1r ∈ₕ ⟨ f/1 ⟩[ R[1/ h ]AsCommRing ]
         helper1 m = PT.map helper2
          where
-         helper2 : Σ[ α ∈ FinVec R (suc n) ]
+         helper2 : Σ[ α ∈ FinVec R n ]
                      h ^ m ≡ linearCombination R' α f
-                 → Σ[ β ∈ FinVec R[1/ h ] (suc n) ]
+                 → Σ[ β ∈ FinVec R[1/ h ] n ]
                      1r ≡ linearCombination R[1/ h ]AsCommRing β f/1
          helper2 (α , hᵐ≡∑αf) = β , path
           where
@@ -306,7 +287,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
            h⁻ᵐ = [ 1r , h ^ m , ∣ m , refl ∣₁ ]
                , eq/ _ _ ((1r , containsOne) , solve! R')
 
-          β : FinVec R[1/ h ] (suc n)
+          β : FinVec R[1/ h ] n
           β i = ((h ^ m) /1) ⁻¹ · α i /1
 
           /1Path : (h ^ m) /1 ≡ ∑ (λ i → α i /1 · f i /1)
@@ -375,7 +356,7 @@ module _ {ℓ : Level} (R' : CommRing ℓ) where
         (Σ≡Prop (λ _ → isPropPropTrunc) (cong (1r ·_) (transportRefl 1r) ∙ ·IdR 1r))))
         (Σ≡Prop (λ _ → isPropPropTrunc) (cong (1r ·_) (transportRefl 1r) ∙ ·IdR 1r)))))
 
-      open LimitFromCommRing R' R[1/ h ]AsCommRing (DLShfDiag (suc n) ℓ)
+      open LimitFromCommRing R' R[1/ h ]AsCommRing (DLShfDiag n ℓ)
                              doubleLocDiag doubleLocCone /1/1Cone
 
       -- get the desired cone in algebras:

From 0d8b4581bdd45743df25c91926711e5b1213ea7c Mon Sep 17 00:00:00 2001
From: Matthias Hutzler <matthias-hutzler@posteo.net>
Date: Thu, 15 Feb 2024 16:01:24 +0100
Subject: [PATCH 3/3] fix layout

---
 Cubical/Algebra/CommRing/Localisation/Limit.agda | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cubical/Algebra/CommRing/Localisation/Limit.agda b/Cubical/Algebra/CommRing/Localisation/Limit.agda
index afd060cb27..6f65e200ac 100644
--- a/Cubical/Algebra/CommRing/Localisation/Limit.agda
+++ b/Cubical/Algebra/CommRing/Localisation/Limit.agda
@@ -155,7 +155,7 @@ module _ (R' : CommRing ℓ) {n : ℕ} (f : FinVec (fst R') n) where
                                                                   (f i ^ l) x)) ⟩
         ∑ (λ i → α i · (f i ^ l · x))       ≡⟨ ∑Ext (λ i → cong (α i ·_) (fˡx≡0 i)) ⟩
         ∑ (λ i → α i · 0r)                  ≡⟨ ∑Ext (λ i → 0RightAnnihilates (α i)) ⟩
-        ∑ (replicateFinVec n 0r)      ≡⟨ ∑0r n ⟩
+        ∑ (replicateFinVec n 0r)            ≡⟨ ∑0r n ⟩
         0r ∎