Skip to content

Commit

Permalink
Deploying to gh-pages from @ 24774d4 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@felixwellen
felixwellen committed Feb 23, 2024
1 parent ba84169 commit fa5267b
Show file tree
Hide file tree
Showing 139 changed files with 3,855 additions and 2,047 deletions.
4 changes: 2 additions & 2 deletions Cubical.Algebra.CommMonoid.GrothendieckGroup.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@


<a id="767" class="Keyword">module</a> <a id="774" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#774" class="Module">_</a> <a id="776" class="Symbol">(</a><a id="777" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#777" class="Bound">M</a> <a id="779" class="Symbol">:</a> <a id="781" href="Cubical.Algebra.CommMonoid.Base.html#1133" class="Function">CommMonoid</a> <a id="792" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#752" class="Generalizable">ℓ</a><a id="793" class="Symbol">)</a> <a id="795" class="Keyword">where</a>
<a id="803" class="Keyword">open</a> <a id="808" href="Cubical.Relation.Binary.Base.html#1664" class="Module">BinaryRelation</a>
<a id="803" class="Keyword">open</a> <a id="808" href="Cubical.Relation.Binary.Base.html#1736" class="Module">BinaryRelation</a>

<a id="826" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#826" class="Function">M²</a> <a id="829" class="Symbol">:</a> <a id="831" href="Cubical.Algebra.CommMonoid.Base.html#1133" class="Function">CommMonoid</a> <a id="842" class="Symbol">_</a>
<a id="846" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#826" class="Function">M²</a> <a id="849" class="Symbol">=</a> <a id="851" href="Cubical.Algebra.CommMonoid.CommMonoidProd.html#296" class="Function">CommMonoidProd</a> <a id="866" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#777" class="Bound">M</a> <a id="868" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#777" class="Bound">M</a>
Expand All @@ -53,7 +53,7 @@
<a id="1143" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1143" class="Function Operator">_+/_</a> <a id="1148" class="Symbol">:</a> <a id="1150" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1062" class="Function">M²/R</a> <a id="1155" class="Symbol">→</a> <a id="1157" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1062" class="Function">M²/R</a> <a id="1162" class="Symbol">→</a> <a id="1164" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1062" class="Function">M²/R</a>
<a id="1173" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1173" class="Bound">x</a> <a id="1175" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1143" class="Function Operator">+/</a> <a id="1178" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1178" class="Bound">y</a> <a id="1180" class="Symbol">=</a> <a id="1182" href="Cubical.HITs.SetQuotients.Properties.html#8108" class="Function">setQuotBinOp</a> <a id="1195" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1245" class="Function">isReflR</a> <a id="1203" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1245" class="Function">isReflR</a> <a id="1211" href="Cubical.Algebra.CommMonoid.Base.html#1012" class="Field Operator">_·_</a> <a id="1215" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1323" class="Function">isCongR</a> <a id="1223" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1173" class="Bound">x</a> <a id="1225" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1178" class="Bound">y</a>
<a id="1233" class="Keyword">where</a>
<a id="1245" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1245" class="Function">isReflR</a> <a id="1253" class="Symbol">:</a> <a id="1255" href="Cubical.Relation.Binary.Base.html#1732" class="Function">isRefl</a> <a id="1262" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#957" class="Function">R</a>
<a id="1245" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1245" class="Function">isReflR</a> <a id="1253" class="Symbol">:</a> <a id="1255" href="Cubical.Relation.Binary.Base.html#1804" class="Function">isRefl</a> <a id="1262" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#957" class="Function">R</a>
<a id="1270" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1245" class="Function">isReflR</a> <a id="1278" class="Symbol">(</a><a id="1279" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1279" class="Bound">a</a> <a id="1281" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1283" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1283" class="Bound">b</a><a id="1284" class="Symbol">)</a> <a id="1286" class="Symbol">=</a> <a id="1288" href="Cubical.Algebra.CommMonoid.Base.html#991" class="Field">ε</a> <a id="1290" href="Agda.Builtin.Sigma.html#235" class="InductiveConstructor Operator">,</a> <a id="1292" href="Cubical.Foundations.Prelude.html#1430" class="Function">cong</a> <a id="1297" class="Symbol">(</a><a id="1298" href="Cubical.Algebra.CommMonoid.Base.html#991" class="Field">ε</a> <a id="1300" href="Cubical.Algebra.CommMonoid.Base.html#1012" class="Field Operator">·_</a><a id="1302" class="Symbol">)</a> <a id="1304" class="Symbol">(</a><a id="1305" href="Cubical.Algebra.CommMonoid.Base.html#741" class="Function">·Comm</a> <a id="1311" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1279" class="Bound">a</a> <a id="1313" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1283" class="Bound">b</a><a id="1314" class="Symbol">)</a>

<a id="1323" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1323" class="Function">isCongR</a> <a id="1331" class="Symbol">:</a> <a id="1333" class="Symbol">∀</a> <a id="1335" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1335" class="Bound">u</a> <a id="1337" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1337" class="Bound">u&#39;</a> <a id="1340" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1340" class="Bound">v</a> <a id="1342" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1342" class="Bound">v&#39;</a> <a id="1345" class="Symbol">→</a> <a id="1347" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#957" class="Function">R</a> <a id="1349" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1335" class="Bound">u</a> <a id="1351" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1337" class="Bound">u&#39;</a> <a id="1354" class="Symbol">→</a> <a id="1356" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#957" class="Function">R</a> <a id="1358" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1340" class="Bound">v</a> <a id="1360" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1342" class="Bound">v&#39;</a> <a id="1363" class="Symbol">→</a> <a id="1365" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#957" class="Function">R</a> <a id="1367" class="Symbol">(</a><a id="1368" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1335" class="Bound">u</a> <a id="1370" href="Cubical.Algebra.CommMonoid.Base.html#1012" class="Field Operator">·</a> <a id="1372" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1340" class="Bound">v</a><a id="1373" class="Symbol">)</a> <a id="1375" class="Symbol">(</a><a id="1376" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1337" class="Bound">u&#39;</a> <a id="1379" href="Cubical.Algebra.CommMonoid.Base.html#1012" class="Field Operator">·</a> <a id="1381" href="Cubical.Algebra.CommMonoid.GrothendieckGroup.html#1342" class="Bound">v&#39;</a><a id="1383" class="Symbol">)</a>
Expand Down
Loading

0 comments on commit fa5267b

Please sign in to comment.