Deploying to gh-pages from @ e9b8b40 🚀

agda · Nov 17, 2023 · 402f173 · 402f173
1 parent 1857add
commit 402f173
Show file tree

Hide file tree

Showing 222 changed files with 4,170 additions and 3,871 deletions.
diff --git a/Cubical.Algebra.AbGroup.Base.html b/Cubical.Algebra.AbGroup.Base.html
@@ -346,9 +346,9 @@
   <a id="11301" href="Cubical.Algebra.AbGroup.Base.html#1682" class="Field">isAbGroup</a> <a id="11311" class="Symbol">(</a><a id="11312" href="Agda.Builtin.Sigma.html#263" class="Field">snd</a> <a id="11316" href="Cubical.Algebra.AbGroup.Base.html#11137" class="Function">HomGroup</a><a id="11324" class="Symbol">)</a> <a id="11326" class="Symbol">=</a>
     <a id="11332" href="Cubical.Algebra.AbGroup.Base.html#2153" class="Function">makeIsAbGroup</a>
     <a id="11350" href="Cubical.Algebra.Group.MorphismProperties.html#3530" class="Function">isSetGroupHom</a>
-    <a id="11368" class="Symbol">(λ</a> <a id="11371" class="Symbol">{</a> <a id="11373" class="Symbol">(</a><a id="11374" href="Cubical.Algebra.AbGroup.Base.html#11374" class="Bound">f</a> <a id="11376" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11378" href="Cubical.Algebra.AbGroup.Base.html#11378" class="Bound">p</a><a id="11379" class="Symbol">)</a> <a id="11381" class="Symbol">(</a><a id="11382" href="Cubical.Algebra.AbGroup.Base.html#11382" class="Bound">g</a> <a id="11384" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11386" href="Cubical.Algebra.AbGroup.Base.html#11386" class="Bound">q</a><a id="11387" class="Symbol">)</a> <a id="11389" class="Symbol">(</a><a id="11390" href="Cubical.Algebra.AbGroup.Base.html#11390" class="Bound">h</a> <a id="11392" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11394" href="Cubical.Algebra.AbGroup.Base.html#11394" class="Bound">r</a><a id="11395" class="Symbol">)</a> <a id="11397" class="Symbol">→</a> <a id="11399" href="Cubical.Data.Sigma.Properties.html#13329" class="Function">Σ≡Prop</a> <a id="11406" class="Symbol">(λ</a> <a id="11409" href="Cubical.Algebra.AbGroup.Base.html#11409" class="Bound">_</a> <a id="11411" class="Symbol">→</a> <a id="11413" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11430" class="Symbol">_</a> <a id="11432" class="Symbol">_)</a>
+    <a id="11368" class="Symbol">(λ</a> <a id="11371" class="Symbol">{</a> <a id="11373" class="Symbol">(</a><a id="11374" href="Cubical.Algebra.AbGroup.Base.html#11374" class="Bound">f</a> <a id="11376" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11378" href="Cubical.Algebra.AbGroup.Base.html#11378" class="Bound">p</a><a id="11379" class="Symbol">)</a> <a id="11381" class="Symbol">(</a><a id="11382" href="Cubical.Algebra.AbGroup.Base.html#11382" class="Bound">g</a> <a id="11384" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11386" href="Cubical.Algebra.AbGroup.Base.html#11386" class="Bound">q</a><a id="11387" class="Symbol">)</a> <a id="11389" class="Symbol">(</a><a id="11390" href="Cubical.Algebra.AbGroup.Base.html#11390" class="Bound">h</a> <a id="11392" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11394" href="Cubical.Algebra.AbGroup.Base.html#11394" class="Bound">r</a><a id="11395" class="Symbol">)</a> <a id="11397" class="Symbol">→</a> <a id="11399" href="Cubical.Data.Sigma.Properties.html#13744" class="Function">Σ≡Prop</a> <a id="11406" class="Symbol">(λ</a> <a id="11409" href="Cubical.Algebra.AbGroup.Base.html#11409" class="Bound">_</a> <a id="11411" class="Symbol">→</a> <a id="11413" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11430" class="Symbol">_</a> <a id="11432" class="Symbol">_)</a>
                                              <a id="11480" class="Symbol">(</a><a id="11481" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="11488" class="Symbol">λ</a> <a id="11490" href="Cubical.Algebra.AbGroup.Base.html#11490" class="Bound">x</a> <a id="11492" class="Symbol">→</a> <a id="11494" href="Cubical.Algebra.AbGroup.Base.html#10234" class="Function">+AssocB</a> <a id="11502" class="Symbol">_</a> <a id="11504" class="Symbol">_</a> <a id="11506" class="Symbol">_)</a> <a id="11509" class="Symbol">})</a>
-    <a id="11516" class="Symbol">(λ</a> <a id="11519" class="Symbol">{</a> <a id="11521" class="Symbol">(</a><a id="11522" href="Cubical.Algebra.AbGroup.Base.html#11522" class="Bound">f</a> <a id="11524" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11526" href="Cubical.Algebra.AbGroup.Base.html#11526" class="Bound">p</a><a id="11527" class="Symbol">)</a> <a id="11529" class="Symbol">→</a> <a id="11531" href="Cubical.Data.Sigma.Properties.html#13329" class="Function">Σ≡Prop</a> <a id="11538" class="Symbol">(λ</a> <a id="11541" href="Cubical.Algebra.AbGroup.Base.html#11541" class="Bound">_</a> <a id="11543" class="Symbol">→</a> <a id="11545" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11562" class="Symbol">_</a> <a id="11564" class="Symbol">_)</a> <a id="11567" class="Symbol">(</a><a id="11568" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="11575" class="Symbol">λ</a> <a id="11577" href="Cubical.Algebra.AbGroup.Base.html#11577" class="Bound">y</a> <a id="11579" class="Symbol">→</a> <a id="11581" href="Cubical.Algebra.AbGroup.Base.html#10186" class="Function">+IdRB</a> <a id="11587" class="Symbol">_)})</a>
-    <a id="11596" class="Symbol">((λ</a> <a id="11600" class="Symbol">{</a> <a id="11602" class="Symbol">(</a><a id="11603" href="Cubical.Algebra.AbGroup.Base.html#11603" class="Bound">f</a> <a id="11605" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11607" href="Cubical.Algebra.AbGroup.Base.html#11607" class="Bound">p</a><a id="11608" class="Symbol">)</a> <a id="11610" class="Symbol">→</a> <a id="11612" href="Cubical.Data.Sigma.Properties.html#13329" class="Function">Σ≡Prop</a> <a id="11619" class="Symbol">(λ</a> <a id="11622" href="Cubical.Algebra.AbGroup.Base.html#11622" class="Bound">_</a> <a id="11624" class="Symbol">→</a> <a id="11626" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11643" class="Symbol">_</a> <a id="11645" class="Symbol">_)</a> <a id="11648" class="Symbol">(</a><a id="11649" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="11656" class="Symbol">λ</a> <a id="11658" href="Cubical.Algebra.AbGroup.Base.html#11658" class="Bound">y</a> <a id="11660" class="Symbol">→</a> <a id="11662" href="Cubical.Algebra.AbGroup.Base.html#10285" class="Function">+InvRB</a> <a id="11669" class="Symbol">_)}))</a>
-    <a id="11679" class="Symbol">(λ</a> <a id="11682" class="Symbol">{</a> <a id="11684" class="Symbol">(</a><a id="11685" href="Cubical.Algebra.AbGroup.Base.html#11685" class="Bound">f</a> <a id="11687" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11689" href="Cubical.Algebra.AbGroup.Base.html#11689" class="Bound">p</a><a id="11690" class="Symbol">)</a> <a id="11692" class="Symbol">(</a><a id="11693" href="Cubical.Algebra.AbGroup.Base.html#11693" class="Bound">g</a> <a id="11695" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11697" href="Cubical.Algebra.AbGroup.Base.html#11697" class="Bound">q</a><a id="11698" class="Symbol">)</a> <a id="11700" class="Symbol">→</a> <a id="11702" href="Cubical.Data.Sigma.Properties.html#13329" class="Function">Σ≡Prop</a> <a id="11709" class="Symbol">(λ</a> <a id="11712" href="Cubical.Algebra.AbGroup.Base.html#11712" class="Bound">_</a> <a id="11714" class="Symbol">→</a> <a id="11716" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11733" class="Symbol">_</a> <a id="11735" class="Symbol">_)</a> <a id="11738" class="Symbol">(</a><a id="11739" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="11746" class="Symbol">λ</a> <a id="11748" href="Cubical.Algebra.AbGroup.Base.html#11748" class="Bound">x</a> <a id="11750" class="Symbol">→</a> <a id="11752" href="Cubical.Algebra.AbGroup.Base.html#10253" class="Function">+CommB</a> <a id="11759" class="Symbol">_</a> <a id="11761" class="Symbol">_)})</a>
+    <a id="11516" class="Symbol">(λ</a> <a id="11519" class="Symbol">{</a> <a id="11521" class="Symbol">(</a><a id="11522" href="Cubical.Algebra.AbGroup.Base.html#11522" class="Bound">f</a> <a id="11524" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11526" href="Cubical.Algebra.AbGroup.Base.html#11526" class="Bound">p</a><a id="11527" class="Symbol">)</a> <a id="11529" class="Symbol">→</a> <a id="11531" href="Cubical.Data.Sigma.Properties.html#13744" class="Function">Σ≡Prop</a> <a id="11538" class="Symbol">(λ</a> <a id="11541" href="Cubical.Algebra.AbGroup.Base.html#11541" class="Bound">_</a> <a id="11543" class="Symbol">→</a> <a id="11545" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11562" class="Symbol">_</a> <a id="11564" class="Symbol">_)</a> <a id="11567" class="Symbol">(</a><a id="11568" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="11575" class="Symbol">λ</a> <a id="11577" href="Cubical.Algebra.AbGroup.Base.html#11577" class="Bound">y</a> <a id="11579" class="Symbol">→</a> <a id="11581" href="Cubical.Algebra.AbGroup.Base.html#10186" class="Function">+IdRB</a> <a id="11587" class="Symbol">_)})</a>
+    <a id="11596" class="Symbol">((λ</a> <a id="11600" class="Symbol">{</a> <a id="11602" class="Symbol">(</a><a id="11603" href="Cubical.Algebra.AbGroup.Base.html#11603" class="Bound">f</a> <a id="11605" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11607" href="Cubical.Algebra.AbGroup.Base.html#11607" class="Bound">p</a><a id="11608" class="Symbol">)</a> <a id="11610" class="Symbol">→</a> <a id="11612" href="Cubical.Data.Sigma.Properties.html#13744" class="Function">Σ≡Prop</a> <a id="11619" class="Symbol">(λ</a> <a id="11622" href="Cubical.Algebra.AbGroup.Base.html#11622" class="Bound">_</a> <a id="11624" class="Symbol">→</a> <a id="11626" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11643" class="Symbol">_</a> <a id="11645" class="Symbol">_)</a> <a id="11648" class="Symbol">(</a><a id="11649" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="11656" class="Symbol">λ</a> <a id="11658" href="Cubical.Algebra.AbGroup.Base.html#11658" class="Bound">y</a> <a id="11660" class="Symbol">→</a> <a id="11662" href="Cubical.Algebra.AbGroup.Base.html#10285" class="Function">+InvRB</a> <a id="11669" class="Symbol">_)}))</a>
+    <a id="11679" class="Symbol">(λ</a> <a id="11682" class="Symbol">{</a> <a id="11684" class="Symbol">(</a><a id="11685" href="Cubical.Algebra.AbGroup.Base.html#11685" class="Bound">f</a> <a id="11687" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11689" href="Cubical.Algebra.AbGroup.Base.html#11689" class="Bound">p</a><a id="11690" class="Symbol">)</a> <a id="11692" class="Symbol">(</a><a id="11693" href="Cubical.Algebra.AbGroup.Base.html#11693" class="Bound">g</a> <a id="11695" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="11697" href="Cubical.Algebra.AbGroup.Base.html#11697" class="Bound">q</a><a id="11698" class="Symbol">)</a> <a id="11700" class="Symbol">→</a> <a id="11702" href="Cubical.Data.Sigma.Properties.html#13744" class="Function">Σ≡Prop</a> <a id="11709" class="Symbol">(λ</a> <a id="11712" href="Cubical.Algebra.AbGroup.Base.html#11712" class="Bound">_</a> <a id="11714" class="Symbol">→</a> <a id="11716" href="Cubical.Algebra.Group.MorphismProperties.html#3162" class="Function">isPropIsGroupHom</a> <a id="11733" class="Symbol">_</a> <a id="11735" class="Symbol">_)</a> <a id="11738" class="Symbol">(</a><a id="11739" href="Cubical.Foundations.Prelude.html#10257" class="Function">funExt</a> <a id="11746" class="Symbol">λ</a> <a id="11748" href="Cubical.Algebra.AbGroup.Base.html#11748" class="Bound">x</a> <a id="11750" class="Symbol">→</a> <a id="11752" href="Cubical.Algebra.AbGroup.Base.html#10253" class="Function">+CommB</a> <a id="11759" class="Symbol">_</a> <a id="11761" class="Symbol">_)})</a>
 </pre></body></html>