Deploying to gh-pages from @ 4b91241 🚀

agda · Sep 21, 2023 · 5b68690 · 5b68690
1 parent 3857027
commit 5b68690
Show file tree

Hide file tree

Showing 169 changed files with 1,259 additions and 1,259 deletions.
diff --git a/Cubical.Algebra.AbGroup.Base.html b/Cubical.Algebra.AbGroup.Base.html
@@ -76,7 +76,7 @@
   <a id="1748" class="Keyword">open</a> <a id="1753" href="Cubical.Algebra.AbGroup.Base.html#956" class="Module">IsAbGroup</a> <a id="1763" href="Cubical.Algebra.AbGroup.Base.html#1682" class="Field">isAbGroup</a> <a id="1773" class="Keyword">public</a>
 
 <a id="AbGroup"></a><a id="1781" href="Cubical.Algebra.AbGroup.Base.html#1781" class="Function">AbGroup</a> <a id="1789" class="Symbol">:</a> <a id="1791" class="Symbol">∀</a> <a id="1793" href="Cubical.Algebra.AbGroup.Base.html#1793" class="Bound">ℓ</a> <a id="1795" class="Symbol">→</a> <a id="1797" href="Agda.Primitive.html#320" class="Primitive">Type</a> <a id="1802" class="Symbol">(</a><a id="1803" href="Agda.Primitive.html#774" class="Primitive">ℓ-suc</a> <a id="1809" href="Cubical.Algebra.AbGroup.Base.html#1793" class="Bound">ℓ</a><a id="1810" class="Symbol">)</a>
-<a id="1812" href="Cubical.Algebra.AbGroup.Base.html#1781" class="Function">AbGroup</a> <a id="1820" href="Cubical.Algebra.AbGroup.Base.html#1820" class="Bound">ℓ</a> <a id="1822" class="Symbol">=</a> <a id="1824" href="Cubical.Foundations.Structure.html#398" class="Function">TypeWithStr</a> <a id="1836" href="Cubical.Algebra.AbGroup.Base.html#1820" class="Bound">ℓ</a> <a id="1838" href="Cubical.Algebra.AbGroup.Base.html#1530" class="Record">AbGroupStr</a>
+<a id="1812" href="Cubical.Algebra.AbGroup.Base.html#1781" class="Function">AbGroup</a> <a id="1820" href="Cubical.Algebra.AbGroup.Base.html#1820" class="Bound">ℓ</a> <a id="1822" class="Symbol">=</a> <a id="1824" href="Cubical.Foundations.Structure.html#399" class="Function">TypeWithStr</a> <a id="1836" href="Cubical.Algebra.AbGroup.Base.html#1820" class="Bound">ℓ</a> <a id="1838" href="Cubical.Algebra.AbGroup.Base.html#1530" class="Record">AbGroupStr</a>
 
 <a id="1850" class="Keyword">module</a> <a id="1857" href="Cubical.Algebra.AbGroup.Base.html#1857" class="Module">_</a> <a id="1859" class="Symbol">{</a><a id="1860" href="Cubical.Algebra.AbGroup.Base.html#1860" class="Bound">G</a> <a id="1862" class="Symbol">:</a> <a id="1864" href="Agda.Primitive.html#320" class="Primitive">Type</a> <a id="1869" href="Cubical.Algebra.AbGroup.Base.html#935" class="Generalizable">ℓ</a><a id="1870" class="Symbol">}</a> <a id="1872" class="Symbol">{</a><a id="1873" href="Cubical.Algebra.AbGroup.Base.html#1873" class="Bound">0g</a> <a id="1876" class="Symbol">:</a> <a id="1878" href="Cubical.Algebra.AbGroup.Base.html#1860" class="Bound">G</a><a id="1879" class="Symbol">}</a> <a id="1881" class="Symbol">{</a><a id="1882" href="Cubical.Algebra.AbGroup.Base.html#1882" class="Bound Operator">_+_</a> <a id="1886" class="Symbol">:</a> <a id="1888" href="Cubical.Algebra.AbGroup.Base.html#1860" class="Bound">G</a> <a id="1890" class="Symbol">→</a> <a id="1892" href="Cubical.Algebra.AbGroup.Base.html#1860" class="Bound">G</a> <a id="1894" class="Symbol">→</a> <a id="1896" href="Cubical.Algebra.AbGroup.Base.html#1860" class="Bound">G</a><a id="1897" class="Symbol">}</a> <a id="1899" class="Symbol">{</a> <a id="1901" href="Cubical.Algebra.AbGroup.Base.html#1901" class="Bound Operator">-_</a> <a id="1904" class="Symbol">:</a> <a id="1906" href="Cubical.Algebra.AbGroup.Base.html#1860" class="Bound">G</a> <a id="1908" class="Symbol">→</a> <a id="1910" href="Cubical.Algebra.AbGroup.Base.html#1860" class="Bound">G</a><a id="1911" class="Symbol">}</a>
          <a id="1922" class="Symbol">(</a><a id="1923" href="Cubical.Algebra.AbGroup.Base.html#1923" class="Bound">is-setG</a> <a id="1931" class="Symbol">:</a> <a id="1933" href="Cubical.Foundations.Prelude.html#14300" class="Function">isSet</a> <a id="1939" href="Cubical.Algebra.AbGroup.Base.html#1860" class="Bound">G</a><a id="1940" class="Symbol">)</a>
