134 lines
59 KiB
HTML
134 lines
59 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Algebra.Definitions</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">-- Properties of functions, such as associativity and commutativity</a>
|
||
<a id="174" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="248" class="Comment">-- The contents of this module should be accessed via `Algebra`, unless</a>
|
||
<a id="320" class="Comment">-- you want to parameterise it via the equality relation.</a>
|
||
|
||
<a id="379" class="Symbol">{-#</a> <a id="383" class="Keyword">OPTIONS</a> <a id="391" class="Pragma">--without-K</a> <a id="403" class="Pragma">--safe</a> <a id="410" class="Symbol">#-}</a>
|
||
|
||
<a id="415" class="Keyword">open</a> <a id="420" class="Keyword">import</a> <a id="427" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a>
|
||
<a id="448" class="Keyword">open</a> <a id="453" class="Keyword">import</a> <a id="460" href="Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="477" class="Keyword">using</a> <a id="483" class="Symbol">(</a><a id="484" href="Relation.Nullary.html#656" class="Function Operator">¬_</a><a id="486" class="Symbol">)</a>
|
||
|
||
<a id="489" class="Keyword">module</a> <a id="496" href="Algebra.Definitions.html" class="Module">Algebra.Definitions</a>
|
||
<a id="518" class="Symbol">{</a><a id="519" href="Algebra.Definitions.html#519" class="Bound">a</a> <a id="521" href="Algebra.Definitions.html#521" class="Bound">ℓ</a><a id="522" class="Symbol">}</a> <a id="524" class="Symbol">{</a><a id="525" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="527" class="Symbol">:</a> <a id="529" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="533" href="Algebra.Definitions.html#519" class="Bound">a</a><a id="534" class="Symbol">}</a> <a id="538" class="Comment">-- The underlying set</a>
|
||
<a id="562" class="Symbol">(</a><a id="563" href="Algebra.Definitions.html#563" class="Bound Operator">_≈_</a> <a id="567" class="Symbol">:</a> <a id="569" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="573" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="575" href="Algebra.Definitions.html#521" class="Bound">ℓ</a><a id="576" class="Symbol">)</a> <a id="582" class="Comment">-- The underlying equality</a>
|
||
<a id="611" class="Keyword">where</a>
|
||
|
||
<a id="618" class="Keyword">open</a> <a id="623" class="Keyword">import</a> <a id="630" href="Algebra.Core.html" class="Module">Algebra.Core</a>
|
||
<a id="643" class="Keyword">open</a> <a id="648" class="Keyword">import</a> <a id="655" href="Data.Product.html" class="Module">Data.Product</a>
|
||
<a id="668" class="Keyword">open</a> <a id="673" class="Keyword">import</a> <a id="680" href="Data.Sum.Base.html" class="Module">Data.Sum.Base</a>
|
||
|
||
<a id="695" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="768" class="Comment">-- Properties of operations</a>
|
||
|
||
<a id="Congruent₁"></a><a id="797" href="Algebra.Definitions.html#797" class="Function">Congruent₁</a> <a id="808" class="Symbol">:</a> <a id="810" href="Algebra.Core.html#475" class="Function">Op₁</a> <a id="814" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="816" class="Symbol">→</a> <a id="818" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="822" class="Symbol">_</a>
|
||
<a id="824" href="Algebra.Definitions.html#797" class="Function">Congruent₁</a> <a id="835" href="Algebra.Definitions.html#835" class="Bound">f</a> <a id="837" class="Symbol">=</a> <a id="839" href="Algebra.Definitions.html#835" class="Bound">f</a> <a id="841" href="Relation.Binary.Core.html#1563" class="Function Operator">Preserves</a> <a id="851" href="Algebra.Definitions.html#563" class="Bound Operator">_≈_</a> <a id="855" href="Relation.Binary.Core.html#1563" class="Function Operator">⟶</a> <a id="857" href="Algebra.Definitions.html#563" class="Bound Operator">_≈_</a>
|
||
|
||
<a id="Congruent₂"></a><a id="862" href="Algebra.Definitions.html#862" class="Function">Congruent₂</a> <a id="873" class="Symbol">:</a> <a id="875" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="879" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="881" class="Symbol">→</a> <a id="883" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="887" class="Symbol">_</a>
|
||
<a id="889" href="Algebra.Definitions.html#862" class="Function">Congruent₂</a> <a id="900" href="Algebra.Definitions.html#900" class="Bound">∙</a> <a id="902" class="Symbol">=</a> <a id="904" href="Algebra.Definitions.html#900" class="Bound">∙</a> <a id="906" href="Relation.Binary.Core.html#1689" class="Function Operator">Preserves₂</a> <a id="917" href="Algebra.Definitions.html#563" class="Bound Operator">_≈_</a> <a id="921" href="Relation.Binary.Core.html#1689" class="Function Operator">⟶</a> <a id="923" href="Algebra.Definitions.html#563" class="Bound Operator">_≈_</a> <a id="927" href="Relation.Binary.Core.html#1689" class="Function Operator">⟶</a> <a id="929" href="Algebra.Definitions.html#563" class="Bound Operator">_≈_</a>
|
||
|
||
<a id="LeftCongruent"></a><a id="934" href="Algebra.Definitions.html#934" class="Function">LeftCongruent</a> <a id="948" class="Symbol">:</a> <a id="950" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="954" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="956" class="Symbol">→</a> <a id="958" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="962" class="Symbol">_</a>
|
||
<a id="964" href="Algebra.Definitions.html#934" class="Function">LeftCongruent</a> <a id="978" href="Algebra.Definitions.html#978" class="Bound Operator">_∙_</a> <a id="982" class="Symbol">=</a> <a id="984" class="Symbol">∀</a> <a id="986" class="Symbol">{</a><a id="987" href="Algebra.Definitions.html#987" class="Bound">x</a><a id="988" class="Symbol">}</a> <a id="990" class="Symbol">→</a> <a id="992" class="Symbol">(</a><a id="993" href="Algebra.Definitions.html#987" class="Bound">x</a> <a id="995" href="Algebra.Definitions.html#978" class="Bound Operator">∙_</a><a id="997" class="Symbol">)</a> <a id="999" href="Relation.Binary.Core.html#1563" class="Function Operator">Preserves</a> <a id="1009" href="Algebra.Definitions.html#563" class="Bound Operator">_≈_</a> <a id="1013" href="Relation.Binary.Core.html#1563" class="Function Operator">⟶</a> <a id="1015" href="Algebra.Definitions.html#563" class="Bound Operator">_≈_</a>
|
||
|
||
<a id="RightCongruent"></a><a id="1020" href="Algebra.Definitions.html#1020" class="Function">RightCongruent</a> <a id="1035" class="Symbol">:</a> <a id="1037" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1041" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1043" class="Symbol">→</a> <a id="1045" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1049" class="Symbol">_</a>
|
||
<a id="1051" href="Algebra.Definitions.html#1020" class="Function">RightCongruent</a> <a id="1066" href="Algebra.Definitions.html#1066" class="Bound Operator">_∙_</a> <a id="1070" class="Symbol">=</a> <a id="1072" class="Symbol">∀</a> <a id="1074" class="Symbol">{</a><a id="1075" href="Algebra.Definitions.html#1075" class="Bound">x</a><a id="1076" class="Symbol">}</a> <a id="1078" class="Symbol">→</a> <a id="1080" class="Symbol">(</a><a id="1081" href="Algebra.Definitions.html#1066" class="Bound Operator">_∙</a> <a id="1084" href="Algebra.Definitions.html#1075" class="Bound">x</a><a id="1085" class="Symbol">)</a> <a id="1087" href="Relation.Binary.Core.html#1563" class="Function Operator">Preserves</a> <a id="1097" href="Algebra.Definitions.html#563" class="Bound Operator">_≈_</a> <a id="1101" href="Relation.Binary.Core.html#1563" class="Function Operator">⟶</a> <a id="1103" href="Algebra.Definitions.html#563" class="Bound Operator">_≈_</a>
|
||
|
||
<a id="Associative"></a><a id="1108" href="Algebra.Definitions.html#1108" class="Function">Associative</a> <a id="1120" class="Symbol">:</a> <a id="1122" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1126" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1128" class="Symbol">→</a> <a id="1130" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1134" class="Symbol">_</a>
|
||
<a id="1136" href="Algebra.Definitions.html#1108" class="Function">Associative</a> <a id="1148" href="Algebra.Definitions.html#1148" class="Bound Operator">_∙_</a> <a id="1152" class="Symbol">=</a> <a id="1154" class="Symbol">∀</a> <a id="1156" href="Algebra.Definitions.html#1156" class="Bound">x</a> <a id="1158" href="Algebra.Definitions.html#1158" class="Bound">y</a> <a id="1160" href="Algebra.Definitions.html#1160" class="Bound">z</a> <a id="1162" class="Symbol">→</a> <a id="1164" class="Symbol">((</a><a id="1166" href="Algebra.Definitions.html#1156" class="Bound">x</a> <a id="1168" href="Algebra.Definitions.html#1148" class="Bound Operator">∙</a> <a id="1170" href="Algebra.Definitions.html#1158" class="Bound">y</a><a id="1171" class="Symbol">)</a> <a id="1173" href="Algebra.Definitions.html#1148" class="Bound Operator">∙</a> <a id="1175" href="Algebra.Definitions.html#1160" class="Bound">z</a><a id="1176" class="Symbol">)</a> <a id="1178" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="1180" class="Symbol">(</a><a id="1181" href="Algebra.Definitions.html#1156" class="Bound">x</a> <a id="1183" href="Algebra.Definitions.html#1148" class="Bound Operator">∙</a> <a id="1185" class="Symbol">(</a><a id="1186" href="Algebra.Definitions.html#1158" class="Bound">y</a> <a id="1188" href="Algebra.Definitions.html#1148" class="Bound Operator">∙</a> <a id="1190" href="Algebra.Definitions.html#1160" class="Bound">z</a><a id="1191" class="Symbol">))</a>
|
||
|
||
<a id="Commutative"></a><a id="1195" href="Algebra.Definitions.html#1195" class="Function">Commutative</a> <a id="1207" class="Symbol">:</a> <a id="1209" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1213" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1215" class="Symbol">→</a> <a id="1217" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1221" class="Symbol">_</a>
|
||
<a id="1223" href="Algebra.Definitions.html#1195" class="Function">Commutative</a> <a id="1235" href="Algebra.Definitions.html#1235" class="Bound Operator">_∙_</a> <a id="1239" class="Symbol">=</a> <a id="1241" class="Symbol">∀</a> <a id="1243" href="Algebra.Definitions.html#1243" class="Bound">x</a> <a id="1245" href="Algebra.Definitions.html#1245" class="Bound">y</a> <a id="1247" class="Symbol">→</a> <a id="1249" class="Symbol">(</a><a id="1250" href="Algebra.Definitions.html#1243" class="Bound">x</a> <a id="1252" href="Algebra.Definitions.html#1235" class="Bound Operator">∙</a> <a id="1254" href="Algebra.Definitions.html#1245" class="Bound">y</a><a id="1255" class="Symbol">)</a> <a id="1257" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="1259" class="Symbol">(</a><a id="1260" href="Algebra.Definitions.html#1245" class="Bound">y</a> <a id="1262" href="Algebra.Definitions.html#1235" class="Bound Operator">∙</a> <a id="1264" href="Algebra.Definitions.html#1243" class="Bound">x</a><a id="1265" class="Symbol">)</a>
|
||
|
||
<a id="LeftIdentity"></a><a id="1268" href="Algebra.Definitions.html#1268" class="Function">LeftIdentity</a> <a id="1281" class="Symbol">:</a> <a id="1283" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1285" class="Symbol">→</a> <a id="1287" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1291" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1293" class="Symbol">→</a> <a id="1295" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1299" class="Symbol">_</a>
|
||
<a id="1301" href="Algebra.Definitions.html#1268" class="Function">LeftIdentity</a> <a id="1314" href="Algebra.Definitions.html#1314" class="Bound">e</a> <a id="1316" href="Algebra.Definitions.html#1316" class="Bound Operator">_∙_</a> <a id="1320" class="Symbol">=</a> <a id="1322" class="Symbol">∀</a> <a id="1324" href="Algebra.Definitions.html#1324" class="Bound">x</a> <a id="1326" class="Symbol">→</a> <a id="1328" class="Symbol">(</a><a id="1329" href="Algebra.Definitions.html#1314" class="Bound">e</a> <a id="1331" href="Algebra.Definitions.html#1316" class="Bound Operator">∙</a> <a id="1333" href="Algebra.Definitions.html#1324" class="Bound">x</a><a id="1334" class="Symbol">)</a> <a id="1336" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="1338" href="Algebra.Definitions.html#1324" class="Bound">x</a>
|
||
|
||
<a id="RightIdentity"></a><a id="1341" href="Algebra.Definitions.html#1341" class="Function">RightIdentity</a> <a id="1355" class="Symbol">:</a> <a id="1357" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1359" class="Symbol">→</a> <a id="1361" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1365" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1367" class="Symbol">→</a> <a id="1369" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1373" class="Symbol">_</a>
|
||
<a id="1375" href="Algebra.Definitions.html#1341" class="Function">RightIdentity</a> <a id="1389" href="Algebra.Definitions.html#1389" class="Bound">e</a> <a id="1391" href="Algebra.Definitions.html#1391" class="Bound Operator">_∙_</a> <a id="1395" class="Symbol">=</a> <a id="1397" class="Symbol">∀</a> <a id="1399" href="Algebra.Definitions.html#1399" class="Bound">x</a> <a id="1401" class="Symbol">→</a> <a id="1403" class="Symbol">(</a><a id="1404" href="Algebra.Definitions.html#1399" class="Bound">x</a> <a id="1406" href="Algebra.Definitions.html#1391" class="Bound Operator">∙</a> <a id="1408" href="Algebra.Definitions.html#1389" class="Bound">e</a><a id="1409" class="Symbol">)</a> <a id="1411" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="1413" href="Algebra.Definitions.html#1399" class="Bound">x</a>
|
||
|
||
<a id="Identity"></a><a id="1416" href="Algebra.Definitions.html#1416" class="Function">Identity</a> <a id="1425" class="Symbol">:</a> <a id="1427" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1429" class="Symbol">→</a> <a id="1431" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1435" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1437" class="Symbol">→</a> <a id="1439" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1443" class="Symbol">_</a>
|
||
<a id="1445" href="Algebra.Definitions.html#1416" class="Function">Identity</a> <a id="1454" href="Algebra.Definitions.html#1454" class="Bound">e</a> <a id="1456" href="Algebra.Definitions.html#1456" class="Bound">∙</a> <a id="1458" class="Symbol">=</a> <a id="1460" class="Symbol">(</a><a id="1461" href="Algebra.Definitions.html#1268" class="Function">LeftIdentity</a> <a id="1474" href="Algebra.Definitions.html#1454" class="Bound">e</a> <a id="1476" href="Algebra.Definitions.html#1456" class="Bound">∙</a><a id="1477" class="Symbol">)</a> <a id="1479" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="1481" class="Symbol">(</a><a id="1482" href="Algebra.Definitions.html#1341" class="Function">RightIdentity</a> <a id="1496" href="Algebra.Definitions.html#1454" class="Bound">e</a> <a id="1498" href="Algebra.Definitions.html#1456" class="Bound">∙</a><a id="1499" class="Symbol">)</a>
|
||
|
||
<a id="LeftZero"></a><a id="1502" href="Algebra.Definitions.html#1502" class="Function">LeftZero</a> <a id="1511" class="Symbol">:</a> <a id="1513" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1515" class="Symbol">→</a> <a id="1517" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1521" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1523" class="Symbol">→</a> <a id="1525" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1529" class="Symbol">_</a>
|
||
<a id="1531" href="Algebra.Definitions.html#1502" class="Function">LeftZero</a> <a id="1540" href="Algebra.Definitions.html#1540" class="Bound">z</a> <a id="1542" href="Algebra.Definitions.html#1542" class="Bound Operator">_∙_</a> <a id="1546" class="Symbol">=</a> <a id="1548" class="Symbol">∀</a> <a id="1550" href="Algebra.Definitions.html#1550" class="Bound">x</a> <a id="1552" class="Symbol">→</a> <a id="1554" class="Symbol">(</a><a id="1555" href="Algebra.Definitions.html#1540" class="Bound">z</a> <a id="1557" href="Algebra.Definitions.html#1542" class="Bound Operator">∙</a> <a id="1559" href="Algebra.Definitions.html#1550" class="Bound">x</a><a id="1560" class="Symbol">)</a> <a id="1562" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="1564" href="Algebra.Definitions.html#1540" class="Bound">z</a>
|
||
|
||
<a id="RightZero"></a><a id="1567" href="Algebra.Definitions.html#1567" class="Function">RightZero</a> <a id="1577" class="Symbol">:</a> <a id="1579" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1581" class="Symbol">→</a> <a id="1583" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1587" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1589" class="Symbol">→</a> <a id="1591" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1595" class="Symbol">_</a>
|
||
<a id="1597" href="Algebra.Definitions.html#1567" class="Function">RightZero</a> <a id="1607" href="Algebra.Definitions.html#1607" class="Bound">z</a> <a id="1609" href="Algebra.Definitions.html#1609" class="Bound Operator">_∙_</a> <a id="1613" class="Symbol">=</a> <a id="1615" class="Symbol">∀</a> <a id="1617" href="Algebra.Definitions.html#1617" class="Bound">x</a> <a id="1619" class="Symbol">→</a> <a id="1621" class="Symbol">(</a><a id="1622" href="Algebra.Definitions.html#1617" class="Bound">x</a> <a id="1624" href="Algebra.Definitions.html#1609" class="Bound Operator">∙</a> <a id="1626" href="Algebra.Definitions.html#1607" class="Bound">z</a><a id="1627" class="Symbol">)</a> <a id="1629" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="1631" href="Algebra.Definitions.html#1607" class="Bound">z</a>
|
||
|
||
<a id="Zero"></a><a id="1634" href="Algebra.Definitions.html#1634" class="Function">Zero</a> <a id="1639" class="Symbol">:</a> <a id="1641" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1643" class="Symbol">→</a> <a id="1645" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1649" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1651" class="Symbol">→</a> <a id="1653" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1657" class="Symbol">_</a>
|
||
<a id="1659" href="Algebra.Definitions.html#1634" class="Function">Zero</a> <a id="1664" href="Algebra.Definitions.html#1664" class="Bound">z</a> <a id="1666" href="Algebra.Definitions.html#1666" class="Bound">∙</a> <a id="1668" class="Symbol">=</a> <a id="1670" class="Symbol">(</a><a id="1671" href="Algebra.Definitions.html#1502" class="Function">LeftZero</a> <a id="1680" href="Algebra.Definitions.html#1664" class="Bound">z</a> <a id="1682" href="Algebra.Definitions.html#1666" class="Bound">∙</a><a id="1683" class="Symbol">)</a> <a id="1685" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="1687" class="Symbol">(</a><a id="1688" href="Algebra.Definitions.html#1567" class="Function">RightZero</a> <a id="1698" href="Algebra.Definitions.html#1664" class="Bound">z</a> <a id="1700" href="Algebra.Definitions.html#1666" class="Bound">∙</a><a id="1701" class="Symbol">)</a>
|
||
|
||
<a id="LeftInverse"></a><a id="1704" href="Algebra.Definitions.html#1704" class="Function">LeftInverse</a> <a id="1716" class="Symbol">:</a> <a id="1718" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1720" class="Symbol">→</a> <a id="1722" href="Algebra.Core.html#475" class="Function">Op₁</a> <a id="1726" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1728" class="Symbol">→</a> <a id="1730" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1734" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1736" class="Symbol">→</a> <a id="1738" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1742" class="Symbol">_</a>
|
||
<a id="1744" href="Algebra.Definitions.html#1704" class="Function">LeftInverse</a> <a id="1756" href="Algebra.Definitions.html#1756" class="Bound">e</a> <a id="1758" href="Algebra.Definitions.html#1758" class="Bound Operator">_⁻¹</a> <a id="1762" href="Algebra.Definitions.html#1762" class="Bound Operator">_∙_</a> <a id="1766" class="Symbol">=</a> <a id="1768" class="Symbol">∀</a> <a id="1770" href="Algebra.Definitions.html#1770" class="Bound">x</a> <a id="1772" class="Symbol">→</a> <a id="1774" class="Symbol">((</a><a id="1776" href="Algebra.Definitions.html#1770" class="Bound">x</a> <a id="1778" href="Algebra.Definitions.html#1758" class="Bound Operator">⁻¹</a><a id="1780" class="Symbol">)</a> <a id="1782" href="Algebra.Definitions.html#1762" class="Bound Operator">∙</a> <a id="1784" href="Algebra.Definitions.html#1770" class="Bound">x</a><a id="1785" class="Symbol">)</a> <a id="1787" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="1789" href="Algebra.Definitions.html#1756" class="Bound">e</a>
|
||
|
||
<a id="RightInverse"></a><a id="1792" href="Algebra.Definitions.html#1792" class="Function">RightInverse</a> <a id="1805" class="Symbol">:</a> <a id="1807" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1809" class="Symbol">→</a> <a id="1811" href="Algebra.Core.html#475" class="Function">Op₁</a> <a id="1815" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1817" class="Symbol">→</a> <a id="1819" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1823" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1825" class="Symbol">→</a> <a id="1827" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1831" class="Symbol">_</a>
|
||
<a id="1833" href="Algebra.Definitions.html#1792" class="Function">RightInverse</a> <a id="1846" href="Algebra.Definitions.html#1846" class="Bound">e</a> <a id="1848" href="Algebra.Definitions.html#1848" class="Bound Operator">_⁻¹</a> <a id="1852" href="Algebra.Definitions.html#1852" class="Bound Operator">_∙_</a> <a id="1856" class="Symbol">=</a> <a id="1858" class="Symbol">∀</a> <a id="1860" href="Algebra.Definitions.html#1860" class="Bound">x</a> <a id="1862" class="Symbol">→</a> <a id="1864" class="Symbol">(</a><a id="1865" href="Algebra.Definitions.html#1860" class="Bound">x</a> <a id="1867" href="Algebra.Definitions.html#1852" class="Bound Operator">∙</a> <a id="1869" class="Symbol">(</a><a id="1870" href="Algebra.Definitions.html#1860" class="Bound">x</a> <a id="1872" href="Algebra.Definitions.html#1848" class="Bound Operator">⁻¹</a><a id="1874" class="Symbol">))</a> <a id="1877" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="1879" href="Algebra.Definitions.html#1846" class="Bound">e</a>
|
||
|
||
<a id="Inverse"></a><a id="1882" href="Algebra.Definitions.html#1882" class="Function">Inverse</a> <a id="1890" class="Symbol">:</a> <a id="1892" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1894" class="Symbol">→</a> <a id="1896" href="Algebra.Core.html#475" class="Function">Op₁</a> <a id="1900" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1902" class="Symbol">→</a> <a id="1904" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="1908" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1910" class="Symbol">→</a> <a id="1912" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1916" class="Symbol">_</a>
|
||
<a id="1918" href="Algebra.Definitions.html#1882" class="Function">Inverse</a> <a id="1926" href="Algebra.Definitions.html#1926" class="Bound">e</a> <a id="1928" href="Algebra.Definitions.html#1928" class="Bound">⁻¹</a> <a id="1931" href="Algebra.Definitions.html#1931" class="Bound">∙</a> <a id="1933" class="Symbol">=</a> <a id="1935" class="Symbol">(</a><a id="1936" href="Algebra.Definitions.html#1704" class="Function">LeftInverse</a> <a id="1948" href="Algebra.Definitions.html#1926" class="Bound">e</a> <a id="1950" href="Algebra.Definitions.html#1928" class="Bound">⁻¹</a><a id="1952" class="Symbol">)</a> <a id="1954" href="Algebra.Definitions.html#1931" class="Bound">∙</a> <a id="1956" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="1958" class="Symbol">(</a><a id="1959" href="Algebra.Definitions.html#1792" class="Function">RightInverse</a> <a id="1972" href="Algebra.Definitions.html#1926" class="Bound">e</a> <a id="1974" href="Algebra.Definitions.html#1928" class="Bound">⁻¹</a> <a id="1977" href="Algebra.Definitions.html#1931" class="Bound">∙</a><a id="1978" class="Symbol">)</a>
|
||
|
||
<a id="LeftConical"></a><a id="1981" href="Algebra.Definitions.html#1981" class="Function">LeftConical</a> <a id="1993" class="Symbol">:</a> <a id="1995" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="1997" class="Symbol">→</a> <a id="1999" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2003" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2005" class="Symbol">→</a> <a id="2007" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2011" class="Symbol">_</a>
|
||
<a id="2013" href="Algebra.Definitions.html#1981" class="Function">LeftConical</a> <a id="2025" href="Algebra.Definitions.html#2025" class="Bound">e</a> <a id="2027" href="Algebra.Definitions.html#2027" class="Bound Operator">_∙_</a> <a id="2031" class="Symbol">=</a> <a id="2033" class="Symbol">∀</a> <a id="2035" href="Algebra.Definitions.html#2035" class="Bound">x</a> <a id="2037" href="Algebra.Definitions.html#2037" class="Bound">y</a> <a id="2039" class="Symbol">→</a> <a id="2041" class="Symbol">(</a><a id="2042" href="Algebra.Definitions.html#2035" class="Bound">x</a> <a id="2044" href="Algebra.Definitions.html#2027" class="Bound Operator">∙</a> <a id="2046" href="Algebra.Definitions.html#2037" class="Bound">y</a><a id="2047" class="Symbol">)</a> <a id="2049" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="2051" href="Algebra.Definitions.html#2025" class="Bound">e</a> <a id="2053" class="Symbol">→</a> <a id="2055" href="Algebra.Definitions.html#2035" class="Bound">x</a> <a id="2057" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="2059" href="Algebra.Definitions.html#2025" class="Bound">e</a>
|
||
|
||
<a id="RightConical"></a><a id="2062" href="Algebra.Definitions.html#2062" class="Function">RightConical</a> <a id="2075" class="Symbol">:</a> <a id="2077" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2079" class="Symbol">→</a> <a id="2081" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2085" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2087" class="Symbol">→</a> <a id="2089" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2093" class="Symbol">_</a>
|
||
<a id="2095" href="Algebra.Definitions.html#2062" class="Function">RightConical</a> <a id="2108" href="Algebra.Definitions.html#2108" class="Bound">e</a> <a id="2110" href="Algebra.Definitions.html#2110" class="Bound Operator">_∙_</a> <a id="2114" class="Symbol">=</a> <a id="2116" class="Symbol">∀</a> <a id="2118" href="Algebra.Definitions.html#2118" class="Bound">x</a> <a id="2120" href="Algebra.Definitions.html#2120" class="Bound">y</a> <a id="2122" class="Symbol">→</a> <a id="2124" class="Symbol">(</a><a id="2125" href="Algebra.Definitions.html#2118" class="Bound">x</a> <a id="2127" href="Algebra.Definitions.html#2110" class="Bound Operator">∙</a> <a id="2129" href="Algebra.Definitions.html#2120" class="Bound">y</a><a id="2130" class="Symbol">)</a> <a id="2132" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="2134" href="Algebra.Definitions.html#2108" class="Bound">e</a> <a id="2136" class="Symbol">→</a> <a id="2138" href="Algebra.Definitions.html#2120" class="Bound">y</a> <a id="2140" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="2142" href="Algebra.Definitions.html#2108" class="Bound">e</a>
|
||
|
||
<a id="Conical"></a><a id="2145" href="Algebra.Definitions.html#2145" class="Function">Conical</a> <a id="2153" class="Symbol">:</a> <a id="2155" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2157" class="Symbol">→</a> <a id="2159" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2163" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2165" class="Symbol">→</a> <a id="2167" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2171" class="Symbol">_</a>
|
||
<a id="2173" href="Algebra.Definitions.html#2145" class="Function">Conical</a> <a id="2181" href="Algebra.Definitions.html#2181" class="Bound">e</a> <a id="2183" href="Algebra.Definitions.html#2183" class="Bound">∙</a> <a id="2185" class="Symbol">=</a> <a id="2187" class="Symbol">(</a><a id="2188" href="Algebra.Definitions.html#1981" class="Function">LeftConical</a> <a id="2200" href="Algebra.Definitions.html#2181" class="Bound">e</a> <a id="2202" href="Algebra.Definitions.html#2183" class="Bound">∙</a><a id="2203" class="Symbol">)</a> <a id="2205" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="2207" class="Symbol">(</a><a id="2208" href="Algebra.Definitions.html#2062" class="Function">RightConical</a> <a id="2221" href="Algebra.Definitions.html#2181" class="Bound">e</a> <a id="2223" href="Algebra.Definitions.html#2183" class="Bound">∙</a><a id="2224" class="Symbol">)</a>
|
||
|
||
<a id="_DistributesOverˡ_"></a><a id="2227" href="Algebra.Definitions.html#2227" class="Function Operator">_DistributesOverˡ_</a> <a id="2246" class="Symbol">:</a> <a id="2248" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2252" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2254" class="Symbol">→</a> <a id="2256" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2260" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2262" class="Symbol">→</a> <a id="2264" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2268" class="Symbol">_</a>
|
||
<a id="2270" href="Algebra.Definitions.html#2270" class="Bound Operator">_*_</a> <a id="2274" href="Algebra.Definitions.html#2227" class="Function Operator">DistributesOverˡ</a> <a id="2291" href="Algebra.Definitions.html#2291" class="Bound Operator">_+_</a> <a id="2295" class="Symbol">=</a>
|
||
<a id="2299" class="Symbol">∀</a> <a id="2301" href="Algebra.Definitions.html#2301" class="Bound">x</a> <a id="2303" href="Algebra.Definitions.html#2303" class="Bound">y</a> <a id="2305" href="Algebra.Definitions.html#2305" class="Bound">z</a> <a id="2307" class="Symbol">→</a> <a id="2309" class="Symbol">(</a><a id="2310" href="Algebra.Definitions.html#2301" class="Bound">x</a> <a id="2312" href="Algebra.Definitions.html#2270" class="Bound Operator">*</a> <a id="2314" class="Symbol">(</a><a id="2315" href="Algebra.Definitions.html#2303" class="Bound">y</a> <a id="2317" href="Algebra.Definitions.html#2291" class="Bound Operator">+</a> <a id="2319" href="Algebra.Definitions.html#2305" class="Bound">z</a><a id="2320" class="Symbol">))</a> <a id="2323" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="2325" class="Symbol">((</a><a id="2327" href="Algebra.Definitions.html#2301" class="Bound">x</a> <a id="2329" href="Algebra.Definitions.html#2270" class="Bound Operator">*</a> <a id="2331" href="Algebra.Definitions.html#2303" class="Bound">y</a><a id="2332" class="Symbol">)</a> <a id="2334" href="Algebra.Definitions.html#2291" class="Bound Operator">+</a> <a id="2336" class="Symbol">(</a><a id="2337" href="Algebra.Definitions.html#2301" class="Bound">x</a> <a id="2339" href="Algebra.Definitions.html#2270" class="Bound Operator">*</a> <a id="2341" href="Algebra.Definitions.html#2305" class="Bound">z</a><a id="2342" class="Symbol">))</a>
|
||
|
||
<a id="_DistributesOverʳ_"></a><a id="2346" href="Algebra.Definitions.html#2346" class="Function Operator">_DistributesOverʳ_</a> <a id="2365" class="Symbol">:</a> <a id="2367" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2371" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2373" class="Symbol">→</a> <a id="2375" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2379" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2381" class="Symbol">→</a> <a id="2383" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2387" class="Symbol">_</a>
|
||
<a id="2389" href="Algebra.Definitions.html#2389" class="Bound Operator">_*_</a> <a id="2393" href="Algebra.Definitions.html#2346" class="Function Operator">DistributesOverʳ</a> <a id="2410" href="Algebra.Definitions.html#2410" class="Bound Operator">_+_</a> <a id="2414" class="Symbol">=</a>
|
||
<a id="2418" class="Symbol">∀</a> <a id="2420" href="Algebra.Definitions.html#2420" class="Bound">x</a> <a id="2422" href="Algebra.Definitions.html#2422" class="Bound">y</a> <a id="2424" href="Algebra.Definitions.html#2424" class="Bound">z</a> <a id="2426" class="Symbol">→</a> <a id="2428" class="Symbol">((</a><a id="2430" href="Algebra.Definitions.html#2422" class="Bound">y</a> <a id="2432" href="Algebra.Definitions.html#2410" class="Bound Operator">+</a> <a id="2434" href="Algebra.Definitions.html#2424" class="Bound">z</a><a id="2435" class="Symbol">)</a> <a id="2437" href="Algebra.Definitions.html#2389" class="Bound Operator">*</a> <a id="2439" href="Algebra.Definitions.html#2420" class="Bound">x</a><a id="2440" class="Symbol">)</a> <a id="2442" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="2444" class="Symbol">((</a><a id="2446" href="Algebra.Definitions.html#2422" class="Bound">y</a> <a id="2448" href="Algebra.Definitions.html#2389" class="Bound Operator">*</a> <a id="2450" href="Algebra.Definitions.html#2420" class="Bound">x</a><a id="2451" class="Symbol">)</a> <a id="2453" href="Algebra.Definitions.html#2410" class="Bound Operator">+</a> <a id="2455" class="Symbol">(</a><a id="2456" href="Algebra.Definitions.html#2424" class="Bound">z</a> <a id="2458" href="Algebra.Definitions.html#2389" class="Bound Operator">*</a> <a id="2460" href="Algebra.Definitions.html#2420" class="Bound">x</a><a id="2461" class="Symbol">))</a>
|
||
|
||
<a id="_DistributesOver_"></a><a id="2465" href="Algebra.Definitions.html#2465" class="Function Operator">_DistributesOver_</a> <a id="2483" class="Symbol">:</a> <a id="2485" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2489" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2491" class="Symbol">→</a> <a id="2493" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2497" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2499" class="Symbol">→</a> <a id="2501" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2505" class="Symbol">_</a>
|
||
<a id="2507" href="Algebra.Definitions.html#2507" class="Bound">*</a> <a id="2509" href="Algebra.Definitions.html#2465" class="Function Operator">DistributesOver</a> <a id="2525" href="Algebra.Definitions.html#2525" class="Bound">+</a> <a id="2527" class="Symbol">=</a> <a id="2529" class="Symbol">(</a><a id="2530" href="Algebra.Definitions.html#2507" class="Bound">*</a> <a id="2532" href="Algebra.Definitions.html#2227" class="Function Operator">DistributesOverˡ</a> <a id="2549" href="Algebra.Definitions.html#2525" class="Bound">+</a><a id="2550" class="Symbol">)</a> <a id="2552" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="2554" class="Symbol">(</a><a id="2555" href="Algebra.Definitions.html#2507" class="Bound">*</a> <a id="2557" href="Algebra.Definitions.html#2346" class="Function Operator">DistributesOverʳ</a> <a id="2574" href="Algebra.Definitions.html#2525" class="Bound">+</a><a id="2575" class="Symbol">)</a>
|
||
|
||
<a id="_IdempotentOn_"></a><a id="2578" href="Algebra.Definitions.html#2578" class="Function Operator">_IdempotentOn_</a> <a id="2593" class="Symbol">:</a> <a id="2595" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2599" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2601" class="Symbol">→</a> <a id="2603" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2605" class="Symbol">→</a> <a id="2607" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2611" class="Symbol">_</a>
|
||
<a id="2613" href="Algebra.Definitions.html#2613" class="Bound Operator">_∙_</a> <a id="2617" href="Algebra.Definitions.html#2578" class="Function Operator">IdempotentOn</a> <a id="2630" href="Algebra.Definitions.html#2630" class="Bound">x</a> <a id="2632" class="Symbol">=</a> <a id="2634" class="Symbol">(</a><a id="2635" href="Algebra.Definitions.html#2630" class="Bound">x</a> <a id="2637" href="Algebra.Definitions.html#2613" class="Bound Operator">∙</a> <a id="2639" href="Algebra.Definitions.html#2630" class="Bound">x</a><a id="2640" class="Symbol">)</a> <a id="2642" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="2644" href="Algebra.Definitions.html#2630" class="Bound">x</a>
|
||
|
||
<a id="Idempotent"></a><a id="2647" href="Algebra.Definitions.html#2647" class="Function">Idempotent</a> <a id="2658" class="Symbol">:</a> <a id="2660" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2664" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2666" class="Symbol">→</a> <a id="2668" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2672" class="Symbol">_</a>
|
||
<a id="2674" href="Algebra.Definitions.html#2647" class="Function">Idempotent</a> <a id="2685" href="Algebra.Definitions.html#2685" class="Bound">∙</a> <a id="2687" class="Symbol">=</a> <a id="2689" class="Symbol">∀</a> <a id="2691" href="Algebra.Definitions.html#2691" class="Bound">x</a> <a id="2693" class="Symbol">→</a> <a id="2695" href="Algebra.Definitions.html#2685" class="Bound">∙</a> <a id="2697" href="Algebra.Definitions.html#2578" class="Function Operator">IdempotentOn</a> <a id="2710" href="Algebra.Definitions.html#2691" class="Bound">x</a>
|
||
|
||
<a id="IdempotentFun"></a><a id="2713" href="Algebra.Definitions.html#2713" class="Function">IdempotentFun</a> <a id="2727" class="Symbol">:</a> <a id="2729" href="Algebra.Core.html#475" class="Function">Op₁</a> <a id="2733" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2735" class="Symbol">→</a> <a id="2737" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2741" class="Symbol">_</a>
|
||
<a id="2743" href="Algebra.Definitions.html#2713" class="Function">IdempotentFun</a> <a id="2757" href="Algebra.Definitions.html#2757" class="Bound">f</a> <a id="2759" class="Symbol">=</a> <a id="2761" class="Symbol">∀</a> <a id="2763" href="Algebra.Definitions.html#2763" class="Bound">x</a> <a id="2765" class="Symbol">→</a> <a id="2767" href="Algebra.Definitions.html#2757" class="Bound">f</a> <a id="2769" class="Symbol">(</a><a id="2770" href="Algebra.Definitions.html#2757" class="Bound">f</a> <a id="2772" href="Algebra.Definitions.html#2763" class="Bound">x</a><a id="2773" class="Symbol">)</a> <a id="2775" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="2777" href="Algebra.Definitions.html#2757" class="Bound">f</a> <a id="2779" href="Algebra.Definitions.html#2763" class="Bound">x</a>
|
||
|
||
<a id="Selective"></a><a id="2782" href="Algebra.Definitions.html#2782" class="Function">Selective</a> <a id="2792" class="Symbol">:</a> <a id="2794" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2798" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2800" class="Symbol">→</a> <a id="2802" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2806" class="Symbol">_</a>
|
||
<a id="2808" href="Algebra.Definitions.html#2782" class="Function">Selective</a> <a id="2818" href="Algebra.Definitions.html#2818" class="Bound Operator">_∙_</a> <a id="2822" class="Symbol">=</a> <a id="2824" class="Symbol">∀</a> <a id="2826" href="Algebra.Definitions.html#2826" class="Bound">x</a> <a id="2828" href="Algebra.Definitions.html#2828" class="Bound">y</a> <a id="2830" class="Symbol">→</a> <a id="2832" class="Symbol">(</a><a id="2833" href="Algebra.Definitions.html#2826" class="Bound">x</a> <a id="2835" href="Algebra.Definitions.html#2818" class="Bound Operator">∙</a> <a id="2837" href="Algebra.Definitions.html#2828" class="Bound">y</a><a id="2838" class="Symbol">)</a> <a id="2840" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="2842" href="Algebra.Definitions.html#2826" class="Bound">x</a> <a id="2844" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="2846" class="Symbol">(</a><a id="2847" href="Algebra.Definitions.html#2826" class="Bound">x</a> <a id="2849" href="Algebra.Definitions.html#2818" class="Bound Operator">∙</a> <a id="2851" href="Algebra.Definitions.html#2828" class="Bound">y</a><a id="2852" class="Symbol">)</a> <a id="2854" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="2856" href="Algebra.Definitions.html#2828" class="Bound">y</a>
|
||
|
||
<a id="_Absorbs_"></a><a id="2859" href="Algebra.Definitions.html#2859" class="Function Operator">_Absorbs_</a> <a id="2869" class="Symbol">:</a> <a id="2871" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2875" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2877" class="Symbol">→</a> <a id="2879" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2883" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2885" class="Symbol">→</a> <a id="2887" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2891" class="Symbol">_</a>
|
||
<a id="2893" href="Algebra.Definitions.html#2893" class="Bound Operator">_∙_</a> <a id="2897" href="Algebra.Definitions.html#2859" class="Function Operator">Absorbs</a> <a id="2905" href="Algebra.Definitions.html#2905" class="Bound Operator">_∘_</a> <a id="2909" class="Symbol">=</a> <a id="2911" class="Symbol">∀</a> <a id="2913" href="Algebra.Definitions.html#2913" class="Bound">x</a> <a id="2915" href="Algebra.Definitions.html#2915" class="Bound">y</a> <a id="2917" class="Symbol">→</a> <a id="2919" class="Symbol">(</a><a id="2920" href="Algebra.Definitions.html#2913" class="Bound">x</a> <a id="2922" href="Algebra.Definitions.html#2893" class="Bound Operator">∙</a> <a id="2924" class="Symbol">(</a><a id="2925" href="Algebra.Definitions.html#2913" class="Bound">x</a> <a id="2927" href="Algebra.Definitions.html#2905" class="Bound Operator">∘</a> <a id="2929" href="Algebra.Definitions.html#2915" class="Bound">y</a><a id="2930" class="Symbol">))</a> <a id="2933" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="2935" href="Algebra.Definitions.html#2913" class="Bound">x</a>
|
||
|
||
<a id="Absorptive"></a><a id="2938" href="Algebra.Definitions.html#2938" class="Function">Absorptive</a> <a id="2949" class="Symbol">:</a> <a id="2951" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2955" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2957" class="Symbol">→</a> <a id="2959" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="2963" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="2965" class="Symbol">→</a> <a id="2967" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2971" class="Symbol">_</a>
|
||
<a id="2973" href="Algebra.Definitions.html#2938" class="Function">Absorptive</a> <a id="2984" href="Algebra.Definitions.html#2984" class="Bound">∙</a> <a id="2986" href="Algebra.Definitions.html#2986" class="Bound">∘</a> <a id="2988" class="Symbol">=</a> <a id="2990" class="Symbol">(</a><a id="2991" href="Algebra.Definitions.html#2984" class="Bound">∙</a> <a id="2993" href="Algebra.Definitions.html#2859" class="Function Operator">Absorbs</a> <a id="3001" href="Algebra.Definitions.html#2986" class="Bound">∘</a><a id="3002" class="Symbol">)</a> <a id="3004" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="3006" class="Symbol">(</a><a id="3007" href="Algebra.Definitions.html#2986" class="Bound">∘</a> <a id="3009" href="Algebra.Definitions.html#2859" class="Function Operator">Absorbs</a> <a id="3017" href="Algebra.Definitions.html#2984" class="Bound">∙</a><a id="3018" class="Symbol">)</a>
|
||
|
||
<a id="Involutive"></a><a id="3021" href="Algebra.Definitions.html#3021" class="Function">Involutive</a> <a id="3032" class="Symbol">:</a> <a id="3034" href="Algebra.Core.html#475" class="Function">Op₁</a> <a id="3038" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="3040" class="Symbol">→</a> <a id="3042" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3046" class="Symbol">_</a>
|
||
<a id="3048" href="Algebra.Definitions.html#3021" class="Function">Involutive</a> <a id="3059" href="Algebra.Definitions.html#3059" class="Bound">f</a> <a id="3061" class="Symbol">=</a> <a id="3063" class="Symbol">∀</a> <a id="3065" href="Algebra.Definitions.html#3065" class="Bound">x</a> <a id="3067" class="Symbol">→</a> <a id="3069" href="Algebra.Definitions.html#3059" class="Bound">f</a> <a id="3071" class="Symbol">(</a><a id="3072" href="Algebra.Definitions.html#3059" class="Bound">f</a> <a id="3074" href="Algebra.Definitions.html#3065" class="Bound">x</a><a id="3075" class="Symbol">)</a> <a id="3077" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="3079" href="Algebra.Definitions.html#3065" class="Bound">x</a>
|
||
|
||
<a id="LeftCancellative"></a><a id="3082" href="Algebra.Definitions.html#3082" class="Function">LeftCancellative</a> <a id="3099" class="Symbol">:</a> <a id="3101" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="3105" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="3107" class="Symbol">→</a> <a id="3109" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3113" class="Symbol">_</a>
|
||
<a id="3115" href="Algebra.Definitions.html#3082" class="Function">LeftCancellative</a> <a id="3132" href="Algebra.Definitions.html#3132" class="Bound Operator">_•_</a> <a id="3136" class="Symbol">=</a> <a id="3138" class="Symbol">∀</a> <a id="3140" href="Algebra.Definitions.html#3140" class="Bound">x</a> <a id="3142" class="Symbol">{</a><a id="3143" href="Algebra.Definitions.html#3143" class="Bound">y</a> <a id="3145" href="Algebra.Definitions.html#3145" class="Bound">z</a><a id="3146" class="Symbol">}</a> <a id="3148" class="Symbol">→</a> <a id="3150" class="Symbol">(</a><a id="3151" href="Algebra.Definitions.html#3140" class="Bound">x</a> <a id="3153" href="Algebra.Definitions.html#3132" class="Bound Operator">•</a> <a id="3155" href="Algebra.Definitions.html#3143" class="Bound">y</a><a id="3156" class="Symbol">)</a> <a id="3158" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="3160" class="Symbol">(</a><a id="3161" href="Algebra.Definitions.html#3140" class="Bound">x</a> <a id="3163" href="Algebra.Definitions.html#3132" class="Bound Operator">•</a> <a id="3165" href="Algebra.Definitions.html#3145" class="Bound">z</a><a id="3166" class="Symbol">)</a> <a id="3168" class="Symbol">→</a> <a id="3170" href="Algebra.Definitions.html#3143" class="Bound">y</a> <a id="3172" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="3174" href="Algebra.Definitions.html#3145" class="Bound">z</a>
|
||
|
||
<a id="RightCancellative"></a><a id="3177" href="Algebra.Definitions.html#3177" class="Function">RightCancellative</a> <a id="3195" class="Symbol">:</a> <a id="3197" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="3201" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="3203" class="Symbol">→</a> <a id="3205" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3209" class="Symbol">_</a>
|
||
<a id="3211" href="Algebra.Definitions.html#3177" class="Function">RightCancellative</a> <a id="3229" href="Algebra.Definitions.html#3229" class="Bound Operator">_•_</a> <a id="3233" class="Symbol">=</a> <a id="3235" class="Symbol">∀</a> <a id="3237" class="Symbol">{</a><a id="3238" href="Algebra.Definitions.html#3238" class="Bound">x</a><a id="3239" class="Symbol">}</a> <a id="3241" href="Algebra.Definitions.html#3241" class="Bound">y</a> <a id="3243" href="Algebra.Definitions.html#3243" class="Bound">z</a> <a id="3245" class="Symbol">→</a> <a id="3247" class="Symbol">(</a><a id="3248" href="Algebra.Definitions.html#3241" class="Bound">y</a> <a id="3250" href="Algebra.Definitions.html#3229" class="Bound Operator">•</a> <a id="3252" href="Algebra.Definitions.html#3238" class="Bound">x</a><a id="3253" class="Symbol">)</a> <a id="3255" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="3257" class="Symbol">(</a><a id="3258" href="Algebra.Definitions.html#3243" class="Bound">z</a> <a id="3260" href="Algebra.Definitions.html#3229" class="Bound Operator">•</a> <a id="3262" href="Algebra.Definitions.html#3238" class="Bound">x</a><a id="3263" class="Symbol">)</a> <a id="3265" class="Symbol">→</a> <a id="3267" href="Algebra.Definitions.html#3241" class="Bound">y</a> <a id="3269" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="3271" href="Algebra.Definitions.html#3243" class="Bound">z</a>
|
||
|
||
<a id="Cancellative"></a><a id="3274" href="Algebra.Definitions.html#3274" class="Function">Cancellative</a> <a id="3287" class="Symbol">:</a> <a id="3289" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="3293" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="3295" class="Symbol">→</a> <a id="3297" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3301" class="Symbol">_</a>
|
||
<a id="3303" href="Algebra.Definitions.html#3274" class="Function">Cancellative</a> <a id="3316" href="Algebra.Definitions.html#3316" class="Bound Operator">_•_</a> <a id="3320" class="Symbol">=</a> <a id="3322" class="Symbol">(</a><a id="3323" href="Algebra.Definitions.html#3082" class="Function">LeftCancellative</a> <a id="3340" href="Algebra.Definitions.html#3316" class="Bound Operator">_•_</a><a id="3343" class="Symbol">)</a> <a id="3345" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="3347" class="Symbol">(</a><a id="3348" href="Algebra.Definitions.html#3177" class="Function">RightCancellative</a> <a id="3366" href="Algebra.Definitions.html#3316" class="Bound Operator">_•_</a><a id="3369" class="Symbol">)</a>
|
||
|
||
<a id="AlmostLeftCancellative"></a><a id="3372" href="Algebra.Definitions.html#3372" class="Function">AlmostLeftCancellative</a> <a id="3395" class="Symbol">:</a> <a id="3397" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="3399" class="Symbol">→</a> <a id="3401" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="3405" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="3407" class="Symbol">→</a> <a id="3409" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3413" class="Symbol">_</a>
|
||
<a id="3415" href="Algebra.Definitions.html#3372" class="Function">AlmostLeftCancellative</a> <a id="3438" href="Algebra.Definitions.html#3438" class="Bound">e</a> <a id="3440" href="Algebra.Definitions.html#3440" class="Bound Operator">_•_</a> <a id="3444" class="Symbol">=</a> <a id="3446" class="Symbol">∀</a> <a id="3448" class="Symbol">{</a><a id="3449" href="Algebra.Definitions.html#3449" class="Bound">x</a><a id="3450" class="Symbol">}</a> <a id="3452" href="Algebra.Definitions.html#3452" class="Bound">y</a> <a id="3454" href="Algebra.Definitions.html#3454" class="Bound">z</a> <a id="3456" class="Symbol">→</a> <a id="3458" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="3460" href="Algebra.Definitions.html#3449" class="Bound">x</a> <a id="3462" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="3464" href="Algebra.Definitions.html#3438" class="Bound">e</a> <a id="3466" class="Symbol">→</a> <a id="3468" class="Symbol">(</a><a id="3469" href="Algebra.Definitions.html#3449" class="Bound">x</a> <a id="3471" href="Algebra.Definitions.html#3440" class="Bound Operator">•</a> <a id="3473" href="Algebra.Definitions.html#3452" class="Bound">y</a><a id="3474" class="Symbol">)</a> <a id="3476" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="3478" class="Symbol">(</a><a id="3479" href="Algebra.Definitions.html#3449" class="Bound">x</a> <a id="3481" href="Algebra.Definitions.html#3440" class="Bound Operator">•</a> <a id="3483" href="Algebra.Definitions.html#3454" class="Bound">z</a><a id="3484" class="Symbol">)</a> <a id="3486" class="Symbol">→</a> <a id="3488" href="Algebra.Definitions.html#3452" class="Bound">y</a> <a id="3490" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="3492" href="Algebra.Definitions.html#3454" class="Bound">z</a>
|
||
|
||
<a id="AlmostRightCancellative"></a><a id="3495" href="Algebra.Definitions.html#3495" class="Function">AlmostRightCancellative</a> <a id="3519" class="Symbol">:</a> <a id="3521" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="3523" class="Symbol">→</a> <a id="3525" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="3529" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="3531" class="Symbol">→</a> <a id="3533" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3537" class="Symbol">_</a>
|
||
<a id="3539" href="Algebra.Definitions.html#3495" class="Function">AlmostRightCancellative</a> <a id="3563" href="Algebra.Definitions.html#3563" class="Bound">e</a> <a id="3565" href="Algebra.Definitions.html#3565" class="Bound Operator">_•_</a> <a id="3569" class="Symbol">=</a> <a id="3571" class="Symbol">∀</a> <a id="3573" class="Symbol">{</a><a id="3574" href="Algebra.Definitions.html#3574" class="Bound">x</a><a id="3575" class="Symbol">}</a> <a id="3577" href="Algebra.Definitions.html#3577" class="Bound">y</a> <a id="3579" href="Algebra.Definitions.html#3579" class="Bound">z</a> <a id="3581" class="Symbol">→</a> <a id="3583" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="3585" href="Algebra.Definitions.html#3574" class="Bound">x</a> <a id="3587" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="3589" href="Algebra.Definitions.html#3563" class="Bound">e</a> <a id="3591" class="Symbol">→</a> <a id="3593" class="Symbol">(</a><a id="3594" href="Algebra.Definitions.html#3577" class="Bound">y</a> <a id="3596" href="Algebra.Definitions.html#3565" class="Bound Operator">•</a> <a id="3598" href="Algebra.Definitions.html#3574" class="Bound">x</a><a id="3599" class="Symbol">)</a> <a id="3601" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="3603" class="Symbol">(</a><a id="3604" href="Algebra.Definitions.html#3579" class="Bound">z</a> <a id="3606" href="Algebra.Definitions.html#3565" class="Bound Operator">•</a> <a id="3608" href="Algebra.Definitions.html#3574" class="Bound">x</a><a id="3609" class="Symbol">)</a> <a id="3611" class="Symbol">→</a> <a id="3613" href="Algebra.Definitions.html#3577" class="Bound">y</a> <a id="3615" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="3617" href="Algebra.Definitions.html#3579" class="Bound">z</a>
|
||
|
||
<a id="AlmostCancellative"></a><a id="3620" href="Algebra.Definitions.html#3620" class="Function">AlmostCancellative</a> <a id="3639" class="Symbol">:</a> <a id="3641" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="3643" class="Symbol">→</a> <a id="3645" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="3649" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="3651" class="Symbol">→</a> <a id="3653" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3657" class="Symbol">_</a>
|
||
<a id="3659" href="Algebra.Definitions.html#3620" class="Function">AlmostCancellative</a> <a id="3678" href="Algebra.Definitions.html#3678" class="Bound">e</a> <a id="3680" href="Algebra.Definitions.html#3680" class="Bound Operator">_•_</a> <a id="3684" class="Symbol">=</a> <a id="3686" href="Algebra.Definitions.html#3372" class="Function">AlmostLeftCancellative</a> <a id="3709" href="Algebra.Definitions.html#3678" class="Bound">e</a> <a id="3711" href="Algebra.Definitions.html#3680" class="Bound Operator">_•_</a> <a id="3715" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="3717" href="Algebra.Definitions.html#3495" class="Function">AlmostRightCancellative</a> <a id="3741" href="Algebra.Definitions.html#3678" class="Bound">e</a> <a id="3743" href="Algebra.Definitions.html#3680" class="Bound Operator">_•_</a>
|
||
|
||
<a id="Interchangable"></a><a id="3748" href="Algebra.Definitions.html#3748" class="Function">Interchangable</a> <a id="3763" class="Symbol">:</a> <a id="3765" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="3769" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="3771" class="Symbol">→</a> <a id="3773" href="Algebra.Core.html#518" class="Function">Op₂</a> <a id="3777" href="Algebra.Definitions.html#525" class="Bound">A</a> <a id="3779" class="Symbol">→</a> <a id="3781" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3785" class="Symbol">_</a>
|
||
<a id="3787" href="Algebra.Definitions.html#3748" class="Function">Interchangable</a> <a id="3802" href="Algebra.Definitions.html#3802" class="Bound Operator">_∘_</a> <a id="3806" href="Algebra.Definitions.html#3806" class="Bound Operator">_∙_</a> <a id="3810" class="Symbol">=</a> <a id="3812" class="Symbol">∀</a> <a id="3814" href="Algebra.Definitions.html#3814" class="Bound">w</a> <a id="3816" href="Algebra.Definitions.html#3816" class="Bound">x</a> <a id="3818" href="Algebra.Definitions.html#3818" class="Bound">y</a> <a id="3820" href="Algebra.Definitions.html#3820" class="Bound">z</a> <a id="3822" class="Symbol">→</a> <a id="3824" class="Symbol">((</a><a id="3826" href="Algebra.Definitions.html#3814" class="Bound">w</a> <a id="3828" href="Algebra.Definitions.html#3806" class="Bound Operator">∙</a> <a id="3830" href="Algebra.Definitions.html#3816" class="Bound">x</a><a id="3831" class="Symbol">)</a> <a id="3833" href="Algebra.Definitions.html#3802" class="Bound Operator">∘</a> <a id="3835" class="Symbol">(</a><a id="3836" href="Algebra.Definitions.html#3818" class="Bound">y</a> <a id="3838" href="Algebra.Definitions.html#3806" class="Bound Operator">∙</a> <a id="3840" href="Algebra.Definitions.html#3820" class="Bound">z</a><a id="3841" class="Symbol">))</a> <a id="3844" href="Algebra.Definitions.html#563" class="Bound Operator">≈</a> <a id="3846" class="Symbol">((</a><a id="3848" href="Algebra.Definitions.html#3814" class="Bound">w</a> <a id="3850" href="Algebra.Definitions.html#3802" class="Bound Operator">∘</a> <a id="3852" href="Algebra.Definitions.html#3818" class="Bound">y</a><a id="3853" class="Symbol">)</a> <a id="3855" href="Algebra.Definitions.html#3806" class="Bound Operator">∙</a> <a id="3857" class="Symbol">(</a><a id="3858" href="Algebra.Definitions.html#3816" class="Bound">x</a> <a id="3860" href="Algebra.Definitions.html#3802" class="Bound Operator">∘</a> <a id="3862" href="Algebra.Definitions.html#3820" class="Bound">z</a><a id="3863" class="Symbol">))</a>
|
||
</pre></body></html> |