/usr/share/doc/agda-stdlib-doc/html/Relation.Binary.On.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 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 | <!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Relation.Binary.On</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">-- Many properties which hold for _∼_ also hold for _∼_ on f</a>
<a id="167" class="Comment">------------------------------------------------------------------------</a>
<a id="241" class="Keyword">open</a> <a id="246" class="Keyword">import</a> <a id="253" href="Relation.Binary.html" class="Module">Relation.Binary</a>
<a id="270" class="Keyword">module</a> <a id="277" href="Relation.Binary.On.html" class="Module">Relation.Binary.On</a> <a id="296" class="Keyword">where</a>
<a id="303" class="Keyword">open</a> <a id="308" class="Keyword">import</a> <a id="315" href="Function.html" class="Module">Function</a>
<a id="324" class="Keyword">open</a> <a id="329" class="Keyword">import</a> <a id="336" href="Data.Product.html" class="Module">Data.Product</a>
<a id="350" class="Keyword">module</a> <a id="357" href="Relation.Binary.On.html#357" class="Module">_</a> <a id="359" class="Symbol">{</a><a id="360" href="Relation.Binary.On.html#360" class="Bound">a</a> <a id="362" href="Relation.Binary.On.html#362" class="Bound">b</a><a id="363" class="Symbol">}</a> <a id="365" class="Symbol">{</a><a id="366" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="368" class="Symbol">:</a> <a id="370" class="PrimitiveType">Set</a> <a id="374" href="Relation.Binary.On.html#360" class="Bound">a</a><a id="375" class="Symbol">}</a> <a id="377" class="Symbol">{</a><a id="378" href="Relation.Binary.On.html#378" class="Bound">B</a> <a id="380" class="Symbol">:</a> <a id="382" class="PrimitiveType">Set</a> <a id="386" href="Relation.Binary.On.html#362" class="Bound">b</a><a id="387" class="Symbol">}</a> <a id="389" class="Symbol">(</a><a id="390" href="Relation.Binary.On.html#390" class="Bound">f</a> <a id="392" class="Symbol">:</a> <a id="394" href="Relation.Binary.On.html#378" class="Bound">B</a> <a id="396" class="Symbol">→</a> <a id="398" href="Relation.Binary.On.html#366" class="Bound">A</a><a id="399" class="Symbol">)</a> <a id="401" class="Keyword">where</a>
<a id="410" href="Relation.Binary.On.html#410" class="Function">implies</a> <a id="418" class="Symbol">:</a> <a id="420" class="Symbol">∀</a> <a id="422" class="Symbol">{</a><a id="423" href="Relation.Binary.On.html#423" class="Bound">ℓ₁</a> <a id="426" href="Relation.Binary.On.html#426" class="Bound">ℓ₂</a><a id="428" class="Symbol">}</a> <a id="430" class="Symbol">(</a><a id="431" href="Relation.Binary.On.html#431" class="Bound">≈</a> <a id="433" class="Symbol">:</a> <a id="435" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="439" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="441" href="Relation.Binary.On.html#423" class="Bound">ℓ₁</a><a id="443" class="Symbol">)</a> <a id="445" class="Symbol">(</a><a id="446" href="Relation.Binary.On.html#446" class="Bound">∼</a> <a id="448" class="Symbol">:</a> <a id="450" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="454" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="456" href="Relation.Binary.On.html#426" class="Bound">ℓ₂</a><a id="458" class="Symbol">)</a> <a id="460" class="Symbol">→</a>
<a id="474" href="Relation.Binary.On.html#431" class="Bound">≈</a> <a id="476" href="Relation.Binary.Core.html#_%E2%87%92_" class="Function Operator">⇒</a> <a id="478" href="Relation.Binary.On.html#446" class="Bound">∼</a> <a id="480" class="Symbol">→</a> <a id="482" class="Symbol">(</a><a id="483" href="Relation.Binary.On.html#431" class="Bound">≈</a> <a id="485" href="Function.html#_on_" class="Function Operator">on</a> <a id="488" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="489" class="Symbol">)</a> <a id="491" href="Relation.Binary.Core.html#_%E2%87%92_" class="Function Operator">⇒</a> <a id="493" class="Symbol">(</a><a id="494" href="Relation.Binary.On.html#446" class="Bound">∼</a> <a id="496" href="Function.html#_on_" class="Function Operator">on</a> <a id="499" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="500" class="Symbol">)</a>
<a id="504" href="Relation.Binary.On.html#410" class="Function">implies</a> <a id="512" class="Symbol">_</a> <a id="514" class="Symbol">_</a> <a id="516" href="Relation.Binary.On.html#516" class="Bound">impl</a> <a id="521" class="Symbol">=</a> <a id="523" href="Relation.Binary.On.html#516" class="Bound">impl</a>
<a id="531" href="Relation.Binary.On.html#531" class="Function">reflexive</a> <a id="541" class="Symbol">:</a> <a id="543" class="Symbol">∀</a> <a id="545" class="Symbol">{</a><a id="546" href="Relation.Binary.On.html#546" class="Bound">ℓ</a><a id="547" class="Symbol">}</a> <a id="549" class="Symbol">(</a><a id="550" href="Relation.Binary.On.html#550" class="Bound">∼</a> <a id="552" class="Symbol">:</a> <a id="554" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="558" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="560" href="Relation.Binary.On.html#546" class="Bound">ℓ</a><a id="561" class="Symbol">)</a> <a id="563" class="Symbol">→</a> <a id="565" href="Relation.Binary.Core.html#Reflexive" class="Function">Reflexive</a> <a id="575" href="Relation.Binary.On.html#550" class="Bound">∼</a> <a id="577" class="Symbol">→</a> <a id="579" href="Relation.Binary.Core.html#Reflexive" class="Function">Reflexive</a> <a id="589" class="Symbol">(</a><a id="590" href="Relation.Binary.On.html#550" class="Bound">∼</a> <a id="592" href="Function.html#_on_" class="Function Operator">on</a> <a id="595" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="596" class="Symbol">)</a>
<a id="600" href="Relation.Binary.On.html#531" class="Function">reflexive</a> <a id="610" class="Symbol">_</a> <a id="612" href="Relation.Binary.On.html#612" class="Bound">refl</a> <a id="617" class="Symbol">=</a> <a id="619" href="Relation.Binary.On.html#612" class="Bound">refl</a>
<a id="627" href="Relation.Binary.On.html#627" class="Function">irreflexive</a> <a id="639" class="Symbol">:</a> <a id="641" class="Symbol">∀</a> <a id="643" class="Symbol">{</a><a id="644" href="Relation.Binary.On.html#644" class="Bound">ℓ₁</a> <a id="647" href="Relation.Binary.On.html#647" class="Bound">ℓ₂</a><a id="649" class="Symbol">}</a> <a id="651" class="Symbol">(</a><a id="652" href="Relation.Binary.On.html#652" class="Bound">≈</a> <a id="654" class="Symbol">:</a> <a id="656" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="660" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="662" href="Relation.Binary.On.html#644" class="Bound">ℓ₁</a><a id="664" class="Symbol">)</a> <a id="666" class="Symbol">(</a><a id="667" href="Relation.Binary.On.html#667" class="Bound">∼</a> <a id="669" class="Symbol">:</a> <a id="671" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="675" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="677" href="Relation.Binary.On.html#647" class="Bound">ℓ₂</a><a id="679" class="Symbol">)</a> <a id="681" class="Symbol">→</a>
<a id="699" href="Relation.Binary.Core.html#Irreflexive" class="Function">Irreflexive</a> <a id="711" href="Relation.Binary.On.html#652" class="Bound">≈</a> <a id="713" href="Relation.Binary.On.html#667" class="Bound">∼</a> <a id="715" class="Symbol">→</a> <a id="717" href="Relation.Binary.Core.html#Irreflexive" class="Function">Irreflexive</a> <a id="729" class="Symbol">(</a><a id="730" href="Relation.Binary.On.html#652" class="Bound">≈</a> <a id="732" href="Function.html#_on_" class="Function Operator">on</a> <a id="735" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="736" class="Symbol">)</a> <a id="738" class="Symbol">(</a><a id="739" href="Relation.Binary.On.html#667" class="Bound">∼</a> <a id="741" href="Function.html#_on_" class="Function Operator">on</a> <a id="744" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="745" class="Symbol">)</a>
<a id="749" href="Relation.Binary.On.html#627" class="Function">irreflexive</a> <a id="761" class="Symbol">_</a> <a id="763" class="Symbol">_</a> <a id="765" href="Relation.Binary.On.html#765" class="Bound">irrefl</a> <a id="772" class="Symbol">=</a> <a id="774" href="Relation.Binary.On.html#765" class="Bound">irrefl</a>
<a id="784" href="Relation.Binary.On.html#784" class="Function">symmetric</a> <a id="794" class="Symbol">:</a> <a id="796" class="Symbol">∀</a> <a id="798" class="Symbol">{</a><a id="799" href="Relation.Binary.On.html#799" class="Bound">ℓ</a><a id="800" class="Symbol">}</a> <a id="802" class="Symbol">(</a><a id="803" href="Relation.Binary.On.html#803" class="Bound">∼</a> <a id="805" class="Symbol">:</a> <a id="807" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="811" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="813" href="Relation.Binary.On.html#799" class="Bound">ℓ</a><a id="814" class="Symbol">)</a> <a id="816" class="Symbol">→</a> <a id="818" href="Relation.Binary.Core.html#Symmetric" class="Function">Symmetric</a> <a id="828" href="Relation.Binary.On.html#803" class="Bound">∼</a> <a id="830" class="Symbol">→</a> <a id="832" href="Relation.Binary.Core.html#Symmetric" class="Function">Symmetric</a> <a id="842" class="Symbol">(</a><a id="843" href="Relation.Binary.On.html#803" class="Bound">∼</a> <a id="845" href="Function.html#_on_" class="Function Operator">on</a> <a id="848" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="849" class="Symbol">)</a>
<a id="853" href="Relation.Binary.On.html#784" class="Function">symmetric</a> <a id="863" class="Symbol">_</a> <a id="865" href="Relation.Binary.On.html#865" class="Bound">sym</a> <a id="869" class="Symbol">=</a> <a id="871" href="Relation.Binary.On.html#865" class="Bound">sym</a>
<a id="878" href="Relation.Binary.On.html#878" class="Function">transitive</a> <a id="889" class="Symbol">:</a> <a id="891" class="Symbol">∀</a> <a id="893" class="Symbol">{</a><a id="894" href="Relation.Binary.On.html#894" class="Bound">ℓ</a><a id="895" class="Symbol">}</a> <a id="897" class="Symbol">(</a><a id="898" href="Relation.Binary.On.html#898" class="Bound">∼</a> <a id="900" class="Symbol">:</a> <a id="902" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="906" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="908" href="Relation.Binary.On.html#894" class="Bound">ℓ</a><a id="909" class="Symbol">)</a> <a id="911" class="Symbol">→</a> <a id="913" href="Relation.Binary.Core.html#Transitive" class="Function">Transitive</a> <a id="924" href="Relation.Binary.On.html#898" class="Bound">∼</a> <a id="926" class="Symbol">→</a> <a id="928" href="Relation.Binary.Core.html#Transitive" class="Function">Transitive</a> <a id="939" class="Symbol">(</a><a id="940" href="Relation.Binary.On.html#898" class="Bound">∼</a> <a id="942" href="Function.html#_on_" class="Function Operator">on</a> <a id="945" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="946" class="Symbol">)</a>
<a id="950" href="Relation.Binary.On.html#878" class="Function">transitive</a> <a id="961" class="Symbol">_</a> <a id="963" href="Relation.Binary.On.html#963" class="Bound">trans</a> <a id="969" class="Symbol">=</a> <a id="971" href="Relation.Binary.On.html#963" class="Bound">trans</a>
<a id="980" href="Relation.Binary.On.html#980" class="Function">antisymmetric</a> <a id="994" class="Symbol">:</a> <a id="996" class="Symbol">∀</a> <a id="998" class="Symbol">{</a><a id="999" href="Relation.Binary.On.html#999" class="Bound">ℓ₁</a> <a id="1002" href="Relation.Binary.On.html#1002" class="Bound">ℓ₂</a><a id="1004" class="Symbol">}</a> <a id="1006" class="Symbol">(</a><a id="1007" href="Relation.Binary.On.html#1007" class="Bound">≈</a> <a id="1009" class="Symbol">:</a> <a id="1011" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1015" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="1017" href="Relation.Binary.On.html#999" class="Bound">ℓ₁</a><a id="1019" class="Symbol">)</a> <a id="1021" class="Symbol">(</a><a id="1022" href="Relation.Binary.On.html#1022" class="Bound">≤</a> <a id="1024" class="Symbol">:</a> <a id="1026" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1030" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="1032" href="Relation.Binary.On.html#1002" class="Bound">ℓ₂</a><a id="1034" class="Symbol">)</a> <a id="1036" class="Symbol">→</a>
<a id="1056" href="Relation.Binary.Core.html#Antisymmetric" class="Function">Antisymmetric</a> <a id="1070" href="Relation.Binary.On.html#1007" class="Bound">≈</a> <a id="1072" href="Relation.Binary.On.html#1022" class="Bound">≤</a> <a id="1074" class="Symbol">→</a> <a id="1076" href="Relation.Binary.Core.html#Antisymmetric" class="Function">Antisymmetric</a> <a id="1090" class="Symbol">(</a><a id="1091" href="Relation.Binary.On.html#1007" class="Bound">≈</a> <a id="1093" href="Function.html#_on_" class="Function Operator">on</a> <a id="1096" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="1097" class="Symbol">)</a> <a id="1099" class="Symbol">(</a><a id="1100" href="Relation.Binary.On.html#1022" class="Bound">≤</a> <a id="1102" href="Function.html#_on_" class="Function Operator">on</a> <a id="1105" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="1106" class="Symbol">)</a>
<a id="1110" href="Relation.Binary.On.html#980" class="Function">antisymmetric</a> <a id="1124" class="Symbol">_</a> <a id="1126" class="Symbol">_</a> <a id="1128" href="Relation.Binary.On.html#1128" class="Bound">antisym</a> <a id="1136" class="Symbol">=</a> <a id="1138" href="Relation.Binary.On.html#1128" class="Bound">antisym</a>
<a id="1149" href="Relation.Binary.On.html#1149" class="Function">asymmetric</a> <a id="1160" class="Symbol">:</a> <a id="1162" class="Symbol">∀</a> <a id="1164" class="Symbol">{</a><a id="1165" href="Relation.Binary.On.html#1165" class="Bound">ℓ</a><a id="1166" class="Symbol">}</a> <a id="1168" class="Symbol">(</a><a id="1169" href="Relation.Binary.On.html#1169" class="Bound"><</a> <a id="1171" class="Symbol">:</a> <a id="1173" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1177" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="1179" href="Relation.Binary.On.html#1165" class="Bound">ℓ</a><a id="1180" class="Symbol">)</a> <a id="1182" class="Symbol">→</a> <a id="1184" href="Relation.Binary.Core.html#Asymmetric" class="Function">Asymmetric</a> <a id="1195" href="Relation.Binary.On.html#1169" class="Bound"><</a> <a id="1197" class="Symbol">→</a> <a id="1199" href="Relation.Binary.Core.html#Asymmetric" class="Function">Asymmetric</a> <a id="1210" class="Symbol">(</a><a id="1211" href="Relation.Binary.On.html#1169" class="Bound"><</a> <a id="1213" href="Function.html#_on_" class="Function Operator">on</a> <a id="1216" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="1217" class="Symbol">)</a>
<a id="1221" href="Relation.Binary.On.html#1149" class="Function">asymmetric</a> <a id="1232" class="Symbol">_</a> <a id="1234" href="Relation.Binary.On.html#1234" class="Bound">asym</a> <a id="1239" class="Symbol">=</a> <a id="1241" href="Relation.Binary.On.html#1234" class="Bound">asym</a>
<a id="1249" href="Relation.Binary.On.html#1249" class="Function">respects</a> <a id="1258" class="Symbol">:</a> <a id="1260" class="Symbol">∀</a> <a id="1262" class="Symbol">{</a><a id="1263" href="Relation.Binary.On.html#1263" class="Bound">ℓ</a> <a id="1265" href="Relation.Binary.On.html#1265" class="Bound">p</a><a id="1266" class="Symbol">}</a> <a id="1268" class="Symbol">(</a><a id="1269" href="Relation.Binary.On.html#1269" class="Bound">∼</a> <a id="1271" class="Symbol">:</a> <a id="1273" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1277" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="1279" href="Relation.Binary.On.html#1263" class="Bound">ℓ</a><a id="1280" class="Symbol">)</a> <a id="1282" class="Symbol">(</a><a id="1283" href="Relation.Binary.On.html#1283" class="Bound">P</a> <a id="1285" class="Symbol">:</a> <a id="1287" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="1289" class="Symbol">→</a> <a id="1291" class="PrimitiveType">Set</a> <a id="1295" href="Relation.Binary.On.html#1265" class="Bound">p</a><a id="1296" class="Symbol">)</a> <a id="1298" class="Symbol">→</a>
<a id="1313" href="Relation.Binary.On.html#1283" class="Bound">P</a> <a id="1315" href="Relation.Binary.Core.html#_Respects_" class="Function Operator">Respects</a> <a id="1324" href="Relation.Binary.On.html#1269" class="Bound">∼</a> <a id="1326" class="Symbol">→</a> <a id="1328" class="Symbol">(</a><a id="1329" href="Relation.Binary.On.html#1283" class="Bound">P</a> <a id="1331" href="Function.html#_%E2%88%98_" class="Function Operator">∘</a> <a id="1333" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="1334" class="Symbol">)</a> <a id="1336" href="Relation.Binary.Core.html#_Respects_" class="Function Operator">Respects</a> <a id="1345" class="Symbol">(</a><a id="1346" href="Relation.Binary.On.html#1269" class="Bound">∼</a> <a id="1348" href="Function.html#_on_" class="Function Operator">on</a> <a id="1351" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="1352" class="Symbol">)</a>
<a id="1356" href="Relation.Binary.On.html#1249" class="Function">respects</a> <a id="1365" class="Symbol">_</a> <a id="1367" class="Symbol">_</a> <a id="1369" href="Relation.Binary.On.html#1369" class="Bound">resp</a> <a id="1374" class="Symbol">=</a> <a id="1376" href="Relation.Binary.On.html#1369" class="Bound">resp</a>
<a id="1384" href="Relation.Binary.On.html#1384" class="Function">respects₂</a> <a id="1394" class="Symbol">:</a> <a id="1396" class="Symbol">∀</a> <a id="1398" class="Symbol">{</a><a id="1399" href="Relation.Binary.On.html#1399" class="Bound">ℓ₁</a> <a id="1402" href="Relation.Binary.On.html#1402" class="Bound">ℓ₂</a><a id="1404" class="Symbol">}</a> <a id="1406" class="Symbol">(</a><a id="1407" href="Relation.Binary.On.html#1407" class="Bound">∼₁</a> <a id="1410" class="Symbol">:</a> <a id="1412" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1416" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="1418" href="Relation.Binary.On.html#1399" class="Bound">ℓ₁</a><a id="1420" class="Symbol">)</a> <a id="1422" class="Symbol">(</a><a id="1423" href="Relation.Binary.On.html#1423" class="Bound">∼₂</a> <a id="1426" class="Symbol">:</a> <a id="1428" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1432" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="1434" href="Relation.Binary.On.html#1402" class="Bound">ℓ₂</a><a id="1436" class="Symbol">)</a> <a id="1438" class="Symbol">→</a>
<a id="1454" href="Relation.Binary.On.html#1407" class="Bound">∼₁</a> <a id="1457" href="Relation.Binary.Core.html#_Respects%E2%82%82_" class="Function Operator">Respects₂</a> <a id="1467" href="Relation.Binary.On.html#1423" class="Bound">∼₂</a> <a id="1470" class="Symbol">→</a> <a id="1472" class="Symbol">(</a><a id="1473" href="Relation.Binary.On.html#1407" class="Bound">∼₁</a> <a id="1476" href="Function.html#_on_" class="Function Operator">on</a> <a id="1479" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="1480" class="Symbol">)</a> <a id="1482" href="Relation.Binary.Core.html#_Respects%E2%82%82_" class="Function Operator">Respects₂</a> <a id="1492" class="Symbol">(</a><a id="1493" href="Relation.Binary.On.html#1423" class="Bound">∼₂</a> <a id="1496" href="Function.html#_on_" class="Function Operator">on</a> <a id="1499" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="1500" class="Symbol">)</a>
<a id="1504" href="Relation.Binary.On.html#1384" class="Function">respects₂</a> <a id="1514" class="Symbol">_</a> <a id="1516" class="Symbol">_</a> <a id="1518" class="Symbol">(</a><a id="1519" href="Relation.Binary.On.html#1519" class="Bound">resp₁</a> <a id="1525" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1527" href="Relation.Binary.On.html#1527" class="Bound">resp₂</a><a id="1532" class="Symbol">)</a> <a id="1534" class="Symbol">=</a>
<a id="1540" class="Symbol">((λ</a> <a id="1544" class="Symbol">{</a><a id="1545" href="Relation.Binary.On.html#1545" class="Bound">_</a><a id="1546" class="Symbol">}</a> <a id="1548" class="Symbol">{</a><a id="1549" href="Relation.Binary.On.html#1549" class="Bound">_</a><a id="1550" class="Symbol">}</a> <a id="1552" class="Symbol">{</a><a id="1553" href="Relation.Binary.On.html#1553" class="Bound">_</a><a id="1554" class="Symbol">}</a> <a id="1556" class="Symbol">→</a> <a id="1558" href="Relation.Binary.On.html#1519" class="Bound">resp₁</a><a id="1563" class="Symbol">)</a> <a id="1565" href="Data.Product.html#%CE%A3._%2C_" class="InductiveConstructor Operator">,</a> <a id="1567" class="Symbol">λ</a> <a id="1569" class="Symbol">{</a><a id="1570" href="Relation.Binary.On.html#1570" class="Bound">_</a><a id="1571" class="Symbol">}</a> <a id="1573" class="Symbol">{</a><a id="1574" href="Relation.Binary.On.html#1574" class="Bound">_</a><a id="1575" class="Symbol">}</a> <a id="1577" class="Symbol">{</a><a id="1578" href="Relation.Binary.On.html#1578" class="Bound">_</a><a id="1579" class="Symbol">}</a> <a id="1581" class="Symbol">→</a> <a id="1583" href="Relation.Binary.On.html#1527" class="Bound">resp₂</a><a id="1588" class="Symbol">)</a>
<a id="1593" href="Relation.Binary.On.html#1593" class="Function">decidable</a> <a id="1603" class="Symbol">:</a> <a id="1605" class="Symbol">∀</a> <a id="1607" class="Symbol">{</a><a id="1608" href="Relation.Binary.On.html#1608" class="Bound">ℓ</a><a id="1609" class="Symbol">}</a> <a id="1611" class="Symbol">(</a><a id="1612" href="Relation.Binary.On.html#1612" class="Bound">∼</a> <a id="1614" class="Symbol">:</a> <a id="1616" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1620" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="1622" href="Relation.Binary.On.html#1608" class="Bound">ℓ</a><a id="1623" class="Symbol">)</a> <a id="1625" class="Symbol">→</a> <a id="1627" href="Relation.Binary.Core.html#Decidable" class="Function">Decidable</a> <a id="1637" href="Relation.Binary.On.html#1612" class="Bound">∼</a> <a id="1639" class="Symbol">→</a> <a id="1641" href="Relation.Binary.Core.html#Decidable" class="Function">Decidable</a> <a id="1651" class="Symbol">(</a><a id="1652" href="Relation.Binary.On.html#1612" class="Bound">∼</a> <a id="1654" href="Function.html#_on_" class="Function Operator">on</a> <a id="1657" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="1658" class="Symbol">)</a>
<a id="1662" href="Relation.Binary.On.html#1593" class="Function">decidable</a> <a id="1672" class="Symbol">_</a> <a id="1674" href="Relation.Binary.On.html#1674" class="Bound">dec</a> <a id="1678" class="Symbol">=</a> <a id="1680" class="Symbol">λ</a> <a id="1682" href="Relation.Binary.On.html#1682" class="Bound">x</a> <a id="1684" href="Relation.Binary.On.html#1684" class="Bound">y</a> <a id="1686" class="Symbol">→</a> <a id="1688" href="Relation.Binary.On.html#1674" class="Bound">dec</a> <a id="1692" class="Symbol">(</a><a id="1693" href="Relation.Binary.On.html#390" class="Bound">f</a> <a id="1695" href="Relation.Binary.On.html#1682" class="Bound">x</a><a id="1696" class="Symbol">)</a> <a id="1698" class="Symbol">(</a><a id="1699" href="Relation.Binary.On.html#390" class="Bound">f</a> <a id="1701" href="Relation.Binary.On.html#1684" class="Bound">y</a><a id="1702" class="Symbol">)</a>
<a id="1707" href="Relation.Binary.On.html#1707" class="Function">total</a> <a id="1713" class="Symbol">:</a> <a id="1715" class="Symbol">∀</a> <a id="1717" class="Symbol">{</a><a id="1718" href="Relation.Binary.On.html#1718" class="Bound">ℓ</a><a id="1719" class="Symbol">}</a> <a id="1721" class="Symbol">(</a><a id="1722" href="Relation.Binary.On.html#1722" class="Bound">∼</a> <a id="1724" class="Symbol">:</a> <a id="1726" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1730" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="1732" href="Relation.Binary.On.html#1718" class="Bound">ℓ</a><a id="1733" class="Symbol">)</a> <a id="1735" class="Symbol">→</a> <a id="1737" href="Relation.Binary.Consequences.html#Total" class="Function">Total</a> <a id="1743" href="Relation.Binary.On.html#1722" class="Bound">∼</a> <a id="1745" class="Symbol">→</a> <a id="1747" href="Relation.Binary.Consequences.html#Total" class="Function">Total</a> <a id="1753" class="Symbol">(</a><a id="1754" href="Relation.Binary.On.html#1722" class="Bound">∼</a> <a id="1756" href="Function.html#_on_" class="Function Operator">on</a> <a id="1759" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="1760" class="Symbol">)</a>
<a id="1764" href="Relation.Binary.On.html#1707" class="Function">total</a> <a id="1770" class="Symbol">_</a> <a id="1772" href="Relation.Binary.On.html#1772" class="Bound">tot</a> <a id="1776" class="Symbol">=</a> <a id="1778" class="Symbol">λ</a> <a id="1780" href="Relation.Binary.On.html#1780" class="Bound">x</a> <a id="1782" href="Relation.Binary.On.html#1782" class="Bound">y</a> <a id="1784" class="Symbol">→</a> <a id="1786" href="Relation.Binary.On.html#1772" class="Bound">tot</a> <a id="1790" class="Symbol">(</a><a id="1791" href="Relation.Binary.On.html#390" class="Bound">f</a> <a id="1793" href="Relation.Binary.On.html#1780" class="Bound">x</a><a id="1794" class="Symbol">)</a> <a id="1796" class="Symbol">(</a><a id="1797" href="Relation.Binary.On.html#390" class="Bound">f</a> <a id="1799" href="Relation.Binary.On.html#1782" class="Bound">y</a><a id="1800" class="Symbol">)</a>
<a id="1805" href="Relation.Binary.On.html#1805" class="Function">trichotomous</a> <a id="1818" class="Symbol">:</a> <a id="1820" class="Symbol">∀</a> <a id="1822" class="Symbol">{</a><a id="1823" href="Relation.Binary.On.html#1823" class="Bound">ℓ₁</a> <a id="1826" href="Relation.Binary.On.html#1826" class="Bound">ℓ₂</a><a id="1828" class="Symbol">}</a> <a id="1830" class="Symbol">(</a><a id="1831" href="Relation.Binary.On.html#1831" class="Bound">≈</a> <a id="1833" class="Symbol">:</a> <a id="1835" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1839" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="1841" href="Relation.Binary.On.html#1823" class="Bound">ℓ₁</a><a id="1843" class="Symbol">)</a> <a id="1845" class="Symbol">(</a><a id="1846" href="Relation.Binary.On.html#1846" class="Bound"><</a> <a id="1848" class="Symbol">:</a> <a id="1850" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="1854" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="1856" href="Relation.Binary.On.html#1826" class="Bound">ℓ₂</a><a id="1858" class="Symbol">)</a> <a id="1860" class="Symbol">→</a>
<a id="1879" href="Relation.Binary.Core.html#Trichotomous" class="Function">Trichotomous</a> <a id="1892" href="Relation.Binary.On.html#1831" class="Bound">≈</a> <a id="1894" href="Relation.Binary.On.html#1846" class="Bound"><</a> <a id="1896" class="Symbol">→</a> <a id="1898" href="Relation.Binary.Core.html#Trichotomous" class="Function">Trichotomous</a> <a id="1911" class="Symbol">(</a><a id="1912" href="Relation.Binary.On.html#1831" class="Bound">≈</a> <a id="1914" href="Function.html#_on_" class="Function Operator">on</a> <a id="1917" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="1918" class="Symbol">)</a> <a id="1920" class="Symbol">(</a><a id="1921" href="Relation.Binary.On.html#1846" class="Bound"><</a> <a id="1923" href="Function.html#_on_" class="Function Operator">on</a> <a id="1926" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="1927" class="Symbol">)</a>
<a id="1931" href="Relation.Binary.On.html#1805" class="Function">trichotomous</a> <a id="1944" class="Symbol">_</a> <a id="1946" class="Symbol">_</a> <a id="1948" href="Relation.Binary.On.html#1948" class="Bound">compare</a> <a id="1956" class="Symbol">=</a> <a id="1958" class="Symbol">λ</a> <a id="1960" href="Relation.Binary.On.html#1960" class="Bound">x</a> <a id="1962" href="Relation.Binary.On.html#1962" class="Bound">y</a> <a id="1964" class="Symbol">→</a> <a id="1966" href="Relation.Binary.On.html#1948" class="Bound">compare</a> <a id="1974" class="Symbol">(</a><a id="1975" href="Relation.Binary.On.html#390" class="Bound">f</a> <a id="1977" href="Relation.Binary.On.html#1960" class="Bound">x</a><a id="1978" class="Symbol">)</a> <a id="1980" class="Symbol">(</a><a id="1981" href="Relation.Binary.On.html#390" class="Bound">f</a> <a id="1983" href="Relation.Binary.On.html#1962" class="Bound">y</a><a id="1984" class="Symbol">)</a>
<a id="1989" href="Relation.Binary.On.html#1989" class="Function">isEquivalence</a> <a id="2003" class="Symbol">:</a> <a id="2005" class="Symbol">∀</a> <a id="2007" class="Symbol">{</a><a id="2008" href="Relation.Binary.On.html#2008" class="Bound">ℓ</a><a id="2009" class="Symbol">}</a> <a id="2011" class="Symbol">{</a><a id="2012" href="Relation.Binary.On.html#2012" class="Bound">≈</a> <a id="2014" class="Symbol">:</a> <a id="2016" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="2020" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="2022" href="Relation.Binary.On.html#2008" class="Bound">ℓ</a><a id="2023" class="Symbol">}</a> <a id="2025" class="Symbol">→</a>
<a id="2045" href="Relation.Binary.Core.html#IsEquivalence" class="Record">IsEquivalence</a> <a id="2059" href="Relation.Binary.On.html#2012" class="Bound">≈</a> <a id="2061" class="Symbol">→</a> <a id="2063" href="Relation.Binary.Core.html#IsEquivalence" class="Record">IsEquivalence</a> <a id="2077" class="Symbol">(</a><a id="2078" href="Relation.Binary.On.html#2012" class="Bound">≈</a> <a id="2080" href="Function.html#_on_" class="Function Operator">on</a> <a id="2083" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="2084" class="Symbol">)</a>
<a id="2088" href="Relation.Binary.On.html#1989" class="Function">isEquivalence</a> <a id="2102" class="Symbol">{</a><a id="2103" class="Argument">≈</a> <a id="2105" class="Symbol">=</a> <a id="2107" href="Relation.Binary.On.html#2107" class="Bound">≈</a><a id="2108" class="Symbol">}</a> <a id="2110" href="Relation.Binary.On.html#2110" class="Bound">eq</a> <a id="2113" class="Symbol">=</a> <a id="2115" class="Keyword">record</a>
<a id="2126" class="Symbol">{</a> <a id="2128" class="Field">refl</a> <a id="2134" class="Symbol">=</a> <a id="2136" href="Relation.Binary.On.html#531" class="Function">reflexive</a> <a id="2147" href="Relation.Binary.On.html#2107" class="Bound">≈</a> <a id="2149" href="Relation.Binary.Core.html#4934" class="Field">Eq.refl</a>
<a id="2161" class="Symbol">;</a> <a id="2163" class="Field">sym</a> <a id="2169" class="Symbol">=</a> <a id="2171" href="Relation.Binary.On.html#784" class="Function">symmetric</a> <a id="2182" href="Relation.Binary.On.html#2107" class="Bound">≈</a> <a id="2184" href="Relation.Binary.Core.html#4960" class="Field">Eq.sym</a>
<a id="2195" class="Symbol">;</a> <a id="2197" class="Field">trans</a> <a id="2203" class="Symbol">=</a> <a id="2205" href="Relation.Binary.On.html#878" class="Function">transitive</a> <a id="2216" href="Relation.Binary.On.html#2107" class="Bound">≈</a> <a id="2218" href="Relation.Binary.Core.html#4986" class="Field">Eq.trans</a>
<a id="2231" class="Symbol">}</a>
<a id="2237" class="Keyword">where</a> <a id="2243" class="Keyword">module</a> <a id="Eq" href="Relation.Binary.On.html#Eq" class="Module">Eq</a> <a id="2253" class="Symbol">=</a> <a id="2255" href="Relation.Binary.Core.html#IsEquivalence" class="Module">IsEquivalence</a> <a id="2269" href="Relation.Binary.On.html#2110" class="Bound">eq</a>
<a id="2275" href="Relation.Binary.On.html#2275" class="Function">isPreorder</a> <a id="2286" class="Symbol">:</a> <a id="2288" class="Symbol">∀</a> <a id="2290" class="Symbol">{</a><a id="2291" href="Relation.Binary.On.html#2291" class="Bound">ℓ₁</a> <a id="2294" href="Relation.Binary.On.html#2294" class="Bound">ℓ₂</a><a id="2296" class="Symbol">}</a> <a id="2298" class="Symbol">{</a><a id="2299" href="Relation.Binary.On.html#2299" class="Bound">≈</a> <a id="2301" class="Symbol">:</a> <a id="2303" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="2307" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="2309" href="Relation.Binary.On.html#2291" class="Bound">ℓ₁</a><a id="2311" class="Symbol">}</a> <a id="2313" class="Symbol">{</a><a id="2314" href="Relation.Binary.On.html#2314" class="Bound">∼</a> <a id="2316" class="Symbol">:</a> <a id="2318" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="2322" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="2324" href="Relation.Binary.On.html#2294" class="Bound">ℓ₂</a><a id="2326" class="Symbol">}</a> <a id="2328" class="Symbol">→</a>
<a id="2345" href="Relation.Binary.html#IsPreorder" class="Record">IsPreorder</a> <a id="2356" href="Relation.Binary.On.html#2299" class="Bound">≈</a> <a id="2358" href="Relation.Binary.On.html#2314" class="Bound">∼</a> <a id="2360" class="Symbol">→</a> <a id="2362" href="Relation.Binary.html#IsPreorder" class="Record">IsPreorder</a> <a id="2373" class="Symbol">(</a><a id="2374" href="Relation.Binary.On.html#2299" class="Bound">≈</a> <a id="2376" href="Function.html#_on_" class="Function Operator">on</a> <a id="2379" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="2380" class="Symbol">)</a> <a id="2382" class="Symbol">(</a><a id="2383" href="Relation.Binary.On.html#2314" class="Bound">∼</a> <a id="2385" href="Function.html#_on_" class="Function Operator">on</a> <a id="2388" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="2389" class="Symbol">)</a>
<a id="2393" href="Relation.Binary.On.html#2275" class="Function">isPreorder</a> <a id="2404" class="Symbol">{</a><a id="2405" class="Argument">≈</a> <a id="2407" class="Symbol">=</a> <a id="2409" href="Relation.Binary.On.html#2409" class="Bound">≈</a><a id="2410" class="Symbol">}</a> <a id="2412" class="Symbol">{</a><a id="2413" href="Relation.Binary.On.html#2413" class="Bound">∼</a><a id="2414" class="Symbol">}</a> <a id="2416" href="Relation.Binary.On.html#2416" class="Bound">pre</a> <a id="2420" class="Symbol">=</a> <a id="2422" class="Keyword">record</a>
<a id="2433" class="Symbol">{</a> <a id="2435" class="Field">isEquivalence</a> <a id="2449" class="Symbol">=</a> <a id="2451" href="Relation.Binary.On.html#1989" class="Function">isEquivalence</a> <a id="2465" href="Relation.Binary.html#1054" class="Field">Pre.isEquivalence</a>
<a id="2487" class="Symbol">;</a> <a id="2489" class="Field">reflexive</a> <a id="2503" class="Symbol">=</a> <a id="2505" href="Relation.Binary.On.html#410" class="Function">implies</a> <a id="2513" href="Relation.Binary.On.html#2409" class="Bound">≈</a> <a id="2515" href="Relation.Binary.On.html#2413" class="Bound">∼</a> <a id="2517" href="Relation.Binary.html#1160" class="Field">Pre.reflexive</a>
<a id="2535" class="Symbol">;</a> <a id="2537" class="Field">trans</a> <a id="2551" class="Symbol">=</a> <a id="2553" href="Relation.Binary.On.html#878" class="Function">transitive</a> <a id="2564" href="Relation.Binary.On.html#2413" class="Bound">∼</a> <a id="2566" href="Relation.Binary.html#1190" class="Field">Pre.trans</a>
<a id="2580" class="Symbol">}</a>
<a id="2586" class="Keyword">where</a> <a id="2592" class="Keyword">module</a> <a id="Pre" href="Relation.Binary.On.html#Pre" class="Module">Pre</a> <a id="2603" class="Symbol">=</a> <a id="2605" href="Relation.Binary.html#IsPreorder" class="Module">IsPreorder</a> <a id="2616" href="Relation.Binary.On.html#2416" class="Bound">pre</a>
<a id="2623" href="Relation.Binary.On.html#2623" class="Function">isDecEquivalence</a> <a id="2640" class="Symbol">:</a> <a id="2642" class="Symbol">∀</a> <a id="2644" class="Symbol">{</a><a id="2645" href="Relation.Binary.On.html#2645" class="Bound">ℓ</a><a id="2646" class="Symbol">}</a> <a id="2648" class="Symbol">{</a><a id="2649" href="Relation.Binary.On.html#2649" class="Bound">≈</a> <a id="2651" class="Symbol">:</a> <a id="2653" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="2657" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="2659" href="Relation.Binary.On.html#2645" class="Bound">ℓ</a><a id="2660" class="Symbol">}</a> <a id="2662" class="Symbol">→</a>
<a id="2685" href="Relation.Binary.html#IsDecEquivalence" class="Record">IsDecEquivalence</a> <a id="2702" href="Relation.Binary.On.html#2649" class="Bound">≈</a> <a id="2704" class="Symbol">→</a> <a id="2706" href="Relation.Binary.html#IsDecEquivalence" class="Record">IsDecEquivalence</a> <a id="2723" class="Symbol">(</a><a id="2724" href="Relation.Binary.On.html#2649" class="Bound">≈</a> <a id="2726" href="Function.html#_on_" class="Function Operator">on</a> <a id="2729" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="2730" class="Symbol">)</a>
<a id="2734" href="Relation.Binary.On.html#2623" class="Function">isDecEquivalence</a> <a id="2751" class="Symbol">{</a><a id="2752" class="Argument">≈</a> <a id="2754" class="Symbol">=</a> <a id="2756" href="Relation.Binary.On.html#2756" class="Bound">≈</a><a id="2757" class="Symbol">}</a> <a id="2759" href="Relation.Binary.On.html#2759" class="Bound">dec</a> <a id="2763" class="Symbol">=</a> <a id="2765" class="Keyword">record</a>
<a id="2776" class="Symbol">{</a> <a id="2778" class="Field">isEquivalence</a> <a id="2792" class="Symbol">=</a> <a id="2794" href="Relation.Binary.On.html#1989" class="Function">isEquivalence</a> <a id="2808" href="Relation.Binary.html#2858" class="Field">Dec.isEquivalence</a>
<a id="2830" class="Symbol">;</a> <a id="2832" class="Field Operator">_≟_</a> <a id="2846" class="Symbol">=</a> <a id="2848" href="Relation.Binary.On.html#1593" class="Function">decidable</a> <a id="2858" href="Relation.Binary.On.html#2756" class="Bound">≈</a> <a id="2860" href="Relation.Binary.html#2896" class="Field Operator">Dec._≟_</a>
<a id="2872" class="Symbol">}</a>
<a id="2878" class="Keyword">where</a> <a id="2884" class="Keyword">module</a> <a id="Dec" href="Relation.Binary.On.html#Dec" class="Module">Dec</a> <a id="2895" class="Symbol">=</a> <a id="2897" href="Relation.Binary.html#IsDecEquivalence" class="Module">IsDecEquivalence</a> <a id="2914" href="Relation.Binary.On.html#2759" class="Bound">dec</a>
<a id="2921" href="Relation.Binary.On.html#2921" class="Function">isPartialOrder</a> <a id="2936" class="Symbol">:</a> <a id="2938" class="Symbol">∀</a> <a id="2940" class="Symbol">{</a><a id="2941" href="Relation.Binary.On.html#2941" class="Bound">ℓ₁</a> <a id="2944" href="Relation.Binary.On.html#2944" class="Bound">ℓ₂</a><a id="2946" class="Symbol">}</a> <a id="2948" class="Symbol">{</a><a id="2949" href="Relation.Binary.On.html#2949" class="Bound">≈</a> <a id="2951" class="Symbol">:</a> <a id="2953" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="2957" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="2959" href="Relation.Binary.On.html#2941" class="Bound">ℓ₁</a><a id="2961" class="Symbol">}</a> <a id="2963" class="Symbol">{</a><a id="2964" href="Relation.Binary.On.html#2964" class="Bound">≤</a> <a id="2966" class="Symbol">:</a> <a id="2968" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="2972" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="2974" href="Relation.Binary.On.html#2944" class="Bound">ℓ₂</a><a id="2976" class="Symbol">}</a> <a id="2978" class="Symbol">→</a>
<a id="2999" href="Relation.Binary.html#IsPartialOrder" class="Record">IsPartialOrder</a> <a id="3014" href="Relation.Binary.On.html#2949" class="Bound">≈</a> <a id="3016" href="Relation.Binary.On.html#2964" class="Bound">≤</a> <a id="3018" class="Symbol">→</a>
<a id="3039" href="Relation.Binary.html#IsPartialOrder" class="Record">IsPartialOrder</a> <a id="3054" class="Symbol">(</a><a id="3055" href="Relation.Binary.On.html#2949" class="Bound">≈</a> <a id="3057" href="Function.html#_on_" class="Function Operator">on</a> <a id="3060" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="3061" class="Symbol">)</a> <a id="3063" class="Symbol">(</a><a id="3064" href="Relation.Binary.On.html#2964" class="Bound">≤</a> <a id="3066" href="Function.html#_on_" class="Function Operator">on</a> <a id="3069" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="3070" class="Symbol">)</a>
<a id="3074" href="Relation.Binary.On.html#2921" class="Function">isPartialOrder</a> <a id="3089" class="Symbol">{</a><a id="3090" class="Argument">≈</a> <a id="3092" class="Symbol">=</a> <a id="3094" href="Relation.Binary.On.html#3094" class="Bound">≈</a><a id="3095" class="Symbol">}</a> <a id="3097" class="Symbol">{</a><a id="3098" href="Relation.Binary.On.html#3098" class="Bound">≤</a><a id="3099" class="Symbol">}</a> <a id="3101" href="Relation.Binary.On.html#3101" class="Bound">po</a> <a id="3104" class="Symbol">=</a> <a id="3106" class="Keyword">record</a>
<a id="3117" class="Symbol">{</a> <a id="3119" class="Field">isPreorder</a> <a id="3130" class="Symbol">=</a> <a id="3132" href="Relation.Binary.On.html#2275" class="Function">isPreorder</a> <a id="3143" href="Relation.Binary.html#3572" class="Field">Po.isPreorder</a>
<a id="3161" class="Symbol">;</a> <a id="3163" class="Field">antisym</a> <a id="3174" class="Symbol">=</a> <a id="3176" href="Relation.Binary.On.html#980" class="Function">antisymmetric</a> <a id="3190" href="Relation.Binary.On.html#3094" class="Bound">≈</a> <a id="3192" href="Relation.Binary.On.html#3098" class="Bound">≤</a> <a id="3194" href="Relation.Binary.html#3608" class="Field">Po.antisym</a>
<a id="3209" class="Symbol">}</a>
<a id="3215" class="Keyword">where</a> <a id="3221" class="Keyword">module</a> <a id="Po" href="Relation.Binary.On.html#Po" class="Module">Po</a> <a id="3231" class="Symbol">=</a> <a id="3233" href="Relation.Binary.html#IsPartialOrder" class="Module">IsPartialOrder</a> <a id="3248" href="Relation.Binary.On.html#3101" class="Bound">po</a>
<a id="3254" href="Relation.Binary.On.html#3254" class="Function">isDecPartialOrder</a> <a id="3272" class="Symbol">:</a> <a id="3274" class="Symbol">∀</a> <a id="3276" class="Symbol">{</a><a id="3277" href="Relation.Binary.On.html#3277" class="Bound">ℓ₁</a> <a id="3280" href="Relation.Binary.On.html#3280" class="Bound">ℓ₂</a><a id="3282" class="Symbol">}</a> <a id="3284" class="Symbol">{</a><a id="3285" href="Relation.Binary.On.html#3285" class="Bound">≈</a> <a id="3287" class="Symbol">:</a> <a id="3289" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="3293" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="3295" href="Relation.Binary.On.html#3277" class="Bound">ℓ₁</a><a id="3297" class="Symbol">}</a> <a id="3299" class="Symbol">{</a><a id="3300" href="Relation.Binary.On.html#3300" class="Bound">≤</a> <a id="3302" class="Symbol">:</a> <a id="3304" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="3308" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="3310" href="Relation.Binary.On.html#3280" class="Bound">ℓ₂</a><a id="3312" class="Symbol">}</a> <a id="3314" class="Symbol">→</a>
<a id="3338" href="Relation.Binary.html#IsDecPartialOrder" class="Record">IsDecPartialOrder</a> <a id="3356" href="Relation.Binary.On.html#3285" class="Bound">≈</a> <a id="3358" href="Relation.Binary.On.html#3300" class="Bound">≤</a> <a id="3360" class="Symbol">→</a>
<a id="3384" href="Relation.Binary.html#IsDecPartialOrder" class="Record">IsDecPartialOrder</a> <a id="3402" class="Symbol">(</a><a id="3403" href="Relation.Binary.On.html#3285" class="Bound">≈</a> <a id="3405" href="Function.html#_on_" class="Function Operator">on</a> <a id="3408" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="3409" class="Symbol">)</a> <a id="3411" class="Symbol">(</a><a id="3412" href="Relation.Binary.On.html#3300" class="Bound">≤</a> <a id="3414" href="Function.html#_on_" class="Function Operator">on</a> <a id="3417" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="3418" class="Symbol">)</a>
<a id="3422" href="Relation.Binary.On.html#3254" class="Function">isDecPartialOrder</a> <a id="3440" href="Relation.Binary.On.html#3440" class="Bound">dpo</a> <a id="3444" class="Symbol">=</a> <a id="3446" class="Keyword">record</a>
<a id="3457" class="Symbol">{</a> <a id="3459" class="Field">isPartialOrder</a> <a id="3474" class="Symbol">=</a> <a id="3476" href="Relation.Binary.On.html#2921" class="Function">isPartialOrder</a> <a id="3491" href="Relation.Binary.html#4359" class="Field">DPO.isPartialOrder</a>
<a id="3514" class="Symbol">;</a> <a id="3516" class="Field Operator">_≟_</a> <a id="3531" class="Symbol">=</a> <a id="3533" href="Relation.Binary.On.html#1593" class="Function">decidable</a> <a id="3543" class="Symbol">_</a> <a id="3545" href="Relation.Binary.html#4403" class="Field Operator">DPO._≟_</a>
<a id="3557" class="Symbol">;</a> <a id="3559" class="Field Operator">_≤?_</a> <a id="3574" class="Symbol">=</a> <a id="3576" href="Relation.Binary.On.html#1593" class="Function">decidable</a> <a id="3586" class="Symbol">_</a> <a id="3588" href="Relation.Binary.html#4438" class="Field Operator">DPO._≤?_</a>
<a id="3601" class="Symbol">}</a>
<a id="3607" class="Keyword">where</a> <a id="3613" class="Keyword">module</a> <a id="DPO" href="Relation.Binary.On.html#DPO" class="Module">DPO</a> <a id="3624" class="Symbol">=</a> <a id="3626" href="Relation.Binary.html#IsDecPartialOrder" class="Module">IsDecPartialOrder</a> <a id="3644" href="Relation.Binary.On.html#3440" class="Bound">dpo</a>
<a id="3651" href="Relation.Binary.On.html#3651" class="Function">isStrictPartialOrder</a> <a id="3672" class="Symbol">:</a> <a id="3674" class="Symbol">∀</a> <a id="3676" class="Symbol">{</a><a id="3677" href="Relation.Binary.On.html#3677" class="Bound">ℓ₁</a> <a id="3680" href="Relation.Binary.On.html#3680" class="Bound">ℓ₂</a><a id="3682" class="Symbol">}</a> <a id="3684" class="Symbol">{</a><a id="3685" href="Relation.Binary.On.html#3685" class="Bound">≈</a> <a id="3687" class="Symbol">:</a> <a id="3689" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="3693" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="3695" href="Relation.Binary.On.html#3677" class="Bound">ℓ₁</a><a id="3697" class="Symbol">}</a> <a id="3699" class="Symbol">{</a><a id="3700" href="Relation.Binary.On.html#3700" class="Bound"><</a> <a id="3702" class="Symbol">:</a> <a id="3704" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="3708" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="3710" href="Relation.Binary.On.html#3680" class="Bound">ℓ₂</a><a id="3712" class="Symbol">}</a> <a id="3714" class="Symbol">→</a>
<a id="3741" href="Relation.Binary.html#IsStrictPartialOrder" class="Record">IsStrictPartialOrder</a> <a id="3762" href="Relation.Binary.On.html#3685" class="Bound">≈</a> <a id="3764" href="Relation.Binary.On.html#3700" class="Bound"><</a> <a id="3766" class="Symbol">→</a>
<a id="3793" href="Relation.Binary.html#IsStrictPartialOrder" class="Record">IsStrictPartialOrder</a> <a id="3814" class="Symbol">(</a><a id="3815" href="Relation.Binary.On.html#3685" class="Bound">≈</a> <a id="3817" href="Function.html#_on_" class="Function Operator">on</a> <a id="3820" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="3821" class="Symbol">)</a> <a id="3823" class="Symbol">(</a><a id="3824" href="Relation.Binary.On.html#3700" class="Bound"><</a> <a id="3826" href="Function.html#_on_" class="Function Operator">on</a> <a id="3829" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="3830" class="Symbol">)</a>
<a id="3834" href="Relation.Binary.On.html#3651" class="Function">isStrictPartialOrder</a> <a id="3855" class="Symbol">{</a><a id="3856" class="Argument">≈</a> <a id="3858" class="Symbol">=</a> <a id="3860" href="Relation.Binary.On.html#3860" class="Bound">≈</a><a id="3861" class="Symbol">}</a> <a id="3863" class="Symbol">{</a><a id="3864" href="Relation.Binary.On.html#3864" class="Bound"><</a><a id="3865" class="Symbol">}</a> <a id="3867" href="Relation.Binary.On.html#3867" class="Bound">spo</a> <a id="3871" class="Symbol">=</a> <a id="3873" class="Keyword">record</a>
<a id="3884" class="Symbol">{</a> <a id="3886" class="Field">isEquivalence</a> <a id="3900" class="Symbol">=</a> <a id="3902" href="Relation.Binary.On.html#1989" class="Function">isEquivalence</a> <a id="3916" href="Relation.Binary.html#5684" class="Field">Spo.isEquivalence</a>
<a id="3938" class="Symbol">;</a> <a id="3940" class="Field">irrefl</a> <a id="3954" class="Symbol">=</a> <a id="3956" href="Relation.Binary.On.html#627" class="Function">irreflexive</a> <a id="3968" href="Relation.Binary.On.html#3860" class="Bound">≈</a> <a id="3970" href="Relation.Binary.On.html#3864" class="Bound"><</a> <a id="3972" href="Relation.Binary.html#5722" class="Field">Spo.irrefl</a>
<a id="3987" class="Symbol">;</a> <a id="3989" class="Field">trans</a> <a id="4003" class="Symbol">=</a> <a id="4005" href="Relation.Binary.On.html#878" class="Function">transitive</a> <a id="4016" href="Relation.Binary.On.html#3864" class="Bound"><</a> <a id="4018" href="Relation.Binary.html#5762" class="Field">Spo.trans</a>
<a id="4032" class="Symbol">;</a> <a id="4034" class="Field"><-resp-≈</a> <a id="4048" class="Symbol">=</a> <a id="4050" href="Relation.Binary.On.html#1384" class="Function">respects₂</a> <a id="4060" href="Relation.Binary.On.html#3864" class="Bound"><</a> <a id="4062" href="Relation.Binary.On.html#3860" class="Bound">≈</a> <a id="4064" href="Relation.Binary.html#5797" class="Field">Spo.<-resp-≈</a>
<a id="4081" class="Symbol">}</a>
<a id="4087" class="Keyword">where</a> <a id="4093" class="Keyword">module</a> <a id="Spo" href="Relation.Binary.On.html#Spo" class="Module">Spo</a> <a id="4104" class="Symbol">=</a> <a id="4106" href="Relation.Binary.html#IsStrictPartialOrder" class="Module">IsStrictPartialOrder</a> <a id="4127" href="Relation.Binary.On.html#3867" class="Bound">spo</a>
<a id="4134" href="Relation.Binary.On.html#4134" class="Function">isTotalOrder</a> <a id="4147" class="Symbol">:</a> <a id="4149" class="Symbol">∀</a> <a id="4151" class="Symbol">{</a><a id="4152" href="Relation.Binary.On.html#4152" class="Bound">ℓ₁</a> <a id="4155" href="Relation.Binary.On.html#4155" class="Bound">ℓ₂</a><a id="4157" class="Symbol">}</a> <a id="4159" class="Symbol">{</a><a id="4160" href="Relation.Binary.On.html#4160" class="Bound">≈</a> <a id="4162" class="Symbol">:</a> <a id="4164" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="4168" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="4170" href="Relation.Binary.On.html#4152" class="Bound">ℓ₁</a><a id="4172" class="Symbol">}</a> <a id="4174" class="Symbol">{</a><a id="4175" href="Relation.Binary.On.html#4175" class="Bound">≤</a> <a id="4177" class="Symbol">:</a> <a id="4179" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="4183" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="4185" href="Relation.Binary.On.html#4155" class="Bound">ℓ₂</a><a id="4187" class="Symbol">}</a> <a id="4189" class="Symbol">→</a>
<a id="4208" href="Relation.Binary.html#IsTotalOrder" class="Record">IsTotalOrder</a> <a id="4221" href="Relation.Binary.On.html#4160" class="Bound">≈</a> <a id="4223" href="Relation.Binary.On.html#4175" class="Bound">≤</a> <a id="4225" class="Symbol">→</a>
<a id="4244" href="Relation.Binary.html#IsTotalOrder" class="Record">IsTotalOrder</a> <a id="4257" class="Symbol">(</a><a id="4258" href="Relation.Binary.On.html#4160" class="Bound">≈</a> <a id="4260" href="Function.html#_on_" class="Function Operator">on</a> <a id="4263" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="4264" class="Symbol">)</a> <a id="4266" class="Symbol">(</a><a id="4267" href="Relation.Binary.On.html#4175" class="Bound">≤</a> <a id="4269" href="Function.html#_on_" class="Function Operator">on</a> <a id="4272" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="4273" class="Symbol">)</a>
<a id="4277" href="Relation.Binary.On.html#4134" class="Function">isTotalOrder</a> <a id="4290" class="Symbol">{</a><a id="4291" class="Argument">≈</a> <a id="4293" class="Symbol">=</a> <a id="4295" href="Relation.Binary.On.html#4295" class="Bound">≈</a><a id="4296" class="Symbol">}</a> <a id="4298" class="Symbol">{</a><a id="4299" href="Relation.Binary.On.html#4299" class="Bound">≤</a><a id="4300" class="Symbol">}</a> <a id="4302" href="Relation.Binary.On.html#4302" class="Bound">to</a> <a id="4305" class="Symbol">=</a> <a id="4307" class="Keyword">record</a>
<a id="4318" class="Symbol">{</a> <a id="4320" class="Field">isPartialOrder</a> <a id="4335" class="Symbol">=</a> <a id="4337" href="Relation.Binary.On.html#2921" class="Function">isPartialOrder</a> <a id="4352" href="Relation.Binary.html#8023" class="Field">To.isPartialOrder</a>
<a id="4374" class="Symbol">;</a> <a id="4376" class="Field">total</a> <a id="4391" class="Symbol">=</a> <a id="4393" href="Relation.Binary.On.html#1707" class="Function">total</a> <a id="4399" href="Relation.Binary.On.html#4299" class="Bound">≤</a> <a id="4401" href="Relation.Binary.html#8067" class="Field">To.total</a>
<a id="4414" class="Symbol">}</a>
<a id="4420" class="Keyword">where</a> <a id="4426" class="Keyword">module</a> <a id="To" href="Relation.Binary.On.html#To" class="Module">To</a> <a id="4436" class="Symbol">=</a> <a id="4438" href="Relation.Binary.html#IsTotalOrder" class="Module">IsTotalOrder</a> <a id="4451" href="Relation.Binary.On.html#4302" class="Bound">to</a>
<a id="4457" href="Relation.Binary.On.html#4457" class="Function">isDecTotalOrder</a> <a id="4473" class="Symbol">:</a> <a id="4475" class="Symbol">∀</a> <a id="4477" class="Symbol">{</a><a id="4478" href="Relation.Binary.On.html#4478" class="Bound">ℓ₁</a> <a id="4481" href="Relation.Binary.On.html#4481" class="Bound">ℓ₂</a><a id="4483" class="Symbol">}</a> <a id="4485" class="Symbol">{</a><a id="4486" href="Relation.Binary.On.html#4486" class="Bound">≈</a> <a id="4488" class="Symbol">:</a> <a id="4490" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="4494" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="4496" href="Relation.Binary.On.html#4478" class="Bound">ℓ₁</a><a id="4498" class="Symbol">}</a> <a id="4500" class="Symbol">{</a><a id="4501" href="Relation.Binary.On.html#4501" class="Bound">≤</a> <a id="4503" class="Symbol">:</a> <a id="4505" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="4509" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="4511" href="Relation.Binary.On.html#4481" class="Bound">ℓ₂</a><a id="4513" class="Symbol">}</a> <a id="4515" class="Symbol">→</a>
<a id="4537" href="Relation.Binary.html#IsDecTotalOrder" class="Record">IsDecTotalOrder</a> <a id="4553" href="Relation.Binary.On.html#4486" class="Bound">≈</a> <a id="4555" href="Relation.Binary.On.html#4501" class="Bound">≤</a> <a id="4557" class="Symbol">→</a>
<a id="4579" href="Relation.Binary.html#IsDecTotalOrder" class="Record">IsDecTotalOrder</a> <a id="4595" class="Symbol">(</a><a id="4596" href="Relation.Binary.On.html#4486" class="Bound">≈</a> <a id="4598" href="Function.html#_on_" class="Function Operator">on</a> <a id="4601" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="4602" class="Symbol">)</a> <a id="4604" class="Symbol">(</a><a id="4605" href="Relation.Binary.On.html#4501" class="Bound">≤</a> <a id="4607" href="Function.html#_on_" class="Function Operator">on</a> <a id="4610" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="4611" class="Symbol">)</a>
<a id="4615" href="Relation.Binary.On.html#4457" class="Function">isDecTotalOrder</a> <a id="4631" class="Symbol">{</a><a id="4632" class="Argument">≈</a> <a id="4634" class="Symbol">=</a> <a id="4636" href="Relation.Binary.On.html#4636" class="Bound">≈</a><a id="4637" class="Symbol">}</a> <a id="4639" class="Symbol">{</a><a id="4640" href="Relation.Binary.On.html#4640" class="Bound">≤</a><a id="4641" class="Symbol">}</a> <a id="4643" href="Relation.Binary.On.html#4643" class="Bound">dec</a> <a id="4647" class="Symbol">=</a> <a id="4649" class="Keyword">record</a>
<a id="4660" class="Symbol">{</a> <a id="4662" class="Field">isTotalOrder</a> <a id="4675" class="Symbol">=</a> <a id="4677" href="Relation.Binary.On.html#4134" class="Function">isTotalOrder</a> <a id="4690" href="Relation.Binary.html#8803" class="Field">Dec.isTotalOrder</a>
<a id="4711" class="Symbol">;</a> <a id="4713" class="Field Operator">_≟_</a> <a id="4726" class="Symbol">=</a> <a id="4728" href="Relation.Binary.On.html#1593" class="Function">decidable</a> <a id="4738" href="Relation.Binary.On.html#4636" class="Bound">≈</a> <a id="4740" href="Relation.Binary.html#8843" class="Field Operator">Dec._≟_</a>
<a id="4752" class="Symbol">;</a> <a id="4754" class="Field Operator">_≤?_</a> <a id="4767" class="Symbol">=</a> <a id="4769" href="Relation.Binary.On.html#1593" class="Function">decidable</a> <a id="4779" href="Relation.Binary.On.html#4640" class="Bound">≤</a> <a id="4781" href="Relation.Binary.html#8876" class="Field Operator">Dec._≤?_</a>
<a id="4794" class="Symbol">}</a>
<a id="4800" class="Keyword">where</a> <a id="4806" class="Keyword">module</a> <a id="Dec" href="Relation.Binary.On.html#Dec" class="Module">Dec</a> <a id="4817" class="Symbol">=</a> <a id="4819" href="Relation.Binary.html#IsDecTotalOrder" class="Module">IsDecTotalOrder</a> <a id="4835" href="Relation.Binary.On.html#4643" class="Bound">dec</a>
<a id="4842" href="Relation.Binary.On.html#4842" class="Function">isStrictTotalOrder</a> <a id="4861" class="Symbol">:</a> <a id="4863" class="Symbol">∀</a> <a id="4865" class="Symbol">{</a><a id="4866" href="Relation.Binary.On.html#4866" class="Bound">ℓ₁</a> <a id="4869" href="Relation.Binary.On.html#4869" class="Bound">ℓ₂</a><a id="4871" class="Symbol">}</a> <a id="4873" class="Symbol">{</a><a id="4874" href="Relation.Binary.On.html#4874" class="Bound">≈</a> <a id="4876" class="Symbol">:</a> <a id="4878" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="4882" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="4884" href="Relation.Binary.On.html#4866" class="Bound">ℓ₁</a><a id="4886" class="Symbol">}</a> <a id="4888" class="Symbol">{</a><a id="4889" href="Relation.Binary.On.html#4889" class="Bound"><</a> <a id="4891" class="Symbol">:</a> <a id="4893" href="Relation.Binary.Core.html#Rel" class="Function">Rel</a> <a id="4897" href="Relation.Binary.On.html#366" class="Bound">A</a> <a id="4899" href="Relation.Binary.On.html#4869" class="Bound">ℓ₂</a><a id="4901" class="Symbol">}</a> <a id="4903" class="Symbol">→</a>
<a id="4928" href="Relation.Binary.html#IsStrictTotalOrder" class="Record">IsStrictTotalOrder</a> <a id="4947" href="Relation.Binary.On.html#4874" class="Bound">≈</a> <a id="4949" href="Relation.Binary.On.html#4889" class="Bound"><</a> <a id="4951" class="Symbol">→</a>
<a id="4976" href="Relation.Binary.html#IsStrictTotalOrder" class="Record">IsStrictTotalOrder</a> <a id="4995" class="Symbol">(</a><a id="4996" href="Relation.Binary.On.html#4874" class="Bound">≈</a> <a id="4998" href="Function.html#_on_" class="Function Operator">on</a> <a id="5001" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="5002" class="Symbol">)</a> <a id="5004" class="Symbol">(</a><a id="5005" href="Relation.Binary.On.html#4889" class="Bound"><</a> <a id="5007" href="Function.html#_on_" class="Function Operator">on</a> <a id="5010" href="Relation.Binary.On.html#390" class="Bound">f</a><a id="5011" class="Symbol">)</a>
<a id="5015" href="Relation.Binary.On.html#4842" class="Function">isStrictTotalOrder</a> <a id="5034" class="Symbol">{</a><a id="5035" class="Argument">≈</a> <a id="5037" class="Symbol">=</a> <a id="5039" href="Relation.Binary.On.html#5039" class="Bound">≈</a><a id="5040" class="Symbol">}</a> <a id="5042" class="Symbol">{</a><a id="5043" href="Relation.Binary.On.html#5043" class="Bound"><</a><a id="5044" class="Symbol">}</a> <a id="5046" href="Relation.Binary.On.html#5046" class="Bound">sto</a> <a id="5050" class="Symbol">=</a> <a id="5052" class="Keyword">record</a>
<a id="5063" class="Symbol">{</a> <a id="5065" class="Field">isEquivalence</a> <a id="5079" class="Symbol">=</a> <a id="5081" href="Relation.Binary.On.html#1989" class="Function">isEquivalence</a> <a id="5095" href="Relation.Binary.html#10183" class="Field">Sto.isEquivalence</a>
<a id="5117" class="Symbol">;</a> <a id="5119" class="Field">trans</a> <a id="5133" class="Symbol">=</a> <a id="5135" href="Relation.Binary.On.html#878" class="Function">transitive</a> <a id="5146" href="Relation.Binary.On.html#5043" class="Bound"><</a> <a id="5148" href="Relation.Binary.html#10221" class="Field">Sto.trans</a>
<a id="5162" class="Symbol">;</a> <a id="5164" class="Field">compare</a> <a id="5178" class="Symbol">=</a> <a id="5180" href="Relation.Binary.On.html#1805" class="Function">trichotomous</a> <a id="5193" href="Relation.Binary.On.html#5039" class="Bound">≈</a> <a id="5195" href="Relation.Binary.On.html#5043" class="Bound"><</a> <a id="5197" href="Relation.Binary.html#10256" class="Field">Sto.compare</a>
<a id="5213" class="Symbol">}</a>
<a id="5219" class="Keyword">where</a> <a id="5225" class="Keyword">module</a> <a id="Sto" href="Relation.Binary.On.html#Sto" class="Module">Sto</a> <a id="5236" class="Symbol">=</a> <a id="5238" href="Relation.Binary.html#IsStrictTotalOrder" class="Module">IsStrictTotalOrder</a> <a id="5257" href="Relation.Binary.On.html#5046" class="Bound">sto</a>
<a id="preorder" href="Relation.Binary.On.html#preorder" class="Function">preorder</a> <a id="5271" class="Symbol">:</a> <a id="5273" class="Symbol">∀</a> <a id="5275" class="Symbol">{</a><a id="5276" href="Relation.Binary.On.html#5276" class="Bound">p₁</a> <a id="5279" href="Relation.Binary.On.html#5279" class="Bound">p₂</a> <a id="5282" href="Relation.Binary.On.html#5282" class="Bound">p₃</a> <a id="5285" href="Relation.Binary.On.html#5285" class="Bound">b</a><a id="5286" class="Symbol">}</a> <a id="5288" class="Symbol">{</a><a id="5289" href="Relation.Binary.On.html#5289" class="Bound">B</a> <a id="5291" class="Symbol">:</a> <a id="5293" class="PrimitiveType">Set</a> <a id="5297" href="Relation.Binary.On.html#5285" class="Bound">b</a><a id="5298" class="Symbol">}</a> <a id="5300" class="Symbol">(</a><a id="5301" href="Relation.Binary.On.html#5301" class="Bound">P</a> <a id="5303" class="Symbol">:</a> <a id="5305" href="Relation.Binary.html#Preorder" class="Record">Preorder</a> <a id="5314" href="Relation.Binary.On.html#5276" class="Bound">p₁</a> <a id="5317" href="Relation.Binary.On.html#5279" class="Bound">p₂</a> <a id="5320" href="Relation.Binary.On.html#5282" class="Bound">p₃</a><a id="5322" class="Symbol">)</a> <a id="5324" class="Symbol">→</a>
<a id="5337" class="Symbol">(</a><a id="5338" href="Relation.Binary.On.html#5289" class="Bound">B</a> <a id="5340" class="Symbol">→</a> <a id="5342" href="Relation.Binary.html#Preorder.Carrier" class="Field">Preorder.Carrier</a> <a id="5359" href="Relation.Binary.On.html#5301" class="Bound">P</a><a id="5360" class="Symbol">)</a> <a id="5362" class="Symbol">→</a> <a id="5364" href="Relation.Binary.html#Preorder" class="Record">Preorder</a> <a id="5373" class="Symbol">_</a> <a id="5375" class="Symbol">_</a> <a id="5377" class="Symbol">_</a>
<a id="5379" href="Relation.Binary.On.html#preorder" class="Function">preorder</a> <a id="5388" href="Relation.Binary.On.html#5388" class="Bound">P</a> <a id="5390" href="Relation.Binary.On.html#5390" class="Bound">f</a> <a id="5392" class="Symbol">=</a> <a id="5394" class="Keyword">record</a>
<a id="5403" class="Symbol">{</a> <a id="5405" class="Field">isPreorder</a> <a id="5416" class="Symbol">=</a> <a id="5418" href="Relation.Binary.On.html#2275" class="Function">isPreorder</a> <a id="5429" href="Relation.Binary.On.html#5390" class="Bound">f</a> <a id="5431" class="Symbol">(</a><a id="5432" href="Relation.Binary.html#Preorder.isPreorder" class="Field">Preorder.isPreorder</a> <a id="5452" href="Relation.Binary.On.html#5388" class="Bound">P</a><a id="5453" class="Symbol">)</a>
<a id="5457" class="Symbol">}</a>
<a id="setoid" href="Relation.Binary.On.html#setoid" class="Function">setoid</a> <a id="5467" class="Symbol">:</a> <a id="5469" class="Symbol">∀</a> <a id="5471" class="Symbol">{</a><a id="5472" href="Relation.Binary.On.html#5472" class="Bound">s₁</a> <a id="5475" href="Relation.Binary.On.html#5475" class="Bound">s₂</a> <a id="5478" href="Relation.Binary.On.html#5478" class="Bound">b</a><a id="5479" class="Symbol">}</a> <a id="5481" class="Symbol">{</a><a id="5482" href="Relation.Binary.On.html#5482" class="Bound">B</a> <a id="5484" class="Symbol">:</a> <a id="5486" class="PrimitiveType">Set</a> <a id="5490" href="Relation.Binary.On.html#5478" class="Bound">b</a><a id="5491" class="Symbol">}</a> <a id="5493" class="Symbol">(</a><a id="5494" href="Relation.Binary.On.html#5494" class="Bound">S</a> <a id="5496" class="Symbol">:</a> <a id="5498" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="5505" href="Relation.Binary.On.html#5472" class="Bound">s₁</a> <a id="5508" href="Relation.Binary.On.html#5475" class="Bound">s₂</a><a id="5510" class="Symbol">)</a> <a id="5512" class="Symbol">→</a>
<a id="5523" class="Symbol">(</a><a id="5524" href="Relation.Binary.On.html#5482" class="Bound">B</a> <a id="5526" class="Symbol">→</a> <a id="5528" href="Relation.Binary.html#Setoid.Carrier" class="Field">Setoid.Carrier</a> <a id="5543" href="Relation.Binary.On.html#5494" class="Bound">S</a><a id="5544" class="Symbol">)</a> <a id="5546" class="Symbol">→</a> <a id="5548" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="5555" class="Symbol">_</a> <a id="5557" class="Symbol">_</a>
<a id="5559" href="Relation.Binary.On.html#setoid" class="Function">setoid</a> <a id="5566" href="Relation.Binary.On.html#5566" class="Bound">S</a> <a id="5568" href="Relation.Binary.On.html#5568" class="Bound">f</a> <a id="5570" class="Symbol">=</a> <a id="5572" class="Keyword">record</a>
<a id="5581" class="Symbol">{</a> <a id="5583" class="Field">isEquivalence</a> <a id="5597" class="Symbol">=</a> <a id="5599" href="Relation.Binary.On.html#1989" class="Function">isEquivalence</a> <a id="5613" href="Relation.Binary.On.html#5568" class="Bound">f</a> <a id="5615" class="Symbol">(</a><a id="5616" href="Relation.Binary.html#Setoid.isEquivalence" class="Field">Setoid.isEquivalence</a> <a id="5637" href="Relation.Binary.On.html#5566" class="Bound">S</a><a id="5638" class="Symbol">)</a>
<a id="5642" class="Symbol">}</a>
<a id="decSetoid" href="Relation.Binary.On.html#decSetoid" class="Function">decSetoid</a> <a id="5655" class="Symbol">:</a> <a id="5657" class="Symbol">∀</a> <a id="5659" class="Symbol">{</a><a id="5660" href="Relation.Binary.On.html#5660" class="Bound">d₁</a> <a id="5663" href="Relation.Binary.On.html#5663" class="Bound">d₂</a> <a id="5666" href="Relation.Binary.On.html#5666" class="Bound">b</a><a id="5667" class="Symbol">}</a> <a id="5669" class="Symbol">{</a><a id="5670" href="Relation.Binary.On.html#5670" class="Bound">B</a> <a id="5672" class="Symbol">:</a> <a id="5674" class="PrimitiveType">Set</a> <a id="5678" href="Relation.Binary.On.html#5666" class="Bound">b</a><a id="5679" class="Symbol">}</a> <a id="5681" class="Symbol">(</a><a id="5682" href="Relation.Binary.On.html#5682" class="Bound">D</a> <a id="5684" class="Symbol">:</a> <a id="5686" href="Relation.Binary.html#DecSetoid" class="Record">DecSetoid</a> <a id="5696" href="Relation.Binary.On.html#5660" class="Bound">d₁</a> <a id="5699" href="Relation.Binary.On.html#5663" class="Bound">d₂</a><a id="5701" class="Symbol">)</a> <a id="5703" class="Symbol">→</a>
<a id="5717" class="Symbol">(</a><a id="5718" href="Relation.Binary.On.html#5670" class="Bound">B</a> <a id="5720" class="Symbol">→</a> <a id="5722" href="Relation.Binary.html#DecSetoid.Carrier" class="Field">DecSetoid.Carrier</a> <a id="5740" href="Relation.Binary.On.html#5682" class="Bound">D</a><a id="5741" class="Symbol">)</a> <a id="5743" class="Symbol">→</a> <a id="5745" href="Relation.Binary.html#DecSetoid" class="Record">DecSetoid</a> <a id="5755" class="Symbol">_</a> <a id="5757" class="Symbol">_</a>
<a id="5759" href="Relation.Binary.On.html#decSetoid" class="Function">decSetoid</a> <a id="5769" href="Relation.Binary.On.html#5769" class="Bound">D</a> <a id="5771" href="Relation.Binary.On.html#5771" class="Bound">f</a> <a id="5773" class="Symbol">=</a> <a id="5775" class="Keyword">record</a>
<a id="5784" class="Symbol">{</a> <a id="5786" class="Field">isDecEquivalence</a> <a id="5803" class="Symbol">=</a> <a id="5805" href="Relation.Binary.On.html#2623" class="Function">isDecEquivalence</a> <a id="5822" href="Relation.Binary.On.html#5771" class="Bound">f</a> <a id="5824" class="Symbol">(</a><a id="5825" href="Relation.Binary.html#DecSetoid.isDecEquivalence" class="Field">DecSetoid.isDecEquivalence</a> <a id="5852" href="Relation.Binary.On.html#5769" class="Bound">D</a><a id="5853" class="Symbol">)</a>
<a id="5857" class="Symbol">}</a>
<a id="poset" href="Relation.Binary.On.html#poset" class="Function">poset</a> <a id="5866" class="Symbol">:</a> <a id="5868" class="Symbol">∀</a> <a id="5870" class="Symbol">{</a><a id="5871" href="Relation.Binary.On.html#5871" class="Bound">p₁</a> <a id="5874" href="Relation.Binary.On.html#5874" class="Bound">p₂</a> <a id="5877" href="Relation.Binary.On.html#5877" class="Bound">p₃</a> <a id="5880" href="Relation.Binary.On.html#5880" class="Bound">b</a><a id="5881" class="Symbol">}</a> <a id="5883" class="Symbol">{</a><a id="5884" href="Relation.Binary.On.html#5884" class="Bound">B</a> <a id="5886" class="Symbol">:</a> <a id="5888" class="PrimitiveType">Set</a> <a id="5892" href="Relation.Binary.On.html#5880" class="Bound">b</a><a id="5893" class="Symbol">}</a> <a id="5895" class="Symbol">(</a><a id="5896" href="Relation.Binary.On.html#5896" class="Bound">P</a> <a id="5898" class="Symbol">:</a> <a id="5900" href="Relation.Binary.html#Poset" class="Record">Poset</a> <a id="5906" href="Relation.Binary.On.html#5871" class="Bound">p₁</a> <a id="5909" href="Relation.Binary.On.html#5874" class="Bound">p₂</a> <a id="5912" href="Relation.Binary.On.html#5877" class="Bound">p₃</a><a id="5914" class="Symbol">)</a> <a id="5916" class="Symbol">→</a>
<a id="5926" class="Symbol">(</a><a id="5927" href="Relation.Binary.On.html#5884" class="Bound">B</a> <a id="5929" class="Symbol">→</a> <a id="5931" href="Relation.Binary.html#Poset.Carrier" class="Field">Poset.Carrier</a> <a id="5945" href="Relation.Binary.On.html#5896" class="Bound">P</a><a id="5946" class="Symbol">)</a> <a id="5948" class="Symbol">→</a> <a id="5950" href="Relation.Binary.html#Poset" class="Record">Poset</a> <a id="5956" class="Symbol">_</a> <a id="5958" class="Symbol">_</a> <a id="5960" class="Symbol">_</a>
<a id="5962" href="Relation.Binary.On.html#poset" class="Function">poset</a> <a id="5968" href="Relation.Binary.On.html#5968" class="Bound">P</a> <a id="5970" href="Relation.Binary.On.html#5970" class="Bound">f</a> <a id="5972" class="Symbol">=</a> <a id="5974" class="Keyword">record</a>
<a id="5983" class="Symbol">{</a> <a id="5985" class="Field">isPartialOrder</a> <a id="6000" class="Symbol">=</a> <a id="6002" href="Relation.Binary.On.html#2921" class="Function">isPartialOrder</a> <a id="6017" href="Relation.Binary.On.html#5970" class="Bound">f</a> <a id="6019" class="Symbol">(</a><a id="6020" href="Relation.Binary.html#Poset.isPartialOrder" class="Field">Poset.isPartialOrder</a> <a id="6041" href="Relation.Binary.On.html#5968" class="Bound">P</a><a id="6042" class="Symbol">)</a>
<a id="6046" class="Symbol">}</a>
<a id="decPoset" href="Relation.Binary.On.html#decPoset" class="Function">decPoset</a> <a id="6058" class="Symbol">:</a> <a id="6060" class="Symbol">∀</a> <a id="6062" class="Symbol">{</a><a id="6063" href="Relation.Binary.On.html#6063" class="Bound">d₁</a> <a id="6066" href="Relation.Binary.On.html#6066" class="Bound">d₂</a> <a id="6069" href="Relation.Binary.On.html#6069" class="Bound">d₃</a> <a id="6072" href="Relation.Binary.On.html#6072" class="Bound">b</a><a id="6073" class="Symbol">}</a> <a id="6075" class="Symbol">{</a><a id="6076" href="Relation.Binary.On.html#6076" class="Bound">B</a> <a id="6078" class="Symbol">:</a> <a id="6080" class="PrimitiveType">Set</a> <a id="6084" href="Relation.Binary.On.html#6072" class="Bound">b</a><a id="6085" class="Symbol">}</a> <a id="6087" class="Symbol">(</a><a id="6088" href="Relation.Binary.On.html#6088" class="Bound">D</a> <a id="6090" class="Symbol">:</a> <a id="6092" href="Relation.Binary.html#DecPoset" class="Record">DecPoset</a> <a id="6101" href="Relation.Binary.On.html#6063" class="Bound">d₁</a> <a id="6104" href="Relation.Binary.On.html#6066" class="Bound">d₂</a> <a id="6107" href="Relation.Binary.On.html#6069" class="Bound">d₃</a><a id="6109" class="Symbol">)</a> <a id="6111" class="Symbol">→</a>
<a id="6124" class="Symbol">(</a><a id="6125" href="Relation.Binary.On.html#6076" class="Bound">B</a> <a id="6127" class="Symbol">→</a> <a id="6129" href="Relation.Binary.html#DecPoset.Carrier" class="Field">DecPoset.Carrier</a> <a id="6146" href="Relation.Binary.On.html#6088" class="Bound">D</a><a id="6147" class="Symbol">)</a> <a id="6149" class="Symbol">→</a> <a id="6151" href="Relation.Binary.html#DecPoset" class="Record">DecPoset</a> <a id="6160" class="Symbol">_</a> <a id="6162" class="Symbol">_</a> <a id="6164" class="Symbol">_</a>
<a id="6166" href="Relation.Binary.On.html#decPoset" class="Function">decPoset</a> <a id="6175" href="Relation.Binary.On.html#6175" class="Bound">D</a> <a id="6177" href="Relation.Binary.On.html#6177" class="Bound">f</a> <a id="6179" class="Symbol">=</a> <a id="6181" class="Keyword">record</a>
<a id="6190" class="Symbol">{</a> <a id="6192" class="Field">isDecPartialOrder</a> <a id="6210" class="Symbol">=</a>
<a id="6218" href="Relation.Binary.On.html#3254" class="Function">isDecPartialOrder</a> <a id="6236" href="Relation.Binary.On.html#6177" class="Bound">f</a> <a id="6238" class="Symbol">(</a><a id="6239" href="Relation.Binary.html#DecPoset.isDecPartialOrder" class="Field">DecPoset.isDecPartialOrder</a> <a id="6266" href="Relation.Binary.On.html#6175" class="Bound">D</a><a id="6267" class="Symbol">)</a>
<a id="6271" class="Symbol">}</a>
<a id="strictPartialOrder" href="Relation.Binary.On.html#strictPartialOrder" class="Function">strictPartialOrder</a> <a id="6293" class="Symbol">:</a>
<a id="6297" class="Symbol">∀</a> <a id="6299" class="Symbol">{</a><a id="6300" href="Relation.Binary.On.html#6300" class="Bound">s₁</a> <a id="6303" href="Relation.Binary.On.html#6303" class="Bound">s₂</a> <a id="6306" href="Relation.Binary.On.html#6306" class="Bound">s₃</a> <a id="6309" href="Relation.Binary.On.html#6309" class="Bound">b</a><a id="6310" class="Symbol">}</a> <a id="6312" class="Symbol">{</a><a id="6313" href="Relation.Binary.On.html#6313" class="Bound">B</a> <a id="6315" class="Symbol">:</a> <a id="6317" class="PrimitiveType">Set</a> <a id="6321" href="Relation.Binary.On.html#6309" class="Bound">b</a><a id="6322" class="Symbol">}</a> <a id="6324" class="Symbol">(</a><a id="6325" href="Relation.Binary.On.html#6325" class="Bound">S</a> <a id="6327" class="Symbol">:</a> <a id="6329" href="Relation.Binary.html#StrictPartialOrder" class="Record">StrictPartialOrder</a> <a id="6348" href="Relation.Binary.On.html#6300" class="Bound">s₁</a> <a id="6351" href="Relation.Binary.On.html#6303" class="Bound">s₂</a> <a id="6354" href="Relation.Binary.On.html#6306" class="Bound">s₃</a><a id="6356" class="Symbol">)</a> <a id="6358" class="Symbol">→</a>
<a id="6362" class="Symbol">(</a><a id="6363" href="Relation.Binary.On.html#6313" class="Bound">B</a> <a id="6365" class="Symbol">→</a> <a id="6367" href="Relation.Binary.html#StrictPartialOrder.Carrier" class="Field">StrictPartialOrder.Carrier</a> <a id="6394" href="Relation.Binary.On.html#6325" class="Bound">S</a><a id="6395" class="Symbol">)</a> <a id="6397" class="Symbol">→</a> <a id="6399" href="Relation.Binary.html#StrictPartialOrder" class="Record">StrictPartialOrder</a> <a id="6418" class="Symbol">_</a> <a id="6420" class="Symbol">_</a> <a id="6422" class="Symbol">_</a>
<a id="6424" href="Relation.Binary.On.html#strictPartialOrder" class="Function">strictPartialOrder</a> <a id="6443" href="Relation.Binary.On.html#6443" class="Bound">S</a> <a id="6445" href="Relation.Binary.On.html#6445" class="Bound">f</a> <a id="6447" class="Symbol">=</a> <a id="6449" class="Keyword">record</a>
<a id="6458" class="Symbol">{</a> <a id="6460" class="Field">isStrictPartialOrder</a> <a id="6481" class="Symbol">=</a>
<a id="6489" href="Relation.Binary.On.html#3651" class="Function">isStrictPartialOrder</a> <a id="6510" href="Relation.Binary.On.html#6445" class="Bound">f</a> <a id="6512" class="Symbol">(</a><a id="6513" href="Relation.Binary.html#StrictPartialOrder.isStrictPartialOrder" class="Field">StrictPartialOrder.isStrictPartialOrder</a> <a id="6553" href="Relation.Binary.On.html#6443" class="Bound">S</a><a id="6554" class="Symbol">)</a>
<a id="6558" class="Symbol">}</a>
<a id="totalOrder" href="Relation.Binary.On.html#totalOrder" class="Function">totalOrder</a> <a id="6572" class="Symbol">:</a> <a id="6574" class="Symbol">∀</a> <a id="6576" class="Symbol">{</a><a id="6577" href="Relation.Binary.On.html#6577" class="Bound">t₁</a> <a id="6580" href="Relation.Binary.On.html#6580" class="Bound">t₂</a> <a id="6583" href="Relation.Binary.On.html#6583" class="Bound">t₃</a> <a id="6586" href="Relation.Binary.On.html#6586" class="Bound">b</a><a id="6587" class="Symbol">}</a> <a id="6589" class="Symbol">{</a><a id="6590" href="Relation.Binary.On.html#6590" class="Bound">B</a> <a id="6592" class="Symbol">:</a> <a id="6594" class="PrimitiveType">Set</a> <a id="6598" href="Relation.Binary.On.html#6586" class="Bound">b</a><a id="6599" class="Symbol">}</a> <a id="6601" class="Symbol">(</a><a id="6602" href="Relation.Binary.On.html#6602" class="Bound">T</a> <a id="6604" class="Symbol">:</a> <a id="6606" href="Relation.Binary.html#TotalOrder" class="Record">TotalOrder</a> <a id="6617" href="Relation.Binary.On.html#6577" class="Bound">t₁</a> <a id="6620" href="Relation.Binary.On.html#6580" class="Bound">t₂</a> <a id="6623" href="Relation.Binary.On.html#6583" class="Bound">t₃</a><a id="6625" class="Symbol">)</a> <a id="6627" class="Symbol">→</a>
<a id="6642" class="Symbol">(</a><a id="6643" href="Relation.Binary.On.html#6590" class="Bound">B</a> <a id="6645" class="Symbol">→</a> <a id="6647" href="Relation.Binary.html#TotalOrder.Carrier" class="Field">TotalOrder.Carrier</a> <a id="6666" href="Relation.Binary.On.html#6602" class="Bound">T</a><a id="6667" class="Symbol">)</a> <a id="6669" class="Symbol">→</a> <a id="6671" href="Relation.Binary.html#TotalOrder" class="Record">TotalOrder</a> <a id="6682" class="Symbol">_</a> <a id="6684" class="Symbol">_</a> <a id="6686" class="Symbol">_</a>
<a id="6688" href="Relation.Binary.On.html#totalOrder" class="Function">totalOrder</a> <a id="6699" href="Relation.Binary.On.html#6699" class="Bound">T</a> <a id="6701" href="Relation.Binary.On.html#6701" class="Bound">f</a> <a id="6703" class="Symbol">=</a> <a id="6705" class="Keyword">record</a>
<a id="6714" class="Symbol">{</a> <a id="6716" class="Field">isTotalOrder</a> <a id="6729" class="Symbol">=</a> <a id="6731" href="Relation.Binary.On.html#4134" class="Function">isTotalOrder</a> <a id="6744" href="Relation.Binary.On.html#6701" class="Bound">f</a> <a id="6746" class="Symbol">(</a><a id="6747" href="Relation.Binary.html#TotalOrder.isTotalOrder" class="Field">TotalOrder.isTotalOrder</a> <a id="6771" href="Relation.Binary.On.html#6699" class="Bound">T</a><a id="6772" class="Symbol">)</a>
<a id="6776" class="Symbol">}</a>
<a id="decTotalOrder" href="Relation.Binary.On.html#decTotalOrder" class="Function">decTotalOrder</a> <a id="6793" class="Symbol">:</a>
<a id="6797" class="Symbol">∀</a> <a id="6799" class="Symbol">{</a><a id="6800" href="Relation.Binary.On.html#6800" class="Bound">d₁</a> <a id="6803" href="Relation.Binary.On.html#6803" class="Bound">d₂</a> <a id="6806" href="Relation.Binary.On.html#6806" class="Bound">d₃</a> <a id="6809" href="Relation.Binary.On.html#6809" class="Bound">b</a><a id="6810" class="Symbol">}</a> <a id="6812" class="Symbol">{</a><a id="6813" href="Relation.Binary.On.html#6813" class="Bound">B</a> <a id="6815" class="Symbol">:</a> <a id="6817" class="PrimitiveType">Set</a> <a id="6821" href="Relation.Binary.On.html#6809" class="Bound">b</a><a id="6822" class="Symbol">}</a> <a id="6824" class="Symbol">(</a><a id="6825" href="Relation.Binary.On.html#6825" class="Bound">D</a> <a id="6827" class="Symbol">:</a> <a id="6829" href="Relation.Binary.html#DecTotalOrder" class="Record">DecTotalOrder</a> <a id="6843" href="Relation.Binary.On.html#6800" class="Bound">d₁</a> <a id="6846" href="Relation.Binary.On.html#6803" class="Bound">d₂</a> <a id="6849" href="Relation.Binary.On.html#6806" class="Bound">d₃</a><a id="6851" class="Symbol">)</a> <a id="6853" class="Symbol">→</a>
<a id="6857" class="Symbol">(</a><a id="6858" href="Relation.Binary.On.html#6813" class="Bound">B</a> <a id="6860" class="Symbol">→</a> <a id="6862" href="Relation.Binary.html#DecTotalOrder.Carrier" class="Field">DecTotalOrder.Carrier</a> <a id="6884" href="Relation.Binary.On.html#6825" class="Bound">D</a><a id="6885" class="Symbol">)</a> <a id="6887" class="Symbol">→</a> <a id="6889" href="Relation.Binary.html#DecTotalOrder" class="Record">DecTotalOrder</a> <a id="6903" class="Symbol">_</a> <a id="6905" class="Symbol">_</a> <a id="6907" class="Symbol">_</a>
<a id="6909" href="Relation.Binary.On.html#decTotalOrder" class="Function">decTotalOrder</a> <a id="6923" href="Relation.Binary.On.html#6923" class="Bound">D</a> <a id="6925" href="Relation.Binary.On.html#6925" class="Bound">f</a> <a id="6927" class="Symbol">=</a> <a id="6929" class="Keyword">record</a>
<a id="6938" class="Symbol">{</a> <a id="6940" class="Field">isDecTotalOrder</a> <a id="6956" class="Symbol">=</a> <a id="6958" href="Relation.Binary.On.html#4457" class="Function">isDecTotalOrder</a> <a id="6974" href="Relation.Binary.On.html#6925" class="Bound">f</a> <a id="6976" class="Symbol">(</a><a id="6977" href="Relation.Binary.html#DecTotalOrder.isDecTotalOrder" class="Field">DecTotalOrder.isDecTotalOrder</a> <a id="7007" href="Relation.Binary.On.html#6923" class="Bound">D</a><a id="7008" class="Symbol">)</a>
<a id="7012" class="Symbol">}</a>
<a id="strictTotalOrder" href="Relation.Binary.On.html#strictTotalOrder" class="Function">strictTotalOrder</a> <a id="7032" class="Symbol">:</a>
<a id="7036" class="Symbol">∀</a> <a id="7038" class="Symbol">{</a><a id="7039" href="Relation.Binary.On.html#7039" class="Bound">s₁</a> <a id="7042" href="Relation.Binary.On.html#7042" class="Bound">s₂</a> <a id="7045" href="Relation.Binary.On.html#7045" class="Bound">s₃</a> <a id="7048" href="Relation.Binary.On.html#7048" class="Bound">b</a><a id="7049" class="Symbol">}</a> <a id="7051" class="Symbol">{</a><a id="7052" href="Relation.Binary.On.html#7052" class="Bound">B</a> <a id="7054" class="Symbol">:</a> <a id="7056" class="PrimitiveType">Set</a> <a id="7060" href="Relation.Binary.On.html#7048" class="Bound">b</a><a id="7061" class="Symbol">}</a> <a id="7063" class="Symbol">(</a><a id="7064" href="Relation.Binary.On.html#7064" class="Bound">S</a> <a id="7066" class="Symbol">:</a> <a id="7068" href="Relation.Binary.html#StrictTotalOrder" class="Record">StrictTotalOrder</a> <a id="7085" href="Relation.Binary.On.html#7039" class="Bound">s₁</a> <a id="7088" href="Relation.Binary.On.html#7042" class="Bound">s₂</a> <a id="7091" href="Relation.Binary.On.html#7045" class="Bound">s₃</a><a id="7093" class="Symbol">)</a> <a id="7095" class="Symbol">→</a>
<a id="7099" class="Symbol">(</a><a id="7100" href="Relation.Binary.On.html#7052" class="Bound">B</a> <a id="7102" class="Symbol">→</a> <a id="7104" href="Relation.Binary.html#StrictTotalOrder.Carrier" class="Field">StrictTotalOrder.Carrier</a> <a id="7129" href="Relation.Binary.On.html#7064" class="Bound">S</a><a id="7130" class="Symbol">)</a> <a id="7132" class="Symbol">→</a> <a id="7134" href="Relation.Binary.html#StrictTotalOrder" class="Record">StrictTotalOrder</a> <a id="7151" class="Symbol">_</a> <a id="7153" class="Symbol">_</a> <a id="7155" class="Symbol">_</a>
<a id="7157" href="Relation.Binary.On.html#strictTotalOrder" class="Function">strictTotalOrder</a> <a id="7174" href="Relation.Binary.On.html#7174" class="Bound">S</a> <a id="7176" href="Relation.Binary.On.html#7176" class="Bound">f</a> <a id="7178" class="Symbol">=</a> <a id="7180" class="Keyword">record</a>
<a id="7189" class="Symbol">{</a> <a id="7191" class="Field">isStrictTotalOrder</a> <a id="7210" class="Symbol">=</a>
<a id="7218" href="Relation.Binary.On.html#4842" class="Function">isStrictTotalOrder</a> <a id="7237" href="Relation.Binary.On.html#7176" class="Bound">f</a> <a id="7239" class="Symbol">(</a><a id="7240" href="Relation.Binary.html#StrictTotalOrder.isStrictTotalOrder" class="Field">StrictTotalOrder.isStrictTotalOrder</a> <a id="7276" href="Relation.Binary.On.html#7174" class="Bound">S</a><a id="7277" class="Symbol">)</a>
<a id="7281" class="Symbol">}</a>
</pre></body></html>
|