No-eta for CommAlgebras

Cubical/Algebra/CommAlgebra/Base.agda

@@ -29,8 +29,7 @@ record IsCommAlgebra (R : CommRing ℓ) {A : Type ℓ'}
                      (0a : A) (1a : A)
                      (_+_ : A → A → A) (_·_ : A → A → A) (-_ : A → A)
                      (_⋆_ : ⟨ R ⟩ → A → A) : Type (ℓ-max ℓ ℓ') where
-
-  constructor iscommalgebra
+  no-eta-equality
 
   field
     isAlgebra : IsAlgebra (CommRing→Ring R) 0a 1a _+_ _·_ -_ _⋆_
@@ -41,8 +40,7 @@ record IsCommAlgebra (R : CommRing ℓ) {A : Type ℓ'}
 unquoteDecl IsCommAlgebraIsoΣ = declareRecordIsoΣ IsCommAlgebraIsoΣ (quote IsCommAlgebra)
 
 record CommAlgebraStr (R : CommRing ℓ) (A : Type ℓ') : Type (ℓ-max ℓ ℓ') where
-
-  constructor commalgebrastr
+  no-eta-equality
 
   field
     0a             : A
@@ -60,22 +58,43 @@ record CommAlgebraStr (R : CommRing ℓ) (A : Type ℓ') : Type (ℓ-max ℓ ℓ
   infixl 7 _⋆_
   infixl 6 _+_
 
+unquoteDecl CommAlgebraStrIsoΣ = declareRecordIsoΣ CommAlgebraStrIsoΣ (quote CommAlgebraStr)
+
 CommAlgebra : (R : CommRing ℓ) → ∀ ℓ' → Type (ℓ-max ℓ (ℓ-suc ℓ'))
 CommAlgebra R ℓ' = Σ[ A ∈ Type ℓ' ] CommAlgebraStr R A
 
 module _ {R : CommRing ℓ} where
   open CommRingStr (snd R) using (1r) renaming (_+_ to _+r_; _·_ to _·s_)
 
   CommAlgebraStr→AlgebraStr : {A : Type ℓ'} → CommAlgebraStr R A → AlgebraStr (CommRing→Ring R) A
-  CommAlgebraStr→AlgebraStr (commalgebrastr _ _ _ _ _ _ (iscommalgebra isAlgebra ·-comm)) =
-    algebrastr _ _ _ _ _ _ isAlgebra
+  CommAlgebraStr→AlgebraStr {A = A} cstr = x
+    where open AlgebraStr
+          x : AlgebraStr (CommRing→Ring R) A
+          0a x = _
+          1a x = _
+          _+_ x = _
+          _·_ x = _
+          - x = _
+          _⋆_ x = _
+          isAlgebra x = IsCommAlgebra.isAlgebra (CommAlgebraStr.isCommAlgebra cstr)
 
   CommAlgebra→Algebra : (A : CommAlgebra R ℓ') → Algebra (CommRing→Ring R) ℓ'
-  CommAlgebra→Algebra (_ , str) = (_ , CommAlgebraStr→AlgebraStr str)
+  fst (CommAlgebra→Algebra A) = fst A
+  snd (CommAlgebra→Algebra A) = CommAlgebraStr→AlgebraStr (snd A)
 
   CommAlgebra→CommRing : (A : CommAlgebra R ℓ') → CommRing ℓ'
-  CommAlgebra→CommRing (_ , commalgebrastr  _ _ _ _ _ _ (iscommalgebra isAlgebra ·-comm)) =
-    _ , commringstr _ _ _ _ _ (iscommring (IsAlgebra.isRing isAlgebra) ·-comm)
+  CommAlgebra→CommRing (A , str) = x
+    where open CommRingStr
+          open CommAlgebraStr
+          x : CommRing _
+          fst x = A
+          0r (snd x) = _
+          1r (snd x) = _
+          _+_ (snd x) = _
+          _·_ (snd x) = _
+          - snd x = _
+          IsCommRing.isRing (isCommRing (snd x)) = RingStr.isRing (Algebra→Ring (_ , CommAlgebraStr→AlgebraStr str) .snd)
+          IsCommRing.·Comm (isCommRing (snd x)) = CommAlgebraStr.·Comm  str
 
   module _
       {A : Type ℓ'} {0a 1a : A}
@@ -124,6 +143,22 @@ module _ {R : CommRing ℓ} where
                        x · (r ⋆ y) ∎
     makeIsCommAlgebra .IsCommAlgebra.·Comm = ·Comm
 
+  makeCommAlgebraStr :
+    (A : Type ℓ') (0a 1a : A)
+    (_+_ _·_ : A → A → A) ( -_ : A → A) (_⋆_ : ⟨ R ⟩ → A → A)
+    (isCommAlg : IsCommAlgebra R 0a 1a _+_ _·_ -_ _⋆_)
+    → CommAlgebraStr R A
+  makeCommAlgebraStr A 0a 1a _+_ _·_ -_ _⋆_ isCommAlg =
+    record
+      { 0a = 0a
+      ; 1a = 1a
+      ; _+_ = _+_
+      ; _·_ = _·_
+      ; -_ =  -_
+      ; _⋆_ = _⋆_
+      ; isCommAlgebra = isCommAlg
+      }
+
   module _ (S : CommRing ℓ') where
     open CommRingStr (snd S) renaming (1r to 1S)
     open CommRingStr (snd R) using () renaming (_·_ to _·R_; _+_ to _+R_; 1r to 1R)
@@ -253,7 +288,7 @@ isPropIsCommAlgebra R _ _ _ _ _ _ =
       (λ alg → isPropΠ2 λ _ _ → alg .IsAlgebra.is-set _ _))
 
 𝒮ᴰ-CommAlgebra : (R : CommRing ℓ) → DUARel (𝒮-Univ ℓ') (CommAlgebraStr R) (ℓ-max ℓ ℓ')
-𝒮ᴰ-CommAlgebra R =
+𝒮ᴰ-CommAlgebra {ℓ' = ℓ'} R =
   𝒮ᴰ-Record (𝒮-Univ _) (IsCommAlgebraEquiv {R = R})
     (fields:
       data[ 0a ∣ nul ∣ pres0 ]
@@ -262,7 +297,16 @@ isPropIsCommAlgebra R _ _ _ _ _ _ =
       data[ _·_ ∣ bin ∣ pres· ]
       data[ -_ ∣ autoDUARel _ _ ∣ pres- ]
       data[ _⋆_ ∣ autoDUARel _ _ ∣ pres⋆ ]
-      prop[ isCommAlgebra ∣ (λ _ _ → isPropIsCommAlgebra _ _ _ _ _ _ _) ])
+      prop[ isCommAlgebra ∣ (λ A ΣA
+                               → isPropIsCommAlgebra
+                                 {ℓ' = ℓ'}
+                                 R
+                                 (snd (fst (fst (fst (fst (fst ΣA))))))
+                                 (snd (fst (fst (fst (fst ΣA)))))
+                                 (snd (fst (fst (fst ΣA))))
+                                 (snd (fst (fst ΣA)))
+                                 (snd (fst ΣA))
+                                 (snd ΣA)) ])
   where
   open CommAlgebraStr
   open IsAlgebraHom
@@ -279,4 +323,3 @@ uaCommAlgebra {R = R} {A = A} {B = B} = equivFun (CommAlgebraPath R A B)
 
 isGroupoidCommAlgebra : {R : CommRing ℓ} → isGroupoid (CommAlgebra R ℓ')
 isGroupoidCommAlgebra A B = isOfHLevelRespectEquiv 2 (CommAlgebraPath _ _ _) (isSetAlgebraEquiv _ _)
--- -}

Cubical/Algebra/CommAlgebra/FPAlgebra/Base.agda

@@ -51,7 +51,7 @@ module _ {R : CommRing ℓ} where
   evPolyHomomorphic A B f P values =
     (fst f) (evPoly A P values)                         ≡⟨ refl ⟩
     (fst f) (fst (freeInducedHom A values) P)           ≡⟨ refl ⟩
-    fst (f ∘a freeInducedHom A values) P                ≡⟨ cong (λ u → fst u P) (natIndHomR f values) ⟩
+    fst (f ∘a freeInducedHom A values) P                ≡⟨ cong (λ u → fst u P) (natIndHomR {A = A} {B = B} f values) ⟩
     fst (freeInducedHom B (fst f ∘ values)) P           ≡⟨ refl ⟩
     evPoly B P (fst f ∘ values) ∎
     where open AlgebraHoms

Cubical/Algebra/CommAlgebra/FPAlgebra/Instances.agda

@@ -78,13 +78,13 @@ module _ (R : CommRing ℓ) where
         inverse1 : fromA ∘a toA ≡ idAlgebraHom _
         inverse1 =
           fromA ∘a toA
-            ≡⟨ sym (unique _ _ _ _ _ _ (λ i → cong (fst fromA) (
+            ≡⟨ sym (unique _ _ B _ _ _ (λ i → cong (fst fromA) (
                  fst toA (generator n emptyGen i)
                    ≡⟨ inducedHomOnGenerators _ _ _ _ _ _ ⟩
                  Construction.var i
                    ∎))) ⟩
           inducedHom n emptyGen B (generator _ _) (relationsHold _ _)
-            ≡⟨ unique _ _ _ _ _ _ (λ i → refl) ⟩
+            ≡⟨ unique _ _ B _ _ _ (λ i → refl) ⟩
           idAlgebraHom _
             ∎
         inverse2 : toA ∘a fromA ≡ idAlgebraHom _

Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Base.agda

@@ -91,6 +91,6 @@ module Construction (R : CommRing ℓ) where
                                     ⋆-assoc ⋆-rdist-+ ⋆-ldist-+ ·-lid ⋆-assoc-·
 
 _[_] : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R (ℓ-max ℓ ℓ')
-(R [ I ]) = R[ I ] , commalgebrastr 0a 1a _+_ _·_ -_ _⋆_ isCommAlgebra
-  where
-  open Construction R
+fst (R [ I ]) = Construction.R[_] R I
+snd (R [ I ]) = makeCommAlgebraStr _ _ _ _ _ _ _ isCommAlgebra
+  where open Construction R

Cubical/Algebra/CommAlgebra/Properties.agda

@@ -14,6 +14,8 @@ open import Cubical.Foundations.SIP
 open import Cubical.Foundations.GroupoidLaws
 open import Cubical.Foundations.Path
 
+open import Cubical.Functions.Embedding
+
 open import Cubical.Data.Sigma
 
 open import Cubical.Reflection.StrictEquiv
@@ -221,60 +223,37 @@ module CommAlgebraHoms {R : CommRing ℓ} where
   compAssocCommAlgebraHom = compAssocAlgebraHom
 
 module CommAlgebraEquivs {R : CommRing ℓ} where
- open AlgebraEquivs
-
- compCommAlgebraEquiv : {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''} {C : CommAlgebra R ℓ'''}
-                   → CommAlgebraEquiv A B → CommAlgebraEquiv B C → CommAlgebraEquiv A C
- compCommAlgebraEquiv {A = A} {B = B} {C = C} = compAlgebraEquiv {A = CommAlgebra→Algebra A}
-                                                           {B = CommAlgebra→Algebra B}
-                                                           {C = CommAlgebra→Algebra C}
-
+  open AlgebraEquivs
+
+  compCommAlgebraEquiv : {A : CommAlgebra R ℓ'} {B : CommAlgebra R ℓ''} {C : CommAlgebra R ℓ'''}
+                    → CommAlgebraEquiv A B → CommAlgebraEquiv B C → CommAlgebraEquiv A C
+  compCommAlgebraEquiv {A = A} {B = B} {C = C} = compAlgebraEquiv {A = CommAlgebra→Algebra A}
+                                                            {B = CommAlgebra→Algebra B}
+                                                            {C = CommAlgebra→Algebra C}
+
+
+  isSetCommAlgStr : (A : Type ℓ') → isSet (CommAlgebraStr R A)
+  isSetCommAlgStr A =
+    let open CommAlgebraStr
+    in isOfHLevelSucIfInhabited→isOfHLevelSuc 1 (λ str →
+       isOfHLevelRetractFromIso 2 CommAlgebraStrIsoΣ $
+       isSetΣ (str .is-set) λ _ →
+       isSetΣ (str .is-set) (λ _ →
+       isSetΣ (isSet→ (isSet→ (str .is-set))) λ _ →
+       isSetΣ (isSet→ (isSet→ (str .is-set))) (λ _ →
+       isSetΣ (isSet→ (str .is-set)) λ _ →
+       isSetΣSndProp (isSet→ (isSet→ (str .is-set))) (λ _ →
+       isPropIsCommAlgebra R _ _ _ _ _ _))))
 
 -- the CommAlgebra version of uaCompEquiv
 module CommAlgebraUAFunctoriality {R : CommRing ℓ} where
  open CommAlgebraStr
  open CommAlgebraEquivs
 
- CommAlgebra≡ : (A B : CommAlgebra R ℓ') → (
-   Σ[ p ∈ ⟨ A ⟩ ≡ ⟨ B ⟩ ]
-   Σ[ q0 ∈ PathP (λ i → p i) (0a (snd A)) (0a (snd B)) ]
-   Σ[ q1 ∈ PathP (λ i → p i) (1a (snd A)) (1a (snd B)) ]
-   Σ[ r+ ∈ PathP (λ i → p i → p i → p i) (_+_ (snd A)) (_+_ (snd B)) ]
-   Σ[ r· ∈ PathP (λ i → p i → p i → p i) (_·_ (snd A)) (_·_ (snd B)) ]
-   Σ[ s- ∈ PathP (λ i → p i → p i) (-_ (snd A)) (-_ (snd B)) ]
-   Σ[ s⋆ ∈ PathP (λ i → ⟨ R ⟩ → p i → p i) (_⋆_ (snd A)) (_⋆_ (snd B)) ]
-   PathP (λ i → IsCommAlgebra R (q0 i) (q1 i) (r+ i) (r· i) (s- i) (s⋆ i)) (isCommAlgebra (snd A))
-                                                                           (isCommAlgebra (snd B)))
-   ≃ (A ≡ B)
- CommAlgebra≡ A B = isoToEquiv theIso
-   where
-   open Iso
-   theIso : Iso _ _
-   fun theIso (p , q0 , q1 , r+ , r· , s- , s⋆ , t) i = p i
-                 , commalgebrastr (q0 i) (q1 i) (r+ i) (r· i) (s- i) (s⋆ i) (t i)
-   inv theIso x = cong ⟨_⟩ x , cong (0a ∘ snd) x , cong (1a ∘ snd) x
-                , cong (_+_ ∘ snd) x , cong (_·_ ∘ snd) x , cong (-_ ∘ snd) x , cong (_⋆_ ∘ snd) x
-                , cong (isCommAlgebra ∘ snd) x
-   rightInv theIso _ = refl
-   leftInv theIso _ = refl
-
  caracCommAlgebra≡ : {A B : CommAlgebra R ℓ'} (p q : A ≡ B) → cong ⟨_⟩ p ≡ cong ⟨_⟩ q → p ≡ q
- caracCommAlgebra≡ {A = A} {B = B} p q P =
-   sym (transportTransport⁻ (ua (CommAlgebra≡ A B)) p)
-                                    ∙∙ cong (transport (ua (CommAlgebra≡ A B))) helper
-                                    ∙∙ transportTransport⁻ (ua (CommAlgebra≡ A B)) q
-     where
-     helper : transport (sym (ua (CommAlgebra≡ A B))) p ≡ transport (sym (ua (CommAlgebra≡ A B))) q
-     helper = Σ≡Prop
-                (λ _ → isPropΣ
-                          (isOfHLevelPathP' 1 (is-set (snd B)) _ _)
-                          λ _ → isPropΣ (isOfHLevelPathP' 1 (is-set (snd B)) _ _)
-                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
-                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
-                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ λ _ → is-set (snd B)) _ _)
-                          λ _ → isPropΣ (isOfHLevelPathP' 1 (isSetΠ2 λ _ _ → is-set (snd B)) _ _)
-                          λ _ → isOfHLevelPathP 1 (isPropIsCommAlgebra _ _ _ _ _ _ _) _ _)
-               (transportRefl (cong ⟨_⟩ p) ∙ P ∙ sym (transportRefl (cong ⟨_⟩ q)))
+ caracCommAlgebra≡  _ _ α =
+   isEmbedding→Inj (iso→isEmbedding (invIso ΣPathIsoPathΣ)) _ _ $
+   Σ≡Prop (λ _ → isOfHLevelPathP' 1 (isSetCommAlgStr _) _ _) α
 
  uaCompCommAlgebraEquiv : {A B C : CommAlgebra R ℓ'} (f : CommAlgebraEquiv A B) (g : CommAlgebraEquiv B C)
                   → uaCommAlgebra (compCommAlgebraEquiv f g) ≡ uaCommAlgebra f ∙ uaCommAlgebra g
@@ -285,7 +264,6 @@ module CommAlgebraUAFunctoriality {R : CommRing ℓ} where
      ≡⟨ sym (cong-∙ ⟨_⟩ (uaCommAlgebra f) (uaCommAlgebra g)) ⟩
    cong ⟨_⟩ (uaCommAlgebra f ∙ uaCommAlgebra g) ∎)
 
-
 open CommAlgebraHoms
 open CommAlgebraEquivs
 open CommAlgebraUAFunctoriality
@@ -299,6 +277,7 @@ recPT→CommAlgebra 𝓕 σ compCoh = GpdElim.rec→Gpd isGroupoidCommAlgebra 
                           λ x y z → sym (  cong uaCommAlgebra (compCoh x y z)
                                          ∙ uaCompCommAlgebraEquiv (σ x y) (σ y z)))
 
+open CommAlgebraHoms
 
 contrCommAlgebraHom→contrCommAlgebraEquiv : {R : CommRing ℓ} {A : Type ℓ'}
         (σ : A → CommAlgebra R ℓ'')

Cubical/Algebra/CommAlgebra/Subalgebra.agda

@@ -20,14 +20,15 @@ module _ (S : Subalgebra) where
   Subalgebra→CommAlgebra≡ = Subalgebra→Algebra≡ S
 
   Subalgebra→CommAlgebra : CommAlgebra R ℓ'
-  Subalgebra→CommAlgebra =
-      Subalgebra→Algebra S .fst
-    , record
-      { AlgebraStr (Subalgebra→Algebra S .snd)
-      ; isCommAlgebra = iscommalgebra
-          (Subalgebra→Algebra S .snd .AlgebraStr.isAlgebra)
-          (λ x y → Subalgebra→CommAlgebra≡
-            (CommAlgebraStr.·Comm (snd A) (fst x) (fst y)))}
+  fst Subalgebra→CommAlgebra = Subalgebra→Algebra S .fst
+  snd Subalgebra→CommAlgebra = record
+                                { AlgebraStr (Subalgebra→Algebra S .snd)
+                                ; isCommAlgebra = record {
+                                    isAlgebra =
+                                       Subalgebra→Algebra S .snd .AlgebraStr.isAlgebra ;
+                                    ·Comm = λ x y → Subalgebra→CommAlgebra≡
+                                       (CommAlgebraStr.·Comm (snd A) (fst x) (fst y)) }
+                                }
 
   Subalgebra→CommAlgebraHom : CommAlgebraHom Subalgebra→CommAlgebra A
   Subalgebra→CommAlgebraHom = Subalgebra→AlgebraHom S
@@ -41,4 +42,3 @@ module _ (S : Subalgebra) where
                               (λ x y → Subalgebra→CommAlgebra≡ (pres+ x y))
                               (λ x y → Subalgebra→CommAlgebra≡ (pres· x y))
                               (λ x y → Subalgebra→CommAlgebra≡ (pres⋆ x y))
-