/usr/share/doc/agda-stdlib-doc/html/Relation.Binary.NonStrictToStrict.html is in agda-stdlib-doc 0.14-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 | <!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Relation.Binary.NonStrictToStrict</title><link rel="stylesheet" href="Agda.css"></head><body><pre><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">-- Conversion of ≤ to <, along with a number of properties</a>
<a id="165" class="Comment">------------------------------------------------------------------------</a>
<a id="239" class="Comment">-- Possible TODO: Prove that a conversion ≤ → < → ≤ returns a</a>
<a id="301" class="Comment">-- relation equivalent to the original one (and similarly for</a>
<a id="363" class="Comment">-- < → ≤ → <).</a>
<a id="379" class="Keyword">open</a> <a id="384" class="Keyword">import</a> <a id="391" href="Relation.Binary.html" class="Module">Relation.Binary</a>
<a id="408" class="Keyword">module</a> <a id="415" href="Relation.Binary.NonStrictToStrict.html" class="Module">Relation.Binary.NonStrictToStrict</a>
<a id="458" class="Symbol">{</a><a id="459" href="Relation.Binary.NonStrictToStrict.html#459" class="Bound">a</a> <a id="461" href="Relation.Binary.NonStrictToStrict.html#461" class="Bound">ℓ₁</a> <a id="464" href="Relation.Binary.NonStrictToStrict.html#464" class="Bound">ℓ₂</a><a id="466" class="Symbol">}</a> <a id="468" class="Symbol">{</a><a id="469" href="Relation.Binary.NonStrictToStrict.html#469" class="Bound">A</a> <a id="471" class="Symbol">:</a> <a id="473" class="PrimitiveType">Set</a> <a id="477" href="Relation.Binary.NonStrictToStrict.html#459" class="Bound">a</a><a id="478" class="Symbol">}</a>
<a id="489" class="Symbol">(</a><a id="490" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="494" class="Symbol">:</a> <a id="496" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="500" href="Relation.Binary.NonStrictToStrict.html#469" class="Bound">A</a> <a id="502" href="Relation.Binary.NonStrictToStrict.html#461" class="Bound">ℓ₁</a><a id="504" class="Symbol">)</a> <a id="506" class="Symbol">(</a><a id="507" href="Relation.Binary.NonStrictToStrict.html#507" class="Bound Operator">_≤_</a> <a id="511" class="Symbol">:</a> <a id="513" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="517" href="Relation.Binary.NonStrictToStrict.html#469" class="Bound">A</a> <a id="519" href="Relation.Binary.NonStrictToStrict.html#464" class="Bound">ℓ₂</a><a id="521" class="Symbol">)</a>
<a id="532" class="Keyword">where</a>
<a id="539" class="Keyword">open</a> <a id="544" class="Keyword">import</a> <a id="551" href="Relation.Nullary.html" class="Module">Relation.Nullary</a>
<a id="568" class="Keyword">open</a> <a id="573" class="Keyword">import</a> <a id="580" href="Relation.Binary.Consequences.html" class="Module">Relation.Binary.Consequences</a>
<a id="609" class="Keyword">open</a> <a id="614" class="Keyword">import</a> <a id="621" href="Function.html" class="Module">Function</a>
<a id="630" class="Keyword">open</a> <a id="635" class="Keyword">import</a> <a id="642" href="Data.Product.html" class="Module">Data.Product</a>
<a id="655" class="Keyword">open</a> <a id="660" class="Keyword">import</a> <a id="667" href="Data.Sum.html" class="Module">Data.Sum</a>
<a id="677" class="Comment">------------------------------------------------------------------------</a>
<a id="750" class="Comment">-- Conversion</a>
<a id="765" class="Comment">-- _≤_ can be turned into _<_ as follows:</a>
<a id="_<_" href="Relation.Binary.NonStrictToStrict.html#_%3C_" class="Function Operator">_<_</a> <a id="812" class="Symbol">:</a> <a id="814" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="818" href="Relation.Binary.NonStrictToStrict.html#469" class="Bound">A</a> <a id="820" class="Symbol">_</a>
<a id="822" href="Relation.Binary.NonStrictToStrict.html#822" class="Bound">x</a> <a id="824" href="Relation.Binary.NonStrictToStrict.html#_%3C_" class="Function Operator"><</a> <a id="826" href="Relation.Binary.NonStrictToStrict.html#826" class="Bound">y</a> <a id="828" class="Symbol">=</a> <a id="830" class="Symbol">(</a><a id="831" href="Relation.Binary.NonStrictToStrict.html#822" class="Bound">x</a> <a id="833" href="Relation.Binary.NonStrictToStrict.html#507" class="Bound Operator">≤</a> <a id="835" href="Relation.Binary.NonStrictToStrict.html#826" class="Bound">y</a><a id="836" class="Symbol">)</a> <a id="838" href="Data.Product.html#_%C3%97_" class="Function Operator">×</a> <a id="840" href="Relation.Nullary.html#%C2%AC_" class="Function Operator">¬</a> <a id="842" class="Symbol">(</a><a id="843" href="Relation.Binary.NonStrictToStrict.html#822" class="Bound">x</a> <a id="845" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">≈</a> <a id="847" href="Relation.Binary.NonStrictToStrict.html#826" class="Bound">y</a><a id="848" class="Symbol">)</a>
<a id="851" class="Comment">------------------------------------------------------------------------</a>
<a id="924" class="Comment">-- The converted relations have certain properties</a>
<a id="975" class="Comment">-- (if the original relations have certain other properties)</a>
<a id="irrefl" href="Relation.Binary.NonStrictToStrict.html#irrefl" class="Function">irrefl</a> <a id="1044" class="Symbol">:</a> <a id="1046" href="Relation.Binary.Core.html#Irreflexive" class="Function">Irreflexive</a> <a id="1058" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="1062" href="Relation.Binary.NonStrictToStrict.html#_%3C_" class="Function Operator">_<_</a>
<a id="1066" href="Relation.Binary.NonStrictToStrict.html#irrefl" class="Function">irrefl</a> <a id="1073" href="Relation.Binary.NonStrictToStrict.html#1073" class="Bound">x≈y</a> <a id="1077" href="Relation.Binary.NonStrictToStrict.html#1077" class="Bound">x<y</a> <a id="1081" class="Symbol">=</a> <a id="1083" href="Data.Product.html#%CE%A3.proj%E2%82%82" class="Field">proj₂</a> <a id="1089" href="Relation.Binary.NonStrictToStrict.html#1077" class="Bound">x<y</a> <a id="1093" href="Relation.Binary.NonStrictToStrict.html#1073" class="Bound">x≈y</a>
<a id="trans" href="Relation.Binary.NonStrictToStrict.html#trans" class="Function">trans</a> <a id="1104" class="Symbol">:</a> <a id="1106" href="Relation.Binary.html#IsPartialOrder" class="Record">IsPartialOrder</a> <a id="1121" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="1125" href="Relation.Binary.NonStrictToStrict.html#507" class="Bound Operator">_≤_</a> <a id="1129" class="Symbol">→</a> <a id="1131" href="Relation.Binary.Core.html#Transitive" class="Function">Transitive</a> <a id="1142" href="Relation.Binary.NonStrictToStrict.html#_%3C_" class="Function Operator">_<_</a>
<a id="1146" href="Relation.Binary.NonStrictToStrict.html#trans" class="Function">trans</a> <a id="1152" href="Relation.Binary.NonStrictToStrict.html#1152" class="Bound">po</a> <a id="1155" class="Symbol">=</a> <a id="1157" class="Symbol">λ</a> <a id="1159" href="Relation.Binary.NonStrictToStrict.html#1159" class="Bound">x<y</a> <a id="1163" href="Relation.Binary.NonStrictToStrict.html#1163" class="Bound">y<z</a> <a id="1167" class="Symbol">→</a>
<a id="1171" class="Symbol">(</a> <a id="1173" href="Relation.Binary.html#1190" class="Function">PO.trans</a> <a id="1182" class="Symbol">(</a><a id="1183" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a> <a id="1189" href="Relation.Binary.NonStrictToStrict.html#1159" class="Bound">x<y</a><a id="1192" class="Symbol">)</a> <a id="1194" class="Symbol">(</a><a id="1195" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a> <a id="1201" href="Relation.Binary.NonStrictToStrict.html#1163" class="Bound">y<z</a><a id="1204" class="Symbol">)</a>
<a id="1208" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1210" class="Symbol">λ</a> <a id="1212" href="Relation.Binary.NonStrictToStrict.html#1212" class="Bound">x≈z</a> <a id="1216" class="Symbol">→</a> <a id="1218" href="Data.Product.html#%CE%A3.proj%E2%82%82" class="Field">proj₂</a> <a id="1224" href="Relation.Binary.NonStrictToStrict.html#1159" class="Bound">x<y</a> <a id="1228" href="Function.html#_%24_" class="Function Operator">$</a> <a id="1230" href="Relation.Binary.NonStrictToStrict.html#1311" class="Function">lemma</a> <a id="1236" class="Symbol">(</a><a id="1237" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a> <a id="1243" href="Relation.Binary.NonStrictToStrict.html#1159" class="Bound">x<y</a><a id="1246" class="Symbol">)</a> <a id="1248" class="Symbol">(</a><a id="1249" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a> <a id="1255" href="Relation.Binary.NonStrictToStrict.html#1163" class="Bound">y<z</a><a id="1258" class="Symbol">)</a> <a id="1260" href="Relation.Binary.NonStrictToStrict.html#1212" class="Bound">x≈z</a>
<a id="1266" class="Symbol">)</a>
<a id="1270" class="Keyword">where</a>
<a id="1278" class="Keyword">module</a> <a id="PO" href="Relation.Binary.NonStrictToStrict.html#PO" class="Module">PO</a> <a id="1288" class="Symbol">=</a> <a id="1290" href="Relation.Binary.html#IsPartialOrder" class="Module">IsPartialOrder</a> <a id="1305" href="Relation.Binary.NonStrictToStrict.html#1152" class="Bound">po</a>
<a id="1311" href="Relation.Binary.NonStrictToStrict.html#1311" class="Function">lemma</a> <a id="1317" class="Symbol">:</a> <a id="1319" class="Symbol">∀</a> <a id="1321" class="Symbol">{</a><a id="1322" href="Relation.Binary.NonStrictToStrict.html#1322" class="Bound">x</a> <a id="1324" href="Relation.Binary.NonStrictToStrict.html#1324" class="Bound">y</a> <a id="1326" href="Relation.Binary.NonStrictToStrict.html#1326" class="Bound">z</a><a id="1327" class="Symbol">}</a> <a id="1329" class="Symbol">→</a> <a id="1331" href="Relation.Binary.NonStrictToStrict.html#1322" class="Bound">x</a> <a id="1333" href="Relation.Binary.NonStrictToStrict.html#507" class="Bound Operator">≤</a> <a id="1335" href="Relation.Binary.NonStrictToStrict.html#1324" class="Bound">y</a> <a id="1337" class="Symbol">→</a> <a id="1339" href="Relation.Binary.NonStrictToStrict.html#1324" class="Bound">y</a> <a id="1341" href="Relation.Binary.NonStrictToStrict.html#507" class="Bound Operator">≤</a> <a id="1343" href="Relation.Binary.NonStrictToStrict.html#1326" class="Bound">z</a> <a id="1345" class="Symbol">→</a> <a id="1347" href="Relation.Binary.NonStrictToStrict.html#1322" class="Bound">x</a> <a id="1349" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">≈</a> <a id="1351" href="Relation.Binary.NonStrictToStrict.html#1326" class="Bound">z</a> <a id="1353" class="Symbol">→</a> <a id="1355" href="Relation.Binary.NonStrictToStrict.html#1322" class="Bound">x</a> <a id="1357" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">≈</a> <a id="1359" href="Relation.Binary.NonStrictToStrict.html#1324" class="Bound">y</a>
<a id="1363" href="Relation.Binary.NonStrictToStrict.html#1311" class="Function">lemma</a> <a id="1369" href="Relation.Binary.NonStrictToStrict.html#1369" class="Bound">x≤y</a> <a id="1373" href="Relation.Binary.NonStrictToStrict.html#1373" class="Bound">y≤z</a> <a id="1377" href="Relation.Binary.NonStrictToStrict.html#1377" class="Bound">x≈z</a> <a id="1381" class="Symbol">=</a>
<a id="1387" href="Relation.Binary.html#3608" class="Function">PO.antisym</a> <a id="1398" href="Relation.Binary.NonStrictToStrict.html#1369" class="Bound">x≤y</a> <a id="1402" href="Function.html#_%24_" class="Function Operator">$</a> <a id="1404" href="Relation.Binary.html#1190" class="Function">PO.trans</a> <a id="1413" href="Relation.Binary.NonStrictToStrict.html#1373" class="Bound">y≤z</a> <a id="1417" class="Symbol">(</a><a id="1418" href="Relation.Binary.html#1160" class="Function">PO.reflexive</a> <a id="1431" href="Function.html#_%24_" class="Function Operator">$</a> <a id="1433" href="Relation.Binary.Core.html#4960" class="Function">PO.Eq.sym</a> <a id="1443" href="Relation.Binary.NonStrictToStrict.html#1377" class="Bound">x≈z</a><a id="1446" class="Symbol">)</a>
<a id="antisym⟶asym" href="Relation.Binary.NonStrictToStrict.html#antisym%E2%9F%B6asym" class="Function">antisym⟶asym</a> <a id="1462" class="Symbol">:</a> <a id="1464" href="Relation.Binary.Core.html#Antisymmetric" class="Function">Antisymmetric</a> <a id="1478" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="1482" href="Relation.Binary.NonStrictToStrict.html#507" class="Bound Operator">_≤_</a> <a id="1486" class="Symbol">→</a> <a id="1488" href="Relation.Binary.Core.html#Asymmetric" class="Function">Asymmetric</a> <a id="1499" href="Relation.Binary.NonStrictToStrict.html#_%3C_" class="Function Operator">_<_</a>
<a id="1503" href="Relation.Binary.NonStrictToStrict.html#antisym%E2%9F%B6asym" class="Function">antisym⟶asym</a> <a id="1516" href="Relation.Binary.NonStrictToStrict.html#1516" class="Bound">antisym</a> <a id="1524" class="Symbol">(</a><a id="1525" href="Relation.Binary.NonStrictToStrict.html#1525" class="Bound">x≤y</a> <a id="1529" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1531" href="Relation.Binary.NonStrictToStrict.html#1531" class="Bound">¬x≈y</a><a id="1535" class="Symbol">)</a> <a id="1537" class="Symbol">(</a><a id="1538" href="Relation.Binary.NonStrictToStrict.html#1538" class="Bound">y≤x</a> <a id="1542" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1544" href="Relation.Binary.NonStrictToStrict.html#1544" class="Bound">¬y≈x</a><a id="1548" class="Symbol">)</a> <a id="1550" class="Symbol">=</a>
<a id="1554" href="Relation.Binary.NonStrictToStrict.html#1531" class="Bound">¬x≈y</a> <a id="1559" class="Symbol">(</a><a id="1560" href="Relation.Binary.NonStrictToStrict.html#1516" class="Bound">antisym</a> <a id="1568" href="Relation.Binary.NonStrictToStrict.html#1525" class="Bound">x≤y</a> <a id="1572" href="Relation.Binary.NonStrictToStrict.html#1538" class="Bound">y≤x</a><a id="1575" class="Symbol">)</a>
<a id="<-resp-≈" href="Relation.Binary.NonStrictToStrict.html#%3C-resp-%E2%89%88" class="Function"><-resp-≈</a> <a id="1587" class="Symbol">:</a> <a id="1589" href="Relation.Binary.Core.html#IsEquivalence" class="Record">IsEquivalence</a> <a id="1603" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="1607" class="Symbol">→</a> <a id="1609" href="Relation.Binary.NonStrictToStrict.html#507" class="Bound Operator">_≤_</a> <a id="1613" href="Relation.Binary.Core.html#_Respects%E2%82%82_" class="Function Operator">Respects₂</a> <a id="1623" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="1627" class="Symbol">→</a> <a id="1629" href="Relation.Binary.NonStrictToStrict.html#_%3C_" class="Function Operator">_<_</a> <a id="1633" href="Relation.Binary.Core.html#_Respects%E2%82%82_" class="Function Operator">Respects₂</a> <a id="1643" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a>
<a id="1647" href="Relation.Binary.NonStrictToStrict.html#%3C-resp-%E2%89%88" class="Function"><-resp-≈</a> <a id="1656" href="Relation.Binary.NonStrictToStrict.html#1656" class="Bound">eq</a> <a id="1659" href="Relation.Binary.NonStrictToStrict.html#1659" class="Bound">≤-resp-≈</a> <a id="1668" class="Symbol">=</a>
<a id="1672" class="Symbol">(λ</a> <a id="1675" class="Symbol">{</a><a id="1676" href="Relation.Binary.NonStrictToStrict.html#1676" class="Bound">x</a> <a id="1678" href="Relation.Binary.NonStrictToStrict.html#1678" class="Bound">y'</a> <a id="1681" href="Relation.Binary.NonStrictToStrict.html#1681" class="Bound">y</a><a id="1682" class="Symbol">}</a> <a id="1684" href="Relation.Binary.NonStrictToStrict.html#1684" class="Bound">y'≈y</a> <a id="1689" href="Relation.Binary.NonStrictToStrict.html#1689" class="Bound">x<y'</a> <a id="1694" class="Symbol">→</a>
<a id="1700" class="Symbol">(</a> <a id="1702" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a> <a id="1708" href="Relation.Binary.NonStrictToStrict.html#1659" class="Bound">≤-resp-≈</a> <a id="1717" href="Relation.Binary.NonStrictToStrict.html#1684" class="Bound">y'≈y</a> <a id="1722" class="Symbol">(</a><a id="1723" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a> <a id="1729" href="Relation.Binary.NonStrictToStrict.html#1689" class="Bound">x<y'</a><a id="1733" class="Symbol">)</a>
<a id="1739" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1741" class="Symbol">λ</a> <a id="1743" href="Relation.Binary.NonStrictToStrict.html#1743" class="Bound">x≈y</a> <a id="1747" class="Symbol">→</a> <a id="1749" href="Data.Product.html#%CE%A3.proj%E2%82%82" class="Field">proj₂</a> <a id="1755" href="Relation.Binary.NonStrictToStrict.html#1689" class="Bound">x<y'</a> <a id="1760" class="Symbol">(</a><a id="1761" href="Relation.Binary.Core.html#4986" class="Function">Eq.trans</a> <a id="1770" href="Relation.Binary.NonStrictToStrict.html#1743" class="Bound">x≈y</a> <a id="1774" class="Symbol">(</a><a id="1775" href="Relation.Binary.Core.html#4960" class="Function">Eq.sym</a> <a id="1782" href="Relation.Binary.NonStrictToStrict.html#1684" class="Bound">y'≈y</a><a id="1786" class="Symbol">))</a>
<a id="1793" class="Symbol">)</a>
<a id="1797" class="Symbol">)</a> <a id="1799" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a>
<a id="1803" class="Symbol">(λ</a> <a id="1806" class="Symbol">{</a><a id="1807" href="Relation.Binary.NonStrictToStrict.html#1807" class="Bound">y</a> <a id="1809" href="Relation.Binary.NonStrictToStrict.html#1809" class="Bound">x'</a> <a id="1812" href="Relation.Binary.NonStrictToStrict.html#1812" class="Bound">x</a><a id="1813" class="Symbol">}</a> <a id="1815" href="Relation.Binary.NonStrictToStrict.html#1815" class="Bound">x'≈x</a> <a id="1820" href="Relation.Binary.NonStrictToStrict.html#1820" class="Bound">x'<y</a> <a id="1825" class="Symbol">→</a>
<a id="1831" class="Symbol">(</a> <a id="1833" href="Data.Product.html#%CE%A3.proj%E2%82%82" class="Field">proj₂</a> <a id="1839" href="Relation.Binary.NonStrictToStrict.html#1659" class="Bound">≤-resp-≈</a> <a id="1848" href="Relation.Binary.NonStrictToStrict.html#1815" class="Bound">x'≈x</a> <a id="1853" class="Symbol">(</a><a id="1854" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a> <a id="1860" href="Relation.Binary.NonStrictToStrict.html#1820" class="Bound">x'<y</a><a id="1864" class="Symbol">)</a>
<a id="1870" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1872" class="Symbol">λ</a> <a id="1874" href="Relation.Binary.NonStrictToStrict.html#1874" class="Bound">x≈y</a> <a id="1878" class="Symbol">→</a> <a id="1880" href="Data.Product.html#%CE%A3.proj%E2%82%82" class="Field">proj₂</a> <a id="1886" href="Relation.Binary.NonStrictToStrict.html#1820" class="Bound">x'<y</a> <a id="1891" class="Symbol">(</a><a id="1892" href="Relation.Binary.Core.html#4986" class="Function">Eq.trans</a> <a id="1901" href="Relation.Binary.NonStrictToStrict.html#1815" class="Bound">x'≈x</a> <a id="1906" href="Relation.Binary.NonStrictToStrict.html#1874" class="Bound">x≈y</a><a id="1909" class="Symbol">)</a>
<a id="1915" class="Symbol">))</a>
<a id="1920" class="Keyword">where</a> <a id="1926" class="Keyword">module</a> <a id="Eq" href="Relation.Binary.NonStrictToStrict.html#Eq" class="Module">Eq</a> <a id="1936" class="Symbol">=</a> <a id="1938" href="Relation.Binary.Core.html#IsEquivalence" class="Module">IsEquivalence</a> <a id="1952" href="Relation.Binary.NonStrictToStrict.html#1656" class="Bound">eq</a>
<a id="trichotomous" href="Relation.Binary.NonStrictToStrict.html#trichotomous" class="Function">trichotomous</a> <a id="1969" class="Symbol">:</a> <a id="1971" href="Relation.Binary.Core.html#Symmetric" class="Function">Symmetric</a> <a id="1981" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="1985" class="Symbol">→</a> <a id="1987" href="Relation.Binary.Core.html#Decidable" class="Function">Decidable</a> <a id="1997" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="2001" class="Symbol">→</a>
<a id="2018" href="Relation.Binary.Core.html#Antisymmetric" class="Function">Antisymmetric</a> <a id="2032" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="2036" href="Relation.Binary.NonStrictToStrict.html#507" class="Bound Operator">_≤_</a> <a id="2040" class="Symbol">→</a> <a id="2042" href="Relation.Binary.Consequences.html#Total" class="Function">Total</a> <a id="2048" href="Relation.Binary.NonStrictToStrict.html#507" class="Bound Operator">_≤_</a> <a id="2052" class="Symbol">→</a>
<a id="2069" href="Relation.Binary.Core.html#Trichotomous" class="Function">Trichotomous</a> <a id="2082" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="2086" href="Relation.Binary.NonStrictToStrict.html#_%3C_" class="Function Operator">_<_</a>
<a id="2090" href="Relation.Binary.NonStrictToStrict.html#trichotomous" class="Function">trichotomous</a> <a id="2103" href="Relation.Binary.NonStrictToStrict.html#2103" class="Bound">≈-sym</a> <a id="2109" href="Relation.Binary.NonStrictToStrict.html#2109" class="Bound">≈-dec</a> <a id="2115" href="Relation.Binary.NonStrictToStrict.html#2115" class="Bound">antisym</a> <a id="2123" href="Relation.Binary.NonStrictToStrict.html#2123" class="Bound">total</a> <a id="2129" href="Relation.Binary.NonStrictToStrict.html#2129" class="Bound">x</a> <a id="2131" href="Relation.Binary.NonStrictToStrict.html#2131" class="Bound">y</a> <a id="2133" class="Keyword">with</a> <a id="2138" href="Relation.Binary.NonStrictToStrict.html#2109" class="Bound">≈-dec</a> <a id="2144" href="Relation.Binary.NonStrictToStrict.html#2129" class="Bound">x</a> <a id="2146" href="Relation.Binary.NonStrictToStrict.html#2131" class="Bound">y</a>
<a id="2148" class="Symbol">...</a> <a id="2152" class="Symbol">|</a> <a id="2154" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2158" href="Relation.Binary.NonStrictToStrict.html#2158" class="Bound">x≈y</a> <a id="2162" class="Symbol">=</a> <a id="2164" href="Relation.Binary.Core.html#Tri.tri%E2%89%88" class="InductiveConstructor">tri≈</a> <a id="2169" class="Symbol">(</a><a id="2170" href="Relation.Binary.NonStrictToStrict.html#irrefl" class="Function">irrefl</a> <a id="2177" href="Relation.Binary.NonStrictToStrict.html#2158" class="Bound">x≈y</a><a id="2180" class="Symbol">)</a> <a id="2182" href="Relation.Binary.NonStrictToStrict.html#2158" class="Bound">x≈y</a> <a id="2186" class="Symbol">(</a><a id="2187" href="Relation.Binary.NonStrictToStrict.html#irrefl" class="Function">irrefl</a> <a id="2194" class="Symbol">(</a><a id="2195" class="Bound">≈-sym</a> <a id="2201" href="Relation.Binary.NonStrictToStrict.html#2158" class="Bound">x≈y</a><a id="2204" class="Symbol">))</a>
<a id="2207" class="Symbol">...</a> <a id="2211" class="Symbol">|</a> <a id="2213" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2217" href="Relation.Binary.NonStrictToStrict.html#2217" class="Bound">x≉y</a> <a id="2221" class="Keyword">with</a> <a id="2226" class="Bound">total</a> <a id="2232" class="Bound">x</a> <a id="2234" class="Bound">y</a>
<a id="2236" class="Symbol">...</a> <a id="2242" class="Symbol">|</a> <a id="2244" href="Data.Sum.html#_%E2%8A%8E_.inj%E2%82%81" class="InductiveConstructor">inj₁</a> <a id="2249" href="Relation.Binary.NonStrictToStrict.html#2249" class="Bound">x≤y</a> <a id="2253" class="Symbol">=</a> <a id="2255" href="Relation.Binary.Core.html#Tri.tri%3C" class="InductiveConstructor">tri<</a> <a id="2260" class="Symbol">(</a><a id="2261" href="Relation.Binary.NonStrictToStrict.html#2249" class="Bound">x≤y</a> <a id="2265" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="2267" class="Bound">x≉y</a><a id="2270" class="Symbol">)</a> <a id="2272" class="Bound">x≉y</a>
<a id="2300" class="Symbol">(</a><a id="2301" class="Bound">x≉y</a> <a id="2305" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="2307" class="Bound">antisym</a> <a id="2315" href="Relation.Binary.NonStrictToStrict.html#2249" class="Bound">x≤y</a> <a id="2319" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="2321" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a><a id="2326" class="Symbol">)</a>
<a id="2328" class="Symbol">...</a> <a id="2334" class="Symbol">|</a> <a id="2336" href="Data.Sum.html#_%E2%8A%8E_.inj%E2%82%82" class="InductiveConstructor">inj₂</a> <a id="2341" href="Relation.Binary.NonStrictToStrict.html#2341" class="Bound">x≥y</a> <a id="2345" class="Symbol">=</a> <a id="2347" href="Relation.Binary.Core.html#Tri.tri%3E" class="InductiveConstructor">tri></a> <a id="2352" class="Symbol">(</a><a id="2353" class="Bound">x≉y</a> <a id="2357" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="2359" href="Function.html#flip" class="Function">flip</a> <a id="2364" class="Bound">antisym</a> <a id="2372" href="Relation.Binary.NonStrictToStrict.html#2341" class="Bound">x≥y</a> <a id="2376" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="2378" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a><a id="2383" class="Symbol">)</a> <a id="2385" class="Bound">x≉y</a>
<a id="2413" class="Symbol">(</a><a id="2414" href="Relation.Binary.NonStrictToStrict.html#2341" class="Bound">x≥y</a> <a id="2418" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="2420" class="Bound">x≉y</a> <a id="2424" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="2426" class="Bound">≈-sym</a><a id="2431" class="Symbol">)</a>
<a id="decidable" href="Relation.Binary.NonStrictToStrict.html#decidable" class="Function">decidable</a> <a id="2444" class="Symbol">:</a> <a id="2446" href="Relation.Binary.Core.html#Decidable" class="Function">Decidable</a> <a id="2456" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="2460" class="Symbol">→</a> <a id="2462" href="Relation.Binary.Core.html#Decidable" class="Function">Decidable</a> <a id="2472" href="Relation.Binary.NonStrictToStrict.html#507" class="Bound Operator">_≤_</a> <a id="2476" class="Symbol">→</a> <a id="2478" href="Relation.Binary.Core.html#Decidable" class="Function">Decidable</a> <a id="2488" href="Relation.Binary.NonStrictToStrict.html#_%3C_" class="Function Operator">_<_</a>
<a id="2492" href="Relation.Binary.NonStrictToStrict.html#decidable" class="Function">decidable</a> <a id="2502" href="Relation.Binary.NonStrictToStrict.html#2502" class="Bound">≈-dec</a> <a id="2508" href="Relation.Binary.NonStrictToStrict.html#2508" class="Bound">≤-dec</a> <a id="2514" href="Relation.Binary.NonStrictToStrict.html#2514" class="Bound">x</a> <a id="2516" href="Relation.Binary.NonStrictToStrict.html#2516" class="Bound">y</a> <a id="2518" class="Keyword">with</a> <a id="2523" href="Relation.Binary.NonStrictToStrict.html#2502" class="Bound">≈-dec</a> <a id="2529" href="Relation.Binary.NonStrictToStrict.html#2514" class="Bound">x</a> <a id="2531" href="Relation.Binary.NonStrictToStrict.html#2516" class="Bound">y</a> <a id="2533" class="Symbol">|</a> <a id="2535" href="Relation.Binary.NonStrictToStrict.html#2508" class="Bound">≤-dec</a> <a id="2541" href="Relation.Binary.NonStrictToStrict.html#2514" class="Bound">x</a> <a id="2543" href="Relation.Binary.NonStrictToStrict.html#2516" class="Bound">y</a>
<a id="2545" class="Symbol">...</a> <a id="2549" class="Symbol">|</a> <a id="2551" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2555" href="Relation.Binary.NonStrictToStrict.html#2555" class="Bound">x≈y</a> <a id="2559" class="Symbol">|</a> <a id="2561" class="Symbol">_</a> <a id="2569" class="Symbol">=</a> <a id="2571" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2574" class="Symbol">(</a><a id="2575" href="Function.html#flip" class="Function">flip</a> <a id="2580" href="Data.Product.html#%CE%A3.proj%E2%82%82" class="Field">proj₂</a> <a id="2586" href="Relation.Binary.NonStrictToStrict.html#2555" class="Bound">x≈y</a><a id="2589" class="Symbol">)</a>
<a id="2591" class="Symbol">...</a> <a id="2595" class="Symbol">|</a> <a id="2597" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2601" href="Relation.Binary.NonStrictToStrict.html#2601" class="Bound">x≉y</a> <a id="2605" class="Symbol">|</a> <a id="2607" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2611" href="Relation.Binary.NonStrictToStrict.html#2611" class="Bound">x≤y</a> <a id="2615" class="Symbol">=</a> <a id="2617" href="Relation.Nullary.html#Dec.yes" class="InductiveConstructor">yes</a> <a id="2621" class="Symbol">(</a><a id="2622" href="Relation.Binary.NonStrictToStrict.html#2611" class="Bound">x≤y</a> <a id="2626" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="2628" href="Relation.Binary.NonStrictToStrict.html#2601" class="Bound">x≉y</a><a id="2631" class="Symbol">)</a>
<a id="2633" class="Symbol">...</a> <a id="2637" class="Symbol">|</a> <a id="2639" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2643" href="Relation.Binary.NonStrictToStrict.html#2643" class="Bound">x≉y</a> <a id="2647" class="Symbol">|</a> <a id="2649" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2653" href="Relation.Binary.NonStrictToStrict.html#2653" class="Bound">x≰y</a> <a id="2657" class="Symbol">=</a> <a id="2659" href="Relation.Nullary.html#Dec.no" class="InductiveConstructor">no</a> <a id="2662" class="Symbol">(</a><a id="2663" href="Relation.Binary.NonStrictToStrict.html#2653" class="Bound">x≰y</a> <a id="2667" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="2669" href="Data.Product.html#%CE%A3.proj%E2%82%81" class="Field">proj₁</a><a id="2674" class="Symbol">)</a>
<a id="isPartialOrder⟶isStrictPartialOrder" href="Relation.Binary.NonStrictToStrict.html#isPartialOrder%E2%9F%B6isStrictPartialOrder" class="Function">isPartialOrder⟶isStrictPartialOrder</a> <a id="2713" class="Symbol">:</a>
<a id="2717" href="Relation.Binary.html#IsPartialOrder" class="Record">IsPartialOrder</a> <a id="2732" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="2736" href="Relation.Binary.NonStrictToStrict.html#507" class="Bound Operator">_≤_</a> <a id="2740" class="Symbol">→</a> <a id="2742" href="Relation.Binary.html#IsStrictPartialOrder" class="Record">IsStrictPartialOrder</a> <a id="2763" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="2767" href="Relation.Binary.NonStrictToStrict.html#_%3C_" class="Function Operator">_<_</a>
<a id="2771" href="Relation.Binary.NonStrictToStrict.html#isPartialOrder%E2%9F%B6isStrictPartialOrder" class="Function">isPartialOrder⟶isStrictPartialOrder</a> <a id="2807" href="Relation.Binary.NonStrictToStrict.html#2807" class="Bound">po</a> <a id="2810" class="Symbol">=</a> <a id="2812" class="Keyword">record</a>
<a id="2821" class="Symbol">{</a> <a id="2823" class="Field">isEquivalence</a> <a id="2837" class="Symbol">=</a> <a id="2839" href="Relation.Binary.html#1054" class="Function">PO.isEquivalence</a>
<a id="2858" class="Symbol">;</a> <a id="2860" class="Field">irrefl</a> <a id="2874" class="Symbol">=</a> <a id="2876" href="Relation.Binary.NonStrictToStrict.html#irrefl" class="Function">irrefl</a>
<a id="2885" class="Symbol">;</a> <a id="2887" class="Field">trans</a> <a id="2901" class="Symbol">=</a> <a id="2903" href="Relation.Binary.NonStrictToStrict.html#trans" class="Function">trans</a> <a id="2909" href="Relation.Binary.NonStrictToStrict.html#2807" class="Bound">po</a>
<a id="2914" class="Symbol">;</a> <a id="2916" class="Field"><-resp-≈</a> <a id="2930" class="Symbol">=</a> <a id="2932" href="Relation.Binary.NonStrictToStrict.html#%3C-resp-%E2%89%88" class="Function"><-resp-≈</a> <a id="2941" href="Relation.Binary.html#1054" class="Function">PO.isEquivalence</a> <a id="2958" href="Relation.Binary.html#1318" class="Function">PO.≤-resp-≈</a>
<a id="2972" class="Symbol">}</a> <a id="2974" class="Keyword">where</a> <a id="2980" class="Keyword">module</a> <a id="PO" href="Relation.Binary.NonStrictToStrict.html#PO" class="Module">PO</a> <a id="2990" class="Symbol">=</a> <a id="2992" href="Relation.Binary.html#IsPartialOrder" class="Module">IsPartialOrder</a> <a id="3007" href="Relation.Binary.NonStrictToStrict.html#2807" class="Bound">po</a>
<a id="isTotalOrder⟶isStrictTotalOrder" href="Relation.Binary.NonStrictToStrict.html#isTotalOrder%E2%9F%B6isStrictTotalOrder" class="Function">isTotalOrder⟶isStrictTotalOrder</a> <a id="3043" class="Symbol">:</a>
<a id="3047" href="Relation.Binary.Core.html#Decidable" class="Function">Decidable</a> <a id="3057" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="3061" class="Symbol">→</a> <a id="3063" href="Relation.Binary.html#IsTotalOrder" class="Record">IsTotalOrder</a> <a id="3076" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="3080" href="Relation.Binary.NonStrictToStrict.html#507" class="Bound Operator">_≤_</a> <a id="3084" class="Symbol">→</a> <a id="3086" href="Relation.Binary.html#IsStrictTotalOrder" class="Record">IsStrictTotalOrder</a> <a id="3105" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="3109" href="Relation.Binary.NonStrictToStrict.html#_%3C_" class="Function Operator">_<_</a>
<a id="3113" href="Relation.Binary.NonStrictToStrict.html#isTotalOrder%E2%9F%B6isStrictTotalOrder" class="Function">isTotalOrder⟶isStrictTotalOrder</a> <a id="3145" href="Relation.Binary.NonStrictToStrict.html#3145" class="Bound">dec-≈</a> <a id="3151" href="Relation.Binary.NonStrictToStrict.html#3151" class="Bound">tot</a> <a id="3155" class="Symbol">=</a> <a id="3157" class="Keyword">record</a>
<a id="3166" class="Symbol">{</a> <a id="3168" class="Field">isEquivalence</a> <a id="3182" class="Symbol">=</a> <a id="3184" href="Relation.Binary.html#1054" class="Function">TO.isEquivalence</a>
<a id="3203" class="Symbol">;</a> <a id="3205" class="Field">trans</a> <a id="3219" class="Symbol">=</a> <a id="3221" href="Relation.Binary.NonStrictToStrict.html#trans" class="Function">trans</a> <a id="3227" href="Relation.Binary.html#8023" class="Field">TO.isPartialOrder</a>
<a id="3247" class="Symbol">;</a> <a id="3249" class="Field">compare</a> <a id="3263" class="Symbol">=</a> <a id="3265" href="Relation.Binary.NonStrictToStrict.html#trichotomous" class="Function">trichotomous</a> <a id="3278" href="Relation.Binary.Core.html#4960" class="Function">TO.Eq.sym</a> <a id="3288" href="Relation.Binary.NonStrictToStrict.html#3145" class="Bound">dec-≈</a> <a id="3294" href="Relation.Binary.html#3608" class="Function">TO.antisym</a> <a id="3305" href="Relation.Binary.html#8067" class="Field">TO.total</a>
<a id="3316" class="Symbol">}</a> <a id="3318" class="Keyword">where</a> <a id="3324" class="Keyword">module</a> <a id="TO" href="Relation.Binary.NonStrictToStrict.html#TO" class="Module">TO</a> <a id="3334" class="Symbol">=</a> <a id="3336" href="Relation.Binary.html#IsTotalOrder" class="Module">IsTotalOrder</a> <a id="3349" href="Relation.Binary.NonStrictToStrict.html#3151" class="Bound">tot</a>
<a id="isDecTotalOrder⟶isStrictTotalOrder" href="Relation.Binary.NonStrictToStrict.html#isDecTotalOrder%E2%9F%B6isStrictTotalOrder" class="Function">isDecTotalOrder⟶isStrictTotalOrder</a> <a id="3389" class="Symbol">:</a>
<a id="3393" href="Relation.Binary.html#IsDecTotalOrder" class="Record">IsDecTotalOrder</a> <a id="3409" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="3413" href="Relation.Binary.NonStrictToStrict.html#507" class="Bound Operator">_≤_</a> <a id="3417" class="Symbol">→</a> <a id="3419" href="Relation.Binary.html#IsStrictTotalOrder" class="Record">IsStrictTotalOrder</a> <a id="3438" href="Relation.Binary.NonStrictToStrict.html#490" class="Bound Operator">_≈_</a> <a id="3442" href="Relation.Binary.NonStrictToStrict.html#_%3C_" class="Function Operator">_<_</a>
<a id="3446" href="Relation.Binary.NonStrictToStrict.html#isDecTotalOrder%E2%9F%B6isStrictTotalOrder" class="Function">isDecTotalOrder⟶isStrictTotalOrder</a> <a id="3481" href="Relation.Binary.NonStrictToStrict.html#3481" class="Bound">dtot</a> <a id="3486" class="Symbol">=</a>
<a id="3490" href="Relation.Binary.NonStrictToStrict.html#isTotalOrder%E2%9F%B6isStrictTotalOrder" class="Function">isTotalOrder⟶isStrictTotalOrder</a> <a id="3522" href="Relation.Binary.html#8843" class="Field Operator">DTO._≟_</a> <a id="3530" href="Relation.Binary.html#8803" class="Field">DTO.isTotalOrder</a>
<a id="3549" class="Keyword">where</a> <a id="3555" class="Keyword">module</a> <a id="DTO" href="Relation.Binary.NonStrictToStrict.html#DTO" class="Module">DTO</a> <a id="3566" class="Symbol">=</a> <a id="3568" href="Relation.Binary.html#IsDecTotalOrder" class="Module">IsDecTotalOrder</a> <a id="3584" href="Relation.Binary.NonStrictToStrict.html#3481" class="Bound">dtot</a>
</pre></body></html>
|