fix localization, adapt univalence, rearrange base

agda · Aug 9, 2024 · 6e8be4b · 6e8be4b
1 parent 0a43a6a
commit 6e8be4b
Show file tree

Hide file tree

Showing 4 changed files with 178 additions and 121 deletions.
diff --git a/Cubical/Algebra/CommAlgebra/Base.agda b/Cubical/Algebra/CommAlgebra/Base.agda
@@ -33,12 +33,70 @@ module _ {R : CommRing ℓ} where
   ⟨_⟩ₐ : (A : CommAlgebra R ℓ') → Type ℓ'
   ⟨ A ⟩ₐ = A .fst .fst
 
+  {-
+    Contrary to most algebraic structures, this one only contains
+    law and structure of a CommAlgebra, which it is *in addition*
+    to its CommRing structure.
+  -}
+  record CommAlgebraStr (A : Type ℓ') : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
+    open CommRingStr {{...}}
+    instance
+      _ : CommRingStr (R .fst)
+      _ = (R .snd)
+
+    field
+      crStr : CommRingStr A
+      _⋆_ : ⟨ R ⟩ → A → A
+      ⋆Assoc : (r s : ⟨ R ⟩) (x : A) → (r · s) ⋆ x ≡ r ⋆ (s ⋆ x)
+      ⋆DistR+ : (r : ⟨ R ⟩) (x y : A) → r ⋆ (CommRingStr._+_ crStr x y) ≡ CommRingStr._+_ crStr(r ⋆ x) (r ⋆ y)
+      ⋆DistL+ : (r s : ⟨ R ⟩) (x : A) → (r + s) ⋆ x ≡ CommRingStr._+_ crStr (r ⋆ x) (s ⋆ x)
+      ⋆IdL    : (x : A) → 1r ⋆ x ≡ x
+      ⋆AssocL : (r : ⟨ R ⟩) (x y : A) → CommRingStr._·_ crStr (r ⋆ x) y ≡ r ⋆ (CommRingStr._·_ crStr x y)
+    infixl 7 _⋆_
+
+  {- TODO: make laws opaque -}
+  CommAlgebra→CommAlgebraStr : (A : CommAlgebra R ℓ') → CommAlgebraStr ⟨ A ⟩ₐ
+  CommAlgebra→CommAlgebraStr A =
+    let open CommRingStr ⦃...⦄
+        instance
+          _ : CommRingStr (R .fst)
+          _ = R .snd
+          _ = A .fst .snd
+    in record
+       { crStr = A .fst .snd
+       ; _⋆_ = λ r x → (A .snd .fst r) · x
+       ; ⋆Assoc = λ r s x → cong (_· x) (IsCommRingHom.pres· (A .snd .snd) r s) ∙ sym (·Assoc _ _ _)
+       ; ⋆DistR+ = λ r x y → ·DistR+ _ _ _
+       ; ⋆DistL+ = λ r s x → cong (_· x) (IsCommRingHom.pres+ (A .snd .snd) r s) ∙ ·DistL+ _ _ _
+       ; ⋆IdL = λ x → cong (_· x) (IsCommRingHom.pres1 (A .snd .snd)) ∙ ·IdL x
+       ; ⋆AssocL = λ r x y → sym (·Assoc (A .snd .fst r) x y)
+       }
+
+
+{-
+   Homomorphisms of CommAlgebras
+   -----------------------------
+   This is defined as a record instead of a Σ-type to make type inference work
+   better.
+-}
   record IsCommAlgebraHom (A : CommAlgebra R ℓ') (B : CommAlgebra R ℓ'') (f : ⟨ A ⟩ₐ → ⟨ B ⟩ₐ) : Type (ℓ-max ℓ (ℓ-max ℓ' ℓ'')) where
     no-eta-equality
     field
       isCommRingHom : IsCommRingHom (A .fst .snd) f (B .fst .snd)
       commutes : (f , isCommRingHom) ∘cr snd A ≡ snd B
 
+    open IsCommRingHom isCommRingHom public
+    open CommRingStr ⦃...⦄
+    open CommAlgebraStr ⦃...⦄
+    private instance
+      _ = CommAlgebra→CommAlgebraStr A
+      _ = CommAlgebra→CommAlgebraStr B
+      _ = B .fst .snd
+    pres⋆ : (r : ⟨ R ⟩) (x : ⟨ A ⟩ₐ) → f (r ⋆ x) ≡ r ⋆ f x
+    pres⋆ r x = f (r ⋆ x)                    ≡⟨ pres· (A .snd .fst r) x ⟩
+                (f (A .snd .fst r)) · (f x)  ≡⟨ cong (_· (f x)) (cong (λ g → g .fst r) commutes) ⟩
+                r ⋆ f x ∎
+
   unquoteDecl IsCommAlgebraHomIsoΣ = declareRecordIsoΣ IsCommAlgebraHomIsoΣ (quote IsCommAlgebraHom)
 
   isPropIsCommAlgebraHom : (A : CommAlgebra R ℓ') (B : CommAlgebra R ℓ'') (f : ⟨ A ⟩ₐ → ⟨ B ⟩ₐ)
@@ -112,83 +170,32 @@ module _ {R : CommRing ℓ} where
     CommAlgebraHom≡ {B = B} p = Σ≡Prop (λ _ → isPropIsCommAlgebraHom _ _ _) p
       where open CommRingStr (B .fst .snd) using (is-set)
 
+
+{- Equivalences of CommAlgebras -}
   CommAlgebraEquiv : (A : CommAlgebra R ℓ') (B : CommAlgebra R ℓ'') → Type _
-  CommAlgebraEquiv A B = Σ[ f ∈ CommRingEquiv (A .fst) (B .fst) ] (f .fst .fst , f .snd)  ∘cr A .snd ≡ B .snd
+  CommAlgebraEquiv A B = Σ[ f ∈ (⟨ A ⟩ₐ ≃ ⟨ B ⟩ₐ) ] IsCommAlgebraHom A B (f .fst)
 
   idCAlgEquiv : (A : CommAlgebra R ℓ') → CommAlgebraEquiv A A
-  idCAlgEquiv A = (idCommRingEquiv (fst A)) ,
-                   CommRingHom≡ refl
+  idCAlgEquiv A = (idEquiv ⟨ A ⟩ₐ) , isHom
+    where
+      opaque
+        isHom : IsCommAlgebraHom A A (idfun ⟨ A ⟩ₐ)
+        isHom = record { isCommRingHom = idCommRingHom (A .fst) .snd ;
+                         commutes = CommRingHom≡ refl }
 
   CommAlgebraEquiv≡ :
       {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''} {f g : CommAlgebraEquiv A B}
-      → f .fst .fst .fst ≡ g .fst .fst .fst
+      → f .fst .fst ≡ g .fst .fst
       → f ≡ g
   CommAlgebraEquiv≡ {B = B} p =
-    Σ≡Prop (λ _ → isSetΣSndProp (isSetΠ (λ _ → isSetB)) (λ _ → isPropIsCommRingHom _ _ _) _ _)
-           (CommRingEquiv≡ p)
-    where open CommRingStr (B .fst .snd) using () renaming (is-set to isSetB)
+    Σ≡Prop (isPropIsCommAlgebraHom _ _ ∘ fst) (Σ≡Prop isPropIsEquiv p)
 
   isSetCommAlgebraEquiv : (A : CommAlgebra R ℓ') (B : CommAlgebra R ℓ'')
                           → isSet (CommAlgebraEquiv A B)
   isSetCommAlgebraEquiv A B =
-    isSetΣSndProp
-      (isSetCommRingEquiv _ _)
-      (λ e → isSetΣSndProp (isSet→ isSetB) (λ _ → isPropIsCommRingHom _ _ _) _ _)
-    where open CommRingStr (B .fst .snd) using () renaming (is-set to isSetB)
-
-  {-
-    Contrary to most algebraic structures, this one only contains
-    law and structure of a CommAlgebra, which it is *in addition*
-    to its CommRing structure.
-  -}
-  record CommAlgebraStr (A : Type ℓ') : Type (ℓ-suc (ℓ-max ℓ ℓ')) where
-    open CommRingStr {{...}}
-    instance
-      _ : CommRingStr (R .fst)
-      _ = (R .snd)
-
-    field
-      crStr : CommRingStr A
-      _⋆_ : ⟨ R ⟩ → A → A
-      ⋆Assoc : (r s : ⟨ R ⟩) (x : A) → (r · s) ⋆ x ≡ r ⋆ (s ⋆ x)
-      ⋆DistR+ : (r : ⟨ R ⟩) (x y : A) → r ⋆ (CommRingStr._+_ crStr x y) ≡ CommRingStr._+_ crStr(r ⋆ x) (r ⋆ y)
-      ⋆DistL+ : (r s : ⟨ R ⟩) (x : A) → (r + s) ⋆ x ≡ CommRingStr._+_ crStr (r ⋆ x) (s ⋆ x)
-      ⋆IdL    : (x : A) → 1r ⋆ x ≡ x
-      ⋆AssocL : (r : ⟨ R ⟩) (x y : A) → CommRingStr._·_ crStr (r ⋆ x) y ≡ r ⋆ (CommRingStr._·_ crStr x y)
-    infixl 7 _⋆_
-
-  {- TODO: make laws opaque -}
-  CommAlgebra→CommAlgebraStr : (A : CommAlgebra R ℓ') → CommAlgebraStr ⟨ A ⟩ₐ
-  CommAlgebra→CommAlgebraStr A =
-    let open CommRingStr ⦃...⦄
-        instance
-          _ : CommRingStr (R .fst)
-          _ = R .snd
-          _ = A .fst .snd
-    in record
-       { crStr = A .fst .snd
-       ; _⋆_ = λ r x → (A .snd .fst r) · x
-       ; ⋆Assoc = λ r s x → cong (_· x) (IsCommRingHom.pres· (A .snd .snd) r s) ∙ sym (·Assoc _ _ _)
-       ; ⋆DistR+ = λ r x y → ·DistR+ _ _ _
-       ; ⋆DistL+ = λ r s x → cong (_· x) (IsCommRingHom.pres+ (A .snd .snd) r s) ∙ ·DistL+ _ _ _
-       ; ⋆IdL = λ x → cong (_· x) (IsCommRingHom.pres1 (A .snd .snd)) ∙ ·IdL x
-       ; ⋆AssocL = λ r x y → sym (·Assoc (A .snd .fst r) x y)
-       }
-
-  module CommAlgebraHom {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''} (f : CommAlgebraHom A B) where
-    open IsCommRingHom (IsCommAlgebraHom.isCommRingHom (f .snd))
-    open CommRingStr ⦃...⦄
-    open CommAlgebraStr ⦃...⦄
-    private instance
-      _ = CommAlgebra→CommAlgebraStr A
-      _ = CommAlgebra→CommAlgebraStr B
-      _ = B .fst .snd
-
-    opaque
-      pres⋆ : (r : ⟨ R ⟩) (x : ⟨ A ⟩ₐ) → f $ca (r ⋆ x) ≡ r ⋆ f $ca x
-      pres⋆ r x = f $ca (r ⋆ x)                        ≡⟨ pres· (A .snd .fst r) x ⟩
-                  (f $ca (A .snd .fst r)) · (f $ca x)  ≡⟨ cong (_· (f $ca x)) (cong (λ g → g .fst r) (CommAlgebraHom→Triangle f)) ⟩
-                  r ⋆ f $ca x ∎
+     isSetΣSndProp (isSetΣSndProp (isSet→ isSetB) isPropIsEquiv)
+                   (isPropIsCommAlgebraHom _ _ ∘ fst)
+     where open CommRingStr (B .fst .snd) using () renaming (is-set to isSetB)
 
   CommAlgebraHomFromCommRingHom :
     {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''}
@@ -211,6 +218,7 @@ module _ {R : CommRing ℓ} where
               r ⋆ 1r                        ≡⟨ ·IdR _ ⟩
               B .snd .fst r ∎))
 
+
 {- Convenient forgetful functions -}
 module _ {R : CommRing ℓ} where
   CommAlgebra→Ring : (A : CommAlgebra R ℓ') → Ring ℓ'
@@ -222,13 +230,12 @@ module _ {R : CommRing ℓ} where
                              → RingHom (CommAlgebra→Ring A) (CommAlgebra→Ring B)
   CommAlgebraHom→RingHom = CommRingHom→RingHom ∘ CommAlgebraHom→CommRingHom
 
-  CommAlgebraEquiv→CommRingHom : {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''}
-                             → CommAlgebraEquiv A B
-                             → CommRingHom (CommAlgebra→CommRing A) (CommAlgebra→CommRing B)
-  CommAlgebraEquiv→CommRingHom e = CommRingEquiv→CommRingHom (e .fst)
-
   CommAlgebraEquiv→CommAlgebraHom : {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''}
                              → CommAlgebraEquiv A B
                              → CommAlgebraHom A B
-  CommAlgebraEquiv→CommAlgebraHom f =
-    CommRingHom→CommAlgebraHom (CommRingEquiv→CommRingHom (f .fst)) $ CommRingHom≡ (cong (fst) (f .snd))
+  CommAlgebraEquiv→CommAlgebraHom f = (f .fst .fst , f .snd)
+
+  CommAlgebraEquiv→CommRingHom : {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''}
+                             → CommAlgebraEquiv A B
+                             → CommRingHom (CommAlgebra→CommRing A) (CommAlgebra→CommRing B)
+  CommAlgebraEquiv→CommRingHom = CommAlgebraHom→CommRingHom ∘ CommAlgebraEquiv→CommAlgebraHom
diff --git a/Cubical/Algebra/CommAlgebra/Localisation.agda b/Cubical/Algebra/CommAlgebra/Localisation.agda
@@ -109,17 +109,17 @@ module AlgLoc (R : CommRing ℓ)
   χᴬuniqueness : (ψ : CommAlgebraHom S⁻¹RAsCommAlg B) → χᴬ ≡ ψ
   χᴬuniqueness ψ =
     CommAlgebraHom≡ {f = χᴬ}
-      (χᴬ .fst .fst ≡⟨ cong (fst ∘ fst) (χuniqueness (ψ .fst , funExt ψ'r/1≡φr)) ⟩ ψ .fst .fst ∎)
+      (χᴬ  .fst ≡⟨ cong (fst ∘ fst) (χuniqueness (CommAlgebraHom→CommRingHom ψ , funExt ψ'r/1≡φr)) ⟩ ψ .fst ∎)
 
    where
    χuniqueness = S⁻¹RHasUniversalProp (B .fst) φ  S⋆1⊆Bˣ .snd
 
-   ψ'r/1≡φr : ∀ r → ψ .fst .fst (r /1) ≡ fst φ r
+   ψ'r/1≡φr : ∀ r → ψ .fst (r /1) ≡ fst φ r
    ψ'r/1≡φr r =
-    ψ .fst .fst (r /1)    ≡⟨ cong (ψ .fst .fst) (sym (·ₗ-rid _)) ⟩
-    ψ .fst .fst (r ⋆ 1r)  ≡⟨ IsCommAlgebraHom.pres⋆ ψ _ _ ⟩
-    r ⋆ (ψ .fst .fst 1r)  ≡⟨ cong (λ u → r ⋆ u) (pres1 (ψ .fst .snd))  ⟩
-    r ⋆ 1r                ≡⟨ solve! (B .fst) ⟩
+    ψ .fst (r /1)    ≡⟨ cong (ψ .fst) (sym (·ₗ-rid _)) ⟩
+    ψ .fst (r ⋆ 1r)  ≡⟨ IsCommAlgebraHom.pres⋆ (ψ .snd) _ _ ⟩
+    r ⋆ (ψ .fst 1r)  ≡⟨ cong (λ u → r ⋆ u) (IsCommAlgebraHom.pres1 (ψ .snd))  ⟩
+    r ⋆ 1r           ≡⟨ solve! (B .fst) ⟩
     fst φ r ∎
 
 
@@ -130,9 +130,11 @@ module AlgLoc (R : CommRing ℓ)
  S⁻¹RAlgCharEquiv : (A : CommRing ℓ) (φ : CommRingHom R A)
                   → PathToS⁻¹R  R S SMultClosedSubset A φ
                   → CommAlgebraEquiv S⁻¹RAsCommAlg (A , φ)
- S⁻¹RAlgCharEquiv A φ cond .fst = S⁻¹RCharEquiv R S SMultClosedSubset A φ cond
- S⁻¹RAlgCharEquiv A φ cond .snd = CommRingHom≡ (S⁻¹RHasUniversalProp A φ (cond .φS⊆Aˣ) .fst .snd)
-  where open PathToS⁻¹R
+ S⁻¹RAlgCharEquiv A φ cond =
+   CommRingEquiv→CommAlgebraEquiv
+     (S⁻¹RCharEquiv R S SMultClosedSubset A φ cond)
+     (S⁻¹RHasUniversalProp A φ (cond .φS⊆Aˣ) .fst .snd)
+    where open PathToS⁻¹R
 
 -- the special case of localizing at a single element
 R[1/_]AsCommAlgebra : {R : CommRing ℓ} → fst R → CommAlgebra R ℓ
@@ -184,8 +186,8 @@ module AlgLocTwoSubsets (R' : CommRing ℓ)
                     → (∀ s₂ → s₂ ∈ S₂ → s₂ ⋆ 1r ∈ S₁⁻¹Rˣ)
                     → isContr (S₁⁻¹RAsCommAlg ≡ S₂⁻¹RAsCommAlg)
  isContrS₁⁻¹R≡S₂⁻¹R S₁⊆S₂⁻¹Rˣ S₂⊆S₁⁻¹Rˣ = isOfHLevelRetractFromIso 0
-                                            (equivToIso (invEquiv (CommAlgebraPath _ _ _)))
-                                              isContrS₁⁻¹R≅S₂⁻¹R
+                                            (equivToIso (invEquiv (CommAlgebraPath _ _)))
+                                             isContrS₁⁻¹R≅S₂⁻¹R
   where
   χ₁ : CommAlgebraHom S₁⁻¹RAsCommAlg S₂⁻¹RAsCommAlg
   χ₁ = S₁⁻¹RHasAlgUniversalProp S₂⁻¹RAsCommAlg S₁⊆S₂⁻¹Rˣ .fst
@@ -206,12 +208,14 @@ module AlgLocTwoSubsets (R' : CommRing ℓ)
   Iso.leftInv IsoS₁⁻¹RS₂⁻¹R = funExt⁻ (cong ⟨_⟩ₐ→ χ₂∘χ₁≡id)
 
   isContrS₁⁻¹R≅S₂⁻¹R : isContr (CommAlgebraEquiv S₁⁻¹RAsCommAlg S₂⁻¹RAsCommAlg)
-  isContrS₁⁻¹R≅S₂⁻¹R = withOpaqueStr $ center , uniqueness
+  isContrS₁⁻¹R≅S₂⁻¹R = center , uniqueness
    where
-   X₁asCRHom = fst χ₁
+   X₁asCRHom = CommAlgebraHom→CommRingHom χ₁
    center : CommAlgebraEquiv S₁⁻¹RAsCommAlg S₂⁻¹RAsCommAlg
-   fst center = withOpaqueStr $ (isoToEquiv IsoS₁⁻¹RS₂⁻¹R) , snd X₁asCRHom
-   snd center = makeOpaque $ CommRingHom≡ (cong fst (χ₁ .snd))
+   center =
+     CommRingEquiv→CommAlgebraEquiv
+       ((isoToEquiv IsoS₁⁻¹RS₂⁻¹R) , snd X₁asCRHom)
+       (cong fst (CommAlgebraHom→Triangle χ₁))
 
    uniqueness : (φ : CommAlgebraEquiv S₁⁻¹RAsCommAlg S₂⁻¹RAsCommAlg) → center ≡ φ
    uniqueness φ =

diff --git a/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda b/Cubical/Algebra/CommAlgebra/QuotientAlgebra.agda
@@ -124,7 +124,10 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
   open CommRingStr (A .fst .snd)
 
   oneIdealQuotient : CommAlgebraEquiv (A / (1Ideal R A)) (UnitCommAlgebra R {ℓ' = ℓ})
-  oneIdealQuotient .fst .fst =
+  oneIdealQuotient = ?
+
+{-
+.fst .fst =
     withOpaqueStr $
     isoToEquiv (iso ⟨ terminalMap R (A / 1Ideal R A) ⟩ₐ→
                       (λ _ → [ 0r ])
@@ -133,8 +136,6 @@ module _ {R : CommRing ℓ} (A : CommAlgebra R ℓ) where
   oneIdealQuotient .fst .snd = terminalMap R (A / 1Ideal R A) .fst .snd
   oneIdealQuotient .snd = terminalMap R (A / (1Ideal R A)) .snd
 
-{-
-
   zeroIdealQuotient : CommAlgebraEquiv A (A / (0Ideal R A))
   zeroIdealQuotient .fst .fst =
     withOpaqueStr $

diff --git a/Cubical/Algebra/CommAlgebra/Univalence.agda b/Cubical/Algebra/CommAlgebra/Univalence.agda
@@ -22,34 +22,79 @@ private
     ℓ ℓ' ℓ'' : Level
 
 
-CommAlgebraPath :
-  (R : CommRing ℓ)
-  (A B : CommAlgebra R ℓ')
-  → (Σ[ f ∈ CommRingEquiv (A .fst) (B .fst) ] (f .fst .fst , f .snd)  ∘cr A .snd ≡ B .snd)
-  ≃ (A ≡ B)
-CommAlgebraPath R A B =
-  (Σ-cong-equiv
-    (CommRingPath _ _)
-    (λ e → compPathlEquiv (computeSubst e)))
-  ∙ₑ ΣPathTransport≃PathΣ A B
-  where computeSubst :
-          (e : CommRingEquiv (fst A) (fst B))
-          → subst (CommRingHom R) (uaCommRing e) (A .snd)
-            ≡ (CommRingEquiv→CommRingHom e) ∘cr A .snd
-        computeSubst e =
-          CommRingHom≡ $
-            (subst (CommRingHom R) (uaCommRing e) (A .snd)) .fst
-              ≡⟨ sym (substCommSlice (CommRingHom R) (λ X → ⟨ R ⟩ → ⟨ X ⟩) (λ _ → fst) (uaCommRing e) (A .snd)) ⟩
-            subst (λ X → ⟨ R ⟩ → ⟨ X ⟩) (uaCommRing e) (A .snd .fst)
-              ≡⟨ fromPathP (funTypeTransp (λ _ → ⟨ R ⟩) ⟨_⟩ (uaCommRing e) (A .snd .fst)) ⟩
-            subst ⟨_⟩ (uaCommRing e) ∘ A .snd .fst ∘ subst (λ _ → ⟨ R ⟩) (sym (uaCommRing e))
-              ≡⟨ cong ((subst ⟨_⟩ (uaCommRing e) ∘ A .snd .fst) ∘_) (funExt (λ _ → transportRefl _)) ⟩
-            (subst ⟨_⟩ (uaCommRing e) ∘ (A .snd .fst))
-              ≡⟨ funExt (λ _ → uaβ (e .fst) _) ⟩
-            (CommRingEquiv→CommRingHom e ∘cr A .snd) .fst  ∎
-
-uaCommAlgebra : {R : CommRing ℓ} {A B : CommAlgebra R ℓ'} → CommAlgebraEquiv A B → A ≡ B
-uaCommAlgebra {R = R} {A = A} {B = B} = equivFun (CommAlgebraPath R A B)
-
-isGroupoidCommAlgebra : {R : CommRing ℓ} → isGroupoid (CommAlgebra R ℓ')
-isGroupoidCommAlgebra A B = isOfHLevelRespectEquiv 2 (CommAlgebraPath _ _ _) (isSetCommAlgebraEquiv _ _)
+module _ {R : CommRing ℓ} where
+
+  CommAlgebraPath' :
+    (A B : CommAlgebra R ℓ')
+    → (Σ[ f ∈ CommRingEquiv (A .fst) (B .fst) ] (f .fst .fst , f .snd)  ∘cr A .snd ≡ B .snd)
+    ≃ (A ≡ B)
+  CommAlgebraPath' A B =
+    (Σ-cong-equiv
+      (CommRingPath _ _)
+      (λ e → compPathlEquiv (computeSubst e)))
+    ∙ₑ ΣPathTransport≃PathΣ A B
+    where computeSubst :
+            (e : CommRingEquiv (fst A) (fst B))
+            → subst (CommRingHom R) (uaCommRing e) (A .snd)
+              ≡ (CommRingEquiv→CommRingHom e) ∘cr A .snd
+          computeSubst e =
+            CommRingHom≡ $
+              (subst (CommRingHom R) (uaCommRing e) (A .snd)) .fst
+                ≡⟨ sym (substCommSlice (CommRingHom R) (λ X → ⟨ R ⟩ → ⟨ X ⟩) (λ _ → fst) (uaCommRing e) (A .snd)) ⟩
+              subst (λ X → ⟨ R ⟩ → ⟨ X ⟩) (uaCommRing e) (A .snd .fst)
+                ≡⟨ fromPathP (funTypeTransp (λ _ → ⟨ R ⟩) ⟨_⟩ (uaCommRing e) (A .snd .fst)) ⟩
+              subst ⟨_⟩ (uaCommRing e) ∘ A .snd .fst ∘ subst (λ _ → ⟨ R ⟩) (sym (uaCommRing e))
+                ≡⟨ cong ((subst ⟨_⟩ (uaCommRing e) ∘ A .snd .fst) ∘_) (funExt (λ _ → transportRefl _)) ⟩
+              (subst ⟨_⟩ (uaCommRing e) ∘ (A .snd .fst))
+                ≡⟨ funExt (λ _ → uaβ (e .fst) _) ⟩
+              (CommRingEquiv→CommRingHom e ∘cr A .snd) .fst  ∎
+
+
+  CommRingEquiv→CommAlgebraEquiv :
+    {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''}
+    → (e : CommRingEquiv (A .fst) (B .fst))
+    → e .fst .fst ∘ A .snd .fst ≡ B .snd .fst
+    → CommAlgebraEquiv A B
+  CommRingEquiv→CommAlgebraEquiv {A = A} {B = B} e p = e .fst , isHom
+    where
+      opaque
+        isHom : IsCommAlgebraHom A B (e .fst .fst)
+        isHom = record { isCommRingHom = e .snd ; commutes = CommRingHom≡ p }
+
+  CommAlgebraEquiv→CREquivΣ :
+    {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''}
+    → (CommAlgebraEquiv A B)
+      ≃ (Σ[ f ∈ CommRingEquiv (A .fst) (B .fst) ] (f .fst .fst , f .snd)  ∘cr A .snd ≡ B .snd)
+  CommAlgebraEquiv→CREquivΣ =
+    isoToEquiv $
+    iso to from
+        (λ _ → Σ≡Prop (λ _ → isSetCommRingHom _ _ _ _) (Σ≡Prop (λ f → isPropIsCommRingHom _ (f .fst) _) refl))
+        (λ _ → Σ≡Prop (isPropIsCommAlgebraHom _ _ ∘ fst) refl)
+    where to : CommAlgebraEquiv _ _ → _
+          to e = (e .fst , IsCommAlgebraHom.isCommRingHom (e .snd)) , IsCommAlgebraHom.commutes (e .snd)
+
+          from : _ → CommAlgebraEquiv _ _
+          from (e , commutes) = CommRingEquiv→CommAlgebraEquiv e (cong fst commutes)
+
+  CommAlgebraPath :
+    (A B : CommAlgebra R ℓ')
+    → CommAlgebraEquiv A B
+    ≃ (A ≡ B)
+  CommAlgebraPath A B =
+    CommAlgebraEquiv A B
+       ≃⟨ CommAlgebraEquiv→CREquivΣ ⟩
+    Σ[ f ∈ CommRingEquiv (A .fst) (B .fst) ] (f .fst .fst , f .snd)  ∘cr A .snd ≡ B .snd
+       ≃⟨ CommAlgebraPath' A B ⟩
+    A ≡ B  ■
+
+  uaCommAlgebra : {A B : CommAlgebra R ℓ'} → CommAlgebraEquiv A B → A ≡ B
+  uaCommAlgebra {A = A} {B = B} =
+    equivFun $ CommAlgebraPath A B
+
+
+  isGroupoidCommAlgebra : isGroupoid (CommAlgebra R ℓ')
+  isGroupoidCommAlgebra A B =
+    isOfHLevelRespectEquiv
+      2
+      (CommAlgebraPath' _ _)
+      (isSetΣSndProp (isSetCommRingEquiv _ _) λ _ → isSetCommRingHom _ _ _ _)