Opaque FreeCommAlgebra

Cubical/Algebra/Algebra/Base.agda

@@ -50,7 +50,7 @@ record IsAlgebra (R : Ring ℓ) {A : Type ℓ'}
 
   open IsLeftModule +IsLeftModule public
 
-  isRing : IsRing _ _ _ _ _
+  isRing : IsRing 0a 1a _+_ _·_ (-_)
   isRing = isring (IsLeftModule.+IsAbGroup +IsLeftModule) ·IsMonoid ·DistR+ ·DistL+
   open IsRing isRing public
     hiding (_-_; +Assoc; +IdL; +InvL; +IdR; +InvR; +Comm; ·DistR+; ·DistL+; is-set)

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)
@@ -207,9 +242,9 @@ module _ {R : CommRing ℓ} where
                            → (fPres1 : f 1a ≡ 1a)
                            → (fPres+ : (x y : fst M) → f (x + y) ≡ f x + f y)
                            → (fPres· : (x y : fst M) → f (x · y) ≡ f x · f y)
-                           → (fPres⋆ : (r : fst R) (x : fst M) → f (r ⋆ x) ≡ r ⋆ f x)
+                           → (fPres⋆1a : (r : fst R) → f (r ⋆ 1a) ≡ r ⋆ 1a)
                            → CommAlgebraHom M N
-    makeCommAlgebraHom f fPres1 fPres+ fPres· fPres⋆ = f , isHom
+    makeCommAlgebraHom f fPres1 fPres+ fPres· fPres⋆1a = f , isHom
       where fPres0 =
                     f 0a                  ≡⟨ sym (+IdR _) ⟩
                     f 0a + 0a             ≡⟨ cong (λ u → f 0a + u) (sym (+InvR (f 0a))) ⟩
@@ -232,7 +267,14 @@ module _ {R : CommRing ℓ} where
                                (f ((- x) + x) - f x) ≡⟨ cong (λ u → f u - f x) (+InvL x) ⟩
                                (f 0a - f x) ≡⟨ cong (λ u → u - f x) fPres0 ⟩
                                (0a - f x) ≡⟨ +IdL _ ⟩ (- f x) ∎)
-            pres⋆ isHom = fPres⋆
+            pres⋆ isHom r y =
+              f (r ⋆ y)         ≡⟨ cong f (cong (r ⋆_) (sym (·IdL y))) ⟩
+              f (r ⋆ (1a · y))  ≡⟨ cong f (sym (⋆AssocL r 1a y)) ⟩
+              f ((r ⋆ 1a) · y)  ≡⟨ fPres· (r ⋆ 1a) y ⟩
+              f (r ⋆ 1a) · f y  ≡⟨ cong (_· f y) (fPres⋆1a r) ⟩
+              (r ⋆ 1a) · f y    ≡⟨ ⋆AssocL r 1a (f y) ⟩
+              r ⋆ (1a · f y)    ≡⟨ cong (r ⋆_) (·IdL (f y)) ⟩
+              r ⋆ f y           ∎
 
     isPropIsCommAlgebraHom : (f : fst M → fst N) → isProp (IsCommAlgebraHom (snd M) f (snd N))
     isPropIsCommAlgebraHom f = isPropIsAlgebraHom
@@ -253,7 +295,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 +304,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 +330,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

@@ -19,6 +19,7 @@ module Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base where
   For more, see the Properties file.
 -}
 open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.Structure using (⟨_⟩)
 
 open import Cubical.Algebra.CommRing
 open import Cubical.Algebra.CommAlgebra.Base
@@ -90,7 +91,25 @@ module Construction (R : CommRing ℓ) where
                                     ·-assoc ·-lid ldist ·-comm
                                     ⋆-assoc ⋆-rdist-+ ⋆-ldist-+ ·-lid ⋆-assoc-·
 
