univalence for comm algebras with Evans help

Author: felixwellen

Cubical/Algebra/CommAlgebraAlt/Base.agda

@@ -9,10 +9,12 @@ open import Cubical.Foundations.Structure using (⟨_⟩)
 open import Cubical.Foundations.HLevels
 open import Cubical.Foundations.Univalence
 open import Cubical.Foundations.Transport
+open import Cubical.Foundations.Path
 
 open import Cubical.Data.Sigma
 
 open import Cubical.Algebra.CommRing
+open import Cubical.Algebra.CommRing.Univalence
 open import Cubical.Algebra.Ring
 
 private
@@ -75,23 +77,50 @@ module _ {R : CommRing ℓ} where
 
     CommAlgebra≡ :
       {A B : CommAlgebra R ℓ'}
-      → (p : (A .fst) ≡ (B .fst))
-      → (pathToEquiv $ cong fst p) .fst ∘ (A .snd) .fst ≡ (B .snd) .fst
-      → A ≡ B
-    CommAlgebra≡ {A = A} {B = B} p q = ΣPathTransport→PathΣ A B (p , pComm)
-      where
-            pComm : subst (CommRingHom R) p (A .snd) ≡ B .snd
-            pComm =
-              CommRingHom≡
+      → (Σ[ p ∈ ((A .fst) ≡ (B .fst)) ]
+         ((pathToEquiv $ cong fst p) .fst ∘ (A .snd) .fst ≡ (B .snd) .fst))
+      ≃ (A ≡ B)
+    CommAlgebra≡ {A = A} {B = B} =
+      invEquiv
+        (Σ-cong-equiv-prop
+          (idEquiv ((A .fst) ≡ (B .fst)))
+          (λ _ → isSetCommRingHom _ _ _ _) (λ _ → isSet→ is-set _ _)
+          (λ p q → sym (pComm p) ∙ cong fst q) (λ p q → CommRingHom≡ (pComm p ∙ q)))
+      ∙ₑ   ΣPathTransport≃PathΣ A B
+      where open CommRingStr (B .fst .snd) using (is-set)
+            pComm : (p : A .fst ≡ B .fst)
+                    → subst (CommRingHom R) p (A .snd) .fst ≡ (pathToEquiv $ cong (λ r → fst r) p) .fst ∘ A .snd .fst
+            pComm p =
                 (fst (subst (CommRingHom R) p (A .snd))
                    ≡⟨ sym (substCommSlice (CommRingHom R) (λ X → ⟨ R ⟩ → ⟨ X ⟩) (λ _ → fst) p (A .snd)) ⟩
                  subst (λ X → ⟨ R ⟩ → ⟨ X ⟩) p (A .snd .fst)
                    ≡⟨ fromPathP (funTypeTransp (λ _ → ⟨ R ⟩) ⟨_⟩ p (A .snd .fst)) ⟩
                  subst ⟨_⟩ p ∘ A .snd .fst ∘ subst (λ _ → ⟨ R ⟩) (sym p)
                    ≡⟨ cong ((subst ⟨_⟩ p ∘ A .snd .fst) ∘_) (funExt (λ _ → transportRefl _)) ⟩
-                 (pathToEquiv $ cong (λ r → fst r) p) .fst ∘ A .snd .fst
-                   ≡⟨ q ⟩
-                 fst (B .snd) ∎)
+                 (pathToEquiv $ cong (λ r → fst r) p) .fst ∘ A .snd .fst ∎)
+
+    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 = A} {B = 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  ∎
 
   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