Clean up library

CONTRIBUTING.md

@@ -111,6 +111,8 @@ When preparing a PR here are some general guidelines:
 - Avoid importing `Foundations.Everything`; import only the modules in
   `Foundations` you are using. Be reasonably specific in general when
   importing.
+  In particular, avoid importing useless files or useless renaming
+  and try to group them by folder like `Foundations` or `Data`
 
 - Avoid `public` imports, except in modules that are specifically meant
   to collect and re-export results from several modules.

Cubical/Algebra/AbGroup/Instances/Direct-Sum.agda → Cubical/Algebra/AbGroup/Instances/DirectSum.agda

@@ -1,12 +1,12 @@
 {-# OPTIONS --safe #-}
-module Cubical.Algebra.AbGroup.Instances.Direct-Sum where
+module Cubical.Algebra.AbGroup.Instances.DirectSum where
 
 open import Cubical.Foundations.Prelude
 
 open import Cubical.Algebra.AbGroup
 
-open import Cubical.Algebra.Direct-Sum.Base
-open import Cubical.Algebra.Direct-Sum.Properties
+open import Cubical.Algebra.DirectSum.Base
+open import Cubical.Algebra.DirectSum.Properties
 
 open import Cubical.Algebra.Polynomials.Multivariate.Base
 

Cubical/Algebra/AbGroup/TensorProduct.agda

@@ -157,10 +157,10 @@ module _ {AGr : AbGroup ℓ} {BGr : AbGroup ℓ'} where
 
   ∃List : (x : AGr ⨂₁ BGr) → ∃[ l ∈ List (A × B) ] (unlist l ≡ x)
   ∃List =
-    ⊗elimProp (λ _ → squash)
-      (λ a b → ∣ [ a , b ] , ⊗rUnit (a ⊗ b) ∣)
-      λ x y → rec2 squash λ {(l1 , p) (l2 , q)
-                          → ∣ (l1 ++ l2) , unlist++ l1 l2 ∙ cong₂ _+⊗_ p q ∣}
+    ⊗elimProp (λ _ → squash₁)
+      (λ a b → ∣ [ a , b ] , ⊗rUnit (a ⊗ b) ∣₁)
+      λ x y → rec2 squash₁ λ {(l1 , p) (l2 , q)
+                          → ∣ (l1 ++ l2) , unlist++ l1 l2 ∙ cong₂ _+⊗_ p q ∣₁}
 
   ⊗elimPropUnlist : ∀ {ℓ} {C : AGr ⨂₁ BGr → Type ℓ}
            → ((x : _) → isProp (C x))

Cubical/Algebra/CommAlgebra/FPAlgebra.agda

@@ -241,7 +241,7 @@ module _ {R : CommRing ℓ} where
       equiv : CommAlgebraEquiv (FPAlgebra n relations) A
 
   isFPAlgebra : (A : CommAlgebra R ℓ) → Type _
-  isFPAlgebra A = ∥ FinitePresentation A ∥
+  isFPAlgebra A = ∥ FinitePresentation A ∥₁
 
   isFPAlgebraIsProp : {A : CommAlgebra R ℓ} → isProp (isFPAlgebra A)
   isFPAlgebraIsProp = isPropPropTrunc

Cubical/Algebra/CommAlgebra/Localisation.agda

@@ -302,7 +302,7 @@ module DoubleAlgLoc (R : CommRing ℓ) (f g : (fst R)) where
      helper2 : (α : FinVec (fst R) 1)
              → x ^ n ≡ linearCombination R α (replicateFinVec 1 y)
              → x ∈ᵢ √ ⟨ y · x ⟩
-     helper2 α p = ∣ (suc n) , ∣ α , cong (x ·_) p ∙ useSolver x y (α zero) ∣ ∣
+     helper2 α p = ∣ (suc n) , ∣ α , cong (x ·_) p ∙ useSolver x y (α zero) ∣₁ ∣₁
       where
       useSolver : ∀ x y a → x · (a · y + 0r) ≡ a · (y · x) + 0r
       useSolver = solve R

Cubical/Algebra/CommAlgebra/Properties.agda

@@ -300,7 +300,7 @@ recPT→CommAlgebra : {R : CommRing ℓ} {A : Type ℓ'} (𝓕  : A → CommAlge
            → (σ : ∀ x y → CommAlgebraEquiv (𝓕 x) (𝓕 y))
            → (∀ x y z → σ x z ≡ compCommAlgebraEquiv (σ x y) (σ y z))
           ------------------------------------------------------
-           → ∥ A ∥ → CommAlgebra R ℓ''
+           → ∥ A ∥₁ → CommAlgebra R ℓ''
 recPT→CommAlgebra 𝓕 σ compCoh = GpdElim.rec→Gpd isGroupoidCommAlgebra 𝓕
   (3-ConstantCompChar 𝓕 (λ x y → uaCommAlgebra (σ x y))
                           λ x y z → sym (  cong uaCommAlgebra (compCoh x y z)

Cubical/Algebra/CommRing/FGIdeal.agda

@@ -84,7 +84,7 @@ module _ (Ring@(R , str) : CommRing ℓ) where
   {- 0r is the trivial linear Combination -}
   isLinearCombination0 : {n : ℕ} (V : FinVec R n)
                        → isLinearCombination V 0r
-  isLinearCombination0 V = ∣ _ , sym (dist0 V) ∣
+  isLinearCombination0 V = ∣ _ , sym (dist0 V) ∣₁
 
   {- Linear combinations are stable under left multiplication -}
   isLinearCombinationL· : {n : ℕ} (V : FinVec R n) (r : R) {x : R}
@@ -217,7 +217,7 @@ module _ (R' : CommRing ℓ) where
                              λ i → ·Closed (I .snd) _ (∀i→Vi∈I i))
 
  indInIdeal : ∀ {n : ℕ} (U : FinVec R n) (i : Fin n) → U i ∈ ⟨ U ⟩
- indInIdeal U i = ∣ (δ i) , sym (∑Mul1r _ U i) ∣
+ indInIdeal U i = ∣ (δ i) , sym (∑Mul1r _ U i) ∣₁
 
  sucIncl : ∀ {n : ℕ} (U : FinVec R (ℕsuc n)) → ⟨ U ∘ suc ⟩ ⊆ ⟨ U ⟩
  sucIncl U x = PT.map λ (α , x≡∑αUsuc) → (λ { zero → 0r ; (suc i) → α i }) , x≡∑αUsuc ∙ path _ _
@@ -227,7 +227,7 @@ module _ (R' : CommRing ℓ) where
 
  emptyFGIdeal : ∀ (V : FinVec R 0) → ⟨ V ⟩ ≡ 0Ideal
  emptyFGIdeal V = CommIdeal≡Char (λ _ →  PT.rec (is-set _ _) snd)
-                                 (λ _ x≡0 → ∣ (λ ()) , x≡0 ∣)
+                                 (λ _ x≡0 → ∣ (λ ()) , x≡0 ∣₁)
 
  0FGIdealLIncl : {n : ℕ} → ⟨ replicateFinVec n 0r ⟩ ⊆ 0Ideal
  0FGIdealLIncl x = PT.elim (λ _ → is-set _ _)
@@ -244,7 +244,7 @@ module _ (R' : CommRing ℓ) where
  FGIdealAddLemmaLIncl : {n m : ℕ} (U : FinVec R n) (V : FinVec R m)
                       → ⟨ U ++Fin V ⟩ ⊆ (⟨ U ⟩ +i ⟨ V ⟩)
  FGIdealAddLemmaLIncl {n = ℕzero} U V x x∈⟨V⟩ =
-                                  ∣ (0r , x) , ⟨ U ⟩ .snd .contains0 , x∈⟨V⟩ , sym (+Lid x) ∣
+                                  ∣ (0r , x) , ⟨ U ⟩ .snd .contains0 , x∈⟨V⟩ , sym (+Lid x) ∣₁
  FGIdealAddLemmaLIncl {n = ℕsuc n} U V x = PT.rec isPropPropTrunc helperΣ
    where
    helperΣ : Σ[ α ∈ FinVec R _ ] (x ≡ ∑ λ i → α i · (U ++Fin V) i) → x ∈ (⟨ U ⟩ +i ⟨ V ⟩)
@@ -258,7 +258,7 @@ module _ (R' : CommRing ℓ) where
     sumIncl : (∑ λ i → (α ∘ suc) i · ((U ∘ suc) ++Fin V) i) ∈ (⟨ U ⟩ +i ⟨ V ⟩)
     sumIncl = let sum = ∑ λ i → (α ∘ suc) i · ((U ∘ suc) ++Fin V) i in
          +iRespLincl ⟨ U ∘ suc ⟩ ⟨ U ⟩ ⟨ V ⟩ (sucIncl U) sum
-           (FGIdealAddLemmaLIncl (U ∘ suc) V _ ∣ (α ∘ suc) , refl ∣)
+           (FGIdealAddLemmaLIncl (U ∘ suc) V _ ∣ (α ∘ suc) , refl ∣₁)
 
  FGIdealAddLemmaRIncl : {n m : ℕ} (U : FinVec R n) (V : FinVec R m)
                       → (⟨ U ⟩ +i ⟨ V ⟩) ⊆ ⟨ U ++Fin V ⟩
@@ -269,7 +269,7 @@ module _ (R' : CommRing ℓ) where
            → Σ[ β ∈ FinVec R _ ] (z ≡ ∑ λ i → β i · V i)
            → x ≡ y + z
            → x ∈ ⟨ U ++Fin V ⟩
-   helperΣ (y , z) (α , y≡∑αU) (β , z≡∑βV) x≡y+z = ∣ (α ++Fin β) , path ∣
+   helperΣ (y , z) (α , y≡∑αU) (β , z≡∑βV) x≡y+z = ∣ (α ++Fin β) , path ∣₁
     where
     path : x ≡ ∑ λ i → (α ++Fin β) i · (U ++Fin V) i
     path = x                                               ≡⟨ x≡y+z ⟩
@@ -359,7 +359,7 @@ module GeneratingPowers (R' : CommRing ℓ) (n : ℕ) where
 
  lemma : (m : ℕ) (α U : FinVec R (ℕsuc m))
        → (linearCombination R' α U) ^ ((ℕsuc m) ·ℕ n) ∈ ⟨ U ⁿ ⟩
- lemma ℕzero α U = ∣ α ⁿ , path ∣
+ lemma ℕzero α U = ∣ α ⁿ , path ∣₁
   where
   path : (α zero · U zero + 0r) ^ (n +ℕ 0) ≡ α zero ^ n · U zero ^ n + 0r
   path = (α zero · U zero + 0r) ^ (n +ℕ 0) ≡⟨ cong (_^ (n +ℕ 0)) (+Rid _) ⟩

Cubical/Algebra/CommRing/Ideal.agda

@@ -113,7 +113,7 @@ module CommIdeal (R' : CommRing ℓ) where
   +ClosedΣ ((y₁ , z₁) , y₁∈I , z₁∈J , x₁≡y₁+z₁) ((y₂ , z₂) , y₂∈I , z₂∈J , x₂≡y₂+z₂) =
     (y₁ + y₂ , z₁ + z₂) , +Closed (snd I) y₁∈I y₂∈I , +Closed (snd J) z₁∈J z₂∈J
                       , cong₂ (_+_) x₁≡y₁+z₁ x₂≡y₂+z₂ ∙ +ShufflePairs _ _ _ _
- contains0 (snd (I +i J)) = ∣ (0r , 0r) , contains0 (snd I) , contains0 (snd J) , sym (+Rid _) ∣
+ contains0 (snd (I +i J)) = ∣ (0r , 0r) , contains0 (snd I) , contains0 (snd J) , sym (+Rid _) ∣₁
  ·Closed (snd (I +i J)) {x = x} r = map ·ClosedΣ
   where
   ·ClosedΣ : Σ[ (y₁ , z₁) ∈ (R × R) ] ((y₁ ∈ I) × (z₁ ∈ J) × (x ≡ y₁ + z₁))
@@ -135,16 +135,16 @@ module CommIdeal (R' : CommRing ℓ) where
                                  → subst-∈ I (sym (x≡y+z ∙∙ cong (_+ z) y≡0 ∙∙ +Lid z)) z∈I
 
  +iLidRIncl : ∀ (I : CommIdeal) → I ⊆ (0Ideal +i I)
- +iLidRIncl I x x∈I = ∣ (0r , x) , refl , x∈I , sym (+Lid _) ∣
+ +iLidRIncl I x x∈I = ∣ (0r , x) , refl , x∈I , sym (+Lid _) ∣₁
 
  +iLid : ∀ (I : CommIdeal) → 0Ideal +i I ≡ I
  +iLid I = CommIdeal≡Char (+iLidLIncl I) (+iLidRIncl I)
 
  +iLincl : ∀ (I J : CommIdeal) → I ⊆ (I +i J)
- +iLincl I J x x∈I = ∣ (x , 0r) , x∈I , J .snd .contains0 , sym (+Rid x) ∣
+ +iLincl I J x x∈I = ∣ (x , 0r) , x∈I , J .snd .contains0 , sym (+Rid x) ∣₁
 
  +iRincl : ∀ (I J : CommIdeal) → J ⊆ (I +i J)
- +iRincl I J x x∈J = ∣ (0r , x) , I .snd .contains0 , x∈J ,  sym (+Lid x) ∣
+ +iRincl I J x x∈J = ∣ (0r , x) , I .snd .contains0 , x∈J ,  sym (+Lid x) ∣₁
 
  +iRespLincl : ∀ (I J K : CommIdeal) → I ⊆ J → (I +i K) ⊆ (J +i K)
  +iRespLincl I J K I⊆J x = map λ ((y , z) , y∈I , z∈K , x≡y+z) → ((y , z) , I⊆J y y∈I , z∈K , x≡y+z)
@@ -153,15 +153,15 @@ module CommIdeal (R' : CommRing ℓ) where
  +iAssocLIncl I J K x = elim (λ _ → ((I +i J) +i K) .fst x .snd) (uncurry3
            λ (y , z) y∈I → elim (λ _ → isPropΠ λ _ → ((I +i J) +i K) .fst x .snd)
              λ ((u , v) , u∈J , v∈K , z≡u+v) x≡y+z
-               → ∣ (y + u , v) , ∣ _ , y∈I , u∈J , refl ∣ , v∈K
-                                , x≡y+z ∙∙ cong (y +_) z≡u+v ∙∙ +Assoc _ _ _ ∣)
+               → ∣ (y + u , v) , ∣ _ , y∈I , u∈J , refl ∣₁ , v∈K
+                                , x≡y+z ∙∙ cong (y +_) z≡u+v ∙∙ +Assoc _ _ _ ∣₁)
 
  +iAssocRIncl : ∀ (I J K : CommIdeal) → ((I +i J) +i K) ⊆ (I +i (J +i K))
  +iAssocRIncl I J K x = elim (λ _ → (I +i (J +i K)) .fst x .snd) (uncurry3
            λ (y , z) → elim (λ _ → isPropΠ2 λ _ _ → (I +i (J +i K)) .fst x .snd)
              λ ((u , v) , u∈I , v∈J , y≡u+v) z∈K x≡y+z
-               → ∣ (u , v + z) , u∈I , ∣ _ , v∈J , z∈K , refl ∣
-                                      , x≡y+z ∙∙ cong (_+ z) y≡u+v ∙∙ sym (+Assoc _ _ _) ∣)
+               → ∣ (u , v + z) , u∈I , ∣ _ , v∈J , z∈K , refl ∣₁
+                                      , x≡y+z ∙∙ cong (_+ z) y≡u+v ∙∙ sym (+Assoc _ _ _) ∣₁)
 
  +iAssoc : ∀ (I J K : CommIdeal) → I +i (J +i K) ≡ (I +i J) +i K
  +iAssoc I J K = CommIdeal≡Char (+iAssocLIncl I J K) (+iAssocRIncl I J K)
@@ -171,7 +171,7 @@ module CommIdeal (R' : CommRing ℓ) where
                                  → subst-∈ I (sym x≡y+z) (I .snd .+Closed y∈I z∈I)
 
  +iIdemRIncl : ∀ (I : CommIdeal) → I ⊆ (I +i I)
- +iIdemRIncl I x x∈I = ∣ (0r , x) , I .snd .contains0 , x∈I , sym (+Lid _) ∣
+ +iIdemRIncl I x x∈I = ∣ (0r , x) , I .snd .contains0 , x∈I , sym (+Lid _) ∣₁
 
  +iIdem : ∀ (I : CommIdeal) → I +i I ≡ I
  +iIdem I = CommIdeal≡Char (+iIdemLIncl I) (+iIdemRIncl I)
@@ -195,7 +195,7 @@ module CommIdeal (R' : CommRing ℓ) where
                                       , ++FinPres∈ (J .fst) ∀βi∈J ∀δi∈J
     , cong₂ (_+_) x≡∑αβ y≡∑γδ ∙∙ sym (∑Split++ (λ i → α i · β i) (λ i → γ i · δ i))
                               ∙∙ ∑Ext (mul++dist α β γ δ)
- contains0 (snd (I ·i J)) = ∣ 0 , ((λ ()) , (λ ())) , (λ ()) , (λ ()) , refl ∣
+ contains0 (snd (I ·i J)) = ∣ 0 , ((λ ()) , (λ ())) , (λ ()) , (λ ()) , refl ∣₁
  ·Closed (snd (I ·i J)) r = map
   λ (n , (α , β) , ∀αi∈I , ∀βi∈J , x≡∑αβ)
    → n , ((λ i → r · α i) , β) , (λ i → I .snd .·Closed r (∀αi∈I i)) , ∀βi∈J
@@ -205,7 +205,7 @@ module CommIdeal (R' : CommRing ℓ) where
 
  prodInProd : ∀ (I J : CommIdeal) (x y : R) → x ∈ I → y ∈ J → (x · y) ∈ (I ·i J)
  prodInProd _ _ x y x∈I y∈J =
-            ∣ 1 , ((λ _ → x) , λ _ → y) , (λ _ → x∈I) , (λ _ → y∈J) , sym (+Rid _) ∣
+            ∣ 1 , ((λ _ → x) , λ _ → y) , (λ _ → x∈I) , (λ _ → y∈J) , sym (+Rid _) ∣₁
 
  ·iLincl : ∀ (I J : CommIdeal) → (I ·i J) ⊆ I
  ·iLincl I J x = elim (λ _ → I .fst x .snd)
@@ -220,7 +220,7 @@ module CommIdeal (R' : CommRing ℓ) where
  ·iComm I J = CommIdeal≡Char (·iComm⊆ I J) (·iComm⊆ J I)
 
  I⊆I1 : ∀ (I : CommIdeal) → I ⊆ (I ·i 1Ideal)
- I⊆I1 I x x∈I = ∣ 1 , ((λ _ → x) , λ _ → 1r) , (λ _ → x∈I) , (λ _ → lift tt) , useSolver x ∣
+ I⊆I1 I x x∈I = ∣ 1 , ((λ _ → x) , λ _ → 1r) , (λ _ → x∈I) , (λ _ → lift tt) , useSolver x ∣₁
   where
   useSolver : ∀ x → x ≡ x · 1r + 0r
   useSolver = solve R'
@@ -273,7 +273,7 @@ module CommIdeal (R' : CommRing ℓ) where
            (λ ((γi , δi) , γi∈J , δi∈K , βi≡γi+δi) →
               ∣ (α i · γi , α i · δi) , prodInProd I J _ _ (α∈I i) γi∈J
                                       , prodInProd I K _ _ (α∈I i) δi∈K
-                                      , cong (α i ·_) βi≡γi+δi ∙ ·Rdist+ _ _ _ ∣)
+                                      , cong (α i ·_) βi≡γi+δi ∙ ·Rdist+ _ _ _ ∣₁)
            (β∈J+K i))
 
  ·iRdist+iRIncl : ∀ (I J K : CommIdeal) → ((I ·i J) +i (I ·i K)) ⊆ (I ·i (J +i K))

Cubical/Algebra/CommRing/Instances/Int.agda

@@ -5,18 +5,18 @@ open import Cubical.Foundations.Prelude
 
 open import Cubical.Algebra.CommRing
 open import Cubical.Data.Int as Int
-  renaming ( ℤ to ℤType ; _+_ to _+ℤ_; _·_ to _·ℤ_; -_ to -ℤ_)
+  renaming ( ℤ to ℤ ; _+_ to _+ℤ_; _·_ to _·ℤ_; -_ to -ℤ_)
 
 open CommRingStr
 
-ℤ : CommRing ℓ-zero
-fst ℤ = ℤType
-0r (snd ℤ) = 0
-1r (snd ℤ) = 1
-_+_ (snd ℤ) = _+ℤ_
-_·_ (snd ℤ) = _·ℤ_
-- snd ℤ = -ℤ_
-isCommRing (snd ℤ) = isCommRingℤ
+ℤCommRing : CommRing ℓ-zero
+fst ℤCommRing = ℤ
+0r (snd ℤCommRing) = 0
+1r (snd ℤCommRing) = 1
+_+_ (snd ℤCommRing) = _+ℤ_
+_·_ (snd ℤCommRing) = _·ℤ_
+- snd ℤCommRing = -ℤ_
+isCommRing (snd ℤCommRing) = isCommRingℤ
   where
   abstract
     isCommRingℤ : IsCommRing 0 1 _+ℤ_ _·ℤ_ -ℤ_

Cubical/Algebra/CommRing/Instances/MultivariatePoly-Quotient.agda

@@ -14,7 +14,7 @@ open import Cubical.Algebra.Ring
 open import Cubical.Algebra.CommRing
 open import Cubical.Algebra.CommRing.FGIdeal
 open import Cubical.Algebra.CommRing.QuotientRing
-open import Cubical.Algebra.CommRing.Instances.Int renaming (ℤ to ℤCR)
+open import Cubical.Algebra.CommRing.Instances.Int renaming (ℤCommRing to ℤCR)
 
 open import Cubical.Algebra.Polynomials.Multivariate.Base
 open import Cubical.Algebra.CommRing.Instances.MultivariatePoly

Cubical/Algebra/CommRing/Instances/MultivariatePoly-notationZ.agda

@@ -23,25 +23,25 @@ open import Cubical.Algebra.CommRing.Instances.MultivariatePoly-Quotient
 -- Notations for ℤ polynomial rings
 
 ℤ[X] : CommRing ℓ-zero
-ℤ[X] = PolyCommRing ℤ 1
+ℤ[X] = PolyCommRing ℤCommRing 1
 
 ℤ[x] : Type ℓ-zero
 ℤ[x] = fst ℤ[X]
 
 ℤ[X,Y] : CommRing ℓ-zero
-ℤ[X,Y] = PolyCommRing ℤ 2
+ℤ[X,Y] = PolyCommRing ℤCommRing 2
 
 ℤ[x,y] : Type ℓ-zero
 ℤ[x,y] = fst ℤ[X,Y]
 
 ℤ[X,Y,Z] : CommRing ℓ-zero
-ℤ[X,Y,Z] = PolyCommRing ℤ 3
+ℤ[X,Y,Z] = PolyCommRing ℤCommRing 3
 
 ℤ[x,y,z] : Type ℓ-zero
 ℤ[x,y,z] = fst ℤ[X,Y,Z]
 
 ℤ[X1,···,Xn] : (n : ℕ) → CommRing ℓ-zero
-ℤ[X1,···,Xn] n = A[X1,···,Xn] ℤ n
+ℤ[X1,···,Xn] n = A[X1,···,Xn] ℤCommRing n
 
 ℤ[x1,···,xn] : (n : ℕ) → Type ℓ-zero
 ℤ[x1,···,xn] n = fst (ℤ[X1,···,Xn] n)
@@ -51,37 +51,37 @@ open import Cubical.Algebra.CommRing.Instances.MultivariatePoly-Quotient
 -- Notation for quotiented ℤ polynomial ring
 
 <X> : FinVec ℤ[x] 1
-<X> = <Xkʲ> ℤ 1 0 1
+<X> = <Xkʲ> ℤCommRing 1 0 1
 
 <X²> : FinVec ℤ[x] 1
-<X²> = <Xkʲ> ℤ 1 0 2
+<X²> = <Xkʲ> ℤCommRing 1 0 2
 
 <X³> : FinVec ℤ[x] 1
-<X³> = <Xkʲ> ℤ 1 0 3
+<X³> = <Xkʲ> ℤCommRing 1 0 3
 
 <Xᵏ> : (k  : ℕ) → FinVec ℤ[x] 1
-<Xᵏ> k = <Xkʲ> ℤ 1 0 k
+<Xᵏ> k = <Xkʲ> ℤCommRing 1 0 k
 
 ℤ[X]/X : CommRing ℓ-zero
-ℤ[X]/X = A[X1,···,Xn]/<Xkʲ> ℤ 1 0 1
+ℤ[X]/X = A[X1,···,Xn]/<Xkʲ> ℤCommRing 1 0 1
 
 ℤ[x]/x : Type ℓ-zero
 ℤ[x]/x = fst ℤ[X]/X
 
 ℤ[X]/X² : CommRing ℓ-zero
-ℤ[X]/X² = A[X1,···,Xn]/<Xkʲ> ℤ 1 0 2
+ℤ[X]/X² = A[X1,···,Xn]/<Xkʲ> ℤCommRing 1 0 2
 
 ℤ[x]/x² : Type ℓ-zero
 ℤ[x]/x² = fst ℤ[X]/X²
 
 ℤ[X]/X³ : CommRing ℓ-zero
-ℤ[X]/X³ = A[X1,···,Xn]/<Xkʲ> ℤ 1 0 3
+ℤ[X]/X³ = A[X1,···,Xn]/<Xkʲ> ℤCommRing 1 0 3
 
 ℤ[x]/x³ : Type ℓ-zero
 ℤ[x]/x³ = fst ℤ[X]/X³
 
 ℤ[X1,···,Xn]/<X1,···,Xn> : (n : ℕ) → CommRing ℓ-zero
-ℤ[X1,···,Xn]/<X1,···,Xn> n = A[X1,···,Xn]/<X1,···,Xn> ℤ n
+ℤ[X1,···,Xn]/<X1,···,Xn> n = A[X1,···,Xn]/<X1,···,Xn> ℤCommRing n
 
 ℤ[x1,···,xn]/<x1,···,xn> : (n : ℕ) → Type ℓ-zero
 ℤ[x1,···,xn]/<x1,···,xn> n = fst (ℤ[X1,···,Xn]/<X1,···,Xn> n)
@@ -91,8 +91,8 @@ open import Cubical.Algebra.CommRing.Instances.MultivariatePoly-Quotient
 -- they only holds up to a path
 
 ℤ'[X]/X : CommRing ℓ-zero
-ℤ'[X]/X = A[X1,···,Xn]/<X1,···,Xn> ℤ 1
+ℤ'[X]/X = A[X1,···,Xn]/<X1,···,Xn> ℤCommRing 1
 
 equivℤ[X] : ℤ'[X]/X ≡ ℤ[X]/X
-equivℤ[X] = cong (λ X → (A[X1,···,Xn] ℤ 1) / (genIdeal ((A[X1,···,Xn] ℤ 1)) X))
+equivℤ[X] = cong (λ X → (A[X1,···,Xn] ℤCommRing 1) / (genIdeal ((A[X1,···,Xn] ℤCommRing 1)) X))
                    (funExt (λ {zero → refl }))

Cubical/Algebra/CommRing/Instances/MultivariatePoly.agda

@@ -31,20 +31,19 @@ module _
   fst PolyCommRing = Poly A n
   0r (snd PolyCommRing) = 0P
   1r (snd PolyCommRing) = 1P
-  _+_ (snd PolyCommRing) = _Poly+_
-  _·_ (snd PolyCommRing) = _Poly*_
-  - snd PolyCommRing = Poly-inv
+  _+_ (snd PolyCommRing) = _poly+_
+  _·_ (snd PolyCommRing) = _poly*_
+  - snd PolyCommRing = polyInv
   isCommRing (snd PolyCommRing) = makeIsCommRing
                                   trunc
-                                  Poly+-assoc
-                                  Poly+-Rid
-                                  Poly+-rinv
-                                  Poly+-comm
-                                  Poly*-assoc
-                                  Poly*-Rid
-                                  Poly*-Rdist
-                                  Poly*-comm
-
+                                  poly+Assoc
+                                  poly+IdR
+                                  poly+InvR
+                                  poly+Comm
+                                  poly*Assoc
+                                  poly*IdR
+                                  poly*DistR
+                                  poly*Comm
 
 
 -----------------------------------------------------------------------------

Cubical/Algebra/CommRing/Instances/UnivariatePoly.agda

@@ -3,6 +3,8 @@
 module Cubical.Algebra.CommRing.Instances.UnivariatePoly where
 
 open import Cubical.Foundations.Prelude
+open import Cubical.Data.Nat using (ℕ ; zero ; suc)
+
 open import Cubical.Algebra.CommRing
 open import Cubical.Algebra.Polynomials.Univariate.Base
 open import Cubical.Algebra.Polynomials.Univariate.Properties
@@ -31,3 +33,8 @@ UnivariatePoly R = (PolyMod.Poly R) , str
                                       (PolyModTheory.Poly*Rid R)
                                       (PolyModTheory.Poly*LDistrPoly+ R)
                                       (PolyModTheory.Poly*Commutative R)
+
+
+nUnivariatePoly : (A' : CommRing ℓ) → (n : ℕ) → CommRing ℓ
+nUnivariatePoly A' zero = A'
+nUnivariatePoly A' (suc n) = UnivariatePoly (nUnivariatePoly A' n)