(wip) opaque FreeCommAlgebra

agda · Jan 19, 2024 · c1b3508 · c1b3508
1 parent e9cf5c6
commit c1b3508
Show file tree

Hide file tree

Showing 2 changed files with 244 additions and 205 deletions.
diff --git a/Cubical/Algebra/CommAlgebra/FreeCommAlgebra/Base.agda b/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,21 @@ 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
-  open Construction R
+opaque
+
+  _[_] : (R : CommRing ℓ) (I : Type ℓ') → CommAlgebra R (ℓ-max ℓ ℓ')
+  (R [ I ]) = R[ I ] , commalgebrastr 0a 1a _+_ _·_ -_ _⋆_ isCommAlgebra
+    where
+    open Construction R
+
+opaque
+  unfolding _[_]
+
+  const : {R : CommRing ℓ} {I : Type ℓ'} → ⟨ R ⟩ → ⟨ R [ I ] ⟩
+  const = Construction.const
+
+opaque
+  unfolding _[_]
+
+  var : {R : CommRing ℓ} {I : Type ℓ'} → I → ⟨ R [ I ] ⟩
+  var = Construction.var