Deploying to gh-pages from @ 00f0193 🚀

agda · Nov 28, 2024 · 680ac6f · 680ac6f
1 parent ad6a2ed
commit 680ac6f
Show file tree

Hide file tree

Showing 146 changed files with 780 additions and 775 deletions.
diff --git a/Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html b/Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html
@@ -301,7 +301,7 @@
 <a id="11943" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#11858" class="Function">ℤFin→Free→ℤFin</a> <a id="11958" href="Agda.Builtin.Nat.html#221" class="InductiveConstructor">zero</a> <a id="11963" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#11963" class="Bound">x</a> <a id="11965" class="Symbol">=</a> <a id="11967" href="Cubical.Foundations.Prelude.html#19771" class="Function">isContr→isProp</a> <a id="11982" class="Symbol">(</a><a id="11983" href="Cubical.Foundations.Prelude.html#10228" class="Function">subst</a> <a id="11989" class="Symbol">(</a><a id="11990" href="Cubical.Foundations.Prelude.html#15483" class="Function">isContr</a> <a id="11998" href="Cubical.Foundations.Function.html#665" class="Function Operator">∘</a> <a id="12000" href="Cubical.HITs.FreeAbGroup.Base.html#484" class="Datatype">FreeAbGroup</a><a id="12011" class="Symbol">)</a> <a id="12013" class="Symbol">(</a><a id="12014" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="12018" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#12052" class="Function">lem</a><a id="12021" class="Symbol">)</a> <a id="12023" href="Cubical.HITs.FreeAbGroup.Base.html#3175" class="Function">isContr-Free⊥</a><a id="12036" class="Symbol">)</a> <a id="12038" class="Symbol">_</a> <a id="12040" class="Symbol">_</a>
   <a id="12044" class="Keyword">where</a>
   <a id="12052" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#12052" class="Function">lem</a> <a id="12056" class="Symbol">:</a> <a id="12058" href="Cubical.Data.Fin.Inductive.Base.html#453" class="Function">Fin</a> <a id="12062" class="Number">0</a> <a id="12064" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="12066" href="Cubical.Data.Empty.Base.html#145" class="Datatype">⊥</a>
