571 lines
119 KiB
HTML
571 lines
119 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Algebra.Structures</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="74" class="Comment">-- The Agda standard library</a>
|
||
<a id="103" class="Comment">--</a>
|
||
<a id="106" class="Comment">-- Some algebraic structures (not packed up with sets, operations,</a>
|
||
<a id="173" class="Comment">-- etc.)</a>
|
||
<a id="182" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="256" class="Comment">-- The contents of this module should be accessed via `Algebra`, unless</a>
|
||
<a id="328" class="Comment">-- you want to parameterise it via the equality relation.</a>
|
||
|
||
<a id="387" class="Symbol">{-#</a> <a id="391" class="Keyword">OPTIONS</a> <a id="399" class="Pragma">--without-K</a> <a id="411" class="Pragma">--safe</a> <a id="418" class="Symbol">#-}</a>
|
||
|
||
<a id="423" class="Keyword">open</a> <a id="428" class="Keyword">import</a> <a id="435" href="Relation.Binary.html" class="Module">Relation.Binary</a> <a id="451" class="Keyword">using</a> <a id="457" class="Symbol">(</a><a id="458" href="Relation.Binary.Core.html#882" class="Function">Rel</a><a id="461" class="Symbol">;</a> <a id="463" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a><a id="469" class="Symbol">;</a> <a id="471" href="Relation.Binary.Structures.html#1522" class="Record">IsEquivalence</a><a id="484" class="Symbol">)</a>
|
||
|
||
<a id="487" class="Keyword">module</a> <a id="494" href="Algebra.Structures.html" class="Module">Algebra.Structures</a>
|
||
<a id="515" class="Symbol">{</a><a id="516" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="518" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="519" class="Symbol">}</a> <a id="521" class="Symbol">{</a><a id="522" href="Algebra.Structures.html#522" class="Bound">A</a> <a id="524" class="Symbol">:</a> <a id="526" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="530" href="Algebra.Structures.html#516" class="Bound">a</a><a id="531" class="Symbol">}</a> <a id="534" class="Comment">-- The underlying set</a>
|
||
<a id="558" class="Symbol">(</a><a id="559" href="Algebra.Structures.html#559" class="Bound Operator">_≈_</a> <a id="563" class="Symbol">:</a> <a id="565" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="569" href="Algebra.Structures.html#522" class="Bound">A</a> <a id="571" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="572" class="Symbol">)</a> <a id="577" class="Comment">-- The underlying equality relation</a>
|
||
<a id="615" class="Keyword">where</a>
|
||
|
||
<a id="622" class="Comment">-- The file is divided into sections depending on the arities of the</a>
|
||
<a id="691" class="Comment">-- components of the algebraic structure.</a>
|
||
|
||
<a id="734" class="Keyword">open</a> <a id="739" class="Keyword">import</a> <a id="746" href="Algebra.Core.html" class="Module">Algebra.Core</a>
|
||
<a id="759" class="Keyword">open</a> <a id="764" class="Keyword">import</a> <a id="771" href="Algebra.Definitions.html" class="Module">Algebra.Definitions</a> <a id="791" href="Algebra.Structures.html#559" class="Bound Operator">_≈_</a>
|
||
<a id="795" class="Keyword">import</a> <a id="802" href="Algebra.Consequences.Setoid.html" class="Module">Algebra.Consequences.Setoid</a> <a id="830" class="Symbol">as</a> <a id="833" class="Module">Consequences</a>
|
||
<a id="846" class="Keyword">open</a> <a id="851" class="Keyword">import</a> <a id="858" href="Data.Product.html" class="Module">Data.Product</a> <a id="871" class="Keyword">using</a> <a id="877" class="Symbol">(</a><a id="878" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">_,_</a><a id="881" class="Symbol">;</a> <a id="883" href="Agda.Builtin.Sigma.html#252" class="Field">proj₁</a><a id="888" class="Symbol">;</a> <a id="890" href="Agda.Builtin.Sigma.html#264" class="Field">proj₂</a><a id="895" class="Symbol">)</a>
|
||
<a id="897" class="Keyword">open</a> <a id="902" class="Keyword">import</a> <a id="909" href="Level.html" class="Module">Level</a> <a id="915" class="Keyword">using</a> <a id="921" class="Symbol">(</a><a id="922" href="Agda.Primitive.html#810" class="Primitive Operator">_⊔_</a><a id="925" class="Symbol">)</a>
|
||
|
||
<a id="928" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="1001" class="Comment">-- Structures with 1 binary operation</a>
|
||
<a id="1039" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="1113" class="Keyword">record</a> <a id="IsMagma"></a><a id="1120" href="Algebra.Structures.html#1120" class="Record">IsMagma</a> <a id="1128" class="Symbol">(</a><a id="1129" href="Algebra.Structures.html#1129" class="Bound">∙</a> <a id="1131" class="Symbol">:</a> <a id="1133" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1137" href="Algebra.Structures.html#522" class="Bound">A</a><a id="1138" class="Symbol">)</a> <a id="1140" class="Symbol">:</a> <a id="1142" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1146" class="Symbol">(</a><a id="1147" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="1149" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1151" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="1152" class="Symbol">)</a> <a id="1154" class="Keyword">where</a>
|
||
<a id="1162" class="Keyword">field</a>
|
||
<a id="IsMagma.isEquivalence"></a><a id="1172" href="Algebra.Structures.html#1172" class="Field">isEquivalence</a> <a id="1186" class="Symbol">:</a> <a id="1188" href="Relation.Binary.Structures.html#1522" class="Record">IsEquivalence</a> <a id="1202" href="Algebra.Structures.html#559" class="Bound Operator">_≈_</a>
|
||
<a id="IsMagma.∙-cong"></a><a id="1210" href="Algebra.Structures.html#1210" class="Field">∙-cong</a> <a id="1224" class="Symbol">:</a> <a id="1226" href="Algebra.Definitions.html#862" class="Function">Congruent₂</a> <a id="1237" href="Algebra.Structures.html#1129" class="Bound">∙</a>
|
||
|
||
<a id="1242" class="Keyword">open</a> <a id="1247" href="Relation.Binary.Structures.html#1522" class="Module">IsEquivalence</a> <a id="1261" href="Algebra.Structures.html#1172" class="Field">isEquivalence</a> <a id="1275" class="Keyword">public</a>
|
||
|
||
<a id="IsMagma.setoid"></a><a id="1285" href="Algebra.Structures.html#1285" class="Function">setoid</a> <a id="1292" class="Symbol">:</a> <a id="1294" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1301" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="1303" href="Algebra.Structures.html#518" class="Bound">ℓ</a>
|
||
<a id="1307" href="Algebra.Structures.html#1285" class="Function">setoid</a> <a id="1314" class="Symbol">=</a> <a id="1316" class="Keyword">record</a> <a id="1323" class="Symbol">{</a> <a id="1325" href="Relation.Binary.Bundles.html#1132" class="Field">isEquivalence</a> <a id="1339" class="Symbol">=</a> <a id="1341" href="Algebra.Structures.html#1172" class="Field">isEquivalence</a> <a id="1355" class="Symbol">}</a>
|
||
|
||
<a id="IsMagma.∙-congˡ"></a><a id="1360" href="Algebra.Structures.html#1360" class="Function">∙-congˡ</a> <a id="1368" class="Symbol">:</a> <a id="1370" href="Algebra.Definitions.html#934" class="Function">LeftCongruent</a> <a id="1384" href="Algebra.Structures.html#1129" class="Bound">∙</a>
|
||
<a id="1388" href="Algebra.Structures.html#1360" class="Function">∙-congˡ</a> <a id="1396" href="Algebra.Structures.html#1396" class="Bound">y≈z</a> <a id="1400" class="Symbol">=</a> <a id="1402" href="Algebra.Structures.html#1210" class="Field">∙-cong</a> <a id="1409" href="Relation.Binary.Structures.html#1568" class="Function">refl</a> <a id="1414" href="Algebra.Structures.html#1396" class="Bound">y≈z</a>
|
||
|
||
<a id="IsMagma.∙-congʳ"></a><a id="1421" href="Algebra.Structures.html#1421" class="Function">∙-congʳ</a> <a id="1429" class="Symbol">:</a> <a id="1431" href="Algebra.Definitions.html#1020" class="Function">RightCongruent</a> <a id="1446" href="Algebra.Structures.html#1129" class="Bound">∙</a>
|
||
<a id="1450" href="Algebra.Structures.html#1421" class="Function">∙-congʳ</a> <a id="1458" href="Algebra.Structures.html#1458" class="Bound">y≈z</a> <a id="1462" class="Symbol">=</a> <a id="1464" href="Algebra.Structures.html#1210" class="Field">∙-cong</a> <a id="1471" href="Algebra.Structures.html#1458" class="Bound">y≈z</a> <a id="1475" href="Relation.Binary.Structures.html#1568" class="Function">refl</a>
|
||
|
||
|
||
<a id="1482" class="Keyword">record</a> <a id="IsCommutativeMagma"></a><a id="1489" href="Algebra.Structures.html#1489" class="Record">IsCommutativeMagma</a> <a id="1508" class="Symbol">(</a><a id="1509" href="Algebra.Structures.html#1509" class="Bound">∙</a> <a id="1511" class="Symbol">:</a> <a id="1513" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1517" href="Algebra.Structures.html#522" class="Bound">A</a><a id="1518" class="Symbol">)</a> <a id="1520" class="Symbol">:</a> <a id="1522" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1526" class="Symbol">(</a><a id="1527" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="1529" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1531" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="1532" class="Symbol">)</a> <a id="1534" class="Keyword">where</a>
|
||
<a id="1542" class="Keyword">field</a>
|
||
<a id="IsCommutativeMagma.isMagma"></a><a id="1552" href="Algebra.Structures.html#1552" class="Field">isMagma</a> <a id="1560" class="Symbol">:</a> <a id="1562" href="Algebra.Structures.html#1120" class="Record">IsMagma</a> <a id="1570" href="Algebra.Structures.html#1509" class="Bound">∙</a>
|
||
<a id="IsCommutativeMagma.comm"></a><a id="1576" href="Algebra.Structures.html#1576" class="Field">comm</a> <a id="1584" class="Symbol">:</a> <a id="1586" href="Algebra.Definitions.html#1195" class="Function">Commutative</a> <a id="1598" href="Algebra.Structures.html#1509" class="Bound">∙</a>
|
||
|
||
<a id="1603" class="Keyword">open</a> <a id="1608" href="Algebra.Structures.html#1120" class="Module">IsMagma</a> <a id="1616" href="Algebra.Structures.html#1552" class="Field">isMagma</a> <a id="1624" class="Keyword">public</a>
|
||
|
||
|
||
<a id="1633" class="Keyword">record</a> <a id="IsSelectiveMagma"></a><a id="1640" href="Algebra.Structures.html#1640" class="Record">IsSelectiveMagma</a> <a id="1657" class="Symbol">(</a><a id="1658" href="Algebra.Structures.html#1658" class="Bound">∙</a> <a id="1660" class="Symbol">:</a> <a id="1662" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1666" href="Algebra.Structures.html#522" class="Bound">A</a><a id="1667" class="Symbol">)</a> <a id="1669" class="Symbol">:</a> <a id="1671" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1675" class="Symbol">(</a><a id="1676" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="1678" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1680" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="1681" class="Symbol">)</a> <a id="1683" class="Keyword">where</a>
|
||
<a id="1691" class="Keyword">field</a>
|
||
<a id="IsSelectiveMagma.isMagma"></a><a id="1701" href="Algebra.Structures.html#1701" class="Field">isMagma</a> <a id="1709" class="Symbol">:</a> <a id="1711" href="Algebra.Structures.html#1120" class="Record">IsMagma</a> <a id="1719" href="Algebra.Structures.html#1658" class="Bound">∙</a>
|
||
<a id="IsSelectiveMagma.sel"></a><a id="1725" href="Algebra.Structures.html#1725" class="Field">sel</a> <a id="1733" class="Symbol">:</a> <a id="1735" href="Algebra.Definitions.html#2782" class="Function">Selective</a> <a id="1745" href="Algebra.Structures.html#1658" class="Bound">∙</a>
|
||
|
||
<a id="1750" class="Keyword">open</a> <a id="1755" href="Algebra.Structures.html#1120" class="Module">IsMagma</a> <a id="1763" href="Algebra.Structures.html#1701" class="Field">isMagma</a> <a id="1771" class="Keyword">public</a>
|
||
|
||
|
||
<a id="1780" class="Keyword">record</a> <a id="IsSemigroup"></a><a id="1787" href="Algebra.Structures.html#1787" class="Record">IsSemigroup</a> <a id="1799" class="Symbol">(</a><a id="1800" href="Algebra.Structures.html#1800" class="Bound">∙</a> <a id="1802" class="Symbol">:</a> <a id="1804" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1808" href="Algebra.Structures.html#522" class="Bound">A</a><a id="1809" class="Symbol">)</a> <a id="1811" class="Symbol">:</a> <a id="1813" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1817" class="Symbol">(</a><a id="1818" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="1820" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1822" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="1823" class="Symbol">)</a> <a id="1825" class="Keyword">where</a>
|
||
<a id="1833" class="Keyword">field</a>
|
||
<a id="IsSemigroup.isMagma"></a><a id="1843" href="Algebra.Structures.html#1843" class="Field">isMagma</a> <a id="1851" class="Symbol">:</a> <a id="1853" href="Algebra.Structures.html#1120" class="Record">IsMagma</a> <a id="1861" href="Algebra.Structures.html#1800" class="Bound">∙</a>
|
||
<a id="IsSemigroup.assoc"></a><a id="1867" href="Algebra.Structures.html#1867" class="Field">assoc</a> <a id="1875" class="Symbol">:</a> <a id="1877" href="Algebra.Definitions.html#1108" class="Function">Associative</a> <a id="1889" href="Algebra.Structures.html#1800" class="Bound">∙</a>
|
||
|
||
<a id="1894" class="Keyword">open</a> <a id="1899" href="Algebra.Structures.html#1120" class="Module">IsMagma</a> <a id="1907" href="Algebra.Structures.html#1843" class="Field">isMagma</a> <a id="1915" class="Keyword">public</a>
|
||
|
||
|
||
<a id="1924" class="Keyword">record</a> <a id="IsBand"></a><a id="1931" href="Algebra.Structures.html#1931" class="Record">IsBand</a> <a id="1938" class="Symbol">(</a><a id="1939" href="Algebra.Structures.html#1939" class="Bound">∙</a> <a id="1941" class="Symbol">:</a> <a id="1943" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1947" href="Algebra.Structures.html#522" class="Bound">A</a><a id="1948" class="Symbol">)</a> <a id="1950" class="Symbol">:</a> <a id="1952" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1956" class="Symbol">(</a><a id="1957" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="1959" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1961" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="1962" class="Symbol">)</a> <a id="1964" class="Keyword">where</a>
|
||
<a id="1972" class="Keyword">field</a>
|
||
<a id="IsBand.isSemigroup"></a><a id="1982" href="Algebra.Structures.html#1982" class="Field">isSemigroup</a> <a id="1994" class="Symbol">:</a> <a id="1996" href="Algebra.Structures.html#1787" class="Record">IsSemigroup</a> <a id="2008" href="Algebra.Structures.html#1939" class="Bound">∙</a>
|
||
<a id="IsBand.idem"></a><a id="2014" href="Algebra.Structures.html#2014" class="Field">idem</a> <a id="2026" class="Symbol">:</a> <a id="2028" href="Algebra.Definitions.html#2647" class="Function">Idempotent</a> <a id="2039" href="Algebra.Structures.html#1939" class="Bound">∙</a>
|
||
|
||
<a id="2044" class="Keyword">open</a> <a id="2049" href="Algebra.Structures.html#1787" class="Module">IsSemigroup</a> <a id="2061" href="Algebra.Structures.html#1982" class="Field">isSemigroup</a> <a id="2073" class="Keyword">public</a>
|
||
|
||
|
||
<a id="2082" class="Keyword">record</a> <a id="IsCommutativeSemigroup"></a><a id="2089" href="Algebra.Structures.html#2089" class="Record">IsCommutativeSemigroup</a> <a id="2112" class="Symbol">(</a><a id="2113" href="Algebra.Structures.html#2113" class="Bound">∙</a> <a id="2115" class="Symbol">:</a> <a id="2117" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2121" href="Algebra.Structures.html#522" class="Bound">A</a><a id="2122" class="Symbol">)</a> <a id="2124" class="Symbol">:</a> <a id="2126" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2130" class="Symbol">(</a><a id="2131" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="2133" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2135" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="2136" class="Symbol">)</a> <a id="2138" class="Keyword">where</a>
|
||
<a id="2146" class="Keyword">field</a>
|
||
<a id="IsCommutativeSemigroup.isSemigroup"></a><a id="2156" href="Algebra.Structures.html#2156" class="Field">isSemigroup</a> <a id="2168" class="Symbol">:</a> <a id="2170" href="Algebra.Structures.html#1787" class="Record">IsSemigroup</a> <a id="2182" href="Algebra.Structures.html#2113" class="Bound">∙</a>
|
||
<a id="IsCommutativeSemigroup.comm"></a><a id="2188" href="Algebra.Structures.html#2188" class="Field">comm</a> <a id="2200" class="Symbol">:</a> <a id="2202" href="Algebra.Definitions.html#1195" class="Function">Commutative</a> <a id="2214" href="Algebra.Structures.html#2113" class="Bound">∙</a>
|
||
|
||
<a id="2219" class="Keyword">open</a> <a id="2224" href="Algebra.Structures.html#1787" class="Module">IsSemigroup</a> <a id="2236" href="Algebra.Structures.html#2156" class="Field">isSemigroup</a> <a id="2248" class="Keyword">public</a>
|
||
|
||
<a id="IsCommutativeSemigroup.isCommutativeMagma"></a><a id="2258" href="Algebra.Structures.html#2258" class="Function">isCommutativeMagma</a> <a id="2277" class="Symbol">:</a> <a id="2279" href="Algebra.Structures.html#1489" class="Record">IsCommutativeMagma</a> <a id="2298" href="Algebra.Structures.html#2113" class="Bound">∙</a>
|
||
<a id="2302" href="Algebra.Structures.html#2258" class="Function">isCommutativeMagma</a> <a id="2321" class="Symbol">=</a> <a id="2323" class="Keyword">record</a>
|
||
<a id="2334" class="Symbol">{</a> <a id="2336" href="Algebra.Structures.html#1552" class="Field">isMagma</a> <a id="2344" class="Symbol">=</a> <a id="2346" href="Algebra.Structures.html#1843" class="Function">isMagma</a>
|
||
<a id="2358" class="Symbol">;</a> <a id="2360" href="Algebra.Structures.html#1576" class="Field">comm</a> <a id="2368" class="Symbol">=</a> <a id="2370" href="Algebra.Structures.html#2188" class="Field">comm</a>
|
||
<a id="2379" class="Symbol">}</a>
|
||
|
||
|
||
<a id="2383" class="Keyword">record</a> <a id="IsSemilattice"></a><a id="2390" href="Algebra.Structures.html#2390" class="Record">IsSemilattice</a> <a id="2404" class="Symbol">(</a><a id="2405" href="Algebra.Structures.html#2405" class="Bound">∧</a> <a id="2407" class="Symbol">:</a> <a id="2409" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2413" href="Algebra.Structures.html#522" class="Bound">A</a><a id="2414" class="Symbol">)</a> <a id="2416" class="Symbol">:</a> <a id="2418" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2422" class="Symbol">(</a><a id="2423" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="2425" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2427" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="2428" class="Symbol">)</a> <a id="2430" class="Keyword">where</a>
|
||
<a id="2438" class="Keyword">field</a>
|
||
<a id="IsSemilattice.isBand"></a><a id="2448" href="Algebra.Structures.html#2448" class="Field">isBand</a> <a id="2455" class="Symbol">:</a> <a id="2457" href="Algebra.Structures.html#1931" class="Record">IsBand</a> <a id="2464" href="Algebra.Structures.html#2405" class="Bound">∧</a>
|
||
<a id="IsSemilattice.comm"></a><a id="2470" href="Algebra.Structures.html#2470" class="Field">comm</a> <a id="2477" class="Symbol">:</a> <a id="2479" href="Algebra.Definitions.html#1195" class="Function">Commutative</a> <a id="2491" href="Algebra.Structures.html#2405" class="Bound">∧</a>
|
||
|
||
<a id="2496" class="Keyword">open</a> <a id="2501" href="Algebra.Structures.html#1931" class="Module">IsBand</a> <a id="2508" href="Algebra.Structures.html#2448" class="Field">isBand</a> <a id="2515" class="Keyword">public</a>
|
||
<a id="2526" class="Keyword">renaming</a> <a id="2535" class="Symbol">(</a><a id="2536" href="Algebra.Structures.html#1210" class="Function">∙-cong</a> <a id="2543" class="Symbol">to</a> <a id="2546" class="Function">∧-cong</a><a id="2552" class="Symbol">;</a> <a id="2554" href="Algebra.Structures.html#1360" class="Function">∙-congˡ</a> <a id="2562" class="Symbol">to</a> <a id="2565" class="Function">∧-congˡ</a><a id="2572" class="Symbol">;</a> <a id="2574" href="Algebra.Structures.html#1421" class="Function">∙-congʳ</a> <a id="2582" class="Symbol">to</a> <a id="2585" class="Function">∧-congʳ</a><a id="2592" class="Symbol">)</a>
|
||
|
||
|
||
|
||
<a id="2597" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="2670" class="Comment">-- Structures with 1 binary operation & 1 element</a>
|
||
<a id="2720" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="2794" class="Keyword">record</a> <a id="IsMonoid"></a><a id="2801" href="Algebra.Structures.html#2801" class="Record">IsMonoid</a> <a id="2810" class="Symbol">(</a><a id="2811" href="Algebra.Structures.html#2811" class="Bound">∙</a> <a id="2813" class="Symbol">:</a> <a id="2815" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2819" href="Algebra.Structures.html#522" class="Bound">A</a><a id="2820" class="Symbol">)</a> <a id="2822" class="Symbol">(</a><a id="2823" href="Algebra.Structures.html#2823" class="Bound">ε</a> <a id="2825" class="Symbol">:</a> <a id="2827" href="Algebra.Structures.html#522" class="Bound">A</a><a id="2828" class="Symbol">)</a> <a id="2830" class="Symbol">:</a> <a id="2832" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2836" class="Symbol">(</a><a id="2837" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="2839" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2841" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="2842" class="Symbol">)</a> <a id="2844" class="Keyword">where</a>
|
||
<a id="2852" class="Keyword">field</a>
|
||
<a id="IsMonoid.isSemigroup"></a><a id="2862" href="Algebra.Structures.html#2862" class="Field">isSemigroup</a> <a id="2874" class="Symbol">:</a> <a id="2876" href="Algebra.Structures.html#1787" class="Record">IsSemigroup</a> <a id="2888" href="Algebra.Structures.html#2811" class="Bound">∙</a>
|
||
<a id="IsMonoid.identity"></a><a id="2894" href="Algebra.Structures.html#2894" class="Field">identity</a> <a id="2906" class="Symbol">:</a> <a id="2908" href="Algebra.Definitions.html#1416" class="Function">Identity</a> <a id="2917" href="Algebra.Structures.html#2823" class="Bound">ε</a> <a id="2919" href="Algebra.Structures.html#2811" class="Bound">∙</a>
|
||
|
||
<a id="2924" class="Keyword">open</a> <a id="2929" href="Algebra.Structures.html#1787" class="Module">IsSemigroup</a> <a id="2941" href="Algebra.Structures.html#2862" class="Field">isSemigroup</a> <a id="2953" class="Keyword">public</a>
|
||
|
||
<a id="IsMonoid.identityˡ"></a><a id="2963" href="Algebra.Structures.html#2963" class="Function">identityˡ</a> <a id="2973" class="Symbol">:</a> <a id="2975" href="Algebra.Definitions.html#1268" class="Function">LeftIdentity</a> <a id="2988" href="Algebra.Structures.html#2823" class="Bound">ε</a> <a id="2990" href="Algebra.Structures.html#2811" class="Bound">∙</a>
|
||
<a id="2994" href="Algebra.Structures.html#2963" class="Function">identityˡ</a> <a id="3004" class="Symbol">=</a> <a id="3006" href="Agda.Builtin.Sigma.html#252" class="Field">proj₁</a> <a id="3012" href="Algebra.Structures.html#2894" class="Field">identity</a>
|
||
|
||
<a id="IsMonoid.identityʳ"></a><a id="3024" href="Algebra.Structures.html#3024" class="Function">identityʳ</a> <a id="3034" class="Symbol">:</a> <a id="3036" href="Algebra.Definitions.html#1341" class="Function">RightIdentity</a> <a id="3050" href="Algebra.Structures.html#2823" class="Bound">ε</a> <a id="3052" href="Algebra.Structures.html#2811" class="Bound">∙</a>
|
||
<a id="3056" href="Algebra.Structures.html#3024" class="Function">identityʳ</a> <a id="3066" class="Symbol">=</a> <a id="3068" href="Agda.Builtin.Sigma.html#264" class="Field">proj₂</a> <a id="3074" href="Algebra.Structures.html#2894" class="Field">identity</a>
|
||
|
||
|
||
<a id="3085" class="Keyword">record</a> <a id="IsCommutativeMonoid"></a><a id="3092" href="Algebra.Structures.html#3092" class="Record">IsCommutativeMonoid</a> <a id="3112" class="Symbol">(</a><a id="3113" href="Algebra.Structures.html#3113" class="Bound">∙</a> <a id="3115" class="Symbol">:</a> <a id="3117" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="3121" href="Algebra.Structures.html#522" class="Bound">A</a><a id="3122" class="Symbol">)</a> <a id="3124" class="Symbol">(</a><a id="3125" href="Algebra.Structures.html#3125" class="Bound">ε</a> <a id="3127" class="Symbol">:</a> <a id="3129" href="Algebra.Structures.html#522" class="Bound">A</a><a id="3130" class="Symbol">)</a> <a id="3132" class="Symbol">:</a> <a id="3134" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3138" class="Symbol">(</a><a id="3139" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="3141" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3143" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="3144" class="Symbol">)</a> <a id="3146" class="Keyword">where</a>
|
||
<a id="3154" class="Keyword">field</a>
|
||
<a id="IsCommutativeMonoid.isMonoid"></a><a id="3164" href="Algebra.Structures.html#3164" class="Field">isMonoid</a> <a id="3173" class="Symbol">:</a> <a id="3175" href="Algebra.Structures.html#2801" class="Record">IsMonoid</a> <a id="3184" href="Algebra.Structures.html#3113" class="Bound">∙</a> <a id="3186" href="Algebra.Structures.html#3125" class="Bound">ε</a>
|
||
<a id="IsCommutativeMonoid.comm"></a><a id="3192" href="Algebra.Structures.html#3192" class="Field">comm</a> <a id="3201" class="Symbol">:</a> <a id="3203" href="Algebra.Definitions.html#1195" class="Function">Commutative</a> <a id="3215" href="Algebra.Structures.html#3113" class="Bound">∙</a>
|
||
|
||
<a id="3220" class="Keyword">open</a> <a id="3225" href="Algebra.Structures.html#2801" class="Module">IsMonoid</a> <a id="3234" href="Algebra.Structures.html#3164" class="Field">isMonoid</a> <a id="3243" class="Keyword">public</a>
|
||
|
||
<a id="IsCommutativeMonoid.isCommutativeSemigroup"></a><a id="3253" href="Algebra.Structures.html#3253" class="Function">isCommutativeSemigroup</a> <a id="3276" class="Symbol">:</a> <a id="3278" href="Algebra.Structures.html#2089" class="Record">IsCommutativeSemigroup</a> <a id="3301" href="Algebra.Structures.html#3113" class="Bound">∙</a>
|
||
<a id="3305" href="Algebra.Structures.html#3253" class="Function">isCommutativeSemigroup</a> <a id="3328" class="Symbol">=</a> <a id="3330" class="Keyword">record</a>
|
||
<a id="3341" class="Symbol">{</a> <a id="3343" href="Algebra.Structures.html#2156" class="Field">isSemigroup</a> <a id="3355" class="Symbol">=</a> <a id="3357" href="Algebra.Structures.html#2862" class="Function">isSemigroup</a>
|
||
<a id="3373" class="Symbol">;</a> <a id="3375" href="Algebra.Structures.html#2188" class="Field">comm</a> <a id="3387" class="Symbol">=</a> <a id="3389" href="Algebra.Structures.html#3192" class="Field">comm</a>
|
||
<a id="3398" class="Symbol">}</a>
|
||
|
||
<a id="3403" class="Keyword">open</a> <a id="3408" href="Algebra.Structures.html#2089" class="Module">IsCommutativeSemigroup</a> <a id="3431" href="Algebra.Structures.html#3253" class="Function">isCommutativeSemigroup</a> <a id="3454" class="Keyword">public</a>
|
||
<a id="3465" class="Keyword">using</a> <a id="3471" class="Symbol">(</a><a id="3472" href="Algebra.Structures.html#2258" class="Function">isCommutativeMagma</a><a id="3490" class="Symbol">)</a>
|
||
|
||
|
||
<a id="3494" class="Keyword">record</a> <a id="IsIdempotentCommutativeMonoid"></a><a id="3501" href="Algebra.Structures.html#3501" class="Record">IsIdempotentCommutativeMonoid</a> <a id="3531" class="Symbol">(</a><a id="3532" href="Algebra.Structures.html#3532" class="Bound">∙</a> <a id="3534" class="Symbol">:</a> <a id="3536" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="3540" href="Algebra.Structures.html#522" class="Bound">A</a><a id="3541" class="Symbol">)</a>
|
||
<a id="3580" class="Symbol">(</a><a id="3581" href="Algebra.Structures.html#3581" class="Bound">ε</a> <a id="3583" class="Symbol">:</a> <a id="3585" href="Algebra.Structures.html#522" class="Bound">A</a><a id="3586" class="Symbol">)</a> <a id="3588" class="Symbol">:</a> <a id="3590" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3594" class="Symbol">(</a><a id="3595" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="3597" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3599" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="3600" class="Symbol">)</a> <a id="3602" class="Keyword">where</a>
|
||
<a id="3610" class="Keyword">field</a>
|
||
<a id="IsIdempotentCommutativeMonoid.isCommutativeMonoid"></a><a id="3620" href="Algebra.Structures.html#3620" class="Field">isCommutativeMonoid</a> <a id="3640" class="Symbol">:</a> <a id="3642" href="Algebra.Structures.html#3092" class="Record">IsCommutativeMonoid</a> <a id="3662" href="Algebra.Structures.html#3532" class="Bound">∙</a> <a id="3664" href="Algebra.Structures.html#3581" class="Bound">ε</a>
|
||
<a id="IsIdempotentCommutativeMonoid.idem"></a><a id="3670" href="Algebra.Structures.html#3670" class="Field">idem</a> <a id="3690" class="Symbol">:</a> <a id="3692" href="Algebra.Definitions.html#2647" class="Function">Idempotent</a> <a id="3703" href="Algebra.Structures.html#3532" class="Bound">∙</a>
|
||
|
||
<a id="3708" class="Keyword">open</a> <a id="3713" href="Algebra.Structures.html#3092" class="Module">IsCommutativeMonoid</a> <a id="3733" href="Algebra.Structures.html#3620" class="Field">isCommutativeMonoid</a> <a id="3753" class="Keyword">public</a>
|
||
|
||
|
||
<a id="3762" class="Comment">-- Idempotent commutative monoids are also known as bounded lattices.</a>
|
||
<a id="3832" class="Comment">-- Note that the BoundedLattice necessarily uses the notation inherited</a>
|
||
<a id="3904" class="Comment">-- from monoids rather than lattices.</a>
|
||
|
||
<a id="IsBoundedLattice"></a><a id="3943" href="Algebra.Structures.html#3943" class="Function">IsBoundedLattice</a> <a id="3960" class="Symbol">=</a> <a id="3962" href="Algebra.Structures.html#3501" class="Record">IsIdempotentCommutativeMonoid</a>
|
||
|
||
<a id="3993" class="Keyword">module</a> <a id="IsBoundedLattice"></a><a id="4000" href="Algebra.Structures.html#4000" class="Module">IsBoundedLattice</a> <a id="4017" class="Symbol">{</a><a id="4018" href="Algebra.Structures.html#4018" class="Bound">∙</a> <a id="4020" class="Symbol">:</a> <a id="4022" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="4026" href="Algebra.Structures.html#522" class="Bound">A</a><a id="4027" class="Symbol">}</a>
|
||
<a id="4053" class="Symbol">{</a><a id="4054" href="Algebra.Structures.html#4054" class="Bound">ε</a> <a id="4056" class="Symbol">:</a> <a id="4058" href="Algebra.Structures.html#522" class="Bound">A</a><a id="4059" class="Symbol">}</a>
|
||
<a id="4085" class="Symbol">(</a><a id="4086" href="Algebra.Structures.html#4086" class="Bound">isIdemCommMonoid</a> <a id="4103" class="Symbol">:</a> <a id="4105" href="Algebra.Structures.html#3501" class="Record">IsIdempotentCommutativeMonoid</a> <a id="4135" href="Algebra.Structures.html#4018" class="Bound">∙</a> <a id="4137" href="Algebra.Structures.html#4054" class="Bound">ε</a><a id="4138" class="Symbol">)</a> <a id="4140" class="Symbol">=</a>
|
||
<a id="4149" href="Algebra.Structures.html#3501" class="Module">IsIdempotentCommutativeMonoid</a> <a id="4179" href="Algebra.Structures.html#4086" class="Bound">isIdemCommMonoid</a>
|
||
|
||
|
||
<a id="4198" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="4271" class="Comment">-- Structures with 1 binary operation, 1 unary operation & 1 element</a>
|
||
<a id="4340" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="4414" class="Keyword">record</a> <a id="IsGroup"></a><a id="4421" href="Algebra.Structures.html#4421" class="Record">IsGroup</a> <a id="4429" class="Symbol">(</a><a id="4430" href="Algebra.Structures.html#4430" class="Bound Operator">_∙_</a> <a id="4434" class="Symbol">:</a> <a id="4436" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="4440" href="Algebra.Structures.html#522" class="Bound">A</a><a id="4441" class="Symbol">)</a> <a id="4443" class="Symbol">(</a><a id="4444" href="Algebra.Structures.html#4444" class="Bound">ε</a> <a id="4446" class="Symbol">:</a> <a id="4448" href="Algebra.Structures.html#522" class="Bound">A</a><a id="4449" class="Symbol">)</a> <a id="4451" class="Symbol">(</a><a id="4452" href="Algebra.Structures.html#4452" class="Bound Operator">_⁻¹</a> <a id="4456" class="Symbol">:</a> <a id="4458" href="Algebra.Core.html#475" class="Function">Op₁</a> <a id="4462" href="Algebra.Structures.html#522" class="Bound">A</a><a id="4463" class="Symbol">)</a> <a id="4465" class="Symbol">:</a> <a id="4467" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4471" class="Symbol">(</a><a id="4472" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="4474" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="4476" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="4477" class="Symbol">)</a> <a id="4479" class="Keyword">where</a>
|
||
<a id="4487" class="Keyword">field</a>
|
||
<a id="IsGroup.isMonoid"></a><a id="4497" href="Algebra.Structures.html#4497" class="Field">isMonoid</a> <a id="4507" class="Symbol">:</a> <a id="4509" href="Algebra.Structures.html#2801" class="Record">IsMonoid</a> <a id="4518" href="Algebra.Structures.html#4430" class="Bound Operator">_∙_</a> <a id="4522" href="Algebra.Structures.html#4444" class="Bound">ε</a>
|
||
<a id="IsGroup.inverse"></a><a id="4528" href="Algebra.Structures.html#4528" class="Field">inverse</a> <a id="4538" class="Symbol">:</a> <a id="4540" href="Algebra.Definitions.html#1882" class="Function">Inverse</a> <a id="4548" href="Algebra.Structures.html#4444" class="Bound">ε</a> <a id="4550" href="Algebra.Structures.html#4452" class="Bound Operator">_⁻¹</a> <a id="4554" href="Algebra.Structures.html#4430" class="Bound Operator">_∙_</a>
|
||
<a id="IsGroup.⁻¹-cong"></a><a id="4562" href="Algebra.Structures.html#4562" class="Field">⁻¹-cong</a> <a id="4572" class="Symbol">:</a> <a id="4574" href="Algebra.Definitions.html#797" class="Function">Congruent₁</a> <a id="4585" href="Algebra.Structures.html#4452" class="Bound Operator">_⁻¹</a>
|
||
|
||
<a id="4592" class="Keyword">open</a> <a id="4597" href="Algebra.Structures.html#2801" class="Module">IsMonoid</a> <a id="4606" href="Algebra.Structures.html#4497" class="Field">isMonoid</a> <a id="4615" class="Keyword">public</a>
|
||
|
||
<a id="4625" class="Keyword">infixl</a> <a id="4632" class="Number">6</a> <a id="4634" href="Algebra.Structures.html#4640" class="Function Operator">_-_</a>
|
||
<a id="IsGroup._-_"></a><a id="4640" href="Algebra.Structures.html#4640" class="Function Operator">_-_</a> <a id="4644" class="Symbol">:</a> <a id="4646" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="4650" href="Algebra.Structures.html#522" class="Bound">A</a>
|
||
<a id="4654" href="Algebra.Structures.html#4654" class="Bound">x</a> <a id="4656" href="Algebra.Structures.html#4640" class="Function Operator">-</a> <a id="4658" href="Algebra.Structures.html#4658" class="Bound">y</a> <a id="4660" class="Symbol">=</a> <a id="4662" href="Algebra.Structures.html#4654" class="Bound">x</a> <a id="4664" href="Algebra.Structures.html#4430" class="Bound Operator">∙</a> <a id="4666" class="Symbol">(</a><a id="4667" href="Algebra.Structures.html#4658" class="Bound">y</a> <a id="4669" href="Algebra.Structures.html#4452" class="Bound Operator">⁻¹</a><a id="4671" class="Symbol">)</a>
|
||
|
||
<a id="IsGroup.inverseˡ"></a><a id="4676" href="Algebra.Structures.html#4676" class="Function">inverseˡ</a> <a id="4685" class="Symbol">:</a> <a id="4687" href="Algebra.Definitions.html#1704" class="Function">LeftInverse</a> <a id="4699" href="Algebra.Structures.html#4444" class="Bound">ε</a> <a id="4701" href="Algebra.Structures.html#4452" class="Bound Operator">_⁻¹</a> <a id="4705" href="Algebra.Structures.html#4430" class="Bound Operator">_∙_</a>
|
||
<a id="4711" href="Algebra.Structures.html#4676" class="Function">inverseˡ</a> <a id="4720" class="Symbol">=</a> <a id="4722" href="Agda.Builtin.Sigma.html#252" class="Field">proj₁</a> <a id="4728" href="Algebra.Structures.html#4528" class="Field">inverse</a>
|
||
|
||
<a id="IsGroup.inverseʳ"></a><a id="4739" href="Algebra.Structures.html#4739" class="Function">inverseʳ</a> <a id="4748" class="Symbol">:</a> <a id="4750" href="Algebra.Definitions.html#1792" class="Function">RightInverse</a> <a id="4763" href="Algebra.Structures.html#4444" class="Bound">ε</a> <a id="4765" href="Algebra.Structures.html#4452" class="Bound Operator">_⁻¹</a> <a id="4769" href="Algebra.Structures.html#4430" class="Bound Operator">_∙_</a>
|
||
<a id="4775" href="Algebra.Structures.html#4739" class="Function">inverseʳ</a> <a id="4784" class="Symbol">=</a> <a id="4786" href="Agda.Builtin.Sigma.html#264" class="Field">proj₂</a> <a id="4792" href="Algebra.Structures.html#4528" class="Field">inverse</a>
|
||
|
||
<a id="IsGroup.uniqueˡ-⁻¹"></a><a id="4803" href="Algebra.Structures.html#4803" class="Function">uniqueˡ-⁻¹</a> <a id="4814" class="Symbol">:</a> <a id="4816" class="Symbol">∀</a> <a id="4818" href="Algebra.Structures.html#4818" class="Bound">x</a> <a id="4820" href="Algebra.Structures.html#4820" class="Bound">y</a> <a id="4822" class="Symbol">→</a> <a id="4824" class="Symbol">(</a><a id="4825" href="Algebra.Structures.html#4818" class="Bound">x</a> <a id="4827" href="Algebra.Structures.html#4430" class="Bound Operator">∙</a> <a id="4829" href="Algebra.Structures.html#4820" class="Bound">y</a><a id="4830" class="Symbol">)</a> <a id="4832" href="Algebra.Structures.html#559" class="Bound Operator">≈</a> <a id="4834" href="Algebra.Structures.html#4444" class="Bound">ε</a> <a id="4836" class="Symbol">→</a> <a id="4838" href="Algebra.Structures.html#4818" class="Bound">x</a> <a id="4840" href="Algebra.Structures.html#559" class="Bound Operator">≈</a> <a id="4842" class="Symbol">(</a><a id="4843" href="Algebra.Structures.html#4820" class="Bound">y</a> <a id="4845" href="Algebra.Structures.html#4452" class="Bound Operator">⁻¹</a><a id="4847" class="Symbol">)</a>
|
||
<a id="4851" href="Algebra.Structures.html#4803" class="Function">uniqueˡ-⁻¹</a> <a id="4862" class="Symbol">=</a> <a id="4864" href="Algebra.Consequences.Setoid.html#3601" class="Function">Consequences.assoc+id+invʳ⇒invˡ-unique</a>
|
||
<a id="4919" href="Algebra.Structures.html#1285" class="Function">setoid</a> <a id="4926" href="Algebra.Structures.html#1210" class="Function">∙-cong</a> <a id="4933" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="4939" href="Algebra.Structures.html#2894" class="Function">identity</a> <a id="4948" href="Algebra.Structures.html#4739" class="Function">inverseʳ</a>
|
||
|
||
<a id="IsGroup.uniqueʳ-⁻¹"></a><a id="4960" href="Algebra.Structures.html#4960" class="Function">uniqueʳ-⁻¹</a> <a id="4971" class="Symbol">:</a> <a id="4973" class="Symbol">∀</a> <a id="4975" href="Algebra.Structures.html#4975" class="Bound">x</a> <a id="4977" href="Algebra.Structures.html#4977" class="Bound">y</a> <a id="4979" class="Symbol">→</a> <a id="4981" class="Symbol">(</a><a id="4982" href="Algebra.Structures.html#4975" class="Bound">x</a> <a id="4984" href="Algebra.Structures.html#4430" class="Bound Operator">∙</a> <a id="4986" href="Algebra.Structures.html#4977" class="Bound">y</a><a id="4987" class="Symbol">)</a> <a id="4989" href="Algebra.Structures.html#559" class="Bound Operator">≈</a> <a id="4991" href="Algebra.Structures.html#4444" class="Bound">ε</a> <a id="4993" class="Symbol">→</a> <a id="4995" href="Algebra.Structures.html#4977" class="Bound">y</a> <a id="4997" href="Algebra.Structures.html#559" class="Bound Operator">≈</a> <a id="4999" class="Symbol">(</a><a id="5000" href="Algebra.Structures.html#4975" class="Bound">x</a> <a id="5002" href="Algebra.Structures.html#4452" class="Bound Operator">⁻¹</a><a id="5004" class="Symbol">)</a>
|
||
<a id="5008" href="Algebra.Structures.html#4960" class="Function">uniqueʳ-⁻¹</a> <a id="5019" class="Symbol">=</a> <a id="5021" href="Algebra.Consequences.Setoid.html#4088" class="Function">Consequences.assoc+id+invˡ⇒invʳ-unique</a>
|
||
<a id="5076" href="Algebra.Structures.html#1285" class="Function">setoid</a> <a id="5083" href="Algebra.Structures.html#1210" class="Function">∙-cong</a> <a id="5090" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="5096" href="Algebra.Structures.html#2894" class="Function">identity</a> <a id="5105" href="Algebra.Structures.html#4676" class="Function">inverseˡ</a>
|
||
|
||
|
||
<a id="5116" class="Keyword">record</a> <a id="IsAbelianGroup"></a><a id="5123" href="Algebra.Structures.html#5123" class="Record">IsAbelianGroup</a> <a id="5138" class="Symbol">(</a><a id="5139" href="Algebra.Structures.html#5139" class="Bound">∙</a> <a id="5141" class="Symbol">:</a> <a id="5143" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="5147" href="Algebra.Structures.html#522" class="Bound">A</a><a id="5148" class="Symbol">)</a>
|
||
<a id="5172" class="Symbol">(</a><a id="5173" href="Algebra.Structures.html#5173" class="Bound">ε</a> <a id="5175" class="Symbol">:</a> <a id="5177" href="Algebra.Structures.html#522" class="Bound">A</a><a id="5178" class="Symbol">)</a> <a id="5180" class="Symbol">(</a><a id="5181" href="Algebra.Structures.html#5181" class="Bound">⁻¹</a> <a id="5184" class="Symbol">:</a> <a id="5186" href="Algebra.Core.html#475" class="Function">Op₁</a> <a id="5190" href="Algebra.Structures.html#522" class="Bound">A</a><a id="5191" class="Symbol">)</a> <a id="5193" class="Symbol">:</a> <a id="5195" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5199" class="Symbol">(</a><a id="5200" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="5202" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="5204" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="5205" class="Symbol">)</a> <a id="5207" class="Keyword">where</a>
|
||
<a id="5215" class="Keyword">field</a>
|
||
<a id="IsAbelianGroup.isGroup"></a><a id="5225" href="Algebra.Structures.html#5225" class="Field">isGroup</a> <a id="5233" class="Symbol">:</a> <a id="5235" href="Algebra.Structures.html#4421" class="Record">IsGroup</a> <a id="5243" href="Algebra.Structures.html#5139" class="Bound">∙</a> <a id="5245" href="Algebra.Structures.html#5173" class="Bound">ε</a> <a id="5247" href="Algebra.Structures.html#5181" class="Bound">⁻¹</a>
|
||
<a id="IsAbelianGroup.comm"></a><a id="5254" href="Algebra.Structures.html#5254" class="Field">comm</a> <a id="5262" class="Symbol">:</a> <a id="5264" href="Algebra.Definitions.html#1195" class="Function">Commutative</a> <a id="5276" href="Algebra.Structures.html#5139" class="Bound">∙</a>
|
||
|
||
<a id="5281" class="Keyword">open</a> <a id="5286" href="Algebra.Structures.html#4421" class="Module">IsGroup</a> <a id="5294" href="Algebra.Structures.html#5225" class="Field">isGroup</a> <a id="5302" class="Keyword">public</a>
|
||
|
||
<a id="IsAbelianGroup.isCommutativeMonoid"></a><a id="5312" href="Algebra.Structures.html#5312" class="Function">isCommutativeMonoid</a> <a id="5332" class="Symbol">:</a> <a id="5334" href="Algebra.Structures.html#3092" class="Record">IsCommutativeMonoid</a> <a id="5354" href="Algebra.Structures.html#5139" class="Bound">∙</a> <a id="5356" href="Algebra.Structures.html#5173" class="Bound">ε</a>
|
||
<a id="5360" href="Algebra.Structures.html#5312" class="Function">isCommutativeMonoid</a> <a id="5380" class="Symbol">=</a> <a id="5382" class="Keyword">record</a>
|
||
<a id="5393" class="Symbol">{</a> <a id="5395" href="Algebra.Structures.html#3164" class="Field">isMonoid</a> <a id="5404" class="Symbol">=</a> <a id="5406" href="Algebra.Structures.html#4497" class="Function">isMonoid</a>
|
||
<a id="5419" class="Symbol">;</a> <a id="5421" href="Algebra.Structures.html#3192" class="Field">comm</a> <a id="5430" class="Symbol">=</a> <a id="5432" href="Algebra.Structures.html#5254" class="Field">comm</a>
|
||
<a id="5441" class="Symbol">}</a>
|
||
|
||
<a id="5446" class="Keyword">open</a> <a id="5451" href="Algebra.Structures.html#3092" class="Module">IsCommutativeMonoid</a> <a id="5471" href="Algebra.Structures.html#5312" class="Function">isCommutativeMonoid</a> <a id="5491" class="Keyword">public</a>
|
||
<a id="5502" class="Keyword">using</a> <a id="5508" class="Symbol">(</a><a id="5509" href="Algebra.Structures.html#2258" class="Function">isCommutativeMagma</a><a id="5527" class="Symbol">;</a> <a id="5529" href="Algebra.Structures.html#3253" class="Function">isCommutativeSemigroup</a><a id="5551" class="Symbol">)</a>
|
||
|
||
|
||
<a id="5555" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="5628" class="Comment">-- Structures with 2 binary operations</a>
|
||
<a id="5667" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="5741" class="Comment">-- Note that `IsLattice` is not defined in terms of `IsSemilattice`</a>
|
||
<a id="5809" class="Comment">-- because the idempotence laws of ∨ and ∧ can be derived from the</a>
|
||
<a id="5876" class="Comment">-- absorption laws, which makes the corresponding "idem" fields</a>
|
||
<a id="5940" class="Comment">-- redundant. The derived idempotence laws are stated and proved in</a>
|
||
<a id="6009" class="Comment">-- `Algebra.Properties.Lattice` along with the fact that every lattice</a>
|
||
<a id="6080" class="Comment">-- consists of two semilattices.</a>
|
||
|
||
<a id="6114" class="Keyword">record</a> <a id="IsLattice"></a><a id="6121" href="Algebra.Structures.html#6121" class="Record">IsLattice</a> <a id="6131" class="Symbol">(</a><a id="6132" href="Algebra.Structures.html#6132" class="Bound">∨</a> <a id="6134" href="Algebra.Structures.html#6134" class="Bound">∧</a> <a id="6136" class="Symbol">:</a> <a id="6138" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="6142" href="Algebra.Structures.html#522" class="Bound">A</a><a id="6143" class="Symbol">)</a> <a id="6145" class="Symbol">:</a> <a id="6147" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="6151" class="Symbol">(</a><a id="6152" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="6154" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="6156" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="6157" class="Symbol">)</a> <a id="6159" class="Keyword">where</a>
|
||
<a id="6167" class="Keyword">field</a>
|
||
<a id="IsLattice.isEquivalence"></a><a id="6177" href="Algebra.Structures.html#6177" class="Field">isEquivalence</a> <a id="6191" class="Symbol">:</a> <a id="6193" href="Relation.Binary.Structures.html#1522" class="Record">IsEquivalence</a> <a id="6207" href="Algebra.Structures.html#559" class="Bound Operator">_≈_</a>
|
||
<a id="IsLattice.∨-comm"></a><a id="6215" href="Algebra.Structures.html#6215" class="Field">∨-comm</a> <a id="6229" class="Symbol">:</a> <a id="6231" href="Algebra.Definitions.html#1195" class="Function">Commutative</a> <a id="6243" href="Algebra.Structures.html#6132" class="Bound">∨</a>
|
||
<a id="IsLattice.∨-assoc"></a><a id="6249" href="Algebra.Structures.html#6249" class="Field">∨-assoc</a> <a id="6263" class="Symbol">:</a> <a id="6265" href="Algebra.Definitions.html#1108" class="Function">Associative</a> <a id="6277" href="Algebra.Structures.html#6132" class="Bound">∨</a>
|
||
<a id="IsLattice.∨-cong"></a><a id="6283" href="Algebra.Structures.html#6283" class="Field">∨-cong</a> <a id="6297" class="Symbol">:</a> <a id="6299" href="Algebra.Definitions.html#862" class="Function">Congruent₂</a> <a id="6310" href="Algebra.Structures.html#6132" class="Bound">∨</a>
|
||
<a id="IsLattice.∧-comm"></a><a id="6316" href="Algebra.Structures.html#6316" class="Field">∧-comm</a> <a id="6330" class="Symbol">:</a> <a id="6332" href="Algebra.Definitions.html#1195" class="Function">Commutative</a> <a id="6344" href="Algebra.Structures.html#6134" class="Bound">∧</a>
|
||
<a id="IsLattice.∧-assoc"></a><a id="6350" href="Algebra.Structures.html#6350" class="Field">∧-assoc</a> <a id="6364" class="Symbol">:</a> <a id="6366" href="Algebra.Definitions.html#1108" class="Function">Associative</a> <a id="6378" href="Algebra.Structures.html#6134" class="Bound">∧</a>
|
||
<a id="IsLattice.∧-cong"></a><a id="6384" href="Algebra.Structures.html#6384" class="Field">∧-cong</a> <a id="6398" class="Symbol">:</a> <a id="6400" href="Algebra.Definitions.html#862" class="Function">Congruent₂</a> <a id="6411" href="Algebra.Structures.html#6134" class="Bound">∧</a>
|
||
<a id="IsLattice.absorptive"></a><a id="6417" href="Algebra.Structures.html#6417" class="Field">absorptive</a> <a id="6431" class="Symbol">:</a> <a id="6433" href="Algebra.Definitions.html#2938" class="Function">Absorptive</a> <a id="6444" href="Algebra.Structures.html#6132" class="Bound">∨</a> <a id="6446" href="Algebra.Structures.html#6134" class="Bound">∧</a>
|
||
|
||
<a id="6451" class="Keyword">open</a> <a id="6456" href="Relation.Binary.Structures.html#1522" class="Module">IsEquivalence</a> <a id="6470" href="Algebra.Structures.html#6177" class="Field">isEquivalence</a> <a id="6484" class="Keyword">public</a>
|
||
|
||
<a id="IsLattice.∨-absorbs-∧"></a><a id="6494" href="Algebra.Structures.html#6494" class="Function">∨-absorbs-∧</a> <a id="6506" class="Symbol">:</a> <a id="6508" href="Algebra.Structures.html#6132" class="Bound">∨</a> <a id="6510" href="Algebra.Definitions.html#2859" class="Function Operator">Absorbs</a> <a id="6518" href="Algebra.Structures.html#6134" class="Bound">∧</a>
|
||
<a id="6522" href="Algebra.Structures.html#6494" class="Function">∨-absorbs-∧</a> <a id="6534" class="Symbol">=</a> <a id="6536" href="Agda.Builtin.Sigma.html#252" class="Field">proj₁</a> <a id="6542" href="Algebra.Structures.html#6417" class="Field">absorptive</a>
|
||
|
||
<a id="IsLattice.∧-absorbs-∨"></a><a id="6556" href="Algebra.Structures.html#6556" class="Function">∧-absorbs-∨</a> <a id="6568" class="Symbol">:</a> <a id="6570" href="Algebra.Structures.html#6134" class="Bound">∧</a> <a id="6572" href="Algebra.Definitions.html#2859" class="Function Operator">Absorbs</a> <a id="6580" href="Algebra.Structures.html#6132" class="Bound">∨</a>
|
||
<a id="6584" href="Algebra.Structures.html#6556" class="Function">∧-absorbs-∨</a> <a id="6596" class="Symbol">=</a> <a id="6598" href="Agda.Builtin.Sigma.html#264" class="Field">proj₂</a> <a id="6604" href="Algebra.Structures.html#6417" class="Field">absorptive</a>
|
||
|
||
<a id="IsLattice.∧-congˡ"></a><a id="6618" href="Algebra.Structures.html#6618" class="Function">∧-congˡ</a> <a id="6626" class="Symbol">:</a> <a id="6628" href="Algebra.Definitions.html#934" class="Function">LeftCongruent</a> <a id="6642" href="Algebra.Structures.html#6134" class="Bound">∧</a>
|
||
<a id="6646" href="Algebra.Structures.html#6618" class="Function">∧-congˡ</a> <a id="6654" href="Algebra.Structures.html#6654" class="Bound">y≈z</a> <a id="6658" class="Symbol">=</a> <a id="6660" href="Algebra.Structures.html#6384" class="Field">∧-cong</a> <a id="6667" href="Relation.Binary.Structures.html#1568" class="Function">refl</a> <a id="6672" href="Algebra.Structures.html#6654" class="Bound">y≈z</a>
|
||
|
||
<a id="IsLattice.∧-congʳ"></a><a id="6679" href="Algebra.Structures.html#6679" class="Function">∧-congʳ</a> <a id="6687" class="Symbol">:</a> <a id="6689" href="Algebra.Definitions.html#1020" class="Function">RightCongruent</a> <a id="6704" href="Algebra.Structures.html#6134" class="Bound">∧</a>
|
||
<a id="6708" href="Algebra.Structures.html#6679" class="Function">∧-congʳ</a> <a id="6716" href="Algebra.Structures.html#6716" class="Bound">y≈z</a> <a id="6720" class="Symbol">=</a> <a id="6722" href="Algebra.Structures.html#6384" class="Field">∧-cong</a> <a id="6729" href="Algebra.Structures.html#6716" class="Bound">y≈z</a> <a id="6733" href="Relation.Binary.Structures.html#1568" class="Function">refl</a>
|
||
|
||
<a id="IsLattice.∨-congˡ"></a><a id="6741" href="Algebra.Structures.html#6741" class="Function">∨-congˡ</a> <a id="6749" class="Symbol">:</a> <a id="6751" href="Algebra.Definitions.html#934" class="Function">LeftCongruent</a> <a id="6765" href="Algebra.Structures.html#6132" class="Bound">∨</a>
|
||
<a id="6769" href="Algebra.Structures.html#6741" class="Function">∨-congˡ</a> <a id="6777" href="Algebra.Structures.html#6777" class="Bound">y≈z</a> <a id="6781" class="Symbol">=</a> <a id="6783" href="Algebra.Structures.html#6283" class="Field">∨-cong</a> <a id="6790" href="Relation.Binary.Structures.html#1568" class="Function">refl</a> <a id="6795" href="Algebra.Structures.html#6777" class="Bound">y≈z</a>
|
||
|
||
<a id="IsLattice.∨-congʳ"></a><a id="6802" href="Algebra.Structures.html#6802" class="Function">∨-congʳ</a> <a id="6810" class="Symbol">:</a> <a id="6812" href="Algebra.Definitions.html#1020" class="Function">RightCongruent</a> <a id="6827" href="Algebra.Structures.html#6132" class="Bound">∨</a>
|
||
<a id="6831" href="Algebra.Structures.html#6802" class="Function">∨-congʳ</a> <a id="6839" href="Algebra.Structures.html#6839" class="Bound">y≈z</a> <a id="6843" class="Symbol">=</a> <a id="6845" href="Algebra.Structures.html#6283" class="Field">∨-cong</a> <a id="6852" href="Algebra.Structures.html#6839" class="Bound">y≈z</a> <a id="6856" href="Relation.Binary.Structures.html#1568" class="Function">refl</a>
|
||
|
||
|
||
<a id="6863" class="Keyword">record</a> <a id="IsDistributiveLattice"></a><a id="6870" href="Algebra.Structures.html#6870" class="Record">IsDistributiveLattice</a> <a id="6892" class="Symbol">(</a><a id="6893" href="Algebra.Structures.html#6893" class="Bound">∨</a> <a id="6895" href="Algebra.Structures.html#6895" class="Bound">∧</a> <a id="6897" class="Symbol">:</a> <a id="6899" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="6903" href="Algebra.Structures.html#522" class="Bound">A</a><a id="6904" class="Symbol">)</a> <a id="6906" class="Symbol">:</a> <a id="6908" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="6912" class="Symbol">(</a><a id="6913" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="6915" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="6917" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="6918" class="Symbol">)</a> <a id="6920" class="Keyword">where</a>
|
||
<a id="6928" class="Keyword">field</a>
|
||
<a id="IsDistributiveLattice.isLattice"></a><a id="6938" href="Algebra.Structures.html#6938" class="Field">isLattice</a> <a id="6951" class="Symbol">:</a> <a id="6953" href="Algebra.Structures.html#6121" class="Record">IsLattice</a> <a id="6963" href="Algebra.Structures.html#6893" class="Bound">∨</a> <a id="6965" href="Algebra.Structures.html#6895" class="Bound">∧</a>
|
||
<a id="IsDistributiveLattice.∨-distribʳ-∧"></a><a id="6971" href="Algebra.Structures.html#6971" class="Field">∨-distribʳ-∧</a> <a id="6984" class="Symbol">:</a> <a id="6986" href="Algebra.Structures.html#6893" class="Bound">∨</a> <a id="6988" href="Algebra.Definitions.html#2346" class="Function Operator">DistributesOverʳ</a> <a id="7005" href="Algebra.Structures.html#6895" class="Bound">∧</a>
|
||
|
||
<a id="7010" class="Keyword">open</a> <a id="7015" href="Algebra.Structures.html#6121" class="Module">IsLattice</a> <a id="7025" href="Algebra.Structures.html#6938" class="Field">isLattice</a> <a id="7035" class="Keyword">public</a>
|
||
|
||
<a id="IsDistributiveLattice.∨-∧-distribʳ"></a><a id="7045" href="Algebra.Structures.html#7045" class="Function">∨-∧-distribʳ</a> <a id="7058" class="Symbol">=</a> <a id="7060" href="Algebra.Structures.html#6971" class="Field">∨-distribʳ-∧</a>
|
||
<a id="7075" class="Symbol">{-#</a> <a id="7079" class="Keyword">WARNING_ON_USAGE</a> <a id="7096" class="Pragma">∨-∧-distribʳ</a>
|
||
<a id="7111" class="String">"Warning: ∨-∧-distribʳ was deprecated in v1.1.
|
||
Please use ∨-distribʳ-∧ instead."</a>
|
||
<a id="7196" class="Symbol">#-}</a>
|
||
|
||
<a id="7201" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="7274" class="Comment">-- Structures with 2 binary operations & 1 element</a>
|
||
<a id="7325" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="7399" class="Keyword">record</a> <a id="IsNearSemiring"></a><a id="7406" href="Algebra.Structures.html#7406" class="Record">IsNearSemiring</a> <a id="7421" class="Symbol">(</a><a id="7422" href="Algebra.Structures.html#7422" class="Bound">+</a> <a id="7424" href="Algebra.Structures.html#7424" class="Bound">*</a> <a id="7426" class="Symbol">:</a> <a id="7428" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="7432" href="Algebra.Structures.html#522" class="Bound">A</a><a id="7433" class="Symbol">)</a> <a id="7435" class="Symbol">(</a><a id="7436" href="Algebra.Structures.html#7436" class="Bound">0#</a> <a id="7439" class="Symbol">:</a> <a id="7441" href="Algebra.Structures.html#522" class="Bound">A</a><a id="7442" class="Symbol">)</a> <a id="7444" class="Symbol">:</a> <a id="7446" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="7450" class="Symbol">(</a><a id="7451" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="7453" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="7455" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="7456" class="Symbol">)</a> <a id="7458" class="Keyword">where</a>
|
||
<a id="7466" class="Keyword">field</a>
|
||
<a id="IsNearSemiring.+-isMonoid"></a><a id="7476" href="Algebra.Structures.html#7476" class="Field">+-isMonoid</a> <a id="7490" class="Symbol">:</a> <a id="7492" href="Algebra.Structures.html#2801" class="Record">IsMonoid</a> <a id="7501" href="Algebra.Structures.html#7422" class="Bound">+</a> <a id="7503" href="Algebra.Structures.html#7436" class="Bound">0#</a>
|
||
<a id="IsNearSemiring.*-isSemigroup"></a><a id="7510" href="Algebra.Structures.html#7510" class="Field">*-isSemigroup</a> <a id="7524" class="Symbol">:</a> <a id="7526" href="Algebra.Structures.html#1787" class="Record">IsSemigroup</a> <a id="7538" href="Algebra.Structures.html#7424" class="Bound">*</a>
|
||
<a id="IsNearSemiring.distribʳ"></a><a id="7544" href="Algebra.Structures.html#7544" class="Field">distribʳ</a> <a id="7558" class="Symbol">:</a> <a id="7560" href="Algebra.Structures.html#7424" class="Bound">*</a> <a id="7562" href="Algebra.Definitions.html#2346" class="Function Operator">DistributesOverʳ</a> <a id="7579" href="Algebra.Structures.html#7422" class="Bound">+</a>
|
||
<a id="IsNearSemiring.zeroˡ"></a><a id="7585" href="Algebra.Structures.html#7585" class="Field">zeroˡ</a> <a id="7599" class="Symbol">:</a> <a id="7601" href="Algebra.Definitions.html#1502" class="Function">LeftZero</a> <a id="7610" href="Algebra.Structures.html#7436" class="Bound">0#</a> <a id="7613" href="Algebra.Structures.html#7424" class="Bound">*</a>
|
||
|
||
<a id="7618" class="Keyword">open</a> <a id="7623" href="Algebra.Structures.html#2801" class="Module">IsMonoid</a> <a id="7632" href="Algebra.Structures.html#7476" class="Field">+-isMonoid</a> <a id="7643" class="Keyword">public</a>
|
||
<a id="7654" class="Keyword">renaming</a>
|
||
<a id="7667" class="Symbol">(</a> <a id="7669" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="7681" class="Symbol">to</a> <a id="7684" class="Function">+-assoc</a>
|
||
<a id="7696" class="Symbol">;</a> <a id="7698" href="Algebra.Structures.html#1210" class="Function">∙-cong</a> <a id="7710" class="Symbol">to</a> <a id="7713" class="Function">+-cong</a>
|
||
<a id="7724" class="Symbol">;</a> <a id="7726" href="Algebra.Structures.html#1360" class="Function">∙-congˡ</a> <a id="7738" class="Symbol">to</a> <a id="7741" class="Function">+-congˡ</a>
|
||
<a id="7753" class="Symbol">;</a> <a id="7755" href="Algebra.Structures.html#1421" class="Function">∙-congʳ</a> <a id="7767" class="Symbol">to</a> <a id="7770" class="Function">+-congʳ</a>
|
||
<a id="7782" class="Symbol">;</a> <a id="7784" href="Algebra.Structures.html#2894" class="Field">identity</a> <a id="7796" class="Symbol">to</a> <a id="7799" class="Field">+-identity</a>
|
||
<a id="7814" class="Symbol">;</a> <a id="7816" href="Algebra.Structures.html#2963" class="Function">identityˡ</a> <a id="7828" class="Symbol">to</a> <a id="7831" class="Function">+-identityˡ</a>
|
||
<a id="7847" class="Symbol">;</a> <a id="7849" href="Algebra.Structures.html#3024" class="Function">identityʳ</a> <a id="7861" class="Symbol">to</a> <a id="7864" class="Function">+-identityʳ</a>
|
||
<a id="7880" class="Symbol">;</a> <a id="7882" href="Algebra.Structures.html#1843" class="Function">isMagma</a> <a id="7894" class="Symbol">to</a> <a id="7897" class="Function">+-isMagma</a>
|
||
<a id="7911" class="Symbol">;</a> <a id="7913" href="Algebra.Structures.html#2862" class="Field">isSemigroup</a> <a id="7925" class="Symbol">to</a> <a id="7928" class="Field">+-isSemigroup</a>
|
||
<a id="7946" class="Symbol">)</a>
|
||
|
||
<a id="7951" class="Keyword">open</a> <a id="7956" href="Algebra.Structures.html#1787" class="Module">IsSemigroup</a> <a id="7968" href="Algebra.Structures.html#7510" class="Field">*-isSemigroup</a> <a id="7982" class="Keyword">public</a>
|
||
<a id="7993" class="Keyword">using</a> <a id="7999" class="Symbol">()</a>
|
||
<a id="8006" class="Keyword">renaming</a>
|
||
<a id="8019" class="Symbol">(</a> <a id="8021" href="Algebra.Structures.html#1867" class="Field">assoc</a> <a id="8030" class="Symbol">to</a> <a id="8033" class="Field">*-assoc</a>
|
||
<a id="8045" class="Symbol">;</a> <a id="8047" href="Algebra.Structures.html#1210" class="Function">∙-cong</a> <a id="8056" class="Symbol">to</a> <a id="8059" class="Function">*-cong</a>
|
||
<a id="8070" class="Symbol">;</a> <a id="8072" href="Algebra.Structures.html#1360" class="Function">∙-congˡ</a> <a id="8081" class="Symbol">to</a> <a id="8084" class="Function">*-congˡ</a>
|
||
<a id="8096" class="Symbol">;</a> <a id="8098" href="Algebra.Structures.html#1421" class="Function">∙-congʳ</a> <a id="8107" class="Symbol">to</a> <a id="8110" class="Function">*-congʳ</a>
|
||
<a id="8122" class="Symbol">;</a> <a id="8124" href="Algebra.Structures.html#1843" class="Field">isMagma</a> <a id="8133" class="Symbol">to</a> <a id="8136" class="Field">*-isMagma</a>
|
||
<a id="8150" class="Symbol">)</a>
|
||
|
||
|
||
<a id="8154" class="Keyword">record</a> <a id="IsSemiringWithoutOne"></a><a id="8161" href="Algebra.Structures.html#8161" class="Record">IsSemiringWithoutOne</a> <a id="8182" class="Symbol">(</a><a id="8183" href="Algebra.Structures.html#8183" class="Bound">+</a> <a id="8185" href="Algebra.Structures.html#8185" class="Bound">*</a> <a id="8187" class="Symbol">:</a> <a id="8189" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="8193" href="Algebra.Structures.html#522" class="Bound">A</a><a id="8194" class="Symbol">)</a> <a id="8196" class="Symbol">(</a><a id="8197" href="Algebra.Structures.html#8197" class="Bound">0#</a> <a id="8200" class="Symbol">:</a> <a id="8202" href="Algebra.Structures.html#522" class="Bound">A</a><a id="8203" class="Symbol">)</a> <a id="8205" class="Symbol">:</a> <a id="8207" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="8211" class="Symbol">(</a><a id="8212" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="8214" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="8216" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="8217" class="Symbol">)</a> <a id="8219" class="Keyword">where</a>
|
||
<a id="8227" class="Keyword">field</a>
|
||
<a id="IsSemiringWithoutOne.+-isCommutativeMonoid"></a><a id="8237" href="Algebra.Structures.html#8237" class="Field">+-isCommutativeMonoid</a> <a id="8259" class="Symbol">:</a> <a id="8261" href="Algebra.Structures.html#3092" class="Record">IsCommutativeMonoid</a> <a id="8281" href="Algebra.Structures.html#8183" class="Bound">+</a> <a id="8283" href="Algebra.Structures.html#8197" class="Bound">0#</a>
|
||
<a id="IsSemiringWithoutOne.*-isSemigroup"></a><a id="8290" href="Algebra.Structures.html#8290" class="Field">*-isSemigroup</a> <a id="8312" class="Symbol">:</a> <a id="8314" href="Algebra.Structures.html#1787" class="Record">IsSemigroup</a> <a id="8326" href="Algebra.Structures.html#8185" class="Bound">*</a>
|
||
<a id="IsSemiringWithoutOne.distrib"></a><a id="8332" href="Algebra.Structures.html#8332" class="Field">distrib</a> <a id="8354" class="Symbol">:</a> <a id="8356" href="Algebra.Structures.html#8185" class="Bound">*</a> <a id="8358" href="Algebra.Definitions.html#2465" class="Function Operator">DistributesOver</a> <a id="8374" href="Algebra.Structures.html#8183" class="Bound">+</a>
|
||
<a id="IsSemiringWithoutOne.zero"></a><a id="8380" href="Algebra.Structures.html#8380" class="Field">zero</a> <a id="8402" class="Symbol">:</a> <a id="8404" href="Algebra.Definitions.html#1634" class="Function">Zero</a> <a id="8409" href="Algebra.Structures.html#8197" class="Bound">0#</a> <a id="8412" href="Algebra.Structures.html#8185" class="Bound">*</a>
|
||
|
||
<a id="8417" class="Keyword">open</a> <a id="8422" href="Algebra.Structures.html#3092" class="Module">IsCommutativeMonoid</a> <a id="8442" href="Algebra.Structures.html#8237" class="Field">+-isCommutativeMonoid</a> <a id="8464" class="Keyword">public</a>
|
||
<a id="8475" class="Keyword">using</a> <a id="8481" class="Symbol">()</a>
|
||
<a id="8488" class="Keyword">renaming</a>
|
||
<a id="8501" class="Symbol">(</a> <a id="8503" href="Algebra.Structures.html#3192" class="Field">comm</a> <a id="8526" class="Symbol">to</a> <a id="8529" class="Field">+-comm</a>
|
||
<a id="8540" class="Symbol">;</a> <a id="8542" href="Algebra.Structures.html#3164" class="Field">isMonoid</a> <a id="8565" class="Symbol">to</a> <a id="8568" class="Field">+-isMonoid</a>
|
||
<a id="8583" class="Symbol">;</a> <a id="8585" href="Algebra.Structures.html#2258" class="Function">isCommutativeMagma</a> <a id="8608" class="Symbol">to</a> <a id="8611" class="Function">+-isCommutativeMagma</a>
|
||
<a id="8636" class="Symbol">;</a> <a id="8638" href="Algebra.Structures.html#3253" class="Function">isCommutativeSemigroup</a> <a id="8661" class="Symbol">to</a> <a id="8664" class="Function">+-isCommutativeSemigroup</a>
|
||
<a id="8693" class="Symbol">)</a>
|
||
|
||
<a id="IsSemiringWithoutOne.zeroˡ"></a><a id="8698" href="Algebra.Structures.html#8698" class="Function">zeroˡ</a> <a id="8704" class="Symbol">:</a> <a id="8706" href="Algebra.Definitions.html#1502" class="Function">LeftZero</a> <a id="8715" href="Algebra.Structures.html#8197" class="Bound">0#</a> <a id="8718" href="Algebra.Structures.html#8185" class="Bound">*</a>
|
||
<a id="8722" href="Algebra.Structures.html#8698" class="Function">zeroˡ</a> <a id="8728" class="Symbol">=</a> <a id="8730" href="Agda.Builtin.Sigma.html#252" class="Field">proj₁</a> <a id="8736" href="Algebra.Structures.html#8380" class="Field">zero</a>
|
||
|
||
<a id="IsSemiringWithoutOne.zeroʳ"></a><a id="8744" href="Algebra.Structures.html#8744" class="Function">zeroʳ</a> <a id="8750" class="Symbol">:</a> <a id="8752" href="Algebra.Definitions.html#1567" class="Function">RightZero</a> <a id="8762" href="Algebra.Structures.html#8197" class="Bound">0#</a> <a id="8765" href="Algebra.Structures.html#8185" class="Bound">*</a>
|
||
<a id="8769" href="Algebra.Structures.html#8744" class="Function">zeroʳ</a> <a id="8775" class="Symbol">=</a> <a id="8777" href="Agda.Builtin.Sigma.html#264" class="Field">proj₂</a> <a id="8783" href="Algebra.Structures.html#8380" class="Field">zero</a>
|
||
|
||
<a id="IsSemiringWithoutOne.isNearSemiring"></a><a id="8791" href="Algebra.Structures.html#8791" class="Function">isNearSemiring</a> <a id="8806" class="Symbol">:</a> <a id="8808" href="Algebra.Structures.html#7406" class="Record">IsNearSemiring</a> <a id="8823" href="Algebra.Structures.html#8183" class="Bound">+</a> <a id="8825" href="Algebra.Structures.html#8185" class="Bound">*</a> <a id="8827" href="Algebra.Structures.html#8197" class="Bound">0#</a>
|
||
<a id="8832" href="Algebra.Structures.html#8791" class="Function">isNearSemiring</a> <a id="8847" class="Symbol">=</a> <a id="8849" class="Keyword">record</a>
|
||
<a id="8860" class="Symbol">{</a> <a id="8862" href="Algebra.Structures.html#7476" class="Field">+-isMonoid</a> <a id="8876" class="Symbol">=</a> <a id="8878" href="Algebra.Structures.html#8568" class="Function">+-isMonoid</a>
|
||
<a id="8893" class="Symbol">;</a> <a id="8895" href="Algebra.Structures.html#7510" class="Field">*-isSemigroup</a> <a id="8909" class="Symbol">=</a> <a id="8911" href="Algebra.Structures.html#8290" class="Field">*-isSemigroup</a>
|
||
<a id="8929" class="Symbol">;</a> <a id="8931" href="Algebra.Structures.html#7544" class="Field">distribʳ</a> <a id="8945" class="Symbol">=</a> <a id="8947" href="Agda.Builtin.Sigma.html#264" class="Field">proj₂</a> <a id="8953" href="Algebra.Structures.html#8332" class="Field">distrib</a>
|
||
<a id="8965" class="Symbol">;</a> <a id="8967" href="Algebra.Structures.html#7585" class="Field">zeroˡ</a> <a id="8981" class="Symbol">=</a> <a id="8983" href="Algebra.Structures.html#8698" class="Function">zeroˡ</a>
|
||
<a id="8993" class="Symbol">}</a>
|
||
|
||
<a id="8998" class="Keyword">open</a> <a id="9003" href="Algebra.Structures.html#7406" class="Module">IsNearSemiring</a> <a id="9018" href="Algebra.Structures.html#8791" class="Function">isNearSemiring</a> <a id="9033" class="Keyword">public</a>
|
||
<a id="9044" class="Keyword">hiding</a> <a id="9051" class="Symbol">(</a><a id="9052" href="Algebra.Structures.html#7476" class="Field">+-isMonoid</a><a id="9062" class="Symbol">;</a> <a id="9064" href="Algebra.Structures.html#7585" class="Field">zeroˡ</a><a id="9069" class="Symbol">;</a> <a id="9071" href="Algebra.Structures.html#7510" class="Field">*-isSemigroup</a><a id="9084" class="Symbol">)</a>
|
||
|
||
|
||
<a id="9088" class="Keyword">record</a> <a id="IsCommutativeSemiringWithoutOne"></a><a id="9095" href="Algebra.Structures.html#9095" class="Record">IsCommutativeSemiringWithoutOne</a>
|
||
<a id="9136" class="Symbol">(</a><a id="9137" href="Algebra.Structures.html#9137" class="Bound">+</a> <a id="9139" href="Algebra.Structures.html#9139" class="Bound">*</a> <a id="9141" class="Symbol">:</a> <a id="9143" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="9147" href="Algebra.Structures.html#522" class="Bound">A</a><a id="9148" class="Symbol">)</a> <a id="9150" class="Symbol">(</a><a id="9151" href="Algebra.Structures.html#9151" class="Bound">0#</a> <a id="9154" class="Symbol">:</a> <a id="9156" href="Algebra.Structures.html#522" class="Bound">A</a><a id="9157" class="Symbol">)</a> <a id="9159" class="Symbol">:</a> <a id="9161" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="9165" class="Symbol">(</a><a id="9166" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="9168" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="9170" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="9171" class="Symbol">)</a> <a id="9173" class="Keyword">where</a>
|
||
<a id="9181" class="Keyword">field</a>
|
||
<a id="IsCommutativeSemiringWithoutOne.isSemiringWithoutOne"></a><a id="9191" href="Algebra.Structures.html#9191" class="Field">isSemiringWithoutOne</a> <a id="9212" class="Symbol">:</a> <a id="9214" href="Algebra.Structures.html#8161" class="Record">IsSemiringWithoutOne</a> <a id="9235" href="Algebra.Structures.html#9137" class="Bound">+</a> <a id="9237" href="Algebra.Structures.html#9139" class="Bound">*</a> <a id="9239" href="Algebra.Structures.html#9151" class="Bound">0#</a>
|
||
<a id="IsCommutativeSemiringWithoutOne.*-comm"></a><a id="9246" href="Algebra.Structures.html#9246" class="Field">*-comm</a> <a id="9267" class="Symbol">:</a> <a id="9269" href="Algebra.Definitions.html#1195" class="Function">Commutative</a> <a id="9281" href="Algebra.Structures.html#9139" class="Bound">*</a>
|
||
|
||
<a id="9286" class="Keyword">open</a> <a id="9291" href="Algebra.Structures.html#8161" class="Module">IsSemiringWithoutOne</a> <a id="9312" href="Algebra.Structures.html#9191" class="Field">isSemiringWithoutOne</a> <a id="9333" class="Keyword">public</a>
|
||
|
||
<a id="IsCommutativeSemiringWithoutOne.*-isCommutativeSemigroup"></a><a id="9343" href="Algebra.Structures.html#9343" class="Function">*-isCommutativeSemigroup</a> <a id="9368" class="Symbol">:</a> <a id="9370" href="Algebra.Structures.html#2089" class="Record">IsCommutativeSemigroup</a> <a id="9393" href="Algebra.Structures.html#9139" class="Bound">*</a>
|
||
<a id="9397" href="Algebra.Structures.html#9343" class="Function">*-isCommutativeSemigroup</a> <a id="9422" class="Symbol">=</a> <a id="9424" class="Keyword">record</a>
|
||
<a id="9435" class="Symbol">{</a> <a id="9437" href="Algebra.Structures.html#2156" class="Field">isSemigroup</a> <a id="9449" class="Symbol">=</a> <a id="9451" href="Algebra.Structures.html#8290" class="Function">*-isSemigroup</a>
|
||
<a id="9469" class="Symbol">;</a> <a id="9471" href="Algebra.Structures.html#2188" class="Field">comm</a> <a id="9483" class="Symbol">=</a> <a id="9485" href="Algebra.Structures.html#9246" class="Field">*-comm</a>
|
||
<a id="9496" class="Symbol">}</a>
|
||
|
||
<a id="9501" class="Keyword">open</a> <a id="9506" href="Algebra.Structures.html#2089" class="Module">IsCommutativeSemigroup</a> <a id="9529" href="Algebra.Structures.html#9343" class="Function">*-isCommutativeSemigroup</a> <a id="9554" class="Keyword">public</a>
|
||
<a id="9565" class="Keyword">using</a> <a id="9571" class="Symbol">()</a> <a id="9574" class="Keyword">renaming</a> <a id="9583" class="Symbol">(</a><a id="9584" href="Algebra.Structures.html#2258" class="Function">isCommutativeMagma</a> <a id="9603" class="Symbol">to</a> <a id="9606" class="Function">*-isCommutativeMagma</a><a id="9626" class="Symbol">)</a>
|
||
|
||
<a id="9629" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="9702" class="Comment">-- Structures with 2 binary operations & 2 elements</a>
|
||
<a id="9754" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="9828" class="Keyword">record</a> <a id="IsSemiringWithoutAnnihilatingZero"></a><a id="9835" href="Algebra.Structures.html#9835" class="Record">IsSemiringWithoutAnnihilatingZero</a> <a id="9869" class="Symbol">(</a><a id="9870" href="Algebra.Structures.html#9870" class="Bound">+</a> <a id="9872" href="Algebra.Structures.html#9872" class="Bound">*</a> <a id="9874" class="Symbol">:</a> <a id="9876" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="9880" href="Algebra.Structures.html#522" class="Bound">A</a><a id="9881" class="Symbol">)</a>
|
||
<a id="9924" class="Symbol">(</a><a id="9925" href="Algebra.Structures.html#9925" class="Bound">0#</a> <a id="9928" href="Algebra.Structures.html#9928" class="Bound">1#</a> <a id="9931" class="Symbol">:</a> <a id="9933" href="Algebra.Structures.html#522" class="Bound">A</a><a id="9934" class="Symbol">)</a> <a id="9936" class="Symbol">:</a> <a id="9938" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="9942" class="Symbol">(</a><a id="9943" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="9945" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="9947" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="9948" class="Symbol">)</a> <a id="9950" class="Keyword">where</a>
|
||
<a id="9958" class="Keyword">field</a>
|
||
<a id="9968" class="Comment">-- Note that these structures do have an additive unit, but this</a>
|
||
<a id="10037" class="Comment">-- unit does not necessarily annihilate multiplication.</a>
|
||
<a id="IsSemiringWithoutAnnihilatingZero.+-isCommutativeMonoid"></a><a id="10097" href="Algebra.Structures.html#10097" class="Field">+-isCommutativeMonoid</a> <a id="10119" class="Symbol">:</a> <a id="10121" href="Algebra.Structures.html#3092" class="Record">IsCommutativeMonoid</a> <a id="10141" href="Algebra.Structures.html#9870" class="Bound">+</a> <a id="10143" href="Algebra.Structures.html#9925" class="Bound">0#</a>
|
||
<a id="IsSemiringWithoutAnnihilatingZero.*-isMonoid"></a><a id="10150" href="Algebra.Structures.html#10150" class="Field">*-isMonoid</a> <a id="10172" class="Symbol">:</a> <a id="10174" href="Algebra.Structures.html#2801" class="Record">IsMonoid</a> <a id="10183" href="Algebra.Structures.html#9872" class="Bound">*</a> <a id="10185" href="Algebra.Structures.html#9928" class="Bound">1#</a>
|
||
<a id="IsSemiringWithoutAnnihilatingZero.distrib"></a><a id="10192" href="Algebra.Structures.html#10192" class="Field">distrib</a> <a id="10214" class="Symbol">:</a> <a id="10216" href="Algebra.Structures.html#9872" class="Bound">*</a> <a id="10218" href="Algebra.Definitions.html#2465" class="Function Operator">DistributesOver</a> <a id="10234" href="Algebra.Structures.html#9870" class="Bound">+</a>
|
||
|
||
<a id="IsSemiringWithoutAnnihilatingZero.distribˡ"></a><a id="10239" href="Algebra.Structures.html#10239" class="Function">distribˡ</a> <a id="10248" class="Symbol">:</a> <a id="10250" href="Algebra.Structures.html#9872" class="Bound">*</a> <a id="10252" href="Algebra.Definitions.html#2227" class="Function Operator">DistributesOverˡ</a> <a id="10269" href="Algebra.Structures.html#9870" class="Bound">+</a>
|
||
<a id="10273" href="Algebra.Structures.html#10239" class="Function">distribˡ</a> <a id="10282" class="Symbol">=</a> <a id="10284" href="Agda.Builtin.Sigma.html#252" class="Field">proj₁</a> <a id="10290" href="Algebra.Structures.html#10192" class="Field">distrib</a>
|
||
|
||
<a id="IsSemiringWithoutAnnihilatingZero.distribʳ"></a><a id="10301" href="Algebra.Structures.html#10301" class="Function">distribʳ</a> <a id="10310" class="Symbol">:</a> <a id="10312" href="Algebra.Structures.html#9872" class="Bound">*</a> <a id="10314" href="Algebra.Definitions.html#2346" class="Function Operator">DistributesOverʳ</a> <a id="10331" href="Algebra.Structures.html#9870" class="Bound">+</a>
|
||
<a id="10335" href="Algebra.Structures.html#10301" class="Function">distribʳ</a> <a id="10344" class="Symbol">=</a> <a id="10346" href="Agda.Builtin.Sigma.html#264" class="Field">proj₂</a> <a id="10352" href="Algebra.Structures.html#10192" class="Field">distrib</a>
|
||
|
||
<a id="10363" class="Keyword">open</a> <a id="10368" href="Algebra.Structures.html#3092" class="Module">IsCommutativeMonoid</a> <a id="10388" href="Algebra.Structures.html#10097" class="Field">+-isCommutativeMonoid</a> <a id="10410" class="Keyword">public</a>
|
||
<a id="10421" class="Keyword">renaming</a>
|
||
<a id="10434" class="Symbol">(</a> <a id="10436" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="10459" class="Symbol">to</a> <a id="10462" class="Function">+-assoc</a>
|
||
<a id="10474" class="Symbol">;</a> <a id="10476" href="Algebra.Structures.html#1210" class="Function">∙-cong</a> <a id="10499" class="Symbol">to</a> <a id="10502" class="Function">+-cong</a>
|
||
<a id="10513" class="Symbol">;</a> <a id="10515" href="Algebra.Structures.html#1360" class="Function">∙-congˡ</a> <a id="10538" class="Symbol">to</a> <a id="10541" class="Function">+-congˡ</a>
|
||
<a id="10553" class="Symbol">;</a> <a id="10555" href="Algebra.Structures.html#1421" class="Function">∙-congʳ</a> <a id="10578" class="Symbol">to</a> <a id="10581" class="Function">+-congʳ</a>
|
||
<a id="10593" class="Symbol">;</a> <a id="10595" href="Algebra.Structures.html#2894" class="Function">identity</a> <a id="10618" class="Symbol">to</a> <a id="10621" class="Function">+-identity</a>
|
||
<a id="10636" class="Symbol">;</a> <a id="10638" href="Algebra.Structures.html#2963" class="Function">identityˡ</a> <a id="10661" class="Symbol">to</a> <a id="10664" class="Function">+-identityˡ</a>
|
||
<a id="10680" class="Symbol">;</a> <a id="10682" href="Algebra.Structures.html#3024" class="Function">identityʳ</a> <a id="10705" class="Symbol">to</a> <a id="10708" class="Function">+-identityʳ</a>
|
||
<a id="10724" class="Symbol">;</a> <a id="10726" href="Algebra.Structures.html#3192" class="Field">comm</a> <a id="10749" class="Symbol">to</a> <a id="10752" class="Field">+-comm</a>
|
||
<a id="10763" class="Symbol">;</a> <a id="10765" href="Algebra.Structures.html#1843" class="Function">isMagma</a> <a id="10788" class="Symbol">to</a> <a id="10791" class="Function">+-isMagma</a>
|
||
<a id="10805" class="Symbol">;</a> <a id="10807" href="Algebra.Structures.html#2862" class="Function">isSemigroup</a> <a id="10830" class="Symbol">to</a> <a id="10833" class="Function">+-isSemigroup</a>
|
||
<a id="10851" class="Symbol">;</a> <a id="10853" href="Algebra.Structures.html#3164" class="Field">isMonoid</a> <a id="10876" class="Symbol">to</a> <a id="10879" class="Field">+-isMonoid</a>
|
||
<a id="10894" class="Symbol">;</a> <a id="10896" href="Algebra.Structures.html#2258" class="Function">isCommutativeMagma</a> <a id="10919" class="Symbol">to</a> <a id="10922" class="Function">+-isCommutativeMagma</a>
|
||
<a id="10947" class="Symbol">;</a> <a id="10949" href="Algebra.Structures.html#3253" class="Function">isCommutativeSemigroup</a> <a id="10972" class="Symbol">to</a> <a id="10975" class="Function">+-isCommutativeSemigroup</a>
|
||
<a id="11004" class="Symbol">)</a>
|
||
|
||
<a id="11009" class="Keyword">open</a> <a id="11014" href="Algebra.Structures.html#2801" class="Module">IsMonoid</a> <a id="11023" href="Algebra.Structures.html#10150" class="Field">*-isMonoid</a> <a id="11034" class="Keyword">public</a>
|
||
<a id="11045" class="Keyword">using</a> <a id="11051" class="Symbol">()</a>
|
||
<a id="11058" class="Keyword">renaming</a>
|
||
<a id="11071" class="Symbol">(</a> <a id="11073" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="11085" class="Symbol">to</a> <a id="11088" class="Function">*-assoc</a>
|
||
<a id="11100" class="Symbol">;</a> <a id="11102" href="Algebra.Structures.html#1210" class="Function">∙-cong</a> <a id="11114" class="Symbol">to</a> <a id="11117" class="Function">*-cong</a>
|
||
<a id="11128" class="Symbol">;</a> <a id="11130" href="Algebra.Structures.html#1360" class="Function">∙-congˡ</a> <a id="11142" class="Symbol">to</a> <a id="11145" class="Function">*-congˡ</a>
|
||
<a id="11157" class="Symbol">;</a> <a id="11159" href="Algebra.Structures.html#1421" class="Function">∙-congʳ</a> <a id="11171" class="Symbol">to</a> <a id="11174" class="Function">*-congʳ</a>
|
||
<a id="11186" class="Symbol">;</a> <a id="11188" href="Algebra.Structures.html#2894" class="Field">identity</a> <a id="11200" class="Symbol">to</a> <a id="11203" class="Field">*-identity</a>
|
||
<a id="11218" class="Symbol">;</a> <a id="11220" href="Algebra.Structures.html#2963" class="Function">identityˡ</a> <a id="11232" class="Symbol">to</a> <a id="11235" class="Function">*-identityˡ</a>
|
||
<a id="11251" class="Symbol">;</a> <a id="11253" href="Algebra.Structures.html#3024" class="Function">identityʳ</a> <a id="11265" class="Symbol">to</a> <a id="11268" class="Function">*-identityʳ</a>
|
||
<a id="11284" class="Symbol">;</a> <a id="11286" href="Algebra.Structures.html#1843" class="Function">isMagma</a> <a id="11298" class="Symbol">to</a> <a id="11301" class="Function">*-isMagma</a>
|
||
<a id="11315" class="Symbol">;</a> <a id="11317" href="Algebra.Structures.html#2862" class="Field">isSemigroup</a> <a id="11329" class="Symbol">to</a> <a id="11332" class="Field">*-isSemigroup</a>
|
||
<a id="11350" class="Symbol">)</a>
|
||
|
||
|
||
<a id="11354" class="Keyword">record</a> <a id="IsSemiring"></a><a id="11361" href="Algebra.Structures.html#11361" class="Record">IsSemiring</a> <a id="11372" class="Symbol">(</a><a id="11373" href="Algebra.Structures.html#11373" class="Bound">+</a> <a id="11375" href="Algebra.Structures.html#11375" class="Bound">*</a> <a id="11377" class="Symbol">:</a> <a id="11379" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="11383" href="Algebra.Structures.html#522" class="Bound">A</a><a id="11384" class="Symbol">)</a> <a id="11386" class="Symbol">(</a><a id="11387" href="Algebra.Structures.html#11387" class="Bound">0#</a> <a id="11390" href="Algebra.Structures.html#11390" class="Bound">1#</a> <a id="11393" class="Symbol">:</a> <a id="11395" href="Algebra.Structures.html#522" class="Bound">A</a><a id="11396" class="Symbol">)</a> <a id="11398" class="Symbol">:</a> <a id="11400" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="11404" class="Symbol">(</a><a id="11405" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="11407" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="11409" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="11410" class="Symbol">)</a> <a id="11412" class="Keyword">where</a>
|
||
<a id="11420" class="Keyword">field</a>
|
||
<a id="IsSemiring.isSemiringWithoutAnnihilatingZero"></a><a id="11430" href="Algebra.Structures.html#11430" class="Field">isSemiringWithoutAnnihilatingZero</a> <a id="11464" class="Symbol">:</a>
|
||
<a id="11472" href="Algebra.Structures.html#9835" class="Record">IsSemiringWithoutAnnihilatingZero</a> <a id="11506" href="Algebra.Structures.html#11373" class="Bound">+</a> <a id="11508" href="Algebra.Structures.html#11375" class="Bound">*</a> <a id="11510" href="Algebra.Structures.html#11387" class="Bound">0#</a> <a id="11513" href="Algebra.Structures.html#11390" class="Bound">1#</a>
|
||
<a id="IsSemiring.zero"></a><a id="11520" href="Algebra.Structures.html#11520" class="Field">zero</a> <a id="11525" class="Symbol">:</a> <a id="11527" href="Algebra.Definitions.html#1634" class="Function">Zero</a> <a id="11532" href="Algebra.Structures.html#11387" class="Bound">0#</a> <a id="11535" href="Algebra.Structures.html#11375" class="Bound">*</a>
|
||
|
||
<a id="11540" class="Keyword">open</a> <a id="11545" href="Algebra.Structures.html#9835" class="Module">IsSemiringWithoutAnnihilatingZero</a>
|
||
<a id="11588" href="Algebra.Structures.html#11430" class="Field">isSemiringWithoutAnnihilatingZero</a> <a id="11622" class="Keyword">public</a>
|
||
|
||
<a id="IsSemiring.isSemiringWithoutOne"></a><a id="11632" href="Algebra.Structures.html#11632" class="Function">isSemiringWithoutOne</a> <a id="11653" class="Symbol">:</a> <a id="11655" href="Algebra.Structures.html#8161" class="Record">IsSemiringWithoutOne</a> <a id="11676" href="Algebra.Structures.html#11373" class="Bound">+</a> <a id="11678" href="Algebra.Structures.html#11375" class="Bound">*</a> <a id="11680" href="Algebra.Structures.html#11387" class="Bound">0#</a>
|
||
<a id="11685" href="Algebra.Structures.html#11632" class="Function">isSemiringWithoutOne</a> <a id="11706" class="Symbol">=</a> <a id="11708" class="Keyword">record</a>
|
||
<a id="11719" class="Symbol">{</a> <a id="11721" href="Algebra.Structures.html#8237" class="Field">+-isCommutativeMonoid</a> <a id="11743" class="Symbol">=</a> <a id="11745" href="Algebra.Structures.html#10097" class="Function">+-isCommutativeMonoid</a>
|
||
<a id="11771" class="Symbol">;</a> <a id="11773" href="Algebra.Structures.html#8290" class="Field">*-isSemigroup</a> <a id="11795" class="Symbol">=</a> <a id="11797" href="Algebra.Structures.html#11332" class="Function">*-isSemigroup</a>
|
||
<a id="11815" class="Symbol">;</a> <a id="11817" href="Algebra.Structures.html#8332" class="Field">distrib</a> <a id="11839" class="Symbol">=</a> <a id="11841" href="Algebra.Structures.html#10192" class="Function">distrib</a>
|
||
<a id="11853" class="Symbol">;</a> <a id="11855" href="Algebra.Structures.html#8380" class="Field">zero</a> <a id="11877" class="Symbol">=</a> <a id="11879" href="Algebra.Structures.html#11520" class="Field">zero</a>
|
||
<a id="11888" class="Symbol">}</a>
|
||
|
||
<a id="11893" class="Keyword">open</a> <a id="11898" href="Algebra.Structures.html#8161" class="Module">IsSemiringWithoutOne</a> <a id="11919" href="Algebra.Structures.html#11632" class="Function">isSemiringWithoutOne</a> <a id="11940" class="Keyword">public</a>
|
||
<a id="11951" class="Keyword">using</a>
|
||
<a id="11961" class="Symbol">(</a> <a id="11963" href="Algebra.Structures.html#8791" class="Function">isNearSemiring</a>
|
||
<a id="11982" class="Symbol">;</a> <a id="11984" href="Algebra.Structures.html#8698" class="Function">zeroˡ</a>
|
||
<a id="11994" class="Symbol">;</a> <a id="11996" href="Algebra.Structures.html#8744" class="Function">zeroʳ</a>
|
||
<a id="12006" class="Symbol">)</a>
|
||
|
||
|
||
<a id="12010" class="Keyword">record</a> <a id="IsCommutativeSemiring"></a><a id="12017" href="Algebra.Structures.html#12017" class="Record">IsCommutativeSemiring</a> <a id="12039" class="Symbol">(</a><a id="12040" href="Algebra.Structures.html#12040" class="Bound">+</a> <a id="12042" href="Algebra.Structures.html#12042" class="Bound">*</a> <a id="12044" class="Symbol">:</a> <a id="12046" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="12050" href="Algebra.Structures.html#522" class="Bound">A</a><a id="12051" class="Symbol">)</a> <a id="12053" class="Symbol">(</a><a id="12054" href="Algebra.Structures.html#12054" class="Bound">0#</a> <a id="12057" href="Algebra.Structures.html#12057" class="Bound">1#</a> <a id="12060" class="Symbol">:</a> <a id="12062" href="Algebra.Structures.html#522" class="Bound">A</a><a id="12063" class="Symbol">)</a> <a id="12065" class="Symbol">:</a> <a id="12067" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="12071" class="Symbol">(</a><a id="12072" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="12074" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="12076" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="12077" class="Symbol">)</a> <a id="12079" class="Keyword">where</a>
|
||
<a id="12087" class="Keyword">field</a>
|
||
<a id="IsCommutativeSemiring.isSemiring"></a><a id="12097" href="Algebra.Structures.html#12097" class="Field">isSemiring</a> <a id="12108" class="Symbol">:</a> <a id="12110" href="Algebra.Structures.html#11361" class="Record">IsSemiring</a> <a id="12121" href="Algebra.Structures.html#12040" class="Bound">+</a> <a id="12123" href="Algebra.Structures.html#12042" class="Bound">*</a> <a id="12125" href="Algebra.Structures.html#12054" class="Bound">0#</a> <a id="12128" href="Algebra.Structures.html#12057" class="Bound">1#</a>
|
||
<a id="IsCommutativeSemiring.*-comm"></a><a id="12135" href="Algebra.Structures.html#12135" class="Field">*-comm</a> <a id="12146" class="Symbol">:</a> <a id="12148" href="Algebra.Definitions.html#1195" class="Function">Commutative</a> <a id="12160" href="Algebra.Structures.html#12042" class="Bound">*</a>
|
||
|
||
<a id="12165" class="Keyword">open</a> <a id="12170" href="Algebra.Structures.html#11361" class="Module">IsSemiring</a> <a id="12181" href="Algebra.Structures.html#12097" class="Field">isSemiring</a> <a id="12192" class="Keyword">public</a>
|
||
|
||
<a id="IsCommutativeSemiring.isCommutativeSemiringWithoutOne"></a><a id="12202" href="Algebra.Structures.html#12202" class="Function">isCommutativeSemiringWithoutOne</a> <a id="12234" class="Symbol">:</a>
|
||
<a id="12240" href="Algebra.Structures.html#9095" class="Record">IsCommutativeSemiringWithoutOne</a> <a id="12272" href="Algebra.Structures.html#12040" class="Bound">+</a> <a id="12274" href="Algebra.Structures.html#12042" class="Bound">*</a> <a id="12276" href="Algebra.Structures.html#12054" class="Bound">0#</a>
|
||
<a id="12281" href="Algebra.Structures.html#12202" class="Function">isCommutativeSemiringWithoutOne</a> <a id="12313" class="Symbol">=</a> <a id="12315" class="Keyword">record</a>
|
||
<a id="12326" class="Symbol">{</a> <a id="12328" href="Algebra.Structures.html#9191" class="Field">isSemiringWithoutOne</a> <a id="12349" class="Symbol">=</a> <a id="12351" href="Algebra.Structures.html#11632" class="Function">isSemiringWithoutOne</a>
|
||
<a id="12376" class="Symbol">;</a> <a id="12378" href="Algebra.Structures.html#9246" class="Field">*-comm</a> <a id="12385" class="Symbol">=</a> <a id="12387" href="Algebra.Structures.html#12135" class="Field">*-comm</a>
|
||
<a id="12398" class="Symbol">}</a>
|
||
|
||
<a id="12403" class="Keyword">open</a> <a id="12408" href="Algebra.Structures.html#9095" class="Module">IsCommutativeSemiringWithoutOne</a> <a id="12440" href="Algebra.Structures.html#12202" class="Function">isCommutativeSemiringWithoutOne</a> <a id="12472" class="Keyword">public</a>
|
||
<a id="12483" class="Keyword">using</a>
|
||
<a id="12493" class="Symbol">(</a> <a id="12495" href="Algebra.Structures.html#9606" class="Function">*-isCommutativeMagma</a>
|
||
<a id="12520" class="Symbol">;</a> <a id="12522" href="Algebra.Structures.html#9343" class="Function">*-isCommutativeSemigroup</a>
|
||
<a id="12551" class="Symbol">)</a>
|
||
|
||
<a id="IsCommutativeSemiring.*-isCommutativeMonoid"></a><a id="12556" href="Algebra.Structures.html#12556" class="Function">*-isCommutativeMonoid</a> <a id="12578" class="Symbol">:</a> <a id="12580" href="Algebra.Structures.html#3092" class="Record">IsCommutativeMonoid</a> <a id="12600" href="Algebra.Structures.html#12042" class="Bound">*</a> <a id="12602" href="Algebra.Structures.html#12057" class="Bound">1#</a>
|
||
<a id="12607" href="Algebra.Structures.html#12556" class="Function">*-isCommutativeMonoid</a> <a id="12629" class="Symbol">=</a> <a id="12631" class="Keyword">record</a>
|
||
<a id="12642" class="Symbol">{</a> <a id="12644" href="Algebra.Structures.html#3164" class="Field">isMonoid</a> <a id="12653" class="Symbol">=</a> <a id="12655" href="Algebra.Structures.html#10150" class="Function">*-isMonoid</a>
|
||
<a id="12670" class="Symbol">;</a> <a id="12672" href="Algebra.Structures.html#3192" class="Field">comm</a> <a id="12681" class="Symbol">=</a> <a id="12683" href="Algebra.Structures.html#12135" class="Field">*-comm</a>
|
||
<a id="12694" class="Symbol">}</a>
|
||
|
||
|
||
<a id="12698" class="Keyword">record</a> <a id="IsCancellativeCommutativeSemiring"></a><a id="12705" href="Algebra.Structures.html#12705" class="Record">IsCancellativeCommutativeSemiring</a> <a id="12739" class="Symbol">(</a><a id="12740" href="Algebra.Structures.html#12740" class="Bound">+</a> <a id="12742" href="Algebra.Structures.html#12742" class="Bound">*</a> <a id="12744" class="Symbol">:</a> <a id="12746" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="12750" href="Algebra.Structures.html#522" class="Bound">A</a><a id="12751" class="Symbol">)</a> <a id="12753" class="Symbol">(</a><a id="12754" href="Algebra.Structures.html#12754" class="Bound">0#</a> <a id="12757" href="Algebra.Structures.html#12757" class="Bound">1#</a> <a id="12760" class="Symbol">:</a> <a id="12762" href="Algebra.Structures.html#522" class="Bound">A</a><a id="12763" class="Symbol">)</a> <a id="12765" class="Symbol">:</a> <a id="12767" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="12771" class="Symbol">(</a><a id="12772" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="12774" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="12776" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="12777" class="Symbol">)</a> <a id="12779" class="Keyword">where</a>
|
||
<a id="12787" class="Keyword">field</a>
|
||
<a id="IsCancellativeCommutativeSemiring.isCommutativeSemiring"></a><a id="12797" href="Algebra.Structures.html#12797" class="Field">isCommutativeSemiring</a> <a id="12819" class="Symbol">:</a> <a id="12821" href="Algebra.Structures.html#12017" class="Record">IsCommutativeSemiring</a> <a id="12843" href="Algebra.Structures.html#12740" class="Bound">+</a> <a id="12845" href="Algebra.Structures.html#12742" class="Bound">*</a> <a id="12847" href="Algebra.Structures.html#12754" class="Bound">0#</a> <a id="12850" href="Algebra.Structures.html#12757" class="Bound">1#</a>
|
||
<a id="IsCancellativeCommutativeSemiring.*-cancelˡ-nonZero"></a><a id="12857" href="Algebra.Structures.html#12857" class="Field">*-cancelˡ-nonZero</a> <a id="12879" class="Symbol">:</a> <a id="12881" href="Algebra.Definitions.html#3372" class="Function">AlmostLeftCancellative</a> <a id="12904" href="Algebra.Structures.html#12754" class="Bound">0#</a> <a id="12907" href="Algebra.Structures.html#12742" class="Bound">*</a>
|
||
|
||
<a id="12912" class="Keyword">open</a> <a id="12917" href="Algebra.Structures.html#12017" class="Module">IsCommutativeSemiring</a> <a id="12939" href="Algebra.Structures.html#12797" class="Field">isCommutativeSemiring</a> <a id="12961" class="Keyword">public</a>
|
||
|
||
|
||
|
||
<a id="12971" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="13044" class="Comment">-- Structures with 2 binary operations, 1 unary operation & 2 elements</a>
|
||
<a id="13115" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="13189" class="Keyword">record</a> <a id="IsRing"></a><a id="13196" href="Algebra.Structures.html#13196" class="Record">IsRing</a> <a id="13203" class="Symbol">(</a><a id="13204" href="Algebra.Structures.html#13204" class="Bound">+</a> <a id="13206" href="Algebra.Structures.html#13206" class="Bound">*</a> <a id="13208" class="Symbol">:</a> <a id="13210" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="13214" href="Algebra.Structures.html#522" class="Bound">A</a><a id="13215" class="Symbol">)</a> <a id="13217" class="Symbol">(</a><a id="13218" href="Algebra.Structures.html#13218" class="Bound Operator">-_</a> <a id="13221" class="Symbol">:</a> <a id="13223" href="Algebra.Core.html#475" class="Function">Op₁</a> <a id="13227" href="Algebra.Structures.html#522" class="Bound">A</a><a id="13228" class="Symbol">)</a> <a id="13230" class="Symbol">(</a><a id="13231" href="Algebra.Structures.html#13231" class="Bound">0#</a> <a id="13234" href="Algebra.Structures.html#13234" class="Bound">1#</a> <a id="13237" class="Symbol">:</a> <a id="13239" href="Algebra.Structures.html#522" class="Bound">A</a><a id="13240" class="Symbol">)</a> <a id="13242" class="Symbol">:</a> <a id="13244" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="13248" class="Symbol">(</a><a id="13249" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="13251" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="13253" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="13254" class="Symbol">)</a> <a id="13256" class="Keyword">where</a>
|
||
<a id="13264" class="Keyword">field</a>
|
||
<a id="IsRing.+-isAbelianGroup"></a><a id="13274" href="Algebra.Structures.html#13274" class="Field">+-isAbelianGroup</a> <a id="13291" class="Symbol">:</a> <a id="13293" href="Algebra.Structures.html#5123" class="Record">IsAbelianGroup</a> <a id="13308" href="Algebra.Structures.html#13204" class="Bound">+</a> <a id="13310" href="Algebra.Structures.html#13231" class="Bound">0#</a> <a id="13313" href="Algebra.Structures.html#13218" class="Bound Operator">-_</a>
|
||
<a id="IsRing.*-isMonoid"></a><a id="13320" href="Algebra.Structures.html#13320" class="Field">*-isMonoid</a> <a id="13337" class="Symbol">:</a> <a id="13339" href="Algebra.Structures.html#2801" class="Record">IsMonoid</a> <a id="13348" href="Algebra.Structures.html#13206" class="Bound">*</a> <a id="13350" href="Algebra.Structures.html#13234" class="Bound">1#</a>
|
||
<a id="IsRing.distrib"></a><a id="13357" href="Algebra.Structures.html#13357" class="Field">distrib</a> <a id="13374" class="Symbol">:</a> <a id="13376" href="Algebra.Structures.html#13206" class="Bound">*</a> <a id="13378" href="Algebra.Definitions.html#2465" class="Function Operator">DistributesOver</a> <a id="13394" href="Algebra.Structures.html#13204" class="Bound">+</a>
|
||
<a id="IsRing.zero"></a><a id="13400" href="Algebra.Structures.html#13400" class="Field">zero</a> <a id="13417" class="Symbol">:</a> <a id="13419" href="Algebra.Definitions.html#1634" class="Function">Zero</a> <a id="13424" href="Algebra.Structures.html#13231" class="Bound">0#</a> <a id="13427" href="Algebra.Structures.html#13206" class="Bound">*</a>
|
||
|
||
<a id="13432" class="Keyword">open</a> <a id="13437" href="Algebra.Structures.html#5123" class="Module">IsAbelianGroup</a> <a id="13452" href="Algebra.Structures.html#13274" class="Field">+-isAbelianGroup</a> <a id="13469" class="Keyword">public</a>
|
||
<a id="13480" class="Keyword">renaming</a>
|
||
<a id="13493" class="Symbol">(</a> <a id="13495" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="13518" class="Symbol">to</a> <a id="13521" class="Function">+-assoc</a>
|
||
<a id="13533" class="Symbol">;</a> <a id="13535" href="Algebra.Structures.html#1210" class="Function">∙-cong</a> <a id="13558" class="Symbol">to</a> <a id="13561" class="Function">+-cong</a>
|
||
<a id="13572" class="Symbol">;</a> <a id="13574" href="Algebra.Structures.html#1360" class="Function">∙-congˡ</a> <a id="13597" class="Symbol">to</a> <a id="13600" class="Function">+-congˡ</a>
|
||
<a id="13612" class="Symbol">;</a> <a id="13614" href="Algebra.Structures.html#1421" class="Function">∙-congʳ</a> <a id="13637" class="Symbol">to</a> <a id="13640" class="Function">+-congʳ</a>
|
||
<a id="13652" class="Symbol">;</a> <a id="13654" href="Algebra.Structures.html#2894" class="Function">identity</a> <a id="13677" class="Symbol">to</a> <a id="13680" class="Function">+-identity</a>
|
||
<a id="13695" class="Symbol">;</a> <a id="13697" href="Algebra.Structures.html#2963" class="Function">identityˡ</a> <a id="13720" class="Symbol">to</a> <a id="13723" class="Function">+-identityˡ</a>
|
||
<a id="13739" class="Symbol">;</a> <a id="13741" href="Algebra.Structures.html#3024" class="Function">identityʳ</a> <a id="13764" class="Symbol">to</a> <a id="13767" class="Function">+-identityʳ</a>
|
||
<a id="13783" class="Symbol">;</a> <a id="13785" href="Algebra.Structures.html#4528" class="Function">inverse</a> <a id="13808" class="Symbol">to</a> <a id="13811" class="Function">-‿inverse</a>
|
||
<a id="13825" class="Symbol">;</a> <a id="13827" href="Algebra.Structures.html#4676" class="Function">inverseˡ</a> <a id="13850" class="Symbol">to</a> <a id="13853" class="Function">-‿inverseˡ</a>
|
||
<a id="13868" class="Symbol">;</a> <a id="13870" href="Algebra.Structures.html#4739" class="Function">inverseʳ</a> <a id="13893" class="Symbol">to</a> <a id="13896" class="Function">-‿inverseʳ</a>
|
||
<a id="13911" class="Symbol">;</a> <a id="13913" href="Algebra.Structures.html#4562" class="Function">⁻¹-cong</a> <a id="13936" class="Symbol">to</a> <a id="13939" class="Function">-‿cong</a>
|
||
<a id="13950" class="Symbol">;</a> <a id="13952" href="Algebra.Structures.html#5254" class="Field">comm</a> <a id="13975" class="Symbol">to</a> <a id="13978" class="Field">+-comm</a>
|
||
<a id="13989" class="Symbol">;</a> <a id="13991" href="Algebra.Structures.html#1843" class="Function">isMagma</a> <a id="14014" class="Symbol">to</a> <a id="14017" class="Function">+-isMagma</a>
|
||
<a id="14031" class="Symbol">;</a> <a id="14033" href="Algebra.Structures.html#2862" class="Function">isSemigroup</a> <a id="14056" class="Symbol">to</a> <a id="14059" class="Function">+-isSemigroup</a>
|
||
<a id="14077" class="Symbol">;</a> <a id="14079" href="Algebra.Structures.html#4497" class="Function">isMonoid</a> <a id="14102" class="Symbol">to</a> <a id="14105" class="Function">+-isMonoid</a>
|
||
<a id="14120" class="Symbol">;</a> <a id="14122" href="Algebra.Structures.html#2258" class="Function">isCommutativeMagma</a> <a id="14145" class="Symbol">to</a> <a id="14148" class="Function">+-isCommutativeMagma</a>
|
||
<a id="14173" class="Symbol">;</a> <a id="14175" href="Algebra.Structures.html#5312" class="Function">isCommutativeMonoid</a> <a id="14198" class="Symbol">to</a> <a id="14201" class="Function">+-isCommutativeMonoid</a>
|
||
<a id="14227" class="Symbol">;</a> <a id="14229" href="Algebra.Structures.html#3253" class="Function">isCommutativeSemigroup</a> <a id="14252" class="Symbol">to</a> <a id="14255" class="Function">+-isCommutativeSemigroup</a>
|
||
<a id="14284" class="Symbol">;</a> <a id="14286" href="Algebra.Structures.html#5225" class="Field">isGroup</a> <a id="14309" class="Symbol">to</a> <a id="14312" class="Field">+-isGroup</a>
|
||
<a id="14326" class="Symbol">)</a>
|
||
|
||
<a id="14331" class="Keyword">open</a> <a id="14336" href="Algebra.Structures.html#2801" class="Module">IsMonoid</a> <a id="14345" href="Algebra.Structures.html#13320" class="Field">*-isMonoid</a> <a id="14356" class="Keyword">public</a>
|
||
<a id="14367" class="Keyword">using</a> <a id="14373" class="Symbol">()</a>
|
||
<a id="14380" class="Keyword">renaming</a>
|
||
<a id="14393" class="Symbol">(</a> <a id="14395" href="Algebra.Structures.html#1867" class="Function">assoc</a> <a id="14407" class="Symbol">to</a> <a id="14410" class="Function">*-assoc</a>
|
||
<a id="14422" class="Symbol">;</a> <a id="14424" href="Algebra.Structures.html#1210" class="Function">∙-cong</a> <a id="14436" class="Symbol">to</a> <a id="14439" class="Function">*-cong</a>
|
||
<a id="14450" class="Symbol">;</a> <a id="14452" href="Algebra.Structures.html#1360" class="Function">∙-congˡ</a> <a id="14464" class="Symbol">to</a> <a id="14467" class="Function">*-congˡ</a>
|
||
<a id="14479" class="Symbol">;</a> <a id="14481" href="Algebra.Structures.html#1421" class="Function">∙-congʳ</a> <a id="14493" class="Symbol">to</a> <a id="14496" class="Function">*-congʳ</a>
|
||
<a id="14508" class="Symbol">;</a> <a id="14510" href="Algebra.Structures.html#2894" class="Field">identity</a> <a id="14522" class="Symbol">to</a> <a id="14525" class="Field">*-identity</a>
|
||
<a id="14540" class="Symbol">;</a> <a id="14542" href="Algebra.Structures.html#2963" class="Function">identityˡ</a> <a id="14554" class="Symbol">to</a> <a id="14557" class="Function">*-identityˡ</a>
|
||
<a id="14573" class="Symbol">;</a> <a id="14575" href="Algebra.Structures.html#3024" class="Function">identityʳ</a> <a id="14587" class="Symbol">to</a> <a id="14590" class="Function">*-identityʳ</a>
|
||
<a id="14606" class="Symbol">;</a> <a id="14608" href="Algebra.Structures.html#1843" class="Function">isMagma</a> <a id="14620" class="Symbol">to</a> <a id="14623" class="Function">*-isMagma</a>
|
||
<a id="14637" class="Symbol">;</a> <a id="14639" href="Algebra.Structures.html#2862" class="Field">isSemigroup</a> <a id="14651" class="Symbol">to</a> <a id="14654" class="Field">*-isSemigroup</a>
|
||
<a id="14672" class="Symbol">)</a>
|
||
|
||
<a id="IsRing.zeroˡ"></a><a id="14677" href="Algebra.Structures.html#14677" class="Function">zeroˡ</a> <a id="14683" class="Symbol">:</a> <a id="14685" href="Algebra.Definitions.html#1502" class="Function">LeftZero</a> <a id="14694" href="Algebra.Structures.html#13231" class="Bound">0#</a> <a id="14697" href="Algebra.Structures.html#13206" class="Bound">*</a>
|
||
<a id="14701" href="Algebra.Structures.html#14677" class="Function">zeroˡ</a> <a id="14707" class="Symbol">=</a> <a id="14709" href="Agda.Builtin.Sigma.html#252" class="Field">proj₁</a> <a id="14715" href="Algebra.Structures.html#13400" class="Field">zero</a>
|
||
|
||
<a id="IsRing.zeroʳ"></a><a id="14723" href="Algebra.Structures.html#14723" class="Function">zeroʳ</a> <a id="14729" class="Symbol">:</a> <a id="14731" href="Algebra.Definitions.html#1567" class="Function">RightZero</a> <a id="14741" href="Algebra.Structures.html#13231" class="Bound">0#</a> <a id="14744" href="Algebra.Structures.html#13206" class="Bound">*</a>
|
||
<a id="14748" href="Algebra.Structures.html#14723" class="Function">zeroʳ</a> <a id="14754" class="Symbol">=</a> <a id="14756" href="Agda.Builtin.Sigma.html#264" class="Field">proj₂</a> <a id="14762" href="Algebra.Structures.html#13400" class="Field">zero</a>
|
||
|
||
<a id="IsRing.isSemiringWithoutAnnihilatingZero"></a><a id="14770" href="Algebra.Structures.html#14770" class="Function">isSemiringWithoutAnnihilatingZero</a>
|
||
<a id="14808" class="Symbol">:</a> <a id="14810" href="Algebra.Structures.html#9835" class="Record">IsSemiringWithoutAnnihilatingZero</a> <a id="14844" href="Algebra.Structures.html#13204" class="Bound">+</a> <a id="14846" href="Algebra.Structures.html#13206" class="Bound">*</a> <a id="14848" href="Algebra.Structures.html#13231" class="Bound">0#</a> <a id="14851" href="Algebra.Structures.html#13234" class="Bound">1#</a>
|
||
<a id="14856" href="Algebra.Structures.html#14770" class="Function">isSemiringWithoutAnnihilatingZero</a> <a id="14890" class="Symbol">=</a> <a id="14892" class="Keyword">record</a>
|
||
<a id="14903" class="Symbol">{</a> <a id="14905" href="Algebra.Structures.html#10097" class="Field">+-isCommutativeMonoid</a> <a id="14927" class="Symbol">=</a> <a id="14929" href="Algebra.Structures.html#14201" class="Function">+-isCommutativeMonoid</a>
|
||
<a id="14955" class="Symbol">;</a> <a id="14957" href="Algebra.Structures.html#10150" class="Field">*-isMonoid</a> <a id="14979" class="Symbol">=</a> <a id="14981" href="Algebra.Structures.html#13320" class="Field">*-isMonoid</a>
|
||
<a id="14996" class="Symbol">;</a> <a id="14998" href="Algebra.Structures.html#10192" class="Field">distrib</a> <a id="15020" class="Symbol">=</a> <a id="15022" href="Algebra.Structures.html#13357" class="Field">distrib</a>
|
||
<a id="15034" class="Symbol">}</a>
|
||
|
||
<a id="IsRing.isSemiring"></a><a id="15039" href="Algebra.Structures.html#15039" class="Function">isSemiring</a> <a id="15050" class="Symbol">:</a> <a id="15052" href="Algebra.Structures.html#11361" class="Record">IsSemiring</a> <a id="15063" href="Algebra.Structures.html#13204" class="Bound">+</a> <a id="15065" href="Algebra.Structures.html#13206" class="Bound">*</a> <a id="15067" href="Algebra.Structures.html#13231" class="Bound">0#</a> <a id="15070" href="Algebra.Structures.html#13234" class="Bound">1#</a>
|
||
<a id="15075" href="Algebra.Structures.html#15039" class="Function">isSemiring</a> <a id="15086" class="Symbol">=</a> <a id="15088" class="Keyword">record</a>
|
||
<a id="15099" class="Symbol">{</a> <a id="15101" href="Algebra.Structures.html#11430" class="Field">isSemiringWithoutAnnihilatingZero</a> <a id="15135" class="Symbol">=</a>
|
||
<a id="15145" href="Algebra.Structures.html#14770" class="Function">isSemiringWithoutAnnihilatingZero</a>
|
||
<a id="15183" class="Symbol">;</a> <a id="15185" href="Algebra.Structures.html#11520" class="Field">zero</a> <a id="15190" class="Symbol">=</a> <a id="15192" href="Algebra.Structures.html#13400" class="Field">zero</a>
|
||
<a id="15201" class="Symbol">}</a>
|
||
|
||
<a id="15206" class="Keyword">open</a> <a id="15211" href="Algebra.Structures.html#11361" class="Module">IsSemiring</a> <a id="15222" href="Algebra.Structures.html#15039" class="Function">isSemiring</a> <a id="15233" class="Keyword">public</a>
|
||
<a id="15244" class="Keyword">using</a> <a id="15250" class="Symbol">(</a><a id="15251" href="Algebra.Structures.html#10239" class="Function">distribˡ</a><a id="15259" class="Symbol">;</a> <a id="15261" href="Algebra.Structures.html#10301" class="Function">distribʳ</a><a id="15269" class="Symbol">;</a> <a id="15271" href="Algebra.Structures.html#8791" class="Function">isNearSemiring</a><a id="15285" class="Symbol">;</a> <a id="15287" href="Algebra.Structures.html#11632" class="Function">isSemiringWithoutOne</a><a id="15307" class="Symbol">)</a>
|
||
|
||
|
||
<a id="15311" class="Keyword">record</a> <a id="IsCommutativeRing"></a><a id="15318" href="Algebra.Structures.html#15318" class="Record">IsCommutativeRing</a>
|
||
<a id="15345" class="Symbol">(</a><a id="15346" href="Algebra.Structures.html#15346" class="Bound">+</a> <a id="15348" href="Algebra.Structures.html#15348" class="Bound">*</a> <a id="15350" class="Symbol">:</a> <a id="15352" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="15356" href="Algebra.Structures.html#522" class="Bound">A</a><a id="15357" class="Symbol">)</a> <a id="15359" class="Symbol">(</a><a id="15360" href="Algebra.Structures.html#15360" class="Bound">-</a> <a id="15362" class="Symbol">:</a> <a id="15364" href="Algebra.Core.html#475" class="Function">Op₁</a> <a id="15368" href="Algebra.Structures.html#522" class="Bound">A</a><a id="15369" class="Symbol">)</a> <a id="15371" class="Symbol">(</a><a id="15372" href="Algebra.Structures.html#15372" class="Bound">0#</a> <a id="15375" href="Algebra.Structures.html#15375" class="Bound">1#</a> <a id="15378" class="Symbol">:</a> <a id="15380" href="Algebra.Structures.html#522" class="Bound">A</a><a id="15381" class="Symbol">)</a> <a id="15383" class="Symbol">:</a> <a id="15385" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="15389" class="Symbol">(</a><a id="15390" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="15392" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="15394" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="15395" class="Symbol">)</a> <a id="15397" class="Keyword">where</a>
|
||
<a id="15405" class="Keyword">field</a>
|
||
<a id="IsCommutativeRing.isRing"></a><a id="15415" href="Algebra.Structures.html#15415" class="Field">isRing</a> <a id="15422" class="Symbol">:</a> <a id="15424" href="Algebra.Structures.html#13196" class="Record">IsRing</a> <a id="15431" href="Algebra.Structures.html#15346" class="Bound">+</a> <a id="15433" href="Algebra.Structures.html#15348" class="Bound">*</a> <a id="15435" href="Algebra.Structures.html#15360" class="Bound">-</a> <a id="15437" href="Algebra.Structures.html#15372" class="Bound">0#</a> <a id="15440" href="Algebra.Structures.html#15375" class="Bound">1#</a>
|
||
<a id="IsCommutativeRing.*-comm"></a><a id="15447" href="Algebra.Structures.html#15447" class="Field">*-comm</a> <a id="15454" class="Symbol">:</a> <a id="15456" href="Algebra.Definitions.html#1195" class="Function">Commutative</a> <a id="15468" href="Algebra.Structures.html#15348" class="Bound">*</a>
|
||
|
||
<a id="15473" class="Keyword">open</a> <a id="15478" href="Algebra.Structures.html#13196" class="Module">IsRing</a> <a id="15485" href="Algebra.Structures.html#15415" class="Field">isRing</a> <a id="15492" class="Keyword">public</a>
|
||
|
||
<a id="IsCommutativeRing.isCommutativeSemiring"></a><a id="15502" href="Algebra.Structures.html#15502" class="Function">isCommutativeSemiring</a> <a id="15524" class="Symbol">:</a> <a id="15526" href="Algebra.Structures.html#12017" class="Record">IsCommutativeSemiring</a> <a id="15548" href="Algebra.Structures.html#15346" class="Bound">+</a> <a id="15550" href="Algebra.Structures.html#15348" class="Bound">*</a> <a id="15552" href="Algebra.Structures.html#15372" class="Bound">0#</a> <a id="15555" href="Algebra.Structures.html#15375" class="Bound">1#</a>
|
||
<a id="15560" href="Algebra.Structures.html#15502" class="Function">isCommutativeSemiring</a> <a id="15582" class="Symbol">=</a> <a id="15584" class="Keyword">record</a>
|
||
<a id="15595" class="Symbol">{</a> <a id="15597" href="Algebra.Structures.html#12097" class="Field">isSemiring</a> <a id="15608" class="Symbol">=</a> <a id="15610" href="Algebra.Structures.html#15039" class="Function">isSemiring</a>
|
||
<a id="15625" class="Symbol">;</a> <a id="15627" href="Algebra.Structures.html#12135" class="Field">*-comm</a> <a id="15634" class="Symbol">=</a> <a id="15636" href="Algebra.Structures.html#15447" class="Field">*-comm</a>
|
||
<a id="15647" class="Symbol">}</a>
|
||
|
||
<a id="15652" class="Keyword">open</a> <a id="15657" href="Algebra.Structures.html#12017" class="Module">IsCommutativeSemiring</a> <a id="15679" href="Algebra.Structures.html#15502" class="Function">isCommutativeSemiring</a> <a id="15701" class="Keyword">public</a>
|
||
<a id="15712" class="Keyword">using</a>
|
||
<a id="15722" class="Symbol">(</a> <a id="15724" href="Algebra.Structures.html#12202" class="Function">isCommutativeSemiringWithoutOne</a>
|
||
<a id="15760" class="Symbol">;</a> <a id="15762" href="Algebra.Structures.html#9606" class="Function">*-isCommutativeMagma</a>
|
||
<a id="15787" class="Symbol">;</a> <a id="15789" href="Algebra.Structures.html#9343" class="Function">*-isCommutativeSemigroup</a>
|
||
<a id="15818" class="Symbol">;</a> <a id="15820" href="Algebra.Structures.html#12556" class="Function">*-isCommutativeMonoid</a>
|
||
<a id="15846" class="Symbol">)</a>
|
||
|
||
|
||
<a id="15850" class="Keyword">record</a> <a id="IsBooleanAlgebra"></a><a id="15857" href="Algebra.Structures.html#15857" class="Record">IsBooleanAlgebra</a>
|
||
<a id="15883" class="Symbol">(</a><a id="15884" href="Algebra.Structures.html#15884" class="Bound">∨</a> <a id="15886" href="Algebra.Structures.html#15886" class="Bound">∧</a> <a id="15888" class="Symbol">:</a> <a id="15890" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="15894" href="Algebra.Structures.html#522" class="Bound">A</a><a id="15895" class="Symbol">)</a> <a id="15897" class="Symbol">(</a><a id="15898" href="Algebra.Structures.html#15898" class="Bound">¬</a> <a id="15900" class="Symbol">:</a> <a id="15902" href="Algebra.Core.html#475" class="Function">Op₁</a> <a id="15906" href="Algebra.Structures.html#522" class="Bound">A</a><a id="15907" class="Symbol">)</a> <a id="15909" class="Symbol">(</a><a id="15910" href="Algebra.Structures.html#15910" class="Bound">⊤</a> <a id="15912" href="Algebra.Structures.html#15912" class="Bound">⊥</a> <a id="15914" class="Symbol">:</a> <a id="15916" href="Algebra.Structures.html#522" class="Bound">A</a><a id="15917" class="Symbol">)</a> <a id="15919" class="Symbol">:</a> <a id="15921" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="15925" class="Symbol">(</a><a id="15926" href="Algebra.Structures.html#516" class="Bound">a</a> <a id="15928" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="15930" href="Algebra.Structures.html#518" class="Bound">ℓ</a><a id="15931" class="Symbol">)</a> <a id="15933" class="Keyword">where</a>
|
||
<a id="15941" class="Keyword">field</a>
|
||
<a id="IsBooleanAlgebra.isDistributiveLattice"></a><a id="15951" href="Algebra.Structures.html#15951" class="Field">isDistributiveLattice</a> <a id="15973" class="Symbol">:</a> <a id="15975" href="Algebra.Structures.html#6870" class="Record">IsDistributiveLattice</a> <a id="15997" href="Algebra.Structures.html#15884" class="Bound">∨</a> <a id="15999" href="Algebra.Structures.html#15886" class="Bound">∧</a>
|
||
<a id="IsBooleanAlgebra.∨-complementʳ"></a><a id="16005" href="Algebra.Structures.html#16005" class="Field">∨-complementʳ</a> <a id="16027" class="Symbol">:</a> <a id="16029" href="Algebra.Definitions.html#1792" class="Function">RightInverse</a> <a id="16042" href="Algebra.Structures.html#15910" class="Bound">⊤</a> <a id="16044" href="Algebra.Structures.html#15898" class="Bound">¬</a> <a id="16046" href="Algebra.Structures.html#15884" class="Bound">∨</a>
|
||
<a id="IsBooleanAlgebra.∧-complementʳ"></a><a id="16052" href="Algebra.Structures.html#16052" class="Field">∧-complementʳ</a> <a id="16074" class="Symbol">:</a> <a id="16076" href="Algebra.Definitions.html#1792" class="Function">RightInverse</a> <a id="16089" href="Algebra.Structures.html#15912" class="Bound">⊥</a> <a id="16091" href="Algebra.Structures.html#15898" class="Bound">¬</a> <a id="16093" href="Algebra.Structures.html#15886" class="Bound">∧</a>
|
||
<a id="IsBooleanAlgebra.¬-cong"></a><a id="16099" href="Algebra.Structures.html#16099" class="Field">¬-cong</a> <a id="16121" class="Symbol">:</a> <a id="16123" href="Algebra.Definitions.html#797" class="Function">Congruent₁</a> <a id="16134" href="Algebra.Structures.html#15898" class="Bound">¬</a>
|
||
|
||
<a id="16139" class="Keyword">open</a> <a id="16144" href="Algebra.Structures.html#6870" class="Module">IsDistributiveLattice</a> <a id="16166" href="Algebra.Structures.html#15951" class="Field">isDistributiveLattice</a> <a id="16188" class="Keyword">public</a>
|
||
</pre></body></html> |