Skip to content

Commit

Permalink
Deploying to gh-pages from @ 429e617 🚀
Browse files Browse the repository at this point in the history
  • Loading branch information
@github-merge-queue
github-merge-queue[bot] committed Jan 1, 2025
1 parent 7167a49 commit 3255dac
Show file tree
Hide file tree
Showing 67 changed files with 1,296 additions and 1,288 deletions.
658 changes: 333 additions & 325 deletions master/Algebra.Bundles.Raw.html
View file

Large diffs are not rendered by default.

184 changes: 92 additions & 92 deletions master/Algebra.Bundles.html
View file

Large diffs are not rendered by default.

126 changes: 63 additions & 63 deletions master/Algebra.Construct.DirectProduct.html
View file

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions master/Algebra.Construct.Initial.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
<a id="549" class="Keyword">open</a> <a id="554" class="Keyword">import</a> <a id="561" href="Algebra.Bundles.html" class="Module">Algebra.Bundles</a>
<a id="579" class="Keyword">using</a> <a id="585" class="Symbol">(</a><a id="586" href="Algebra.Bundles.html#1758" class="Record">Magma</a><a id="591" class="Symbol">;</a> <a id="593" href="Algebra.Bundles.html#4756" class="Record">Semigroup</a><a id="602" class="Symbol">;</a> <a id="604" href="Algebra.Bundles.html#5119" class="Record">Band</a><a id="608" class="Symbol">)</a>
<a id="610" class="Keyword">open</a> <a id="615" class="Keyword">import</a> <a id="622" href="Algebra.Bundles.Raw.html" class="Module">Algebra.Bundles.Raw</a>
<a id="644" class="Keyword">using</a> <a id="650" class="Symbol">(</a><a id="651" href="Algebra.Bundles.Raw.html#1073" class="Record">RawMagma</a><a id="659" class="Symbol">)</a>
<a id="644" class="Keyword">using</a> <a id="650" class="Symbol">(</a><a id="651" href="Algebra.Bundles.Raw.html#1242" class="Record">RawMagma</a><a id="659" class="Symbol">)</a>
<a id="661" class="Keyword">open</a> <a id="666" class="Keyword">import</a> <a id="673" href="Algebra.Core.html" class="Module">Algebra.Core</a> <a id="686" class="Keyword">using</a> <a id="692" class="Symbol">(</a><a id="693" href="Algebra.Core.html#527" class="Function">Op₂</a><a id="696" class="Symbol">)</a>
<a id="698" class="Keyword">open</a> <a id="703" class="Keyword">import</a> <a id="710" href="Algebra.Definitions.html" class="Module">Algebra.Definitions</a> <a id="730" class="Keyword">using</a> <a id="736" class="Symbol">(</a><a id="737" href="Algebra.Definitions.html#1302" class="Function">Congruent₂</a><a id="747" class="Symbol">)</a>
<a id="749" class="Keyword">open</a> <a id="754" class="Keyword">import</a> <a id="761" href="Algebra.Structures.html" class="Module">Algebra.Structures</a> <a id="780" class="Keyword">using</a> <a id="786" class="Symbol">(</a><a id="787" href="Algebra.Structures.html#1708" class="Record">IsMagma</a><a id="794" class="Symbol">;</a> <a id="796" href="Algebra.Structures.html#3380" class="Record">IsSemigroup</a><a id="807" class="Symbol">;</a> <a id="809" href="Algebra.Structures.html#3524" class="Record">IsBand</a><a id="815" class="Symbol">)</a>
Expand Down Expand Up @@ -69,7 +69,7 @@
<a id="1721" class="Comment">------------------------------------------------------------------------</a>
<a id="1794" class="Comment">-- Raw bundles</a>