-  <a id="12070" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#12052" class="Function">lem</a> <a id="12074" class="Symbol">=</a> <a id="12076" href="Cubical.Foundations.Isomorphism.html#3553" class="Function">isoToPath</a> <a id="12086" class="Symbol">(</a><a id="12087" href="Cubical.Foundations.Isomorphism.html#863" class="InductiveConstructor">iso</a> <a id="12091" href="Cubical.Data.Fin.Inductive.Properties.html#2530" class="Function">¬Fin0</a> <a id="12097" class="Symbol">(λ{()})</a> <a id="12105" class="Symbol">(λ{()})</a> <a id="12113" class="Symbol">λ</a> <a id="12115" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#12115" class="Bound">p</a> <a id="12117" class="Symbol">→</a> <a id="12119" href="Cubical.Data.Empty.Base.html#187" class="Function">⊥.rec</a> <a id="12125" class="Symbol">(</a><a id="12126" href="Cubical.Data.Fin.Inductive.Properties.html#2530" class="Function">¬Fin0</a> <a id="12132" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#12115" class="Bound">p</a><a id="12133" class="Symbol">))</a>
+  <a id="12070" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#12052" class="Function">lem</a> <a id="12074" class="Symbol">=</a> <a id="12076" href="Cubical.Foundations.Isomorphism.html#3714" class="Function">isoToPath</a> <a id="12086" class="Symbol">(</a><a id="12087" href="Cubical.Foundations.Isomorphism.html#863" class="InductiveConstructor">iso</a> <a id="12091" href="Cubical.Data.Fin.Inductive.Properties.html#2530" class="Function">¬Fin0</a> <a id="12097" class="Symbol">(λ{()})</a> <a id="12105" class="Symbol">(λ{()})</a> <a id="12113" class="Symbol">λ</a> <a id="12115" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#12115" class="Bound">p</a> <a id="12117" class="Symbol">→</a> <a id="12119" href="Cubical.Data.Empty.Base.html#187" class="Function">⊥.rec</a> <a id="12125" class="Symbol">(</a><a id="12126" href="Cubical.Data.Fin.Inductive.Properties.html#2530" class="Function">¬Fin0</a> <a id="12132" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#12115" class="Bound">p</a><a id="12133" class="Symbol">))</a>
 <a id="12136" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#11858" class="Function">ℤFin→Free→ℤFin</a> <a id="12151" class="Symbol">(</a><a id="12152" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="12156" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#12156" class="Bound">n</a><a id="12157" class="Symbol">)</a> <a id="12159" class="Symbol">=</a>
   <a id="12163" href="Cubical.HITs.FreeAbGroup.Base.html#2229" class="Function">ElimProp.f</a> <a id="12174" class="Symbol">(</a><a id="12175" href="Cubical.HITs.FreeAbGroup.Base.html#864" class="InductiveConstructor">trunc</a> <a id="12181" class="Symbol">_</a> <a id="12183" class="Symbol">_)</a>
     <a id="12190" class="Symbol">(</a><a id="12191" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#11119" class="Function">ℤFin→Free-ℤFinGenerator</a> <a id="12215" class="Symbol">(</a><a id="12216" href="Agda.Builtin.Nat.html#234" class="InductiveConstructor">suc</a> <a id="12220" href="Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html#12156" class="Bound">n</a><a id="12221" class="Symbol">))</a>

diff --git a/Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html b/Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html
@@ -234,7 +234,7 @@
                              <a id="9895" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#9667" class="Bound">i</a><a id="9896" class="Symbol">)</a>
 
       <a id="9905" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#9905" class="Function">homMapPathFP</a> <a id="9918" class="Symbol">:</a> <a id="9920" class="Symbol">(</a><a id="9921" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#9921" class="Bound">A</a> <a id="9923" class="Symbol">:</a> <a id="9925" href="Cubical.Algebra.CommAlgebra.Base.html#1625" class="Function">CommAlgebra</a> <a id="9937" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1158" class="Bound">R</a> <a id="9939" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1171" class="Bound">ℓ</a><a id="9940" class="Symbol">)→</a> <a id="9943" href="Cubical.Algebra.CommAlgebra.Base.html#7059" class="Function">CommAlgebraHom</a> <a id="9958" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#2719" class="Function">FPAlgebra</a> <a id="9968" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#9921" class="Bound">A</a> <a id="9970" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="9972" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#7101" class="Function">zeroLocus</a> <a id="9982" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#9921" class="Bound">A</a>
-      <a id="9990" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#9905" class="Function">homMapPathFP</a> <a id="10003" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#10003" class="Bound">A</a> <a id="10005" class="Symbol">=</a> <a id="10007" href="Cubical.Foundations.Isomorphism.html#3553" class="Function">isoToPath</a> <a id="10017" class="Symbol">(</a><a id="10018" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#9018" class="Function">FPHomIso</a> <a id="10027" class="Symbol">{</a><a id="10028" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#10003" class="Bound">A</a><a id="10029" class="Symbol">})</a>
+      <a id="9990" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#9905" class="Function">homMapPathFP</a> <a id="10003" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#10003" class="Bound">A</a> <a id="10005" class="Symbol">=</a> <a id="10007" href="Cubical.Foundations.Isomorphism.html#3714" class="Function">isoToPath</a> <a id="10017" class="Symbol">(</a><a id="10018" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#9018" class="Function">FPHomIso</a> <a id="10027" class="Symbol">{</a><a id="10028" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#10003" class="Bound">A</a><a id="10029" class="Symbol">})</a>
 
       <a id="10039" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#10039" class="Function">isSetZeroLocus</a> <a id="10054" class="Symbol">:</a> <a id="10056" class="Symbol">(</a><a id="10057" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#10057" class="Bound">A</a> <a id="10059" class="Symbol">:</a> <a id="10061" href="Cubical.Algebra.CommAlgebra.Base.html#1625" class="Function">CommAlgebra</a> <a id="10073" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1158" class="Bound">R</a> <a id="10075" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#1171" class="Bound">ℓ</a><a id="10076" class="Symbol">)</a> <a id="10078" class="Symbol">→</a> <a id="10080" href="Cubical.Foundations.Prelude.html#15602" class="Function">isSet</a> <a id="10086" class="Symbol">(</a><a id="10087" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#7101" class="Function">zeroLocus</a> <a id="10097" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#10057" class="Bound">A</a><a id="10098" class="Symbol">)</a>
       <a id="10106" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#10039" class="Function">isSetZeroLocus</a> <a id="10121" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#10121" class="Bound">A</a> <a id="10123" class="Symbol">=</a>  <a id="10126" href="Cubical.Foundations.Prelude.html#12692" class="Function">J</a> <a id="10128" class="Symbol">(λ</a> <a id="10131" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#10131" class="Bound">y</a> <a id="10133" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#10133" class="Bound">_</a> <a id="10135" class="Symbol">→</a> <a id="10137" href="Cubical.Foundations.Prelude.html#15602" class="Function">isSet</a> <a id="10143" href="Cubical.Algebra.CommAlgebra.FPAlgebra.Base.html#10131" class="Bound">y</a><a id="10144" class="Symbol">)</a>

diff --git a/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html b/Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html
@@ -294,7 +294,7 @@
 
 <a id="homMapPath"></a><a id="10492" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10492" class="Function">homMapPath</a> <a id="10503" class="Symbol">:</a> <a id="10505" class="Symbol">{</a><a id="10506" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10506" class="Bound">R</a> <a id="10508" class="Symbol">:</a> <a id="10510" href="Cubical.Algebra.CommRing.Base.html#1279" class="Function">CommRing</a> <a id="10519" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#1595" class="Generalizable">ℓ</a><a id="10520" class="Symbol">}</a> <a id="10522" class="Symbol">{</a><a id="10523" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10523" class="Bound">I</a> <a id="10525" class="Symbol">:</a> <a id="10527" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="10532" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#1597" class="Generalizable">ℓ&#39;</a><a id="10534" class="Symbol">}</a> <a id="10536" class="Symbol">(</a><a id="10537" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10537" class="Bound">A</a> <a id="10539" class="Symbol">:</a> <a id="10541" href="Cubical.Algebra.CommAlgebra.Base.html#1625" class="Function">CommAlgebra</a> <a id="10553" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10506" class="Bound">R</a> <a id="10555" class="Symbol">(</a><a id="10556" href="Agda.Primitive.html#961" class="Primitive">ℓ-max</a> <a id="10562" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#1595" class="Generalizable">ℓ</a> <a id="10564" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#1597" class="Generalizable">ℓ&#39;</a><a id="10566" class="Symbol">))</a>
              <a id="10582" class="Symbol">→</a> <a id="10584" href="Cubical.Algebra.CommAlgebra.Base.html#7059" class="Function">CommAlgebraHom</a> <a id="10599" class="Symbol">(</a><a id="10600" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10506" class="Bound">R</a> <a id="10602" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#3710" class="Function Operator">[</a> <a id="10604" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10523" class="Bound">I</a> <a id="10606" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Base.html#3710" class="Function Operator">]</a><a id="10607" class="Symbol">)</a> <a id="10609" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10537" class="Bound">A</a> <a id="10611" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="10613" class="Symbol">(</a><a id="10614" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10523" class="Bound">I</a> <a id="10616" class="Symbol">→</a> <a id="10618" href="Agda.Builtin.Sigma.html#251" class="Field">fst</a> <a id="10622" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10537" class="Bound">A</a><a id="10623" class="Symbol">)</a>
-<a id="10625" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10492" class="Function">homMapPath</a> <a id="10636" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10636" class="Bound">A</a> <a id="10638" class="Symbol">=</a> <a id="10640" href="Cubical.Foundations.Isomorphism.html#3553" class="Function">isoToPath</a> <a id="10650" class="Symbol">(</a><a id="10651" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#9769" class="Function">homMapIso</a> <a id="10661" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10636" class="Bound">A</a><a id="10662" class="Symbol">)</a>
+<a id="10625" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10492" class="Function">homMapPath</a> <a id="10636" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10636" class="Bound">A</a> <a id="10638" class="Symbol">=</a> <a id="10640" href="Cubical.Foundations.Isomorphism.html#3714" class="Function">isoToPath</a> <a id="10650" class="Symbol">(</a><a id="10651" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#9769" class="Function">homMapIso</a> <a id="10661" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10636" class="Bound">A</a><a id="10662" class="Symbol">)</a>
 
 <a id="10665" class="Comment">{- Corollary: Two homomorphisms with the same values on generators are equal -}</a>
 <a id="equalByUMP"></a><a id="10745" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10745" class="Function">equalByUMP</a> <a id="10756" class="Symbol">:</a> <a id="10758" class="Symbol">{</a><a id="10759" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10759" class="Bound">R</a> <a id="10761" class="Symbol">:</a> <a id="10763" href="Cubical.Algebra.CommRing.Base.html#1279" class="Function">CommRing</a> <a id="10772" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#1595" class="Generalizable">ℓ</a><a id="10773" class="Symbol">}</a> <a id="10775" class="Symbol">{</a><a id="10776" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#10776" class="Bound">I</a> <a id="10778" class="Symbol">:</a> <a id="10780" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="10785" href="Cubical.Algebra.CommAlgebra.FreeCommAlgebra.Properties.html#1597" class="Generalizable">ℓ&#39;</a><a id="10787" class="Symbol">}</a>

diff --git a/Cubical.Algebra.CommAlgebra.Instances.Initial.html b/Cubical.Algebra.CommAlgebra.Instances.Initial.html
@@ -93,7 +93,7 @@
                         <a id="3281" class="Symbol">λ</a> <a id="3283" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#3283" class="Bound">f</a> <a id="3285" class="Symbol">→</a> <a id="3287" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="3291" class="Symbol">(</a><a id="3292" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#2232" class="Function">initialMapEq</a> <a id="3305" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#3283" class="Bound">f</a><a id="3306" class="Symbol">)</a>
 
     <a id="3313" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#3313" class="Function">initialityPath</a> <a id="3328" class="Symbol">:</a> <a id="3330" href="Cubical.Algebra.CommAlgebra.Base.html#7059" class="Function">CommAlgebraHom</a> <a id="3345" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#695" class="Function">initialCAlg</a> <a id="3357" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#1385" class="Bound">A</a> <a id="3359" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="3361" href="Cubical.Data.Unit.Base.html#212" class="Function">Unit*</a>
-    <a id="3371" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#3313" class="Function">initialityPath</a> <a id="3386" class="Symbol">=</a> <a id="3388" href="Cubical.Foundations.Isomorphism.html#3553" class="Function">isoToPath</a> <a id="3398" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#3069" class="Function">initialityIso</a>
+    <a id="3371" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#3313" class="Function">initialityPath</a> <a id="3386" class="Symbol">=</a> <a id="3388" href="Cubical.Foundations.Isomorphism.html#3714" class="Function">isoToPath</a> <a id="3398" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#3069" class="Function">initialityIso</a>
 
     <a id="3417" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#3417" class="Function">initialityContr</a> <a id="3433" class="Symbol">:</a> <a id="3435" href="Cubical.Foundations.Prelude.html#15483" class="Function">isContr</a> <a id="3443" class="Symbol">(</a><a id="3444" href="Cubical.Algebra.CommAlgebra.Base.html#7059" class="Function">CommAlgebraHom</a> <a id="3459" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#695" class="Function">initialCAlg</a> <a id="3471" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#1385" class="Bound">A</a><a id="3472" class="Symbol">)</a>
     <a id="3478" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#3417" class="Function">initialityContr</a> <a id="3494" class="Symbol">=</a> <a id="3496" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#1675" class="Function">initialMap</a> <a id="3507" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="3509" class="Symbol">λ</a> <a id="3511" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#3511" class="Bound">ϕ</a> <a id="3513" class="Symbol">→</a> <a id="3515" href="Cubical.Foundations.Prelude.html#968" class="Function">sym</a> <a id="3519" class="Symbol">(</a><a id="3520" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#2232" class="Function">initialMapEq</a> <a id="3533" href="Cubical.Algebra.CommAlgebra.Instances.Initial.html#3511" class="Bound">ϕ</a><a id="3534" class="Symbol">)</a>