Skip to content

Commit

Permalink
Deploying to gh-pages from @ f3d8889 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@mortberg
mortberg committed Sep 11, 2024
1 parent 704893e commit 81a6ff4
Show file tree
Hide file tree
Showing 648 changed files with 23,446 additions and 23,704 deletions.
34 changes: 17 additions & 17 deletions Cubical.Algebra.AbGroup.Base.html
View file

Large diffs are not rendered by default.

138 changes: 69 additions & 69 deletions Cubical.Algebra.AbGroup.Instances.FreeAbGroup.html
View file

Large diffs are not rendered by default.

60 changes: 30 additions & 30 deletions Cubical.Algebra.AbGroup.Instances.Hom.html
View file

Large diffs are not rendered by default.

12 changes: 6 additions & 6 deletions Cubical.Algebra.AbGroup.Instances.IntMod.html
View file

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion Cubical.Algebra.AbGroup.Instances.NProd.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,5 +17,5 @@

<a id="NProd-AbGroup"></a><a id="327" href="Cubical.Algebra.AbGroup.Instances.NProd.html#327" class="Function">NProd-AbGroup</a> <a id="341" class="Symbol">:</a> <a id="343" class="Symbol">(</a><a id="344" href="Cubical.Algebra.AbGroup.Instances.NProd.html#344" class="Bound">G</a> <a id="346" class="Symbol">:</a> <a id="348" class="Symbol">(</a><a id="349" href="Cubical.Algebra.AbGroup.Instances.NProd.html#349" class="Bound">n</a> <a id="351" class="Symbol">:</a> <a id="353" href="Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a><a id="354" class="Symbol">)</a> <a id="356" class="Symbol">→</a> <a id="358" href="Agda.Primitive.html#388" class="Primitive">Type</a> <a id="363" href="Cubical.Algebra.AbGroup.Instances.NProd.html#299" class="Generalizable">ℓ</a><a id="364" class="Symbol">)</a> <a id="366" class="Symbol">→</a> <a id="368" class="Symbol">(</a><a id="369" href="Cubical.Algebra.AbGroup.Instances.NProd.html#369" class="Bound">Gstr</a> <a id="374" class="Symbol">:</a> <a id="376" class="Symbol">(</a><a id="377" href="Cubical.Algebra.AbGroup.Instances.NProd.html#377" class="Bound">n</a> <a id="379" class="Symbol">:</a> <a id="381" href="Agda.Builtin.Nat.html#203" class="Datatype">ℕ</a><a id="382" class="Symbol">)</a> <a id="384" class="Symbol">→</a> <a id="386" href="Cubical.Algebra.AbGroup.Base.html#1530" class="Record">AbGroupStr</a> <a id="397" class="Symbol">(</a><a id="398" href="Cubical.Algebra.AbGroup.Instances.NProd.html#344" class="Bound">G</a> <a id="400" href="Cubical.Algebra.AbGroup.Instances.NProd.html#377" class="Bound">n</a><a id="401" class="Symbol">))</a> <a id="404" class="Symbol">→</a> <a id="406" href="Cubical.Algebra.AbGroup.Base.html#1781" class="Function">AbGroup</a> <a id="414" href="Cubical.Algebra.AbGroup.Instances.NProd.html#299" class="Generalizable">ℓ</a>
<a id="416" href="Cubical.Algebra.AbGroup.Instances.NProd.html#327" class="Function">NProd-AbGroup</a> <a id="430" href="Cubical.Algebra.AbGroup.Instances.NProd.html#430" class="Bound">G</a> <a id="432" href="Cubical.Algebra.AbGroup.Instances.NProd.html#432" class="Bound">Gstr</a> <a id="437" class="Symbol">=</a> <a id="439" href="Cubical.Algebra.AbGroup.Base.html#3356" class="Function">Group→AbGroup</a> <a id="453" class="Symbol">(</a><a id="454" href="Cubical.Algebra.Group.Instances.NProd.html#277" class="Function">NProd-Group</a> <a id="466" href="Cubical.Algebra.AbGroup.Instances.NProd.html#430" class="Bound">G</a> <a id="468" class="Symbol">(λ</a> <a id="471" href="Cubical.Algebra.AbGroup.Instances.NProd.html#471" class="Bound">n</a> <a id="473" class="Symbol">→</a> <a id="475" href="Cubical.Algebra.AbGroup.Base.html#3013" class="Function">AbGroupStr→GroupStr</a> <a id="495" class="Symbol">(</a><a id="496" href="Cubical.Algebra.AbGroup.Instances.NProd.html#432" class="Bound">Gstr</a> <a id="501" href="Cubical.Algebra.AbGroup.Instances.NProd.html#471" class="Bound">n</a><a id="502" class="Symbol">)))</a>
<a id="544" class="Symbol">λ</a> <a id="546" href="Cubical.Algebra.AbGroup.Instances.NProd.html#546" class="Bound">f</a> <a id="548" href="Cubical.Algebra.AbGroup.Instances.NProd.html#548" class="Bound">g</a> <a id="550" class="Symbol">→</a> <a id="552" href="Cubical.Foundations.Prelude.html#10568" class="Function">funExt</a> <a id="559" class="Symbol">λ</a> <a id="561" href="Cubical.Algebra.AbGroup.Instances.NProd.html#561" class="Bound">n</a> <a id="563" class="Symbol">→</a> <a id="565" href="Cubical.Algebra.AbGroup.Base.html#1121" class="Function">+Comm</a> <a id="571" class="Symbol">(</a><a id="572" href="Cubical.Algebra.AbGroup.Instances.NProd.html#432" class="Bound">Gstr</a> <a id="577" href="Cubical.Algebra.AbGroup.Instances.NProd.html#561" class="Bound">n</a><a id="578" class="Symbol">)</a> <a id="580" class="Symbol">_</a> <a id="582" class="Symbol">_</a>
<a id="544" class="Symbol">λ</a> <a id="546" href="Cubical.Algebra.AbGroup.Instances.NProd.html#546" class="Bound">f</a> <a id="548" href="Cubical.Algebra.AbGroup.Instances.NProd.html#548" class="Bound">g</a> <a id="550" class="Symbol">→</a> <a id="552" href="Cubical.Foundations.Prelude.html#10999" class="Function">funExt</a> <a id="559" class="Symbol">λ</a> <a id="561" href="Cubical.Algebra.AbGroup.Instances.NProd.html#561" class="Bound">n</a> <a id="563" class="Symbol">→</a> <a id="565" href="Cubical.Algebra.AbGroup.Base.html#1121" class="Function">+Comm</a> <a id="571" class="Symbol">(</a><a id="572" href="Cubical.Algebra.AbGroup.Instances.NProd.html#432" class="Bound">Gstr</a> <a id="577" href="Cubical.Algebra.AbGroup.Instances.NProd.html#561" class="Bound">n</a><a id="578" class="Symbol">)</a> <a id="580" class="Symbol">_</a> <a id="582" class="Symbol">_</a>
</pre></body></html>
Loading

0 comments on commit 81a6ff4

Please sign in to comment.