remove isSet<AlgebraicStructure> accessors (#1040)

* remove all isSet<AlgebraicStructure> accessors

* collapse some is-set extraction chains

Cubical/Algebra/AbGroup/Base.agda

@@ -138,9 +138,6 @@ module _ ((G , abgroupstr _ _ _ GisGroup) : AbGroup ℓ) where
   AbGroup→CommMonoid .snd .CommMonoidStr.isCommMonoid .IsCommMonoid.isMonoid = IsAbGroup.isMonoid GisGroup
   AbGroup→CommMonoid .snd .CommMonoidStr.isCommMonoid .IsCommMonoid.·Comm = IsAbGroup.+Comm GisGroup
 
-isSetAbGroup : (A : AbGroup ℓ) → isSet ⟨ A ⟩
-isSetAbGroup A = is-set (str A)
-
 AbGroupHom : (G : AbGroup ℓ) (H : AbGroup ℓ') → Type (ℓ-max ℓ ℓ')
 AbGroupHom G H = GroupHom (AbGroup→Group G) (AbGroup→Group H)
 

Cubical/Algebra/Algebra/Base.agda

@@ -111,11 +111,6 @@ module commonExtractors {R : Ring ℓ} where
   Algebra→MultMonoid : (A : Algebra R ℓ') → Monoid ℓ'
   Algebra→MultMonoid A = Ring→MultMonoid (Algebra→Ring A)
 
-  isSetAlgebra : (A : Algebra R ℓ') → isSet ⟨ A ⟩
-  isSetAlgebra A = is-set
-    where
-    open AlgebraStr (str A)
-
   open RingStr (snd R) using (1r; ·DistL+) renaming (_+_ to _+r_; _·_ to _·s_)
 
   module _ {A : Type ℓ'} {0a 1a : A}
@@ -214,23 +209,30 @@ isPropIsAlgebraHom : (R : Ring ℓ) {A : Type ℓ'} {B : Type ℓ''}
                      (AS : AlgebraStr R A) (f : A → B) (BS : AlgebraStr R B)
                    → isProp (IsAlgebraHom AS f BS)
 isPropIsAlgebraHom R AS f BS = isOfHLevelRetractFromIso 1 IsAlgebraHomIsoΣ
-                               (isProp×5 (isSetAlgebra (_ , BS) _ _)
-                                         (isSetAlgebra (_ , BS) _ _)
-                                         (isPropΠ2 λ _ _ → isSetAlgebra (_ , BS) _ _)
-                                         (isPropΠ2 λ _ _ → isSetAlgebra (_ , BS) _ _)
-                                         (isPropΠ λ _ → isSetAlgebra (_ , BS) _ _)
-                                         (isPropΠ2 λ _ _ → isSetAlgebra (_ , BS) _ _))
+                               (isProp×5 (is-set _ _)
+                                         (is-set _ _)
+                                         (isPropΠ2 λ _ _ → is-set _ _)
+                                         (isPropΠ2 λ _ _ → is-set _ _)
+                                         (isPropΠ λ _ → is-set _ _)
+                                         (isPropΠ2 λ _ _ → is-set _ _))
+  where
+  open AlgebraStr BS
 
 isSetAlgebraHom : (M : Algebra R ℓ') (N : Algebra R ℓ'')
                 → isSet (AlgebraHom M N)
-isSetAlgebraHom _ N = isSetΣ (isSetΠ (λ _ → isSetAlgebra N))
+isSetAlgebraHom _ N = isSetΣ (isSetΠ (λ _ → is-set))
                         λ _ → isProp→isSet (isPropIsAlgebraHom _ _ _ _)
+  where
+  open AlgebraStr (str N)
 
 
 isSetAlgebraEquiv : (M : Algebra R ℓ') (N : Algebra R ℓ'')
                   → isSet (AlgebraEquiv M N)
-isSetAlgebraEquiv M N = isSetΣ (isOfHLevel≃ 2 (isSetAlgebra M) (isSetAlgebra N))
+isSetAlgebraEquiv M N = isSetΣ (isOfHLevel≃ 2 M.is-set N.is-set)
                           λ _ → isProp→isSet (isPropIsAlgebraHom _ _ _ _)
+  where
+  module M = AlgebraStr (str M)
+  module N = AlgebraStr (str N)
 
 AlgebraHom≡ : {φ ψ : AlgebraHom A B} → fst φ ≡ fst ψ → φ ≡ ψ
 AlgebraHom≡ = Σ≡Prop λ f → isPropIsAlgebraHom _ _ f _

Cubical/Algebra/Algebra/Subalgebra.agda

@@ -68,7 +68,7 @@ module _ ((S , isSubalgebra) : Subalgebra) where
   Subalgebra→Algebra .snd .algStr._⋆_ r (a , a∈) = r ⋆ a , ⋆-closed r a∈
   Subalgebra→Algebra .snd .algStr.isAlgebra =
     let
-      isSet-A' = isSetΣSndProp (isSetAlgebra A) (∈-isProp S)
+      isSet-A' = isSetΣSndProp is-set (∈-isProp S)
       +Assoc' = λ x y z → Subalgebra→Algebra≡ (+Assoc (fst x) (fst y) (fst z))
       +IdR' = λ x → Subalgebra→Algebra≡ (+IdR (fst x))
       +InvR' = λ x → Subalgebra→Algebra≡ (+InvR (fst x))

Cubical/Algebra/CommAlgebra/Base.agda

@@ -77,11 +77,6 @@ module _ {R : CommRing ℓ} where
   CommAlgebra→CommRing (_ , commalgebrastr  _ _ _ _ _ _ (iscommalgebra isAlgebra ·-comm)) =
     _ , commringstr _ _ _ _ _ (iscommring (IsAlgebra.isRing isAlgebra) ·-comm)
 
-  isSetCommAlgebra : (A : CommAlgebra R ℓ') → isSet ⟨ A ⟩
-  isSetCommAlgebra A = is-set
-    where
-    open CommAlgebraStr (str A)
-
   module _
       {A : Type ℓ'} {0a 1a : A}
       {_+_ _·_ : A → A → A} { -_ : A → A} {_⋆_ : ⟨ R ⟩ → A → A}

Cubical/Algebra/CommAlgebra/FPAlgebra/Base.agda

@@ -169,8 +169,10 @@ module _ {R : CommRing ℓ} where
         universal =
           (inducedHom , inducedHomOnGenerators)
           , λ {(f , mapsValues)
-              → Σ≡Prop (λ _ → isPropΠ (λ _ → isSetCommAlgebra A _ _))
+              → Σ≡Prop (λ _ → isPropΠ (λ _ → is-set _ _))
                        (unique f mapsValues)}
+          where
+          open CommAlgebraStr (str A)
 
       {- ∀ A : Comm-R-Algebra,
          ∀ J : Finitely-generated-Ideal,
@@ -215,10 +217,12 @@ module _ {R : CommRing ℓ} where
       Iso.rightInv (FPHomIso {A}) =
         λ b → Σ≡Prop
                 (λ x → isPropΠ
-                  (λ i → isSetCommAlgebra A
+                  (λ i → is-set
                           (evPoly A (relation i) x)
                           (0a (snd A))))
                 (funExt (inducedHomOnGenerators A (fst b) (snd b)))
+        where
+        open CommAlgebraStr (str A)
       Iso.leftInv (FPHomIso {A}) =
         λ a → Σ≡Prop (λ f → isPropIsCommAlgebraHom {ℓ} {R} {ℓ} {ℓ} {FPAlgebra} {A} f)
                  λ i → fst (unique A

Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Properties.agda

@@ -200,7 +200,7 @@ module Theory {R : CommRing ℓ} {I : Type ℓ'} where
                (s ⋆ 1a) · (t ⋆ 1a) ∎
       in eq i
     inducedMap (C.0-trunc P Q p q i j) =
-      isSetAlgebra (CommAlgebra→Algebra A) (inducedMap P) (inducedMap Q) (cong _ p) (cong _ q) i j
+      is-set (inducedMap P) (inducedMap Q) (cong _ p) (cong _ q) i j
 
     module _ where
       open IsAlgebraHom

Cubical/Algebra/CommAlgebra/Instances/Initial.agda

@@ -35,7 +35,7 @@ module _ (R : CommRing ℓ) where
     initialCAlg .snd .CommAlgebraStr.-_ = _
     initialCAlg .snd .CommAlgebraStr._⋆_ r x = r · x
     initialCAlg .snd .CommAlgebraStr.isCommAlgebra =
-      makeIsCommAlgebra (isSetRing (CommRing→Ring R))
+      makeIsCommAlgebra is-set
                          +Assoc +IdR +InvR +Comm
                          ·Assoc ·IdL
                          ·DistL+ ·Comm

Cubical/Algebra/CommAlgebra/Instances/Pointwise.agda

@@ -17,7 +17,7 @@ module _ {R : CommRing ℓ} (X : Type ℓ'') (A : CommAlgebra R ℓ') where
   pointwiseAlgebra : CommAlgebra R _
   pointwiseAlgebra =
     let open CommAlgebraStr (snd A)
-        isSetX→A = isOfHLevelΠ 2 (λ (x : X) → isSetCommRing (CommAlgebra→CommRing A))
+        isSetX→A = isOfHLevelΠ 2 (λ (x : X) → is-set)
     in commAlgebraFromCommRing
          (pointwiseRing X (CommAlgebra→CommRing A))
          (λ r f → (λ x → r ⋆ (f x)))

Cubical/Algebra/CommAlgebra/LocalisationAlgebra.agda

@@ -223,7 +223,7 @@ module _
         -- The original function we get with the UP respects ⋆.
         original-pres⋆ : type-pres⋆ RLoc.S⁻¹RAsCommRing _⋆_ (original-univ .fst .fst)
         original-pres⋆ r = SQ.elimProp
-          (λ _ _ _ → isSetCommAlgebra B _ _ _ _)
+          (λ _ _ _ → is-set _ _ _ _)
           (λ (a , s , s∈S') → cong (_· _) (ψ .snd .IsAlgebraHom.pres⋆ r a)
                             ∙ ⋆AssocL _ _ _)
 
@@ -252,7 +252,7 @@ module _
                             (fst φ) ∘ RUniv._/1 ≡ (fst ψ))
                  → (χₐ , χₐcomm) ≡ el
         χₐunique (φ' , φ'comm) =
-          Σ≡Prop ((λ _ → isSetΠ (λ _ → isSetCommAlgebra B) _ _)) $ AlgebraHom≡ $
+          Σ≡Prop ((λ _ → isSetΠ (λ _ → is-set) _ _)) $ AlgebraHom≡ $
           cong (fst ∘ fst) -- Get underlying bare function.
                (univ .snd (CommAlgebraHom→RingHom {A = S⁻¹AAsCommAlgebra} {B = B}
                                                   φ' , φ'comm))

Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda

@@ -93,7 +93,9 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstr
   IsAlgebraHom.pres⋆ (snd quotientHom) _ _ = refl
 
 module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstract
-  open CommRingStr {{...}} hiding (_-_; -_; ·IdL; ·DistR+) renaming (_·_ to _·R_; _+_ to _+R_)
+  open CommRingStr {{...}}
+    hiding (_-_; -_; ·IdL; ·DistR+; is-set)
+    renaming (_·_ to _·R_; _+_ to _+R_)
   open CommAlgebraStr ⦃...⦄
 
   instance
@@ -102,66 +104,64 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) (I : IdealsIn A) where abstr
     _ : CommAlgebraStr R ⟨ A ⟩
     _ = snd A
 
-  private
-    LRing : Ring ℓ
-    LRing = CommAlgebra→Ring (A / I)
-    RRing : Ring ℓ
-    RRing = (CommAlgebra→Ring A) Ring./ (CommIdeal→Ideal I)
-
   -- sanity check / maybe a helper function some day
+  -- (These two rings are not definitionally equal, but only because of proofs, not data.)
   CommForget/ : RingEquiv (CommAlgebra→Ring (A / I)) ((CommAlgebra→Ring A) Ring./ (CommIdeal→Ideal I))
-  fst CommForget/ =
-    isoToEquiv
-      (iso
-        (rec (isSetRing LRing) (λ a → [ a ]) λ a b a-b∈I → eq/ a b a-b∈I)
-        (rec (isSetRing RRing) (λ a → [ a ]) (λ a b a-b∈I → eq/ a b a-b∈I))
-        (elimProp (λ _ → isSetRing LRing _ _) λ _ → refl)
-        (elimProp (λ _ → isSetRing RRing _ _) (λ _ → refl)))
+  fst CommForget/ = idEquiv _
   IsRingHom.pres0 (snd CommForget/) = refl
   IsRingHom.pres1 (snd CommForget/) = refl
-  IsRingHom.pres+ (snd CommForget/) = elimProp2 (λ _ _ → isSetRing RRing _ _) (λ _ _ → refl)
-  IsRingHom.pres· (snd CommForget/) = elimProp2 (λ _ _ → isSetRing RRing _ _) (λ _ _ → refl)
-  IsRingHom.pres- (snd CommForget/) = elimProp (λ _ → isSetRing RRing _ _) (λ _ → refl)
-
-  open IsAlgebraHom
-  inducedHom : (B : CommAlgebra R ℓ) (ϕ : CommAlgebraHom A B)
-               → (fst I) ⊆ (fst (kernel A B ϕ))
-               → CommAlgebraHom (A / I) B
-  fst (inducedHom B ϕ I⊆kernel) =
-    let open RingTheory (CommRing→Ring (CommAlgebra→CommRing B))
-        instance
-          _ : CommAlgebraStr R _
-          _ = snd B
-          _ : CommRingStr _
-          _ = snd (CommAlgebra→CommRing B)
-    in rec (isSetCommAlgebra B) (λ x → fst ϕ x)
+  IsRingHom.pres+ (snd CommForget/) = λ _ _ → refl
+  IsRingHom.pres· (snd CommForget/) = λ _ _ → refl
+  IsRingHom.pres- (snd CommForget/) = λ _ → refl
+
+  module _
+    (B : CommAlgebra R ℓ)
+    (ϕ : CommAlgebraHom A B)
+    (I⊆kernel : (fst I) ⊆ (fst (kernel A B ϕ)))
+    where abstract
+
+    open IsAlgebraHom
+    open RingTheory (CommRing→Ring (CommAlgebra→CommRing B))
+
+    private
+      instance
+        _ : CommAlgebraStr R ⟨ B ⟩
+        _ = snd B
+        _ : CommRingStr ⟨ B ⟩
+        _ = snd (CommAlgebra→CommRing B)
+
+    inducedHom : CommAlgebraHom (A / I) B
+    fst inducedHom =
+      rec is-set (λ x → fst ϕ x)
         λ a b a-b∈I →
           equalByDifference
             (fst ϕ a) (fst ϕ b)
             ((fst ϕ a) - (fst ϕ b)     ≡⟨ cong (λ u → (fst ϕ a) + u) (sym (IsAlgebraHom.pres- (snd ϕ) _)) ⟩
              (fst ϕ a) + (fst ϕ (- b)) ≡⟨ sym (IsAlgebraHom.pres+ (snd ϕ) _ _) ⟩
              fst ϕ (a - b)             ≡⟨ I⊆kernel (a - b) a-b∈I ⟩
              0r ∎)
-  pres0 (snd (inducedHom B ϕ kernel⊆I)) = pres0 (snd ϕ)
-  pres1 (snd (inducedHom B ϕ kernel⊆I)) = pres1 (snd ϕ)
-  pres+ (snd (inducedHom B ϕ kernel⊆I)) = elimProp2 (λ _ _ → isSetCommAlgebra B _ _) (pres+ (snd ϕ))
-  pres· (snd (inducedHom B ϕ kernel⊆I)) = elimProp2 (λ _ _ → isSetCommAlgebra B _ _) (pres· (snd ϕ))
-  pres- (snd (inducedHom B ϕ kernel⊆I)) = elimProp (λ _ → isSetCommAlgebra B _ _) (pres- (snd ϕ))
-  pres⋆ (snd (inducedHom B ϕ kernel⊆I)) = λ r → elimProp (λ _ → isSetCommAlgebra B _ _) (pres⋆ (snd ϕ) r)
-
-  inducedHom∘quotientHom : (B : CommAlgebra R ℓ) (ϕ : CommAlgebraHom A B)
-               → (I⊆kerϕ : fst I ⊆ fst (kernel A B ϕ))
-               → inducedHom B ϕ I⊆kerϕ ∘a quotientHom A I ≡ ϕ
-  inducedHom∘quotientHom B ϕ I⊆kerϕ = Σ≡Prop (isPropIsCommAlgebraHom {M = A} {N = B}) (funExt (λ a → refl))
+    pres0 (snd inducedHom) = pres0 (snd ϕ)
+    pres1 (snd inducedHom) = pres1 (snd ϕ)
+    pres+ (snd inducedHom) = elimProp2 (λ _ _ → is-set _ _) (pres+ (snd ϕ))
+    pres· (snd inducedHom) = elimProp2 (λ _ _ → is-set _ _) (pres· (snd ϕ))
+    pres- (snd inducedHom) = elimProp (λ _ → is-set _ _) (pres- (snd ϕ))
+    pres⋆ (snd inducedHom) = λ r → elimProp (λ _ → is-set _ _) (pres⋆ (snd ϕ) r)
+
+    inducedHom∘quotientHom : inducedHom ∘a quotientHom A I ≡ ϕ
+    inducedHom∘quotientHom = Σ≡Prop (isPropIsCommAlgebraHom {M = A} {N = B}) (funExt (λ a → refl))
 
   injectivePrecomp : (B : CommAlgebra R ℓ) (f g : CommAlgebraHom (A / I) B)
                      → f ∘a (quotientHom A I) ≡ g ∘a (quotientHom A I)
                      → f ≡ g
   injectivePrecomp B f g p =
     Σ≡Prop
-      (λ h → isPropIsAlgebraHom (CommRing→Ring R) (snd (CommAlgebra→Algebra (A / I))) h (snd (CommAlgebra→Algebra B)))
-      (descendMapPath (fst f) (fst g) (isSetCommAlgebra B)
+      (λ h → isPropIsCommAlgebraHom {M = A / I} {N = B} h)
+      (descendMapPath (fst f) (fst g) is-set
                       λ x → λ i → fst (p i) x)
+    where
+    instance
+      _ : CommAlgebraStr R ⟨ B ⟩
+      _ = str B
 
 
 {- trivial quotient -}
@@ -181,7 +181,7 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where abstract
   fst zeroIdealQuotient =
     let open RingTheory (CommRing→Ring (CommAlgebra→CommRing A))
     in isoToEquiv (iso (fst (quotientHom A (0Ideal A)))
-                    (rec (isSetCommAlgebra A) (λ x → x) λ x y x-y≡0 → equalByDifference x y x-y≡0)
+                    (rec is-set (λ x → x) λ x y x-y≡0 → equalByDifference x y x-y≡0)
                     (elimProp (λ _ → squash/ _ _) λ _ → refl)
                     λ _ → refl)
   snd zeroIdealQuotient = snd (quotientHom A (0Ideal A))

Cubical/Algebra/CommAlgebra/UnivariatePolyList.agda

@@ -226,7 +226,7 @@ module _ (R : CommRing ℓ) where
     fst (fst (equiv-proof (snd indcuedHomEquivalence) x)) = inducedHom x
     snd (fst (equiv-proof (snd indcuedHomEquivalence) x)) = inducedMapGenerator x
     snd (equiv-proof (snd indcuedHomEquivalence) x) (g , gX≡x) =
-      Σ≡Prop (λ _ → isSetAlgebra A _ _) (sym (inducedHomUnique x g gX≡x))
+      Σ≡Prop (λ _ → is-set _ _) (sym (inducedHomUnique x g gX≡x))
 
     equalByUMP : (f g : AlgebraHom (CommAlgebra→Algebra ListPolyCommAlgebra) A)
                  → fst f X ≡ fst g X

Cubical/Algebra/CommMonoid/Base.agda

@@ -81,11 +81,6 @@ CommMonoidStr→MonoidStr (commmonoidstr _ _ H) = monoidstr _ _ (IsCommMonoid.is
 CommMonoid→Monoid : CommMonoid ℓ → Monoid ℓ
 CommMonoid→Monoid (_ , commmonoidstr  _ _ M) = _ , monoidstr _ _ (IsCommMonoid.isMonoid M)
 
-isSetCommMonoid : (M : CommMonoid ℓ) → isSet ⟨ M ⟩
-isSetCommMonoid M = is-set
-  where
-  open CommMonoidStr (str M)
-
 CommMonoidHom : (L : CommMonoid ℓ) (M : CommMonoid ℓ') → Type (ℓ-max ℓ ℓ')
 CommMonoidHom L M = MonoidHom (CommMonoid→Monoid L) (CommMonoid→Monoid M)
 

Cubical/Algebra/CommMonoid/GrothendieckGroup.agda

@@ -155,7 +155,7 @@ The "groupification" of a monoid comes with a universal morphism and a universal
       f = fst φ
 
     inducedHom : AbGroupHom (Groupification M) A
-    fst inducedHom = elim (λ x → isSetAbGroup A) g proof
+    fst inducedHom = elim (λ x → is-set) g proof
         where
         g = λ (a , b) → f a - f b
         proof : (u v : ⟨ M² M ⟩) (r : R M u v) → g u ≡ g v
@@ -187,7 +187,7 @@ The "groupification" of a monoid comes with a universal morphism and a universal
               f c - f d
                 ∎
 
-    pres· (snd inducedHom) = elimProp2 (λ _ _ → isSetAbGroup A _ _) proof
+    pres· (snd inducedHom) = elimProp2 (λ _ _ → is-set _ _) proof
       where
         rExp : ∀ {x y z} → x ≡ y → x + z ≡ y + z
         rExp r = cong₂ _+_ r refl
@@ -205,7 +205,7 @@ The "groupification" of a monoid comes with a universal morphism and a universal
             lemma = rExp (sym (·Assoc _ _ _) ∙ lExp (·Comm _ _) ∙ ·Assoc _ _ _) ∙ sym (·Assoc _ _ _)
 
     pres1 (snd inducedHom)   = +InvR _
-    presinv (snd inducedHom) = elimProp (λ _ → isSetAbGroup A _ _)
+    presinv (snd inducedHom) = elimProp (λ _ → is-set _ _)
                                         (λ _ → sym (invDistr _ _ ∙ cong₂ _-_ (invInv _) refl))
 
     solution : (m : ⟨ M ⟩) → (fst inducedHom) (i m) ≡ f m

Cubical/Algebra/CommRing/Base.agda

@@ -155,11 +155,6 @@ CommRingPath = ∫ 𝒮ᴰ-CommRing .UARel.ua
 uaCommRing : {A B : CommRing ℓ} → CommRingEquiv A B → A ≡ B
 uaCommRing {A = A} {B = B} = equivFun (CommRingPath A B)
 
-isSetCommRing : ((R , str) : CommRing ℓ) → isSet R
-isSetCommRing R = is-set
-  where
-  open CommRingStr (str R)
-
 CommRingIso : (R : CommRing ℓ) (S : CommRing ℓ') → Type (ℓ-max ℓ ℓ')
 CommRingIso R S = Σ[ e ∈ Iso (R .fst) (S .fst) ]
                      IsRingHom (CommRingStr→RingStr (R .snd)) (e .fun) (CommRingStr→RingStr (S .snd))

Cubical/Algebra/CommRing/Instances/Pointwise.agda

@@ -15,7 +15,7 @@ pointwiseRing X R = (X → fst R) , str
     where
       open CommRingStr (snd R)
 
-      isSetX→R = isOfHLevelΠ 2 (λ _ → isSetCommRing R)
+      isSetX→R = isOfHLevelΠ 2 (λ _ → is-set)
 
       str : CommRingStr (X → fst R)
       CommRingStr.0r str = λ _ → 0r

Cubical/Algebra/CommRing/Quotient/Base.agda

@@ -50,12 +50,12 @@ module Quotient-FGideal-CommRing-Ring
   (gnull : (k : Fin n) → g $r v k ≡ RingStr.0r (snd B))
   where
 
-  open RingStr (snd B) using (0r)
+  open RingStr (snd B) using (0r; is-set)
 
   zeroOnGeneratedIdeal : (x : ⟨ A ⟩) → x ∈ fst (generatedIdeal A v) → g $r x ≡ 0r
   zeroOnGeneratedIdeal x x∈FGIdeal =
     PT.elim
-      (λ _ → isSetRing B (g $r x) 0r)
+      (λ _ → is-set (g $r x) 0r)
       (λ {(α , isLC) → subst _ (sym isLC) (cancelLinearCombination A B g _ α v gnull)})
       x∈FGIdeal
 

Cubical/Algebra/CommRing/Quotient/IdealSum.agda

@@ -105,7 +105,7 @@ module Construction {R : CommRing ℓ} (I J : IdealsIn R) where
 
   kernel-0 : (x : ⟨ R / (I +i J) ⟩) → fst ψ x ≡ 0r → x ≡ 0r
   kernel-0 x ψx≡0 =
-    PT.rec (isSetCommRing (R / (I +i J)) x 0r)
+    PT.rec (is-set x 0r)
            (λ (x' , π+x'≡x) →
              let πx'≡0 : fst π x' ≡ 0r
                  πx'≡0 = fst π x'          ≡⟨⟩
@@ -142,7 +142,7 @@ module Construction {R : CommRing ℓ} (I J : IdealsIn R) where
   embedding : isEmbedding {A = ⟨ R / (I +i J) ⟩} {B = ⟨ (R / I) / π₁J ⟩} (fst ϕ)
   embedding =
     injEmbedding
-          (isSetCommRing ((R / I) / π₁J))
+          is-set
           ϕ-injective