Deploying to gh-pages from @ 21ddf92 🚀

agda · Aug 25, 2023 · 8fc0f51 · 8fc0f51
1 parent 901cfa9
commit 8fc0f51
Show file tree

Hide file tree

Showing 147 changed files with 3,200 additions and 3,185 deletions.
diff --git a/Cubical.Algebra.AbGroup.Base.html b/Cubical.Algebra.AbGroup.Base.html
diff --git a/Cubical.Algebra.AbGroup.Instances.Hom.html b/Cubical.Algebra.AbGroup.Instances.Hom.html
diff --git a/Cubical.Algebra.AbGroup.TensorProduct.html b/Cubical.Algebra.AbGroup.TensorProduct.html
diff --git a/Cubical.Algebra.Algebra.Base.html b/Cubical.Algebra.Algebra.Base.html
diff --git a/Cubical.Algebra.Algebra.Properties.html b/Cubical.Algebra.Algebra.Properties.html
diff --git a/Cubical.Algebra.Algebra.Subalgebra.html b/Cubical.Algebra.Algebra.Subalgebra.html
diff --git a/Cubical.Algebra.CommAlgebra.Base.html b/Cubical.Algebra.CommAlgebra.Base.html
diff --git a/Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html b/Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html
diff --git a/Cubical.Algebra.CommAlgebra.FPAlgebra.Instances.html b/Cubical.Algebra.CommAlgebra.FPAlgebra.Instances.html
diff --git a/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html b/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html
@@ -86,7 +86,7 @@
   <a id="3357" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#3327" class="Function">1a</a> <a id="3360" class="Symbol">=</a> <a id="3362" class="Symbol">(</a><a id="3363" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1224" class="InductiveConstructor">const</a> <a id="3369" href="Cubical.Algebra.CommRing.Base.html#1059" class="Function">1r</a><a id="3371" class="Symbol">)</a>
 
   <a id="Construction.isCommAlgebra"></a><a id="3376" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#3376" class="Function">isCommAlgebra</a> <a id="3390" class="Symbol">:</a> <a id="3392" class="Symbol">{</a><a id="3393" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#3393" class="Bound">I</a> <a id="3395" class="Symbol">:</a> <a id="3397" href="Agda.Primitive.html#320" class="Primitive">Type</a> <a id="3402" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1013" class="Generalizable">ℓ&#39;</a><a id="3404" class="Symbol">}</a> <a id="3406" class="Symbol">→</a> <a id="3408" href="Cubical.Algebra.CommAlgebra.Base.html#677" class="Record">IsCommAlgebra</a> <a id="3422" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1046" class="Bound">R</a> <a id="3424" class="Symbol">{</a><a id="3425" class="Argument">A</a> <a id="3427" class="Symbol">=</a> <a id="3429" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1154" class="Datatype Operator">R[</a> <a id="3432" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#3393" class="Bound">I</a> <a id="3434" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1154" class="Datatype Operator">]</a><a id="3435" class="Symbol">}</a> <a id="3437" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#3278" class="Function">0a</a> <a id="3440" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#3327" class="Function">1a</a> <a id="3443" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1251" class="InductiveConstructor Operator">_+_</a> <a id="3447" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1311" class="InductiveConstructor Operator">_·_</a> <a id="3451" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1286" class="InductiveConstructor Operator">-_</a> <a id="3454" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1971" class="Function Operator">_⋆_</a>
-  <a id="3460" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#3376" class="Function">isCommAlgebra</a> <a id="3474" class="Symbol">=</a> <a id="3476" href="Cubical.Algebra.CommAlgebra.Base.html#3449" class="Function">makeIsCommAlgebra</a> <a id="3494" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1921" class="InductiveConstructor">0-trunc</a>
+  <a id="3460" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#3376" class="Function">isCommAlgebra</a> <a id="3474" class="Symbol">=</a> <a id="3476" href="Cubical.Algebra.CommAlgebra.Base.html#3461" class="Function">makeIsCommAlgebra</a> <a id="3494" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1921" class="InductiveConstructor">0-trunc</a>
                                     <a id="3538" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1367" class="InductiveConstructor">+-assoc</a> <a id="3546" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1426" class="InductiveConstructor">+-rid</a> <a id="3552" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1472" class="InductiveConstructor">+-rinv</a> <a id="3559" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1523" class="InductiveConstructor">+-comm</a>
                                     <a id="3602" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1568" class="InductiveConstructor">·-assoc</a> <a id="3610" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1627" class="InductiveConstructor">·-lid</a> <a id="3616" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1718" class="InductiveConstructor">ldist</a> <a id="3622" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1673" class="InductiveConstructor">·-comm</a>
                                     <a id="3665" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#2042" class="Function">⋆-assoc</a> <a id="3673" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#2643" class="Function">⋆-rdist-+</a> <a id="3683" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#2363" class="Function">⋆-ldist-+</a> <a id="3693" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1627" class="InductiveConstructor">·-lid</a> <a id="3699" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#3101" class="Function">⋆-assoc-·</a>

diff --git a/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.OnCoproduct.html b/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.OnCoproduct.html
diff --git a/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html b/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html