Deploying to gh-pages from @ 3b2a50a 🚀

Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html

@@ -23,7 +23,7 @@
 <a id="685" class="Keyword">open</a> <a id="690" class="Keyword">import</a> <a id="697" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.html" class="Module">Cubical.Algebra.CommAlgebra.FreeCommAlgebra</a>
   <a id="743" class="Keyword">renaming</a> <a id="752" class="Symbol">(</a><a id="753" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#9588" class="Function">inducedHom</a> <a id="764" class="Symbol">to</a> <a id="767" class="Function">freeInducedHom</a><a id="781" class="Symbol">)</a>
 <a id="783" class="Keyword">open</a> <a id="788" class="Keyword">import</a> <a id="795" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html" class="Module">Cubical.Algebra.CommAlgebra.QuotientAlgebra</a>
-  <a id="841" class="Keyword">renaming</a> <a id="850" class="Symbol">(</a><a id="851" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#5453" class="Function">inducedHom</a> <a id="862" class="Symbol">to</a> <a id="865" class="Function">quotientInducedHom</a><a id="883" class="Symbol">)</a>
+  <a id="841" class="Keyword">renaming</a> <a id="850" class="Symbol">(</a><a id="851" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#5506" class="Function">inducedHom</a> <a id="862" class="Symbol">to</a> <a id="865" class="Function">quotientInducedHom</a><a id="883" class="Symbol">)</a>
 <a id="885" class="Keyword">open</a> <a id="890" class="Keyword">import</a> <a id="897" href="Cubical.Algebra.CommAlgebra.Ideal.html" class="Module">Cubical.Algebra.CommAlgebra.Ideal</a>
 <a id="931" class="Keyword">open</a> <a id="936" class="Keyword">import</a> <a id="943" href="Cubical.Algebra.CommAlgebra.FGIdeal.html" class="Module">Cubical.Algebra.CommAlgebra.FGIdeal</a>
 <a id="979" class="Keyword">open</a> <a id="984" class="Keyword">import</a> <a id="991" href="Cubical.Algebra.CommAlgebra.Kernel.html" class="Module">Cubical.Algebra.CommAlgebra.Kernel</a>
@@ -70,10 +70,10 @@
         This also means, the where blocks contain more type declarations than usual.
       -}</a>
       <a id="2719" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2719" class="Function">FPAlgebra</a> <a id="2729" class="Symbol">:</a> <a id="2731" href="Cubical.Algebra.CommAlgebra.Base.html#1625" class="Function">CommAlgebra</a> <a id="2743" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1158" class="Bound">R</a> <a id="2745" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1171" class="Bound">ℓ</a>
-      <a id="2753" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2719" class="Function">FPAlgebra</a> <a id="2763" class="Symbol">=</a> <a id="2765" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1214" class="Function">Polynomials</a> <a id="2777" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2237" class="Bound">n</a> <a id="2779" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#1889" class="Function Operator">/</a> <a id="2781" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2386" class="Function">relationsIdeal</a>
+      <a id="2753" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2719" class="Function">FPAlgebra</a> <a id="2763" class="Symbol">=</a> <a id="2765" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1214" class="Function">Polynomials</a> <a id="2777" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2237" class="Bound">n</a> <a id="2779" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#1834" class="Function Operator">/</a> <a id="2781" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2386" class="Function">relationsIdeal</a>
 
-      <a id="2803" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2803" class="Function">modRelations</a> <a id="2816" class="Symbol">:</a> <a id="2818" href="Cubical.Algebra.CommAlgebra.Base.html#7059" class="Function">CommAlgebraHom</a> <a id="2833" class="Symbol">(</a><a id="2834" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1214" class="Function">Polynomials</a> <a id="2846" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2237" class="Bound">n</a><a id="2847" class="Symbol">)</a> <a id="2849" class="Symbol">(</a><a id="2850" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1214" class="Function">Polynomials</a> <a id="2862" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2237" class="Bound">n</a> <a id="2864" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#1889" class="Function Operator">/</a> <a id="2866" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2386" class="Function">relationsIdeal</a><a id="2880" class="Symbol">)</a>
-      <a id="2888" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2803" class="Function">modRelations</a> <a id="2901" class="Symbol">=</a> <a id="2903" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#3891" class="Function">quotientHom</a> <a id="2915" class="Symbol">(</a><a id="2916" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1214" class="Function">Polynomials</a> <a id="2928" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2237" class="Bound">n</a><a id="2929" class="Symbol">)</a> <a id="2931" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2386" class="Function">relationsIdeal</a>
+      <a id="2803" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2803" class="Function">modRelations</a> <a id="2816" class="Symbol">:</a> <a id="2818" href="Cubical.Algebra.CommAlgebra.Base.html#7059" class="Function">CommAlgebraHom</a> <a id="2833" class="Symbol">(</a><a id="2834" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1214" class="Function">Polynomials</a> <a id="2846" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2237" class="Bound">n</a><a id="2847" class="Symbol">)</a> <a id="2849" class="Symbol">(</a><a id="2850" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1214" class="Function">Polynomials</a> <a id="2862" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2237" class="Bound">n</a> <a id="2864" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#1834" class="Function Operator">/</a> <a id="2866" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2386" class="Function">relationsIdeal</a><a id="2880" class="Symbol">)</a>
+      <a id="2888" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2803" class="Function">modRelations</a> <a id="2901" class="Symbol">=</a> <a id="2903" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#3868" class="Function">quotientHom</a> <a id="2915" class="Symbol">(</a><a id="2916" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1214" class="Function">Polynomials</a> <a id="2928" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2237" class="Bound">n</a><a id="2929" class="Symbol">)</a> <a id="2931" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2386" class="Function">relationsIdeal</a>
 
       <a id="2953" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2953" class="Function">generator</a> <a id="2963" class="Symbol">:</a> <a id="2965" class="Symbol">(</a><a id="2966" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2966" class="Bound">i</a> <a id="2968" class="Symbol">:</a> <a id="2970" href="Cubical.Data.FinData.Base.html#375" class="Datatype">Fin</a> <a id="2974" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2237" class="Bound">n</a><a id="2975" class="Symbol">)</a> <a id="2977" class="Symbol">→</a> <a id="2979" href="Cubical.Foundations.Structure.html#640" class="Function Operator">⟨</a> <a id="2981" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2719" class="Function">FPAlgebra</a> <a id="2991" href="Cubical.Foundations.Structure.html#640" class="Function Operator">⟩</a>
       <a id="2999" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2953" class="Function">generator</a> <a id="3009" class="Symbol">=</a> <a id="3011" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="3015" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2803" class="Function">modRelations</a> <a id="3028" href="Cubical.Foundations.Function.html#653" class="Function Operator">∘</a> <a id="3030" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1203" class="InductiveConstructor">var</a>
@@ -85,7 +85,7 @@
         <a id="3305" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="3309" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2803" class="Function">modRelations</a> <a id="3322" class="Symbol">(</a><a id="3323" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1287" class="Function">evPoly</a> <a id="3330" class="Symbol">(</a><a id="3331" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1214" class="Function">Polynomials</a> <a id="3343" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2237" class="Bound">n</a><a id="3344" class="Symbol">)</a> <a id="3346" class="Symbol">(</a><a id="3347" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2245" class="Bound">relation</a> <a id="3356" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#3152" class="Bound">i</a><a id="3357" class="Symbol">)</a> <a id="3359" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1203" class="InductiveConstructor">var</a><a id="3362" class="Symbol">)</a>
         <a id="3372" href="Cubical.Foundations.Prelude.html#8310" class="Function">≡⟨</a> <a id="3375" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="3380" class="Symbol">(λ</a> <a id="3383" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#3383" class="Bound">u</a> <a id="3385" class="Symbol">→</a> <a id="3387" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="3391" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2803" class="Function">modRelations</a> <a id="3404" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#3383" class="Bound">u</a><a id="3405" class="Symbol">)</a> <a id="3407" class="Symbol">(</a><a id="3408" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1428" class="Function">evPolyPoly</a> <a id="3419" class="Symbol">(</a><a id="3420" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2245" class="Bound">relation</a> <a id="3429" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#3152" class="Bound">i</a><a id="3430" class="Symbol">))</a> <a id="3433" href="Cubical.Foundations.Prelude.html#8310" class="Function">⟩</a>
         <a id="3443" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="3447" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2803" class="Function">modRelations</a> <a id="3460" class="Symbol">(</a><a id="3461" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2245" class="Bound">relation</a> <a id="3470" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#3152" class="Bound">i</a><a id="3471" class="Symbol">)</a>
-        <a id="3481" href="Cubical.Foundations.Prelude.html#8310" class="Function">≡⟨</a> <a id="3484" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#8650" class="Function">isZeroFromIdeal</a> <a id="3500" class="Symbol">{</a><a id="3501" class="Argument">R</a> <a id="3503" class="Symbol">=</a> <a id="3505" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1158" class="Bound">R</a><a id="3506" class="Symbol">}</a>
+        <a id="3481" href="Cubical.Foundations.Prelude.html#8310" class="Function">≡⟨</a> <a id="3484" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#8932" class="Function">isZeroFromIdeal</a> <a id="3500" class="Symbol">{</a><a id="3501" class="Argument">R</a> <a id="3503" class="Symbol">=</a> <a id="3505" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1158" class="Bound">R</a><a id="3506" class="Symbol">}</a>
                            <a id="3535" class="Symbol">{</a><a id="3536" class="Argument">A</a> <a id="3538" class="Symbol">=</a> <a id="3540" class="Symbol">(</a><a id="3541" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1214" class="Function">Polynomials</a> <a id="3553" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2237" class="Bound">n</a><a id="3554" class="Symbol">)}</a>
                            <a id="3584" class="Symbol">{</a><a id="3585" class="Argument">I</a> <a id="3587" class="Symbol">=</a> <a id="3589" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2386" class="Function">relationsIdeal</a><a id="3603" class="Symbol">}</a>
                            <a id="3632" class="Symbol">(</a><a id="3633" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2245" class="Bound">relation</a> <a id="3642" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#3152" class="Bound">i</a><a id="3643" class="Symbol">)</a>
@@ -129,14 +129,14 @@
           <a id="4952" class="Symbol">→</a> <a id="4954" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="4958" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#4684" class="Function">inducedHom</a> <a id="4969" class="Symbol">(</a><a id="4970" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2953" class="Function">generator</a> <a id="4980" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#4931" class="Bound">i</a><a id="4981" class="Symbol">)</a> <a id="4983" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="4985" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#3799" class="Bound">values</a> <a id="4992" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#4931" class="Bound">i</a>
         <a id="5002" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#4895" class="Function">inducedHomOnGenerators</a> <a id="5025" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#5025" class="Bound">i</a> <a id="5027" class="Symbol">=</a>
           <a id="5039" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="5044" class="Symbol">(λ</a> <a id="5047" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#5047" class="Bound">f</a> <a id="5049" class="Symbol">→</a> <a id="5051" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="5055" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#5047" class="Bound">f</a> <a id="5057" class="Symbol">(</a><a id="5058" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#1203" class="InductiveConstructor">var</a> <a id="5062" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#5025" class="Bound">i</a><a id="5063" class="Symbol">))</a>
-          <a id="5076" class="Symbol">(</a><a id="5077" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#6299" class="Function">inducedHom∘quotientHom</a> <a id="5100" class="Symbol">(</a><a id="5101" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1214" class="Function">Polynomials</a> <a id="5113" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2237" class="Bound">n</a><a id="5114" class="Symbol">)</a> <a id="5116" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2386" class="Function">relationsIdeal</a> <a id="5131" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#3769" class="Bound">A</a> <a id="5133" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#4218" class="Function">freeHom</a> <a id="5141" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#4316" class="Function">isInKernel</a><a id="5151" class="Symbol">)</a>
+          <a id="5076" class="Symbol">(</a><a id="5077" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#6435" class="Function">inducedHom∘quotientHom</a> <a id="5100" class="Symbol">(</a><a id="5101" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1214" class="Function">Polynomials</a> <a id="5113" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2237" class="Bound">n</a><a id="5114" class="Symbol">)</a> <a id="5116" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2386" class="Function">relationsIdeal</a> <a id="5131" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#3769" class="Bound">A</a> <a id="5133" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#4218" class="Function">freeHom</a> <a id="5141" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#4316" class="Function">isInKernel</a><a id="5151" class="Symbol">)</a>
 
         <a id="5162" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#5162" class="Function">unique</a> <a id="5169" class="Symbol">:</a>
              <a id="5184" class="Symbol">(</a><a id="5185" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#5185" class="Bound">f</a> <a id="5187" class="Symbol">:</a> <a id="5189" href="Cubical.Algebra.CommAlgebra.Base.html#7059" class="Function">CommAlgebraHom</a> <a id="5204" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2719" class="Function">FPAlgebra</a> <a id="5214" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#3769" class="Bound">A</a><a id="5215" class="Symbol">)</a>
              <a id="5230" class="Symbol">→</a> <a id="5232" class="Symbol">((</a><a id="5234" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#5234" class="Bound">i</a> <a id="5236" class="Symbol">:</a> <a id="5238" href="Cubical.Data.FinData.Base.html#375" class="Datatype">Fin</a> <a id="5242" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2237" class="Bound">n</a><a id="5243" class="Symbol">)</a> <a id="5245" class="Symbol">→</a> <a id="5247" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="5251" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#5185" class="Bound">f</a> <a id="5253" class="Symbol">(</a><a id="5254" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2953" class="Function">generator</a> <a id="5264" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#5234" class="Bound">i</a><a id="5265" class="Symbol">)</a> <a id="5267" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="5269" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#3799" class="Bound">values</a> <a id="5276" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#5234" class="Bound">i</a><a id="5277" class="Symbol">)</a>
              <a id="5292" class="Symbol">→</a> <a id="5294" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#4684" class="Function">inducedHom</a> <a id="5305" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="5307" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#5185" class="Bound">f</a>
         <a id="5317" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#5162" class="Function">unique</a> <a id="5324" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#5324" class="Bound">f</a> <a id="5326" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#5326" class="Bound">hasCorrectValues</a> <a id="5343" class="Symbol">=</a>
-          <a id="5355" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#6460" class="Function">injectivePrecomp</a>
+          <a id="5355" href="Cubical.Algebra.CommAlgebra.QuotientAlgebra.html#6636" class="Function">injectivePrecomp</a>
             <a id="5384" class="Symbol">(</a><a id="5385" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1214" class="Function">Polynomials</a> <a id="5397" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2237" class="Bound">n</a><a id="5398" class="Symbol">)</a>
             <a id="5412" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2386" class="Function">relationsIdeal</a>
             <a id="5439" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#3769" class="Bound">A</a>