Deploying to gh-pages from @ ba0a562 🚀

agda · Jul 24, 2024 · 6de6427 · 6de6427
1 parent 1cc80cc
commit 6de6427
Show file tree

Hide file tree

Showing 161 changed files with 686 additions and 686 deletions.
diff --git a/Cubical.Algebra.AbGroup.Base.html b/Cubical.Algebra.AbGroup.Base.html
@@ -342,9 +342,9 @@
   <a id="11177" href="Cubical.Algebra.AbGroup.Base.html#1682" class="Field">isAbGroup</a> <a id="11187" class="Symbol">(</a><a id="11188" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="11192" href="Cubical.Algebra.AbGroup.Base.html#11013" class="Function">HomGroup</a><a id="11200" class="Symbol">)</a> <a id="11202" class="Symbol">=</a>
     <a id="11208" href="Cubical.Algebra.AbGroup.Base.html#2153" class="Function">makeIsAbGroup</a>
     <a id="11226" href="Cubical.Algebra.Group.MorphismProperties.html#3530" class="Function">isSetGroupHom</a>
-    <a id="11244" class="Symbol">(λ</a> <a id="11247" class="Symbol">{</a> <a id="11249" class="Symbol">(</a><a id="11250" href="Cubical.Algebra.AbGroup.Base.html#11250" class="Bound">f</a> <a id="11252" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11254" href="Cubical.Algebra.AbGroup.Base.html#11254" class="Bound">p</a><a id="11255" class="Symbol">)</a> <a id="11257" class="Symbol">(</a><a id="11258" href="Cubical.Algebra.AbGroup.Base.html#11258" class="Bound">g</a> <a id="11260" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11262" href="Cubical.Algebra.AbGroup.Base.html#11262" class="Bound">q</a><a id="11263" class="Symbol">)</a> <a id="11265" class="Symbol">(</a><a id="11266" href="Cubical.Algebra.AbGroup.Base.html#11266" class="Bound">h</a> <a id="11268" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11270" href="Cubical.Algebra.AbGroup.Base.html#11270" class="Bound">r</a><a id="11271" class="Symbol">)</a> <a id="11273" class="Symbol">→</a> <a id="11275" href="Cubical.Data.Sigma.Properties.html#13827" class="Function">Σ≡Prop</a> <a id="11282" class="Symbol">(λ</a> <a id="11285" href="Cubical.Algebra.AbGroup.Base.html#11285" class="Bound">_</a> <a id="11287" class="Symbol">→</a> <a id="11289" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11306" class="Symbol">_</a> <a id="11308" class="Symbol">_)</a>
+    <a id="11244" class="Symbol">(λ</a> <a id="11247" class="Symbol">{</a> <a id="11249" class="Symbol">(</a><a id="11250" href="Cubical.Algebra.AbGroup.Base.html#11250" class="Bound">f</a> <a id="11252" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11254" href="Cubical.Algebra.AbGroup.Base.html#11254" class="Bound">p</a><a id="11255" class="Symbol">)</a> <a id="11257" class="Symbol">(</a><a id="11258" href="Cubical.Algebra.AbGroup.Base.html#11258" class="Bound">g</a> <a id="11260" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11262" href="Cubical.Algebra.AbGroup.Base.html#11262" class="Bound">q</a><a id="11263" class="Symbol">)</a> <a id="11265" class="Symbol">(</a><a id="11266" href="Cubical.Algebra.AbGroup.Base.html#11266" class="Bound">h</a> <a id="11268" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11270" href="Cubical.Algebra.AbGroup.Base.html#11270" class="Bound">r</a><a id="11271" class="Symbol">)</a> <a id="11273" class="Symbol">→</a> <a id="11275" href="Cubical.Data.Sigma.Properties.html#13825" class="Function">Σ≡Prop</a> <a id="11282" class="Symbol">(λ</a> <a id="11285" href="Cubical.Algebra.AbGroup.Base.html#11285" class="Bound">_</a> <a id="11287" class="Symbol">→</a> <a id="11289" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11306" class="Symbol">_</a> <a id="11308" class="Symbol">_)</a>
                                              <a id="11356" class="Symbol">(</a><a id="11357" href="Cubical.Foundations.Prelude.html#10568" class="Function">funExt</a> <a id="11364" class="Symbol">λ</a> <a id="11366" href="Cubical.Algebra.AbGroup.Base.html#11366" class="Bound">x</a> <a id="11368" class="Symbol">→</a> <a id="11370" href="Cubical.Algebra.AbGroup.Base.html#10234" class="Function">+AssocB</a> <a id="11378" class="Symbol">_</a> <a id="11380" class="Symbol">_</a> <a id="11382" class="Symbol">_)</a> <a id="11385" class="Symbol">})</a>
-    <a id="11392" class="Symbol">(λ</a> <a id="11395" class="Symbol">{</a> <a id="11397" class="Symbol">(</a><a id="11398" href="Cubical.Algebra.AbGroup.Base.html#11398" class="Bound">f</a> <a id="11400" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11402" href="Cubical.Algebra.AbGroup.Base.html#11402" class="Bound">p</a><a id="11403" class="Symbol">)</a> <a id="11405" class="Symbol">→</a> <a id="11407" href="Cubical.Data.Sigma.Properties.html#13827" class="Function">Σ≡Prop</a> <a id="11414" class="Symbol">(λ</a> <a id="11417" href="Cubical.Algebra.AbGroup.Base.html#11417" class="Bound">_</a> <a id="11419" class="Symbol">→</a> <a id="11421" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11438" class="Symbol">_</a> <a id="11440" class="Symbol">_)</a> <a id="11443" class="Symbol">(</a><a id="11444" href="Cubical.Foundations.Prelude.html#10568" class="Function">funExt</a> <a id="11451" class="Symbol">λ</a> <a id="11453" href="Cubical.Algebra.AbGroup.Base.html#11453" class="Bound">y</a> <a id="11455" class="Symbol">→</a> <a id="11457" href="Cubical.Algebra.AbGroup.Base.html#10186" class="Function">+IdRB</a> <a id="11463" class="Symbol">_)})</a>
-    <a id="11472" class="Symbol">((λ</a> <a id="11476" class="Symbol">{</a> <a id="11478" class="Symbol">(</a><a id="11479" href="Cubical.Algebra.AbGroup.Base.html#11479" class="Bound">f</a> <a id="11481" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11483" href="Cubical.Algebra.AbGroup.Base.html#11483" class="Bound">p</a><a id="11484" class="Symbol">)</a> <a id="11486" class="Symbol">→</a> <a id="11488" href="Cubical.Data.Sigma.Properties.html#13827" class="Function">Σ≡Prop</a> <a id="11495" class="Symbol">(λ</a> <a id="11498" href="Cubical.Algebra.AbGroup.Base.html#11498" class="Bound">_</a> <a id="11500" class="Symbol">→</a> <a id="11502" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11519" class="Symbol">_</a> <a id="11521" class="Symbol">_)</a> <a id="11524" class="Symbol">(</a><a id="11525" href="Cubical.Foundations.Prelude.html#10568" class="Function">funExt</a> <a id="11532" class="Symbol">λ</a> <a id="11534" href="Cubical.Algebra.AbGroup.Base.html#11534" class="Bound">y</a> <a id="11536" class="Symbol">→</a> <a id="11538" href="Cubical.Algebra.AbGroup.Base.html#10285" class="Function">+InvRB</a> <a id="11545" class="Symbol">_)}))</a>
-    <a id="11555" class="Symbol">(λ</a> <a id="11558" class="Symbol">{</a> <a id="11560" class="Symbol">(</a><a id="11561" href="Cubical.Algebra.AbGroup.Base.html#11561" class="Bound">f</a> <a id="11563" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11565" href="Cubical.Algebra.AbGroup.Base.html#11565" class="Bound">p</a><a id="11566" class="Symbol">)</a> <a id="11568" class="Symbol">(</a><a id="11569" href="Cubical.Algebra.AbGroup.Base.html#11569" class="Bound">g</a> <a id="11571" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11573" href="Cubical.Algebra.AbGroup.Base.html#11573" class="Bound">q</a><a id="11574" class="Symbol">)</a> <a id="11576" class="Symbol">→</a> <a id="11578" href="Cubical.Data.Sigma.Properties.html#13827" class="Function">Σ≡Prop</a> <a id="11585" class="Symbol">(λ</a> <a id="11588" href="Cubical.Algebra.AbGroup.Base.html#11588" class="Bound">_</a> <a id="11590" class="Symbol">→</a> <a id="11592" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11609" class="Symbol">_</a> <a id="11611" class="Symbol">_)</a> <a id="11614" class="Symbol">(</a><a id="11615" href="Cubical.Foundations.Prelude.html#10568" class="Function">funExt</a> <a id="11622" class="Symbol">λ</a> <a id="11624" href="Cubical.Algebra.AbGroup.Base.html#11624" class="Bound">x</a> <a id="11626" class="Symbol">→</a> <a id="11628" href="Cubical.Algebra.AbGroup.Base.html#10253" class="Function">+CommB</a> <a id="11635" class="Symbol">_</a> <a id="11637" class="Symbol">_)})</a>
+    <a id="11392" class="Symbol">(λ</a> <a id="11395" class="Symbol">{</a> <a id="11397" class="Symbol">(</a><a id="11398" href="Cubical.Algebra.AbGroup.Base.html#11398" class="Bound">f</a> <a id="11400" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11402" href="Cubical.Algebra.AbGroup.Base.html#11402" class="Bound">p</a><a id="11403" class="Symbol">)</a> <a id="11405" class="Symbol">→</a> <a id="11407" href="Cubical.Data.Sigma.Properties.html#13825" class="Function">Σ≡Prop</a> <a id="11414" class="Symbol">(λ</a> <a id="11417" href="Cubical.Algebra.AbGroup.Base.html#11417" class="Bound">_</a> <a id="11419" class="Symbol">→</a> <a id="11421" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11438" class="Symbol">_</a> <a id="11440" class="Symbol">_)</a> <a id="11443" class="Symbol">(</a><a id="11444" href="Cubical.Foundations.Prelude.html#10568" class="Function">funExt</a> <a id="11451" class="Symbol">λ</a> <a id="11453" href="Cubical.Algebra.AbGroup.Base.html#11453" class="Bound">y</a> <a id="11455" class="Symbol">→</a> <a id="11457" href="Cubical.Algebra.AbGroup.Base.html#10186" class="Function">+IdRB</a> <a id="11463" class="Symbol">_)})</a>
+    <a id="11472" class="Symbol">((λ</a> <a id="11476" class="Symbol">{</a> <a id="11478" class="Symbol">(</a><a id="11479" href="Cubical.Algebra.AbGroup.Base.html#11479" class="Bound">f</a> <a id="11481" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11483" href="Cubical.Algebra.AbGroup.Base.html#11483" class="Bound">p</a><a id="11484" class="Symbol">)</a> <a id="11486" class="Symbol">→</a> <a id="11488" href="Cubical.Data.Sigma.Properties.html#13825" class="Function">Σ≡Prop</a> <a id="11495" class="Symbol">(λ</a> <a id="11498" href="Cubical.Algebra.AbGroup.Base.html#11498" class="Bound">_</a> <a id="11500" class="Symbol">→</a> <a id="11502" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11519" class="Symbol">_</a> <a id="11521" class="Symbol">_)</a> <a id="11524" class="Symbol">(</a><a id="11525" href="Cubical.Foundations.Prelude.html#10568" class="Function">funExt</a> <a id="11532" class="Symbol">λ</a> <a id="11534" href="Cubical.Algebra.AbGroup.Base.html#11534" class="Bound">y</a> <a id="11536" class="Symbol">→</a> <a id="11538" href="Cubical.Algebra.AbGroup.Base.html#10285" class="Function">+InvRB</a> <a id="11545" class="Symbol">_)}))</a>
+    <a id="11555" class="Symbol">(λ</a> <a id="11558" class="Symbol">{</a> <a id="11560" class="Symbol">(</a><a id="11561" href="Cubical.Algebra.AbGroup.Base.html#11561" class="Bound">f</a> <a id="11563" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11565" href="Cubical.Algebra.AbGroup.Base.html#11565" class="Bound">p</a><a id="11566" class="Symbol">)</a> <a id="11568" class="Symbol">(</a><a id="11569" href="Cubical.Algebra.AbGroup.Base.html#11569" class="Bound">g</a> <a id="11571" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11573" href="Cubical.Algebra.AbGroup.Base.html#11573" class="Bound">q</a><a id="11574" class="Symbol">)</a> <a id="11576" class="Symbol">→</a> <a id="11578" href="Cubical.Data.Sigma.Properties.html#13825" class="Function">Σ≡Prop</a> <a id="11585" class="Symbol">(λ</a> <a id="11588" href="Cubical.Algebra.AbGroup.Base.html#11588" class="Bound">_</a> <a id="11590" class="Symbol">→</a> <a id="11592" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11609" class="Symbol">_</a> <a id="11611" class="Symbol">_)</a> <a id="11614" class="Symbol">(</a><a id="11615" href="Cubical.Foundations.Prelude.html#10568" class="Function">funExt</a> <a id="11622" class="Symbol">λ</a> <a id="11624" href="Cubical.Algebra.AbGroup.Base.html#11624" class="Bound">x</a> <a id="11626" class="Symbol">→</a> <a id="11628" href="Cubical.Algebra.AbGroup.Base.html#10253" class="Function">+CommB</a> <a id="11635" class="Symbol">_</a> <a id="11637" class="Symbol">_)})</a>
 </pre></body></html>