Pointwise ring and algebra structure (#667)

* pointwise comm ring structure on a function type

* Pointwise algebra structure on a function type

* fix options

* Use copattern

Cubical/Algebra/CommAlgebra/Instances/Pointwise.agda

@@ -0,0 +1,26 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.CommAlgebra.Instances.Pointwise where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Algebra.CommRing.Base
+open import Cubical.Algebra.CommRing.Instances.Pointwise
+open import Cubical.Algebra.CommAlgebra.Base
+
+private
+  variable
+    ℓ : Level
+
+pointwiseAlgebra :  {R : CommRing ℓ} (X : Type ℓ) (A : CommAlgebra R ℓ) → CommAlgebra R ℓ
+pointwiseAlgebra {R = R} X A =
+  let open CommAlgebraStr (snd A)
+      isSetX→A = isOfHLevelΠ 2 (λ (x : X) → isSetCommRing (CommAlgebra→CommRing A))
+  in commAlgebraFromCommRing
+       (pointwiseRing X (CommAlgebra→CommRing A))
+       (λ r f → (λ x → r ⋆ (f x)))
+       (λ r s f i x → ⋆-assoc r s (f x) i)
+       (λ r s f i x → ⋆-ldist r s (f x) i)
+       (λ r f g i x → ⋆-rdist r (f x) (g x) i)
+       (λ f i x → ⋆-lid (f x) i)
+       λ r f g i x → ⋆-lassoc r (f x) (g x) i

Cubical/Algebra/CommRing/Instances/Pointwise.agda

@@ -0,0 +1,36 @@
+{-# OPTIONS --safe #-}
+module Cubical.Algebra.CommRing.Instances.Pointwise where
+
+open import Cubical.Foundations.Prelude
+open import Cubical.Foundations.HLevels
+
+open import Cubical.Algebra.CommRing.Base
+
+private
+  variable
+    ℓ : Level
+
+pointwiseRing : (X : Type ℓ) (R : CommRing ℓ) → CommRing ℓ
+pointwiseRing X R = (X → fst R) , str
+    where
+      open CommRingStr (snd R)
+
+      isSetX→R = isOfHLevelΠ 2 (λ _ → isSetCommRing R)
+
+      str : CommRingStr (X → fst R)
+      CommRingStr.0r str = λ _ → 0r
+      CommRingStr.1r str = λ _ → 1r
+      CommRingStr._+_ str = λ f g → (λ x → f x + g x)
+      CommRingStr._·_ str = λ f g → (λ x → f x · g x)
+      CommRingStr.- str = λ f → (λ x → - f x)
+      CommRingStr.isCommRing str =
+        makeIsCommRing
+           isSetX→R
+           (λ f g h i x → +Assoc (f x) (g x) (h x) i)
+           (λ f i x → +Rid (f x) i)
+           (λ f i x → +Rinv (f x) i)
+           (λ f g i x → +Comm (f x) (g x) i)
+           (λ f g h i x → ·Assoc (f x) (g x) (h x) i)
+           (λ f i x → ·Rid (f x) i)
+           (λ f g h i x → ·Rdist+ (f x) (g x) (h x) i)
+           λ f g i x → ·-comm (f x) (g x) i