<a id="rawMagma"></a><a id="1810" href="Algebra.Construct.Initial.html#1810" class="Function">rawMagma</a> <a id="1819" class="Symbol">:</a> <a id="1821" href="Algebra.Bundles.Raw.html#1073" class="Record">RawMagma</a> <a id="1830" href="Algebra.Construct.Initial.html#529" class="Bound">c</a> <a id="1832" href="Algebra.Construct.Initial.html#531" class="Bound">ℓ</a>
<a id="rawMagma"></a><a id="1810" href="Algebra.Construct.Initial.html#1810" class="Function">rawMagma</a> <a id="1819" class="Symbol">:</a> <a id="1821" href="Algebra.Bundles.Raw.html#1242" class="Record">RawMagma</a> <a id="1830" href="Algebra.Construct.Initial.html#529" class="Bound">c</a> <a id="1832" href="Algebra.Construct.Initial.html#531" class="Bound">ℓ</a>
<a id="1834" href="Algebra.Construct.Initial.html#1810" class="Function">rawMagma</a> <a id="1843" class="Symbol">=</a> <a id="1845" class="Keyword">record</a> <a id="1852" class="Symbol">{</a> <a id="1854" href="Algebra.Construct.Initial.html#1394" class="Module">ℤero</a> <a id="1859" class="Symbol">}</a>

<a id="1862" class="Comment">------------------------------------------------------------------------</a>
Expand Down
2 changes: 1 addition & 1 deletion master/Algebra.Construct.LexProduct.Inner.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@
<a id="973" class="Keyword">renaming</a>
<a id="984" class="Symbol">(</a> <a id="986" href="Algebra.Bundles.html#1836" class="Function">Carrier</a> <a id="995" class="Symbol">to</a> <a id="998" class="Function">A</a>
<a id="1002" class="Symbol">;</a> <a id="1004" href="Algebra.Bundles.html#1856" class="Function Operator">_≈_</a> <a id="1013" class="Symbol">to</a> <a id="1016" class="Function Operator">_≈₁_</a>
<a id="1023" class="Symbol">;</a> <a id="1025" href="Algebra.Bundles.Raw.html#1241" class="Function Operator">_≉_</a> <a id="1034" class="Symbol">to</a> <a id="1037" class="Function Operator">_≉₁_</a>
<a id="1023" class="Symbol">;</a> <a id="1025" href="Relation.Binary.Bundles.Raw.html#891" class="Function Operator">_≉_</a> <a id="1034" class="Symbol">to</a> <a id="1037" class="Function Operator">_≉₁_</a>
<a id="1044" class="Symbol">)</a>

<a id="1047" class="Keyword">open</a> <a id="1052" class="Keyword">module</a> <a id="N"></a><a id="1059" href="Algebra.Construct.LexProduct.Inner.html#1059" class="Module">N</a> <a id="1061" class="Symbol">=</a> <a id="1063" href="Algebra.Bundles.html#1758" class="Module">Magma</a> <a id="1069" href="Algebra.Construct.LexProduct.Inner.html#886" class="Bound">N</a>
Expand Down
2 changes: 1 addition & 1 deletion master/Algebra.Construct.LexProduct.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -29,7 +29,7 @@
<a id="1103" class="Keyword">renaming</a>
<a id="1114" class="Symbol">(</a> <a id="1116" href="Algebra.Bundles.html#1836" class="Field">Carrier</a> <a id="1125" class="Symbol">to</a> <a id="1128" class="Field">A</a>
<a id="1132" class="Symbol">;</a> <a id="1134" href="Algebra.Bundles.html#1856" class="Field Operator">_≈_</a> <a id="1143" class="Symbol">to</a> <a id="1146" class="Field Operator">_≈₁_</a>
<a id="1153" class="Symbol">;</a> <a id="1155" href="Algebra.Bundles.Raw.html#1241" class="Function Operator">_≉_</a> <a id="1164" class="Symbol">to</a> <a id="1167" class="Function Operator">_≉₁_</a>
<a id="1153" class="Symbol">;</a> <a id="1155" href="Relation.Binary.Bundles.Raw.html#891" class="Function Operator">_≉_</a> <a id="1164" class="Symbol">to</a> <a id="1167" class="Function Operator">_≉₁_</a>
<a id="1174" class="Symbol">)</a>