@@ -189,7 +189,7 @@
   <a id="6119" class="Symbol">(</a><a id="6120" href="Cubical.Algebra.AbGroup.Base.html#6120" class="Bound">m</a> <a id="6122" class="Symbol">:</a> <a id="6124" href="Cubical.Algebra.AbGroup.Base.html#6105" class="Bound">A</a> <a id="6126" class="Symbol">→</a> <a id="6128" href="Cubical.Algebra.AbGroup.Base.html#6105" class="Bound">A</a> <a id="6130" class="Symbol">→</a> <a id="6132" href="Cubical.Algebra.AbGroup.Base.html#6105" class="Bound">A</a><a id="6133" class="Symbol">)</a>
   <a id="6137" class="Symbol">(</a><a id="6138" href="Cubical.Algebra.AbGroup.Base.html#6138" class="Bound">u</a> <a id="6140" class="Symbol">:</a> <a id="6142" href="Cubical.Algebra.AbGroup.Base.html#6105" class="Bound">A</a><a id="6143" class="Symbol">)</a>
   <a id="6147" class="Symbol">(</a><a id="6148" href="Cubical.Algebra.AbGroup.Base.html#6148" class="Bound">inverse</a> <a id="6156" class="Symbol">:</a> <a id="6158" href="Cubical.Algebra.AbGroup.Base.html#6105" class="Bound">A</a> <a id="6160" class="Symbol">→</a> <a id="6162" href="Cubical.Algebra.AbGroup.Base.html#6105" class="Bound">A</a><a id="6163" class="Symbol">)</a>
