68 lines
19 KiB
HTML
68 lines
19 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Relation.Binary.Core</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 binary relations</a>
|
||
<a id="140" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="214" class="Comment">-- The contents of this module should be accessed via `Relation.Binary`.</a>
|
||
|
||
<a id="288" class="Symbol">{-#</a> <a id="292" class="Keyword">OPTIONS</a> <a id="300" class="Pragma">--without-K</a> <a id="312" class="Pragma">--safe</a> <a id="319" class="Symbol">#-}</a>
|
||
|
||
<a id="324" class="Keyword">module</a> <a id="331" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a> <a id="352" class="Keyword">where</a>
|
||
|
||
<a id="359" class="Keyword">open</a> <a id="364" class="Keyword">import</a> <a id="371" href="Data.Product.html" class="Module">Data.Product</a> <a id="384" class="Keyword">using</a> <a id="390" class="Symbol">(</a><a id="391" href="Data.Product.html#1167" class="Function Operator">_×_</a><a id="394" class="Symbol">)</a>
|
||
<a id="396" class="Keyword">open</a> <a id="401" class="Keyword">import</a> <a id="408" href="Function.Base.html" class="Module">Function.Base</a> <a id="422" class="Keyword">using</a> <a id="428" class="Symbol">(</a><a id="429" href="Function.Base.html#6285" class="Function Operator">_on_</a><a id="433" class="Symbol">)</a>
|
||
<a id="435" class="Keyword">open</a> <a id="440" class="Keyword">import</a> <a id="447" href="Level.html" class="Module">Level</a> <a id="453" class="Keyword">using</a> <a id="459" class="Symbol">(</a><a id="460" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="465" class="Symbol">;</a> <a id="467" href="Agda.Primitive.html#810" class="Primitive Operator">_⊔_</a><a id="470" class="Symbol">;</a> <a id="472" href="Agda.Primitive.html#780" class="Primitive">suc</a><a id="475" class="Symbol">)</a>
|
||
|
||
<a id="478" class="Keyword">private</a>
|
||
<a id="488" class="Keyword">variable</a>
|
||
<a id="501" href="Relation.Binary.Core.html#501" class="Generalizable">a</a> <a id="503" href="Relation.Binary.Core.html#503" class="Generalizable">b</a> <a id="505" href="Relation.Binary.Core.html#505" class="Generalizable">c</a> <a id="507" href="Relation.Binary.Core.html#507" class="Generalizable">ℓ</a> <a id="509" href="Relation.Binary.Core.html#509" class="Generalizable">ℓ₁</a> <a id="512" href="Relation.Binary.Core.html#512" class="Generalizable">ℓ₂</a> <a id="515" href="Relation.Binary.Core.html#515" class="Generalizable">ℓ₃</a> <a id="518" class="Symbol">:</a> <a id="520" href="Agda.Primitive.html#597" class="Postulate">Level</a>
|
||
<a id="530" href="Relation.Binary.Core.html#530" class="Generalizable">A</a> <a id="532" class="Symbol">:</a> <a id="534" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="538" href="Relation.Binary.Core.html#501" class="Generalizable">a</a>
|
||
<a id="544" href="Relation.Binary.Core.html#544" class="Generalizable">B</a> <a id="546" class="Symbol">:</a> <a id="548" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="552" href="Relation.Binary.Core.html#503" class="Generalizable">b</a>
|
||
<a id="558" href="Relation.Binary.Core.html#558" class="Generalizable">C</a> <a id="560" class="Symbol">:</a> <a id="562" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="566" href="Relation.Binary.Core.html#505" class="Generalizable">c</a>
|
||
|
||
<a id="569" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="642" class="Comment">-- Definitions</a>
|
||
<a id="657" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="731" class="Comment">-- Heterogeneous binary relations</a>
|
||
|
||
<a id="REL"></a><a id="766" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="770" class="Symbol">:</a> <a id="772" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="776" href="Relation.Binary.Core.html#501" class="Generalizable">a</a> <a id="778" class="Symbol">→</a> <a id="780" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="784" href="Relation.Binary.Core.html#503" class="Generalizable">b</a> <a id="786" class="Symbol">→</a> <a id="788" class="Symbol">(</a><a id="789" href="Relation.Binary.Core.html#789" class="Bound">ℓ</a> <a id="791" class="Symbol">:</a> <a id="793" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="798" class="Symbol">)</a> <a id="800" class="Symbol">→</a> <a id="802" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="806" class="Symbol">(</a><a id="807" href="Relation.Binary.Core.html#501" class="Generalizable">a</a> <a id="809" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="811" href="Relation.Binary.Core.html#503" class="Generalizable">b</a> <a id="813" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="815" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="819" href="Relation.Binary.Core.html#789" class="Bound">ℓ</a><a id="820" class="Symbol">)</a>
|
||
<a id="822" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="826" href="Relation.Binary.Core.html#826" class="Bound">A</a> <a id="828" href="Relation.Binary.Core.html#828" class="Bound">B</a> <a id="830" href="Relation.Binary.Core.html#830" class="Bound">ℓ</a> <a id="832" class="Symbol">=</a> <a id="834" href="Relation.Binary.Core.html#826" class="Bound">A</a> <a id="836" class="Symbol">→</a> <a id="838" href="Relation.Binary.Core.html#828" class="Bound">B</a> <a id="840" class="Symbol">→</a> <a id="842" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="846" href="Relation.Binary.Core.html#830" class="Bound">ℓ</a>
|
||
|
||
<a id="849" class="Comment">-- Homogeneous binary relations</a>
|
||
|
||
<a id="Rel"></a><a id="882" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="886" class="Symbol">:</a> <a id="888" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="892" href="Relation.Binary.Core.html#501" class="Generalizable">a</a> <a id="894" class="Symbol">→</a> <a id="896" class="Symbol">(</a><a id="897" href="Relation.Binary.Core.html#897" class="Bound">ℓ</a> <a id="899" class="Symbol">:</a> <a id="901" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="906" class="Symbol">)</a> <a id="908" class="Symbol">→</a> <a id="910" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="914" class="Symbol">(</a><a id="915" href="Relation.Binary.Core.html#501" class="Generalizable">a</a> <a id="917" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="919" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="923" href="Relation.Binary.Core.html#897" class="Bound">ℓ</a><a id="924" class="Symbol">)</a>
|
||
<a id="926" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="930" href="Relation.Binary.Core.html#930" class="Bound">A</a> <a id="932" href="Relation.Binary.Core.html#932" class="Bound">ℓ</a> <a id="934" class="Symbol">=</a> <a id="936" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="940" href="Relation.Binary.Core.html#930" class="Bound">A</a> <a id="942" href="Relation.Binary.Core.html#930" class="Bound">A</a> <a id="944" href="Relation.Binary.Core.html#932" class="Bound">ℓ</a>
|
||
|
||
<a id="947" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="1020" class="Comment">-- Relationships between relations</a>
|
||
<a id="1055" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="1129" class="Keyword">infix</a> <a id="1135" class="Number">4</a> <a id="1137" href="Relation.Binary.Core.html#1254" class="Function Operator">_⇒_</a> <a id="1141" href="Relation.Binary.Core.html#1325" class="Function Operator">_⇔_</a> <a id="1145" href="Relation.Binary.Core.html#1460" class="Function Operator">_=[_]⇒_</a>
|
||
|
||
<a id="1154" class="Comment">-- Implication/containment - could also be written _⊆_.</a>
|
||
<a id="1210" class="Comment">-- and corresponding notion of equivalence</a>
|
||
|
||
<a id="_⇒_"></a><a id="1254" href="Relation.Binary.Core.html#1254" class="Function Operator">_⇒_</a> <a id="1258" class="Symbol">:</a> <a id="1260" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="1264" href="Relation.Binary.Core.html#530" class="Generalizable">A</a> <a id="1266" href="Relation.Binary.Core.html#544" class="Generalizable">B</a> <a id="1268" href="Relation.Binary.Core.html#509" class="Generalizable">ℓ₁</a> <a id="1271" class="Symbol">→</a> <a id="1273" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="1277" href="Relation.Binary.Core.html#530" class="Generalizable">A</a> <a id="1279" href="Relation.Binary.Core.html#544" class="Generalizable">B</a> <a id="1281" href="Relation.Binary.Core.html#512" class="Generalizable">ℓ₂</a> <a id="1284" class="Symbol">→</a> <a id="1286" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1290" class="Symbol">_</a>
|
||
<a id="1292" href="Relation.Binary.Core.html#1292" class="Bound">P</a> <a id="1294" href="Relation.Binary.Core.html#1254" class="Function Operator">⇒</a> <a id="1296" href="Relation.Binary.Core.html#1296" class="Bound">Q</a> <a id="1298" class="Symbol">=</a> <a id="1300" class="Symbol">∀</a> <a id="1302" class="Symbol">{</a><a id="1303" href="Relation.Binary.Core.html#1303" class="Bound">x</a> <a id="1305" href="Relation.Binary.Core.html#1305" class="Bound">y</a><a id="1306" class="Symbol">}</a> <a id="1308" class="Symbol">→</a> <a id="1310" href="Relation.Binary.Core.html#1292" class="Bound">P</a> <a id="1312" href="Relation.Binary.Core.html#1303" class="Bound">x</a> <a id="1314" href="Relation.Binary.Core.html#1305" class="Bound">y</a> <a id="1316" class="Symbol">→</a> <a id="1318" href="Relation.Binary.Core.html#1296" class="Bound">Q</a> <a id="1320" href="Relation.Binary.Core.html#1303" class="Bound">x</a> <a id="1322" href="Relation.Binary.Core.html#1305" class="Bound">y</a>
|
||
|
||
<a id="_⇔_"></a><a id="1325" href="Relation.Binary.Core.html#1325" class="Function Operator">_⇔_</a> <a id="1329" class="Symbol">:</a> <a id="1331" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="1335" href="Relation.Binary.Core.html#530" class="Generalizable">A</a> <a id="1337" href="Relation.Binary.Core.html#544" class="Generalizable">B</a> <a id="1339" href="Relation.Binary.Core.html#509" class="Generalizable">ℓ₁</a> <a id="1342" class="Symbol">→</a> <a id="1344" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="1348" href="Relation.Binary.Core.html#530" class="Generalizable">A</a> <a id="1350" href="Relation.Binary.Core.html#544" class="Generalizable">B</a> <a id="1352" href="Relation.Binary.Core.html#512" class="Generalizable">ℓ₂</a> <a id="1355" class="Symbol">→</a> <a id="1357" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1361" class="Symbol">_</a>
|
||
<a id="1363" href="Relation.Binary.Core.html#1363" class="Bound">P</a> <a id="1365" href="Relation.Binary.Core.html#1325" class="Function Operator">⇔</a> <a id="1367" href="Relation.Binary.Core.html#1367" class="Bound">Q</a> <a id="1369" class="Symbol">=</a> <a id="1371" href="Relation.Binary.Core.html#1363" class="Bound">P</a> <a id="1373" href="Relation.Binary.Core.html#1254" class="Function Operator">⇒</a> <a id="1375" href="Relation.Binary.Core.html#1367" class="Bound">Q</a> <a id="1377" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="1379" href="Relation.Binary.Core.html#1367" class="Bound">Q</a> <a id="1381" href="Relation.Binary.Core.html#1254" class="Function Operator">⇒</a> <a id="1383" href="Relation.Binary.Core.html#1363" class="Bound">P</a>
|
||
|
||
<a id="1386" class="Comment">-- Generalised implication - if P ≡ Q it can be read as "f preserves P".</a>
|
||
|
||
<a id="_=[_]⇒_"></a><a id="1460" href="Relation.Binary.Core.html#1460" class="Function Operator">_=[_]⇒_</a> <a id="1468" class="Symbol">:</a> <a id="1470" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="1474" href="Relation.Binary.Core.html#530" class="Generalizable">A</a> <a id="1476" href="Relation.Binary.Core.html#509" class="Generalizable">ℓ₁</a> <a id="1479" class="Symbol">→</a> <a id="1481" class="Symbol">(</a><a id="1482" href="Relation.Binary.Core.html#530" class="Generalizable">A</a> <a id="1484" class="Symbol">→</a> <a id="1486" href="Relation.Binary.Core.html#544" class="Generalizable">B</a><a id="1487" class="Symbol">)</a> <a id="1489" class="Symbol">→</a> <a id="1491" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="1495" href="Relation.Binary.Core.html#544" class="Generalizable">B</a> <a id="1497" href="Relation.Binary.Core.html#512" class="Generalizable">ℓ₂</a> <a id="1500" class="Symbol">→</a> <a id="1502" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1506" class="Symbol">_</a>
|
||
<a id="1508" href="Relation.Binary.Core.html#1508" class="Bound">P</a> <a id="1510" href="Relation.Binary.Core.html#1460" class="Function Operator">=[</a> <a id="1513" href="Relation.Binary.Core.html#1513" class="Bound">f</a> <a id="1515" href="Relation.Binary.Core.html#1460" class="Function Operator">]⇒</a> <a id="1518" href="Relation.Binary.Core.html#1518" class="Bound">Q</a> <a id="1520" class="Symbol">=</a> <a id="1522" href="Relation.Binary.Core.html#1508" class="Bound">P</a> <a id="1524" href="Relation.Binary.Core.html#1254" class="Function Operator">⇒</a> <a id="1526" class="Symbol">(</a><a id="1527" href="Relation.Binary.Core.html#1518" class="Bound">Q</a> <a id="1529" href="Function.Base.html#6285" class="Function Operator">on</a> <a id="1532" href="Relation.Binary.Core.html#1513" class="Bound">f</a><a id="1533" class="Symbol">)</a>
|
||
|
||
<a id="1536" class="Comment">-- A synonym for _=[_]⇒_.</a>
|
||
|
||
<a id="_Preserves_⟶_"></a><a id="1563" href="Relation.Binary.Core.html#1563" class="Function Operator">_Preserves_⟶_</a> <a id="1577" class="Symbol">:</a> <a id="1579" class="Symbol">(</a><a id="1580" href="Relation.Binary.Core.html#530" class="Generalizable">A</a> <a id="1582" class="Symbol">→</a> <a id="1584" href="Relation.Binary.Core.html#544" class="Generalizable">B</a><a id="1585" class="Symbol">)</a> <a id="1587" class="Symbol">→</a> <a id="1589" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="1593" href="Relation.Binary.Core.html#530" class="Generalizable">A</a> <a id="1595" href="Relation.Binary.Core.html#509" class="Generalizable">ℓ₁</a> <a id="1598" class="Symbol">→</a> <a id="1600" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="1604" href="Relation.Binary.Core.html#544" class="Generalizable">B</a> <a id="1606" href="Relation.Binary.Core.html#512" class="Generalizable">ℓ₂</a> <a id="1609" class="Symbol">→</a> <a id="1611" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1615" class="Symbol">_</a>
|
||
<a id="1617" href="Relation.Binary.Core.html#1617" class="Bound">f</a> <a id="1619" href="Relation.Binary.Core.html#1563" class="Function Operator">Preserves</a> <a id="1629" href="Relation.Binary.Core.html#1629" class="Bound">P</a> <a id="1631" href="Relation.Binary.Core.html#1563" class="Function Operator">⟶</a> <a id="1633" href="Relation.Binary.Core.html#1633" class="Bound">Q</a> <a id="1635" class="Symbol">=</a> <a id="1637" href="Relation.Binary.Core.html#1629" class="Bound">P</a> <a id="1639" href="Relation.Binary.Core.html#1460" class="Function Operator">=[</a> <a id="1642" href="Relation.Binary.Core.html#1617" class="Bound">f</a> <a id="1644" href="Relation.Binary.Core.html#1460" class="Function Operator">]⇒</a> <a id="1647" href="Relation.Binary.Core.html#1633" class="Bound">Q</a>
|
||
|
||
<a id="1650" class="Comment">-- A binary variant of _Preserves_⟶_.</a>
|
||
|
||
<a id="_Preserves₂_⟶_⟶_"></a><a id="1689" href="Relation.Binary.Core.html#1689" class="Function Operator">_Preserves₂_⟶_⟶_</a> <a id="1706" class="Symbol">:</a> <a id="1708" class="Symbol">(</a><a id="1709" href="Relation.Binary.Core.html#530" class="Generalizable">A</a> <a id="1711" class="Symbol">→</a> <a id="1713" href="Relation.Binary.Core.html#544" class="Generalizable">B</a> <a id="1715" class="Symbol">→</a> <a id="1717" href="Relation.Binary.Core.html#558" class="Generalizable">C</a><a id="1718" class="Symbol">)</a> <a id="1720" class="Symbol">→</a> <a id="1722" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="1726" href="Relation.Binary.Core.html#530" class="Generalizable">A</a> <a id="1728" href="Relation.Binary.Core.html#509" class="Generalizable">ℓ₁</a> <a id="1731" class="Symbol">→</a> <a id="1733" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="1737" href="Relation.Binary.Core.html#544" class="Generalizable">B</a> <a id="1739" href="Relation.Binary.Core.html#512" class="Generalizable">ℓ₂</a> <a id="1742" class="Symbol">→</a> <a id="1744" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="1748" href="Relation.Binary.Core.html#558" class="Generalizable">C</a> <a id="1750" href="Relation.Binary.Core.html#515" class="Generalizable">ℓ₃</a> <a id="1753" class="Symbol">→</a> <a id="1755" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1759" class="Symbol">_</a>
|
||
<a id="1761" href="Relation.Binary.Core.html#1761" class="Bound Operator">_∙_</a> <a id="1765" href="Relation.Binary.Core.html#1689" class="Function Operator">Preserves₂</a> <a id="1776" href="Relation.Binary.Core.html#1776" class="Bound">P</a> <a id="1778" href="Relation.Binary.Core.html#1689" class="Function Operator">⟶</a> <a id="1780" href="Relation.Binary.Core.html#1780" class="Bound">Q</a> <a id="1782" href="Relation.Binary.Core.html#1689" class="Function Operator">⟶</a> <a id="1784" href="Relation.Binary.Core.html#1784" class="Bound">R</a> <a id="1786" class="Symbol">=</a> <a id="1788" class="Symbol">∀</a> <a id="1790" class="Symbol">{</a><a id="1791" href="Relation.Binary.Core.html#1791" class="Bound">x</a> <a id="1793" href="Relation.Binary.Core.html#1793" class="Bound">y</a> <a id="1795" href="Relation.Binary.Core.html#1795" class="Bound">u</a> <a id="1797" href="Relation.Binary.Core.html#1797" class="Bound">v</a><a id="1798" class="Symbol">}</a> <a id="1800" class="Symbol">→</a> <a id="1802" href="Relation.Binary.Core.html#1776" class="Bound">P</a> <a id="1804" href="Relation.Binary.Core.html#1791" class="Bound">x</a> <a id="1806" href="Relation.Binary.Core.html#1793" class="Bound">y</a> <a id="1808" class="Symbol">→</a> <a id="1810" href="Relation.Binary.Core.html#1780" class="Bound">Q</a> <a id="1812" href="Relation.Binary.Core.html#1795" class="Bound">u</a> <a id="1814" href="Relation.Binary.Core.html#1797" class="Bound">v</a> <a id="1816" class="Symbol">→</a> <a id="1818" href="Relation.Binary.Core.html#1784" class="Bound">R</a> <a id="1820" class="Symbol">(</a><a id="1821" href="Relation.Binary.Core.html#1791" class="Bound">x</a> <a id="1823" href="Relation.Binary.Core.html#1761" class="Bound Operator">∙</a> <a id="1825" href="Relation.Binary.Core.html#1795" class="Bound">u</a><a id="1826" class="Symbol">)</a> <a id="1828" class="Symbol">(</a><a id="1829" href="Relation.Binary.Core.html#1793" class="Bound">y</a> <a id="1831" href="Relation.Binary.Core.html#1761" class="Bound Operator">∙</a> <a id="1833" href="Relation.Binary.Core.html#1797" class="Bound">v</a><a id="1834" class="Symbol">)</a>
|
||
</pre></body></html> |