<a id="1177" class="Keyword">open</a> <a id="1182" href="Algebra.Bundles.html#1758" class="Module">Magma</a> <a id="1188" href="Algebra.Construct.LexProduct.html#1006" class="Bound">N</a> <a id="1190" class="Keyword">using</a> <a id="1196" class="Symbol">()</a>
Expand Down
4 changes: 2 additions & 2 deletions master/Algebra.Construct.NaturalChoice.MinOp.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -161,8 +161,8 @@
<a id="4624" class="Comment">------------------------------------------------------------------------</a>
<a id="4697" class="Comment">-- Raw bundles</a>

<a id="⊓-rawMagma"></a><a id="4713" href="Algebra.Construct.NaturalChoice.MinOp.html#4713" class="Function">⊓-rawMagma</a> <a id="4724" class="Symbol">:</a> <a id="4726" href="Algebra.Bundles.Raw.html#1073" class="Record">RawMagma</a> <a id="4735" class="Symbol">_</a> <a id="4737" class="Symbol">_</a>
<a id="4739" href="Algebra.Construct.NaturalChoice.MinOp.html#4713" class="Function">⊓-rawMagma</a> <a id="4750" class="Symbol">=</a> <a id="4752" class="Keyword">record</a> <a id="4759" class="Symbol">{</a> <a id="4761" href="Algebra.Bundles.Raw.html#1174" class="Field Operator">_≈_</a> <a id="4765" class="Symbol">=</a> <a id="4767" href="Relation.Binary.Bundles.html#3131" class="Function Operator">_≈_</a> <a id="4771" class="Symbol">;</a> <a id="4773" href="Algebra.Bundles.Raw.html#1202" class="Field Operator">_∙_</a> <a id="4777" class="Symbol">=</a> <a id="4779" href="Algebra.Construct.NaturalChoice.Base.html#1065" class="Field Operator">_⊓_</a> <a id="4783" class="Symbol">}</a>
<a id="⊓-rawMagma"></a><a id="4713" href="Algebra.Construct.NaturalChoice.MinOp.html#4713" class="Function">⊓-rawMagma</a> <a id="4724" class="Symbol">:</a> <a id="4726" href="Algebra.Bundles.Raw.html#1242" class="Record">RawMagma</a> <a id="4735" class="Symbol">_</a> <a id="4737" class="Symbol">_</a>
<a id="4739" href="Algebra.Construct.NaturalChoice.MinOp.html#4713" class="Function">⊓-rawMagma</a> <a id="4750" class="Symbol">=</a> <a id="4752" class="Keyword">record</a> <a id="4759" class="Symbol">{</a> <a id="4761" href="Algebra.Bundles.Raw.html#1343" class="Field Operator">_≈_</a> <a id="4765" class="Symbol">=</a> <a id="4767" href="Relation.Binary.Bundles.html#3131" class="Function Operator">_≈_</a> <a id="4771" class="Symbol">;</a> <a id="4773" href="Algebra.Bundles.Raw.html#1371" class="Field Operator">_∙_</a> <a id="4777" class="Symbol">=</a> <a id="4779" href="Algebra.Construct.NaturalChoice.Base.html#1065" class="Field Operator">_⊓_</a> <a id="4783" class="Symbol">}</a>

<a id="4786" class="Comment">------------------------------------------------------------------------</a>
<a id="4859" class="Comment">-- Bundles</a>
Expand Down
12 changes: 6 additions & 6 deletions master/Algebra.Construct.Terminal.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,22 +34,22 @@
<a id="905" class="Comment">------------------------------------------------------------------------</a>
<a id="978" class="Comment">-- Raw bundles</a>