-  <a id="6167" class="Symbol">(</a><a id="6168" href="Cubical.Algebra.AbGroup.Base.html#6168" class="Bound">e</a> <a id="6170" class="Symbol">:</a> <a id="6172" href="Cubical.Foundations.Structure.html#639" class="Function Operator">⟨</a> <a id="6174" href="Cubical.Algebra.AbGroup.Base.html#6089" class="Bound">G</a> <a id="6176" href="Cubical.Foundations.Structure.html#639" class="Function Operator">⟩</a> <a id="6178" href="Agda.Builtin.Cubical.Glue.html#1005" class="Function Operator">≃</a> <a id="6180" href="Cubical.Algebra.AbGroup.Base.html#6105" class="Bound">A</a><a id="6181" class="Symbol">)</a>
+  <a id="6167" class="Symbol">(</a><a id="6168" href="Cubical.Algebra.AbGroup.Base.html#6168" class="Bound">e</a> <a id="6170" class="Symbol">:</a> <a id="6172" href="Cubical.Foundations.Structure.html#640" class="Function Operator">⟨</a> <a id="6174" href="Cubical.Algebra.AbGroup.Base.html#6089" class="Bound">G</a> <a id="6176" href="Cubical.Foundations.Structure.html#640" class="Function Operator">⟩</a> <a id="6178" href="Agda.Builtin.Cubical.Glue.html#1005" class="Function Operator">≃</a> <a id="6180" href="Cubical.Algebra.AbGroup.Base.html#6105" class="Bound">A</a><a id="6181" class="Symbol">)</a>
   <a id="6185" class="Symbol">(</a><a id="6186" href="Cubical.Algebra.AbGroup.Base.html#6186" class="Bound">p+</a> <a id="6189" class="Symbol">:</a> <a id="6191" class="Symbol">∀</a> <a id="6193" href="Cubical.Algebra.AbGroup.Base.html#6193" class="Bound">x</a> <a id="6195" href="Cubical.Algebra.AbGroup.Base.html#6195" class="Bound">y</a> <a id="6197" class="Symbol">→</a> <a id="6199" href="Cubical.Algebra.AbGroup.Base.html#6168" class="Bound">e</a> <a id="6201" class="Symbol">.</a><a id="6202" href="Agda.Builtin.Sigma.html#234" class="Field">fst</a> <a id="6206" class="Symbol">(</a><a id="6207" href="Cubical.Algebra.AbGroup.Base.html#6089" class="Bound">G</a> <a id="6209" class="Symbol">.</a><a id="6210" href="Agda.Builtin.Sigma.html#246" class="Field">snd</a> <a id="6214" class="Symbol">.</a><a id="6215" href="Cubical.Algebra.AbGroup.Base.html#1634" class="Field Operator">_+_</a> <a id="6219" href="Cubical.Algebra.AbGroup.Base.html#6193" class="Bound">x</a> <a id="6221" href="Cubical.Algebra.AbGroup.Base.html#6195" class="Bound">y</a><a id="6222" class="Symbol">)</a> <a id="6224" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="6226" href="Cubical.Algebra.AbGroup.Base.html#6120" class="Bound">m</a> <a id="6228" class="Symbol">(</a><a id="6229" href="Cubical.Algebra.AbGroup.Base.html#6168" class="Bound">e</a> <a id="6231" class="Symbol">.</a><a id="6232" href="Agda.Builtin.Sigma.html#234" class="Field">fst</a> <a id="6236" href="Cubical.Algebra.AbGroup.Base.html#6193" class="Bound">x</a><a id="6237" class="Symbol">)</a> <a id="6239" class="Symbol">(</a><a id="6240" href="Cubical.Algebra.AbGroup.Base.html#6168" class="Bound">e</a> <a id="6242" class="Symbol">.</a><a id="6243" href="Agda.Builtin.Sigma.html#234" class="Field">fst</a> <a id="6247" href="Cubical.Algebra.AbGroup.Base.html#6195" class="Bound">y</a><a id="6248" class="Symbol">))</a>
   <a id="6253" class="Symbol">(</a><a id="6254" href="Cubical.Algebra.AbGroup.Base.html#6254" class="Bound">pu</a> <a id="6257" class="Symbol">:</a> <a id="6259" href="Cubical.Algebra.AbGroup.Base.html#6168" class="Bound">e</a> <a id="6261" class="Symbol">.</a><a id="6262" href="Agda.Builtin.Sigma.html#234" class="Field">fst</a> <a id="6266" class="Symbol">(</a><a id="6267" href="Cubical.Algebra.AbGroup.Base.html#6089" class="Bound">G</a> <a id="6269" class="Symbol">.</a><a id="6270" href="Agda.Builtin.Sigma.html#246" class="Field">snd</a> <a id="6274" class="Symbol">.</a><a id="6275" href="Cubical.Algebra.AbGroup.Base.html#1616" class="Field">0g</a><a id="6277" class="Symbol">)</a> <a id="6279" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="6281" href="Cubical.Algebra.AbGroup.Base.html#6138" class="Bound">u</a><a id="6282" class="Symbol">)</a>
   <a id="6286" class="Symbol">(</a><a id="6287" href="Cubical.Algebra.AbGroup.Base.html#6287" class="Bound">pinv</a> <a id="6292" class="Symbol">:</a> <a id="6294" class="Symbol">∀</a> <a id="6296" href="Cubical.Algebra.AbGroup.Base.html#6296" class="Bound">x</a> <a id="6298" class="Symbol">→</a> <a id="6300" href="Cubical.Algebra.AbGroup.Base.html#6168" class="Bound">e</a> <a id="6302" class="Symbol">.</a><a id="6303" href="Agda.Builtin.Sigma.html#234" class="Field">fst</a> <a id="6307" class="Symbol">(</a><a id="6308" href="Cubical.Algebra.AbGroup.Base.html#6089" class="Bound">G</a> <a id="6310" class="Symbol">.</a><a id="6311" href="Agda.Builtin.Sigma.html#246" class="Field">snd</a> <a id="6315" class="Symbol">.</a><a id="6316" href="Cubical.Algebra.AbGroup.Base.html#1660" class="Field Operator">-_</a> <a id="6319" href="Cubical.Algebra.AbGroup.Base.html#6296" class="Bound">x</a><a id="6320" class="Symbol">)</a> <a id="6322" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="6324" href="Cubical.Algebra.AbGroup.Base.html#6148" class="Bound">inverse</a> <a id="6332" class="Symbol">(</a><a id="6333" href="Cubical.Algebra.AbGroup.Base.html#6168" class="Bound">e</a> <a id="6335" class="Symbol">.</a><a id="6336" href="Agda.Builtin.Sigma.html#234" class="Field">fst</a> <a id="6340" href="Cubical.Algebra.AbGroup.Base.html#6296" class="Bound">x</a><a id="6341" class="Symbol">))</a>