-_[_] : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R (ℓ-max ℓ ℓ')
-(R [ I ]) = R[ I ] , commalgebrastr 0a 1a _+_ _·_ -_ _⋆_ isCommAlgebra
-  where
+
+
+module _ (R : CommRing ℓ) (I : Type ℓ') where
   open Construction R
+  opaque
+    freeCAlgStr : CommAlgebraStr R (R[ I ])
+    freeCAlgStr = makeCommAlgebraStr _ _ _ _ _ _ _ isCommAlgebra
+
+_[_] : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R (ℓ-max ℓ ℓ')
+fst (R [ I ]) = Construction.R[_] R I
+snd (R [ I ]) = freeCAlgStr R I
+
+_[_]ᵣ : (R : CommRing ℓ) (I : Type ℓ') → CommRing (ℓ-max ℓ ℓ')
+(R [ I ]ᵣ) = CommAlgebra→CommRing (R [ I ])
+
+opaque
+  const : {R : CommRing ℓ} {I : Type ℓ'} → ⟨ R ⟩ → ⟨ R [ I ] ⟩
+  const = Construction.const
+
+opaque
+  var : {R : CommRing ℓ} {I : Type ℓ'} → I → ⟨ R [ I ] ⟩
+  var = Construction.var

Cubical/Algebra/CommAlgebra/FreeCommAlgebra/OnCoproduct.agda

@@ -13,9 +13,8 @@ open import Cubical.Foundations.Prelude
 open import Cubical.Foundations.Equiv
 open import Cubical.Foundations.Equiv.BiInvertible
 open import Cubical.Foundations.Isomorphism
-open import Cubical.Foundations.Structure
+open import Cubical.Foundations.Structure using (⟨_⟩; str)
 open import Cubical.Foundations.GroupoidLaws
-open import Cubical.Foundations.Structure
 
 open import Cubical.Data.Sum as ⊎
 open import Cubical.Data.Sigma
@@ -30,9 +29,62 @@ private variable
     ℓ ℓ' : Level
 
 module CalculateFreeCommAlgebraOnCoproduct (R : CommRing ℓ) (I J : Type ℓ) where
-  open Construction using (var; const)
   open CommAlgebraStr ⦃...⦄
 
+  R[I⊎J] : CommAlgebra R ℓ
+  R[I⊎J] = R [ I ⊎ J ]
+
+  R[I]→R[I⊎J] : CommAlgebraHom (R [ I ]) R[I⊎J]
+  R[I]→R[I⊎J] = inducedHom (R [ I ⊎ J ]) (λ i → var (inl i))
+
+  R[I]AsRing : CommRing ℓ
+  R[I]AsRing = CommAlgebra→CommRing (R [ I ])
+
+  R[I⊎J]overR[I] : CommAlgebra R[I]AsRing ℓ
+  R[I⊎J]overR[I] = Iso.inv (CommAlgChar.CommAlgIso (CommAlgebra→CommRing (R [ I ])))
+                   (CommAlgebra→CommRing (R [ I ⊎ J ]) ,
+                    (CommAlgebraHom→CommRingHom (R [ I ]) (R [ I ⊎ J ]) R[I]→R[I⊎J]))
+
+  module UniversalPropertyOfR[I⊎J]overR[I]
+    (A : CommAlgebra R[I]AsRing ℓ)
+    (φ : J → ⟨ A ⟩)
+    where
+
+    private instance
+      _ : CommAlgebraStr R[I]AsRing ⟨ A ⟩
+      _ = str A
+
+    AOverR : CommAlgebra R ℓ
+    AOverR = (baseChange baseRingHom A)
+
+    _ : Type ℓ
+    _ = CommAlgebraHom R[I⊎J] (baseChange baseRingHom A)
+
+    inducedHomOverR : CommAlgebraHom R[I⊎J] AOverR
+    inducedHomOverR = inducedHom AOverR (⊎.rec (λ i → var i ⋆ 1a) φ)
+
+    inducedHomOverR[I] : CommAlgebraHom R[I⊎J]overR[I] A
+    fst inducedHomOverR[I] = fst inducedHomOverR
+    snd inducedHomOverR[I] = record
+                              { pres0 = homStr .pres0
+                              ; pres1 = homStr .pres1
+                              ; pres+ = homStr .pres+
+                              ; pres· = homStr .pres·
+                              ; pres- = homStr .pres-
+                              ; pres⋆ = λ r x → f (r ⋆ x) ≡⟨ {!!} ⟩
+                                                r ⋆ f x ∎
+                              }
+        where open IsAlgebraHom
+              homStr = inducedHomOverR .snd
+              f = inducedHomOverR .fst
+              instance
+                _ = R[I⊎J]overR[I] .snd
+                _ = A .snd
+
+--  (r : R[I]) → (y : R[I⊎J]) → f (r ⋆ 1a) ≡ r ⋆ 1a
+--  (r : R[I]) → (y : R[I⊎J]) → f (var (inl i)) ≡ var i ⋆ 1a
+
+{-
   {-
      We start by defining R[I][J] and R[I⊎J] as R[I] algebras,
      which we need later to use universal properties
@@ -71,22 +123,30 @@ module CalculateFreeCommAlgebraOnCoproduct (R : CommRing ℓ) (I J : Type ℓ) w
                   (⊎.rec (λ i → const (var i))
                          λ j → var j)
 
+  isoR : Iso (CommAlgebra R ℓ) (CommAlgChar.CommRingWithHom R)
   isoR = CommAlgChar.CommAlgIso R
+
+  isoR[I] : Iso (CommAlgebra (CommAlgebra→CommRing (R [ I ])) ℓ)
+                (CommAlgChar.CommRingWithHom (CommAlgebra→CommRing (R [ I ])))
   isoR[I] = CommAlgChar.CommAlgIso (CommAlgebra→CommRing (R [ I ]))
+
+  asHomOverR[I] : CommAlgChar.CommRingWithHom (CommAlgebra→CommRing (R [ I ]))
   asHomOverR[I] = Iso.fun isoR[I] R[I⊎J]overR[I]
+
+  asHomOverR : CommAlgChar.CommRingWithHom R
   asHomOverR = Iso.fun isoR (R [ I ⊎ J ])
 
   ≡RingHoms : snd asHomOverR[I] ∘r baseRingHom ≡ baseRingHom
   ≡RingHoms =
-    RingHom≡
+    {!RingHom≡
       (funExt λ x →
         fst (snd asHomOverR[I] ∘r baseRingHom) x ≡⟨⟩
         fst (snd asHomOverR[I]) (const x · 1a)   ≡⟨⟩
         (const x · 1a) ⋆ 1a                      ≡⟨ cong (_⋆ 1a) (·IdR (const x)) ⟩
         const x ⋆ 1a                             ≡⟨⟩
         (fst ψ (const x)) · 1a                   ≡⟨⟩
         (const x · const 1r) · 1a                ≡⟨ cong (_· 1a) (·IdR (const x)) ⟩
-        const x · 1a ∎)
+        const x · 1a ∎)!}
 
   ≡R[I⊎J] =
     baseChange baseRingHom R[I⊎J]overR[I]                                                     ≡⟨⟩
@@ -256,3 +316,4 @@ module _ {R : CommRing ℓ} {I J : Type ℓ} where
       invr-rightInv asBiInv = toFromOverR[I]
       invl asBiInv = fst from
       invl-leftInv asBiInv = fromTo
+-- -}