<a id="rawMagma"></a><a id="994" href="Algebra.Construct.Terminal.html#994" class="Function">rawMagma</a> <a id="1003" class="Symbol">:</a> <a id="1005" href="Algebra.Bundles.Raw.html#1073" class="Record">RawMagma</a> <a id="1014" href="Algebra.Construct.Terminal.html#555" class="Bound">c</a> <a id="1016" href="Algebra.Construct.Terminal.html#557" class="Bound">ℓ</a>
<a id="rawMagma"></a><a id="994" href="Algebra.Construct.Terminal.html#994" class="Function">rawMagma</a> <a id="1003" class="Symbol">:</a> <a id="1005" href="Algebra.Bundles.Raw.html#1242" class="Record">RawMagma</a> <a id="1014" href="Algebra.Construct.Terminal.html#555" class="Bound">c</a> <a id="1016" href="Algebra.Construct.Terminal.html#557" class="Bound">ℓ</a>
<a id="1018" href="Algebra.Construct.Terminal.html#994" class="Function">rawMagma</a> <a id="1027" class="Symbol">=</a> <a id="1029" class="Keyword">record</a> <a id="1036" class="Symbol">{</a> <a id="1038" href="Algebra.Construct.Terminal.html#809" class="Module">𝕆ne</a> <a id="1042" class="Symbol">}</a>

<a id="rawMonoid"></a><a id="1045" href="Algebra.Construct.Terminal.html#1045" class="Function">rawMonoid</a> <a id="1055" class="Symbol">:</a> <a id="1057" href="Algebra.Bundles.Raw.html#1534" class="Record">RawMonoid</a> <a id="1067" href="Algebra.Construct.Terminal.html#555" class="Bound">c</a> <a id="1069" href="Algebra.Construct.Terminal.html#557" class="Bound">ℓ</a>
<a id="rawMonoid"></a><a id="1045" href="Algebra.Construct.Terminal.html#1045" class="Function">rawMonoid</a> <a id="1055" class="Symbol">:</a> <a id="1057" href="Algebra.Bundles.Raw.html#1758" class="Record">RawMonoid</a> <a id="1067" href="Algebra.Construct.Terminal.html#555" class="Bound">c</a> <a id="1069" href="Algebra.Construct.Terminal.html#557" class="Bound">ℓ</a>
<a id="1071" href="Algebra.Construct.Terminal.html#1045" class="Function">rawMonoid</a> <a id="1081" class="Symbol">=</a> <a id="1083" class="Keyword">record</a> <a id="1090" class="Symbol">{</a> <a id="1092" href="Algebra.Construct.Terminal.html#809" class="Module">𝕆ne</a> <a id="1096" class="Symbol">}</a>

<a id="rawGroup"></a><a id="1099" href="Algebra.Construct.Terminal.html#1099" class="Function">rawGroup</a> <a id="1108" class="Symbol">:</a> <a id="1110" href="Algebra.Bundles.Raw.html#2067" class="Record">RawGroup</a> <a id="1119" href="Algebra.Construct.Terminal.html#555" class="Bound">c</a> <a id="1121" href="Algebra.Construct.Terminal.html#557" class="Bound">ℓ</a>
<a id="rawGroup"></a><a id="1099" href="Algebra.Construct.Terminal.html#1099" class="Function">rawGroup</a> <a id="1108" class="Symbol">:</a> <a id="1110" href="Algebra.Bundles.Raw.html#2291" class="Record">RawGroup</a> <a id="1119" href="Algebra.Construct.Terminal.html#555" class="Bound">c</a> <a id="1121" href="Algebra.Construct.Terminal.html#557" class="Bound">ℓ</a>
<a id="1123" href="Algebra.Construct.Terminal.html#1099" class="Function">rawGroup</a> <a id="1132" class="Symbol">=</a> <a id="1134" class="Keyword">record</a> <a id="1141" class="Symbol">{</a> <a id="1143" href="Algebra.Construct.Terminal.html#809" class="Module">𝕆ne</a> <a id="1147" class="Symbol">}</a>