@@ -235,7 +235,7 @@
 <a id="7552" class="Comment">-- over the unit and inverse from G to A.</a>
 <a id="7594" class="Keyword">module</a> <a id="7601" href="Cubical.Algebra.AbGroup.Base.html#7601" class="Module">_</a> <a id="7603" class="Symbol">(</a><a id="7604" href="Cubical.Algebra.AbGroup.Base.html#7604" class="Bound">G</a> <a id="7606" class="Symbol">:</a> <a id="7608" href="Cubical.Algebra.AbGroup.Base.html#1781" class="Function">AbGroup</a> <a id="7616" href="Cubical.Algebra.AbGroup.Base.html#935" class="Generalizable">ℓ</a><a id="7617" class="Symbol">)</a> <a id="7619" class="Symbol">{</a><a id="7620" href="Cubical.Algebra.AbGroup.Base.html#7620" class="Bound">A</a> <a id="7622" class="Symbol">:</a> <a id="7624" href="Agda.Primitive.html#320" class="Primitive">Type</a> <a id="7629" href="Cubical.Algebra.AbGroup.Base.html#935" class="Generalizable">ℓ</a><a id="7630" class="Symbol">}</a>
   <a id="7634" class="Symbol">(</a><a id="7635" href="Cubical.Algebra.AbGroup.Base.html#7635" class="Bound">m</a> <a id="7637" class="Symbol">:</a> <a id="7639" href="Cubical.Algebra.AbGroup.Base.html#7620" class="Bound">A</a> <a id="7641" class="Symbol">→</a> <a id="7643" href="Cubical.Algebra.AbGroup.Base.html#7620" class="Bound">A</a> <a id="7645" class="Symbol">→</a> <a id="7647" href="Cubical.Algebra.AbGroup.Base.html#7620" class="Bound">A</a><a id="7648" class="Symbol">)</a>