<a id="rawNearSemiring"></a><a id="1150" href="Algebra.Construct.Terminal.html#1150" class="Function">rawNearSemiring</a> <a id="1166" class="Symbol">:</a> <a id="1168" href="Algebra.Bundles.Raw.html#2651" class="Record">RawNearSemiring</a> <a id="1184" href="Algebra.Construct.Terminal.html#555" class="Bound">c</a> <a id="1186" href="Algebra.Construct.Terminal.html#557" class="Bound">ℓ</a>
<a id="rawNearSemiring"></a><a id="1150" href="Algebra.Construct.Terminal.html#1150" class="Function">rawNearSemiring</a> <a id="1166" class="Symbol">:</a> <a id="1168" href="Algebra.Bundles.Raw.html#2875" class="Record">RawNearSemiring</a> <a id="1184" href="Algebra.Construct.Terminal.html#555" class="Bound">c</a> <a id="1186" href="Algebra.Construct.Terminal.html#557" class="Bound">ℓ</a>
<a id="1188" href="Algebra.Construct.Terminal.html#1150" class="Function">rawNearSemiring</a> <a id="1204" class="Symbol">=</a> <a id="1206" class="Keyword">record</a> <a id="1213" class="Symbol">{</a> <a id="1215" href="Algebra.Construct.Terminal.html#809" class="Module">𝕆ne</a> <a id="1219" class="Symbol">}</a>

<a id="rawSemiring"></a><a id="1222" href="Algebra.Construct.Terminal.html#1222" class="Function">rawSemiring</a> <a id="1234" class="Symbol">:</a> <a id="1236" href="Algebra.Bundles.Raw.html#3363" class="Record">RawSemiring</a> <a id="1248" href="Algebra.Construct.Terminal.html#555" class="Bound">c</a> <a id="1250" href="Algebra.Construct.Terminal.html#557" class="Bound">ℓ</a>
<a id="rawSemiring"></a><a id="1222" href="Algebra.Construct.Terminal.html#1222" class="Function">rawSemiring</a> <a id="1234" class="Symbol">:</a> <a id="1236" href="Algebra.Bundles.Raw.html#3587" class="Record">RawSemiring</a> <a id="1248" href="Algebra.Construct.Terminal.html#555" class="Bound">c</a> <a id="1250" href="Algebra.Construct.Terminal.html#557" class="Bound">ℓ</a>
<a id="1252" href="Algebra.Construct.Terminal.html#1222" class="Function">rawSemiring</a> <a id="1264" class="Symbol">=</a> <a id="1266" class="Keyword">record</a> <a id="1273" class="Symbol">{</a> <a id="1275" href="Algebra.Construct.Terminal.html#809" class="Module">𝕆ne</a> <a id="1279" class="Symbol">}</a>

<a id="rawRing"></a><a id="1282" href="Algebra.Construct.Terminal.html#1282" class="Function">rawRing</a> <a id="1290" class="Symbol">:</a> <a id="1292" href="Algebra.Bundles.Raw.html#5061" class="Record">RawRing</a> <a id="1300" href="Algebra.Construct.Terminal.html#555" class="Bound">c</a> <a id="1302" href="Algebra.Construct.Terminal.html#557" class="Bound">ℓ</a>
<a id="rawRing"></a><a id="1282" href="Algebra.Construct.Terminal.html#1282" class="Function">rawRing</a> <a id="1290" class="Symbol">:</a> <a id="1292" href="Algebra.Bundles.Raw.html#5285" class="Record">RawRing</a> <a id="1300" href="Algebra.Construct.Terminal.html#555" class="Bound">c</a> <a id="1302" href="Algebra.Construct.Terminal.html#557" class="Bound">ℓ</a>
<a id="1304" href="Algebra.Construct.Terminal.html#1282" class="Function">rawRing</a> <a id="1312" class="Symbol">=</a> <a id="1314" class="Keyword">record</a> <a id="1321" class="Symbol">{</a> <a id="1323" href="Algebra.Construct.Terminal.html#809" class="Module">𝕆ne</a> <a id="1327" class="Symbol">}</a>