-  <a id="7652" class="Symbol">(</a><a id="7653" href="Cubical.Algebra.AbGroup.Base.html#7653" class="Bound">e</a> <a id="7655" class="Symbol">:</a> <a id="7657" href="Cubical.Foundations.Structure.html#639" class="Function Operator">⟨</a> <a id="7659" href="Cubical.Algebra.AbGroup.Base.html#7604" class="Bound">G</a> <a id="7661" href="Cubical.Foundations.Structure.html#639" class="Function Operator">⟩</a> <a id="7663" href="Agda.Builtin.Cubical.Glue.html#1005" class="Function Operator">≃</a> <a id="7665" href="Cubical.Algebra.AbGroup.Base.html#7620" class="Bound">A</a><a id="7666" class="Symbol">)</a>
+  <a id="7652" class="Symbol">(</a><a id="7653" href="Cubical.Algebra.AbGroup.Base.html#7653" class="Bound">e</a> <a id="7655" class="Symbol">:</a> <a id="7657" href="Cubical.Foundations.Structure.html#640" class="Function Operator">⟨</a> <a id="7659" href="Cubical.Algebra.AbGroup.Base.html#7604" class="Bound">G</a> <a id="7661" href="Cubical.Foundations.Structure.html#640" class="Function Operator">⟩</a> <a id="7663" href="Agda.Builtin.Cubical.Glue.html#1005" class="Function Operator">≃</a> <a id="7665" href="Cubical.Algebra.AbGroup.Base.html#7620" class="Bound">A</a><a id="7666" class="Symbol">)</a>
   <a id="7670" class="Symbol">(</a><a id="7671" href="Cubical.Algebra.AbGroup.Base.html#7671" class="Bound">p·</a> <a id="7674" class="Symbol">:</a> <a id="7676" class="Symbol">∀</a> <a id="7678" href="Cubical.Algebra.AbGroup.Base.html#7678" class="Bound">x</a> <a id="7680" href="Cubical.Algebra.AbGroup.Base.html#7680" class="Bound">y</a> <a id="7682" class="Symbol">→</a> <a id="7684" href="Cubical.Algebra.AbGroup.Base.html#7653" class="Bound">e</a> <a id="7686" class="Symbol">.</a><a id="7687" href="Agda.Builtin.Sigma.html#234" class="Field">fst</a> <a id="7691" class="Symbol">(</a><a id="7692" href="Cubical.Algebra.AbGroup.Base.html#7604" class="Bound">G</a> <a id="7694" class="Symbol">.</a><a id="7695" href="Agda.Builtin.Sigma.html#246" class="Field">snd</a> <a id="7699" class="Symbol">.</a><a id="7700" href="Cubical.Algebra.AbGroup.Base.html#1634" class="Field Operator">_+_</a> <a id="7704" href="Cubical.Algebra.AbGroup.Base.html#7678" class="Bound">x</a> <a id="7706" href="Cubical.Algebra.AbGroup.Base.html#7680" class="Bound">y</a><a id="7707" class="Symbol">)</a> <a id="7709" href="Agda.Builtin.Cubical.Path.html#272" class="Function Operator">≡</a> <a id="7711" href="Cubical.Algebra.AbGroup.Base.html#7635" class="Bound">m</a> <a id="7713" class="Symbol">(</a><a id="7714" href="Cubical.Algebra.AbGroup.Base.html#7653" class="Bound">e</a> <a id="7716" class="Symbol">.</a><a id="7717" href="Agda.Builtin.Sigma.html#234" class="Field">fst</a> <a id="7721" href="Cubical.Algebra.AbGroup.Base.html#7678" class="Bound">x</a><a id="7722" class="Symbol">)</a> <a id="7724" class="Symbol">(</a><a id="7725" href="Cubical.Algebra.AbGroup.Base.html#7653" class="Bound">e</a> <a id="7727" class="Symbol">.</a><a id="7728" href="Agda.Builtin.Sigma.html#234" class="Field">fst</a> <a id="7732" href="Cubical.Algebra.AbGroup.Base.html#7680" class="Bound">y</a><a id="7733" class="Symbol">))</a>
   <a id="7738" class="Keyword">where</a>