<a id="1330" class="Comment">------------------------------------------------------------------------</a>
Expand Down
4 changes: 2 additions & 2 deletions master/Algebra.Construct.Zero.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
<a id="804" class="Keyword">module</a> <a id="811" href="Algebra.Construct.Zero.html" class="Module">Algebra.Construct.Zero</a> <a id="834" class="Symbol">{</a><a id="835" href="Algebra.Construct.Zero.html#835" class="Bound">c</a> <a id="837" href="Algebra.Construct.Zero.html#837" class="Bound">ℓ</a> <a id="839" class="Symbol">:</a> <a id="841" href="Agda.Primitive.html#742" class="Postulate">Level</a><a id="846" class="Symbol">}</a> <a id="848" class="Keyword">where</a>

<a id="855" class="Keyword">open</a> <a id="860" class="Keyword">import</a> <a id="867" href="Algebra.Bundles.Raw.html" class="Module">Algebra.Bundles.Raw</a>
<a id="889" class="Keyword">using</a> <a id="895" class="Symbol">(</a><a id="896" href="Algebra.Bundles.Raw.html#1073" class="Record">RawMagma</a><a id="904" class="Symbol">)</a>
<a id="889" class="Keyword">using</a> <a id="895" class="Symbol">(</a><a id="896" href="Algebra.Bundles.Raw.html#1242" class="Record">RawMagma</a><a id="904" class="Symbol">)</a>
<a id="906" class="Keyword">open</a> <a id="911" class="Keyword">import</a> <a id="918" href="Algebra.Bundles.html" class="Module">Algebra.Bundles</a>
<a id="936" class="Keyword">using</a> <a id="942" class="Symbol">(</a><a id="943" href="Algebra.Bundles.html#1758" class="Record">Magma</a><a id="948" class="Symbol">;</a> <a id="950" href="Algebra.Bundles.html#4756" class="Record">Semigroup</a><a id="959" class="Symbol">;</a> <a id="961" href="Algebra.Bundles.html#5119" class="Record">Band</a><a id="965" class="Symbol">)</a>

Expand All @@ -40,7 +40,7 @@

<a id="1499" class="Comment">-- Version 2.0</a>

<a id="rawMagma"></a><a id="1515" href="Algebra.Construct.Zero.html#1515" class="Function">rawMagma</a> <a id="1524" class="Symbol">:</a> <a id="1526" href="Algebra.Bundles.Raw.html#1073" class="Record">RawMagma</a> <a id="1535" href="Algebra.Construct.Zero.html#835" class="Bound">c</a> <a id="1537" href="Algebra.Construct.Zero.html#837" class="Bound">ℓ</a>
<a id="rawMagma"></a><a id="1515" href="Algebra.Construct.Zero.html#1515" class="Function">rawMagma</a> <a id="1524" class="Symbol">:</a> <a id="1526" href="Algebra.Bundles.Raw.html#1242" class="Record">RawMagma</a> <a id="1535" href="Algebra.Construct.Zero.html#835" class="Bound">c</a> <a id="1537" href="Algebra.Construct.Zero.html#837" class="Bound">ℓ</a>
<a id="1539" href="Algebra.Construct.Zero.html#1515" class="Function">rawMagma</a> <a id="1548" class="Symbol">=</a> <a id="1550" href="Algebra.Construct.Terminal.html#994" class="Function">Algebra.Construct.Terminal.rawMagma</a>

<a id="1587" class="Symbol">{-#</a> <a id="1591" class="Keyword">WARNING_ON_USAGE</a> <a id="1608" class="Pragma">rawMagma</a>
Expand Down
Loading

0 comments on commit 3255dac

Please sign in to comment.