301 lines
63 KiB
HTML
301 lines
63 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Relation.Binary.Bundles</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="74" class="Comment">-- The Agda standard library</a>
|
||
<a id="103" class="Comment">--</a>
|
||
<a id="106" class="Comment">-- Bundles for homogeneous binary relations</a>
|
||
<a id="150" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="224" class="Comment">-- The contents of this module should be accessed via `Relation.Binary`.</a>
|
||
|
||
<a id="298" class="Symbol">{-#</a> <a id="302" class="Keyword">OPTIONS</a> <a id="310" class="Pragma">--without-K</a> <a id="322" class="Pragma">--safe</a> <a id="329" class="Symbol">#-}</a>
|
||
|
||
<a id="334" class="Keyword">module</a> <a id="341" href="Relation.Binary.Bundles.html" class="Module">Relation.Binary.Bundles</a> <a id="365" class="Keyword">where</a>
|
||
|
||
<a id="372" class="Keyword">open</a> <a id="377" class="Keyword">import</a> <a id="384" href="Level.html" class="Module">Level</a>
|
||
<a id="390" class="Keyword">open</a> <a id="395" class="Keyword">import</a> <a id="402" href="Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="419" class="Keyword">using</a> <a id="425" class="Symbol">(</a><a id="426" href="Relation.Nullary.html#656" class="Function Operator">¬_</a><a id="428" class="Symbol">)</a>
|
||
<a id="430" class="Keyword">open</a> <a id="435" class="Keyword">import</a> <a id="442" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a>
|
||
<a id="463" class="Keyword">open</a> <a id="468" class="Keyword">import</a> <a id="475" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a>
|
||
<a id="503" class="Keyword">open</a> <a id="508" class="Keyword">import</a> <a id="515" href="Relation.Binary.Structures.html" class="Module">Relation.Binary.Structures</a>
|
||
|
||
<a id="543" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="616" class="Comment">-- Setoids</a>
|
||
<a id="627" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="701" class="Keyword">record</a> <a id="PartialSetoid"></a><a id="708" href="Relation.Binary.Bundles.html#708" class="Record">PartialSetoid</a> <a id="722" href="Relation.Binary.Bundles.html#722" class="Bound">a</a> <a id="724" href="Relation.Binary.Bundles.html#724" class="Bound">ℓ</a> <a id="726" class="Symbol">:</a> <a id="728" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="732" class="Symbol">(</a><a id="733" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="737" class="Symbol">(</a><a id="738" href="Relation.Binary.Bundles.html#722" class="Bound">a</a> <a id="740" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="742" href="Relation.Binary.Bundles.html#724" class="Bound">ℓ</a><a id="743" class="Symbol">))</a> <a id="746" class="Keyword">where</a>
|
||
<a id="754" class="Keyword">field</a>
|
||
<a id="PartialSetoid.Carrier"></a><a id="764" href="Relation.Binary.Bundles.html#764" class="Field">Carrier</a> <a id="785" class="Symbol">:</a> <a id="787" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="791" href="Relation.Binary.Bundles.html#722" class="Bound">a</a>
|
||
<a id="PartialSetoid._≈_"></a><a id="797" href="Relation.Binary.Bundles.html#797" class="Field Operator">_≈_</a> <a id="818" class="Symbol">:</a> <a id="820" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="824" href="Relation.Binary.Bundles.html#764" class="Field">Carrier</a> <a id="832" href="Relation.Binary.Bundles.html#724" class="Bound">ℓ</a>
|
||
<a id="PartialSetoid.isPartialEquivalence"></a><a id="838" href="Relation.Binary.Bundles.html#838" class="Field">isPartialEquivalence</a> <a id="859" class="Symbol">:</a> <a id="861" href="Relation.Binary.Structures.html#1119" class="Record">IsPartialEquivalence</a> <a id="882" href="Relation.Binary.Bundles.html#797" class="Field Operator">_≈_</a>
|
||
|
||
<a id="889" class="Keyword">open</a> <a id="894" href="Relation.Binary.Structures.html#1119" class="Module">IsPartialEquivalence</a> <a id="915" href="Relation.Binary.Bundles.html#838" class="Field">isPartialEquivalence</a> <a id="936" class="Keyword">public</a>
|
||
|
||
<a id="946" class="Keyword">infix</a> <a id="952" class="Number">4</a> <a id="954" href="Relation.Binary.Bundles.html#960" class="Function Operator">_≉_</a>
|
||
<a id="PartialSetoid._≉_"></a><a id="960" href="Relation.Binary.Bundles.html#960" class="Function Operator">_≉_</a> <a id="964" class="Symbol">:</a> <a id="966" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="970" href="Relation.Binary.Bundles.html#764" class="Field">Carrier</a> <a id="978" class="Symbol">_</a>
|
||
<a id="982" href="Relation.Binary.Bundles.html#982" class="Bound">x</a> <a id="984" href="Relation.Binary.Bundles.html#960" class="Function Operator">≉</a> <a id="986" href="Relation.Binary.Bundles.html#986" class="Bound">y</a> <a id="988" class="Symbol">=</a> <a id="990" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="992" class="Symbol">(</a><a id="993" href="Relation.Binary.Bundles.html#982" class="Bound">x</a> <a id="995" href="Relation.Binary.Bundles.html#797" class="Field Operator">≈</a> <a id="997" href="Relation.Binary.Bundles.html#986" class="Bound">y</a><a id="998" class="Symbol">)</a>
|
||
|
||
|
||
<a id="1002" class="Keyword">record</a> <a id="Setoid"></a><a id="1009" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1016" href="Relation.Binary.Bundles.html#1016" class="Bound">c</a> <a id="1018" href="Relation.Binary.Bundles.html#1018" class="Bound">ℓ</a> <a id="1020" class="Symbol">:</a> <a id="1022" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1026" class="Symbol">(</a><a id="1027" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="1031" class="Symbol">(</a><a id="1032" href="Relation.Binary.Bundles.html#1016" class="Bound">c</a> <a id="1034" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1036" href="Relation.Binary.Bundles.html#1018" class="Bound">ℓ</a><a id="1037" class="Symbol">))</a> <a id="1040" class="Keyword">where</a>
|
||
<a id="1048" class="Keyword">infix</a> <a id="1054" class="Number">4</a> <a id="1056" href="Relation.Binary.Bundles.html#1098" class="Field Operator">_≈_</a>
|
||
<a id="1062" class="Keyword">field</a>
|
||
<a id="Setoid.Carrier"></a><a id="1072" href="Relation.Binary.Bundles.html#1072" class="Field">Carrier</a> <a id="1086" class="Symbol">:</a> <a id="1088" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1092" href="Relation.Binary.Bundles.html#1016" class="Bound">c</a>
|
||
<a id="Setoid._≈_"></a><a id="1098" href="Relation.Binary.Bundles.html#1098" class="Field Operator">_≈_</a> <a id="1112" class="Symbol">:</a> <a id="1114" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="1118" href="Relation.Binary.Bundles.html#1072" class="Field">Carrier</a> <a id="1126" href="Relation.Binary.Bundles.html#1018" class="Bound">ℓ</a>
|
||
<a id="Setoid.isEquivalence"></a><a id="1132" href="Relation.Binary.Bundles.html#1132" class="Field">isEquivalence</a> <a id="1146" class="Symbol">:</a> <a id="1148" href="Relation.Binary.Structures.html#1522" class="Record">IsEquivalence</a> <a id="1162" href="Relation.Binary.Bundles.html#1098" class="Field Operator">_≈_</a>
|
||
|
||
<a id="1169" class="Keyword">open</a> <a id="1174" href="Relation.Binary.Structures.html#1522" class="Module">IsEquivalence</a> <a id="1188" href="Relation.Binary.Bundles.html#1132" class="Field">isEquivalence</a> <a id="1202" class="Keyword">public</a>
|
||
|
||
<a id="Setoid.partialSetoid"></a><a id="1212" href="Relation.Binary.Bundles.html#1212" class="Function">partialSetoid</a> <a id="1226" class="Symbol">:</a> <a id="1228" href="Relation.Binary.Bundles.html#708" class="Record">PartialSetoid</a> <a id="1242" href="Relation.Binary.Bundles.html#1016" class="Bound">c</a> <a id="1244" href="Relation.Binary.Bundles.html#1018" class="Bound">ℓ</a>
|
||
<a id="1248" href="Relation.Binary.Bundles.html#1212" class="Function">partialSetoid</a> <a id="1262" class="Symbol">=</a> <a id="1264" class="Keyword">record</a>
|
||
<a id="1275" class="Symbol">{</a> <a id="1277" href="Relation.Binary.Bundles.html#838" class="Field">isPartialEquivalence</a> <a id="1298" class="Symbol">=</a> <a id="1300" href="Relation.Binary.Structures.html#1697" class="Function">isPartialEquivalence</a>
|
||
<a id="1325" class="Symbol">}</a>
|
||
|
||
<a id="1330" class="Keyword">open</a> <a id="1335" href="Relation.Binary.Bundles.html#708" class="Module">PartialSetoid</a> <a id="1349" href="Relation.Binary.Bundles.html#1212" class="Function">partialSetoid</a> <a id="1363" class="Keyword">public</a> <a id="1370" class="Keyword">using</a> <a id="1376" class="Symbol">(</a><a id="1377" href="Relation.Binary.Bundles.html#960" class="Function Operator">_≉_</a><a id="1380" class="Symbol">)</a>
|
||
|
||
|
||
<a id="1384" class="Keyword">record</a> <a id="DecSetoid"></a><a id="1391" href="Relation.Binary.Bundles.html#1391" class="Record">DecSetoid</a> <a id="1401" href="Relation.Binary.Bundles.html#1401" class="Bound">c</a> <a id="1403" href="Relation.Binary.Bundles.html#1403" class="Bound">ℓ</a> <a id="1405" class="Symbol">:</a> <a id="1407" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1411" class="Symbol">(</a><a id="1412" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="1416" class="Symbol">(</a><a id="1417" href="Relation.Binary.Bundles.html#1401" class="Bound">c</a> <a id="1419" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1421" href="Relation.Binary.Bundles.html#1403" class="Bound">ℓ</a><a id="1422" class="Symbol">))</a> <a id="1425" class="Keyword">where</a>
|
||
<a id="1433" class="Keyword">infix</a> <a id="1439" class="Number">4</a> <a id="1441" href="Relation.Binary.Bundles.html#1486" class="Field Operator">_≈_</a>
|
||
<a id="1447" class="Keyword">field</a>
|
||
<a id="DecSetoid.Carrier"></a><a id="1457" href="Relation.Binary.Bundles.html#1457" class="Field">Carrier</a> <a id="1474" class="Symbol">:</a> <a id="1476" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1480" href="Relation.Binary.Bundles.html#1401" class="Bound">c</a>
|
||
<a id="DecSetoid._≈_"></a><a id="1486" href="Relation.Binary.Bundles.html#1486" class="Field Operator">_≈_</a> <a id="1503" class="Symbol">:</a> <a id="1505" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="1509" href="Relation.Binary.Bundles.html#1457" class="Field">Carrier</a> <a id="1517" href="Relation.Binary.Bundles.html#1403" class="Bound">ℓ</a>
|
||
<a id="DecSetoid.isDecEquivalence"></a><a id="1523" href="Relation.Binary.Bundles.html#1523" class="Field">isDecEquivalence</a> <a id="1540" class="Symbol">:</a> <a id="1542" href="Relation.Binary.Structures.html#1824" class="Record">IsDecEquivalence</a> <a id="1559" href="Relation.Binary.Bundles.html#1486" class="Field Operator">_≈_</a>
|
||
|
||
<a id="1566" class="Keyword">open</a> <a id="1571" href="Relation.Binary.Structures.html#1824" class="Module">IsDecEquivalence</a> <a id="1588" href="Relation.Binary.Bundles.html#1523" class="Field">isDecEquivalence</a> <a id="1605" class="Keyword">public</a>
|
||
|
||
<a id="DecSetoid.setoid"></a><a id="1615" href="Relation.Binary.Bundles.html#1615" class="Function">setoid</a> <a id="1622" class="Symbol">:</a> <a id="1624" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1631" href="Relation.Binary.Bundles.html#1401" class="Bound">c</a> <a id="1633" href="Relation.Binary.Bundles.html#1403" class="Bound">ℓ</a>
|
||
<a id="1637" href="Relation.Binary.Bundles.html#1615" class="Function">setoid</a> <a id="1644" class="Symbol">=</a> <a id="1646" class="Keyword">record</a>
|
||
<a id="1657" class="Symbol">{</a> <a id="1659" href="Relation.Binary.Bundles.html#1132" class="Field">isEquivalence</a> <a id="1673" class="Symbol">=</a> <a id="1675" href="Relation.Binary.Structures.html#1887" class="Function">isEquivalence</a>
|
||
<a id="1693" class="Symbol">}</a>
|
||
|
||
<a id="1698" class="Keyword">open</a> <a id="1703" href="Relation.Binary.Bundles.html#1009" class="Module">Setoid</a> <a id="1710" href="Relation.Binary.Bundles.html#1615" class="Function">setoid</a> <a id="1717" class="Keyword">public</a> <a id="1724" class="Keyword">using</a> <a id="1730" class="Symbol">(</a><a id="1731" href="Relation.Binary.Bundles.html#1212" class="Function">partialSetoid</a><a id="1744" class="Symbol">;</a> <a id="1746" href="Relation.Binary.Bundles.html#960" class="Function Operator">_≉_</a><a id="1749" class="Symbol">)</a>
|
||
|
||
|
||
<a id="1753" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="1826" class="Comment">-- Preorders</a>
|
||
<a id="1839" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="1913" class="Keyword">record</a> <a id="Preorder"></a><a id="1920" href="Relation.Binary.Bundles.html#1920" class="Record">Preorder</a> <a id="1929" href="Relation.Binary.Bundles.html#1929" class="Bound">c</a> <a id="1931" href="Relation.Binary.Bundles.html#1931" class="Bound">ℓ₁</a> <a id="1934" href="Relation.Binary.Bundles.html#1934" class="Bound">ℓ₂</a> <a id="1937" class="Symbol">:</a> <a id="1939" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1943" class="Symbol">(</a><a id="1944" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="1948" class="Symbol">(</a><a id="1949" href="Relation.Binary.Bundles.html#1929" class="Bound">c</a> <a id="1951" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1953" href="Relation.Binary.Bundles.html#1931" class="Bound">ℓ₁</a> <a id="1956" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1958" href="Relation.Binary.Bundles.html#1934" class="Bound">ℓ₂</a><a id="1960" class="Symbol">))</a> <a id="1963" class="Keyword">where</a>
|
||
<a id="1971" class="Keyword">infix</a> <a id="1977" class="Number">4</a> <a id="1979" href="Relation.Binary.Bundles.html#2022" class="Field Operator">_≈_</a> <a id="1983" href="Relation.Binary.Bundles.html#2083" class="Field Operator">_∼_</a>
|
||
<a id="1989" class="Keyword">field</a>
|
||
<a id="Preorder.Carrier"></a><a id="1999" href="Relation.Binary.Bundles.html#1999" class="Field">Carrier</a> <a id="2010" class="Symbol">:</a> <a id="2012" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2016" href="Relation.Binary.Bundles.html#1929" class="Bound">c</a>
|
||
<a id="Preorder._≈_"></a><a id="2022" href="Relation.Binary.Bundles.html#2022" class="Field Operator">_≈_</a> <a id="2033" class="Symbol">:</a> <a id="2035" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="2039" href="Relation.Binary.Bundles.html#1999" class="Field">Carrier</a> <a id="2047" href="Relation.Binary.Bundles.html#1931" class="Bound">ℓ₁</a> <a id="2051" class="Comment">-- The underlying equality.</a>
|
||
<a id="Preorder._∼_"></a><a id="2083" href="Relation.Binary.Bundles.html#2083" class="Field Operator">_∼_</a> <a id="2094" class="Symbol">:</a> <a id="2096" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="2100" href="Relation.Binary.Bundles.html#1999" class="Field">Carrier</a> <a id="2108" href="Relation.Binary.Bundles.html#1934" class="Bound">ℓ₂</a> <a id="2112" class="Comment">-- The relation.</a>
|
||
<a id="Preorder.isPreorder"></a><a id="2133" href="Relation.Binary.Bundles.html#2133" class="Field">isPreorder</a> <a id="2144" class="Symbol">:</a> <a id="2146" href="Relation.Binary.Structures.html#2163" class="Record">IsPreorder</a> <a id="2157" href="Relation.Binary.Bundles.html#2022" class="Field Operator">_≈_</a> <a id="2161" href="Relation.Binary.Bundles.html#2083" class="Field Operator">_∼_</a>
|
||
|
||
<a id="2168" class="Keyword">open</a> <a id="2173" href="Relation.Binary.Structures.html#2163" class="Module">IsPreorder</a> <a id="2184" href="Relation.Binary.Bundles.html#2133" class="Field">isPreorder</a> <a id="2195" class="Keyword">public</a>
|
||
<a id="2206" class="Keyword">hiding</a> <a id="2213" class="Symbol">(</a><a id="2214" class="Keyword">module</a> <a id="2221" href="Relation.Binary.Structures.html#2402" class="Module">Eq</a><a id="2223" class="Symbol">)</a>
|
||
|
||
<a id="2228" class="Keyword">module</a> <a id="Preorder.Eq"></a><a id="2235" href="Relation.Binary.Bundles.html#2235" class="Module">Eq</a> <a id="2238" class="Keyword">where</a>
|
||
<a id="Preorder.Eq.setoid"></a><a id="2248" href="Relation.Binary.Bundles.html#2248" class="Function">setoid</a> <a id="2255" class="Symbol">:</a> <a id="2257" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="2264" href="Relation.Binary.Bundles.html#1929" class="Bound">c</a> <a id="2266" href="Relation.Binary.Bundles.html#1931" class="Bound">ℓ₁</a>
|
||
<a id="2273" href="Relation.Binary.Bundles.html#2248" class="Function">setoid</a> <a id="2280" class="Symbol">=</a> <a id="2282" class="Keyword">record</a>
|
||
<a id="2295" class="Symbol">{</a> <a id="2297" href="Relation.Binary.Bundles.html#1132" class="Field">isEquivalence</a> <a id="2311" class="Symbol">=</a> <a id="2313" href="Relation.Binary.Structures.html#2228" class="Function">isEquivalence</a>
|
||
<a id="2333" class="Symbol">}</a>
|
||
|
||
<a id="2340" class="Keyword">open</a> <a id="2345" href="Relation.Binary.Bundles.html#1009" class="Module">Setoid</a> <a id="2352" href="Relation.Binary.Bundles.html#2248" class="Function">setoid</a> <a id="2359" class="Keyword">public</a>
|
||
|
||
|
||
<a id="2368" class="Keyword">record</a> <a id="TotalPreorder"></a><a id="2375" href="Relation.Binary.Bundles.html#2375" class="Record">TotalPreorder</a> <a id="2389" href="Relation.Binary.Bundles.html#2389" class="Bound">c</a> <a id="2391" href="Relation.Binary.Bundles.html#2391" class="Bound">ℓ₁</a> <a id="2394" href="Relation.Binary.Bundles.html#2394" class="Bound">ℓ₂</a> <a id="2397" class="Symbol">:</a> <a id="2399" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2403" class="Symbol">(</a><a id="2404" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="2408" class="Symbol">(</a><a id="2409" href="Relation.Binary.Bundles.html#2389" class="Bound">c</a> <a id="2411" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2413" href="Relation.Binary.Bundles.html#2391" class="Bound">ℓ₁</a> <a id="2416" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2418" href="Relation.Binary.Bundles.html#2394" class="Bound">ℓ₂</a><a id="2420" class="Symbol">))</a> <a id="2423" class="Keyword">where</a>
|
||
<a id="2431" class="Keyword">infix</a> <a id="2437" class="Number">4</a> <a id="2439" href="Relation.Binary.Bundles.html#2487" class="Field Operator">_≈_</a> <a id="2443" href="Relation.Binary.Bundles.html#2553" class="Field Operator">_≲_</a>
|
||
<a id="2449" class="Keyword">field</a>
|
||
<a id="TotalPreorder.Carrier"></a><a id="2459" href="Relation.Binary.Bundles.html#2459" class="Field">Carrier</a> <a id="2475" class="Symbol">:</a> <a id="2477" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2481" href="Relation.Binary.Bundles.html#2389" class="Bound">c</a>
|
||
<a id="TotalPreorder._≈_"></a><a id="2487" href="Relation.Binary.Bundles.html#2487" class="Field Operator">_≈_</a> <a id="2503" class="Symbol">:</a> <a id="2505" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="2509" href="Relation.Binary.Bundles.html#2459" class="Field">Carrier</a> <a id="2517" href="Relation.Binary.Bundles.html#2391" class="Bound">ℓ₁</a> <a id="2521" class="Comment">-- The underlying equality.</a>
|
||
<a id="TotalPreorder._≲_"></a><a id="2553" href="Relation.Binary.Bundles.html#2553" class="Field Operator">_≲_</a> <a id="2569" class="Symbol">:</a> <a id="2571" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="2575" href="Relation.Binary.Bundles.html#2459" class="Field">Carrier</a> <a id="2583" href="Relation.Binary.Bundles.html#2394" class="Bound">ℓ₂</a> <a id="2587" class="Comment">-- The relation.</a>
|
||
<a id="TotalPreorder.isTotalPreorder"></a><a id="2608" href="Relation.Binary.Bundles.html#2608" class="Field">isTotalPreorder</a> <a id="2624" class="Symbol">:</a> <a id="2626" href="Relation.Binary.Structures.html#2733" class="Record">IsTotalPreorder</a> <a id="2642" href="Relation.Binary.Bundles.html#2487" class="Field Operator">_≈_</a> <a id="2646" href="Relation.Binary.Bundles.html#2553" class="Field Operator">_≲_</a>
|
||
|
||
<a id="2653" class="Keyword">open</a> <a id="2658" href="Relation.Binary.Structures.html#2733" class="Module">IsTotalPreorder</a> <a id="2674" href="Relation.Binary.Bundles.html#2608" class="Field">isTotalPreorder</a> <a id="2690" class="Keyword">public</a>
|
||
<a id="2701" class="Keyword">hiding</a> <a id="2708" class="Symbol">(</a><a id="2709" class="Keyword">module</a> <a id="2716" href="Relation.Binary.Structures.html#2402" class="Module">Eq</a><a id="2718" class="Symbol">)</a>
|
||
|
||
<a id="TotalPreorder.preorder"></a><a id="2723" href="Relation.Binary.Bundles.html#2723" class="Function">preorder</a> <a id="2732" class="Symbol">:</a> <a id="2734" href="Relation.Binary.Bundles.html#1920" class="Record">Preorder</a> <a id="2743" href="Relation.Binary.Bundles.html#2389" class="Bound">c</a> <a id="2745" href="Relation.Binary.Bundles.html#2391" class="Bound">ℓ₁</a> <a id="2748" href="Relation.Binary.Bundles.html#2394" class="Bound">ℓ₂</a>
|
||
<a id="2753" href="Relation.Binary.Bundles.html#2723" class="Function">preorder</a> <a id="2762" class="Symbol">=</a> <a id="2764" class="Keyword">record</a> <a id="2771" class="Symbol">{</a> <a id="2773" href="Relation.Binary.Bundles.html#2133" class="Field">isPreorder</a> <a id="2784" class="Symbol">=</a> <a id="2786" href="Relation.Binary.Structures.html#2803" class="Function">isPreorder</a> <a id="2797" class="Symbol">}</a>
|
||
|
||
<a id="2802" class="Keyword">open</a> <a id="2807" href="Relation.Binary.Bundles.html#1920" class="Module">Preorder</a> <a id="2816" href="Relation.Binary.Bundles.html#2723" class="Function">preorder</a> <a id="2825" class="Keyword">public</a>
|
||
<a id="2836" class="Keyword">using</a> <a id="2842" class="Symbol">(</a><a id="2843" class="Keyword">module</a> <a id="2850" href="Relation.Binary.Bundles.html#2235" class="Module">Eq</a><a id="2852" class="Symbol">)</a>
|
||
|
||
|
||
<a id="2856" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="2929" class="Comment">-- Partial orders</a>
|
||
<a id="2947" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="3021" class="Keyword">record</a> <a id="Poset"></a><a id="3028" href="Relation.Binary.Bundles.html#3028" class="Record">Poset</a> <a id="3034" href="Relation.Binary.Bundles.html#3034" class="Bound">c</a> <a id="3036" href="Relation.Binary.Bundles.html#3036" class="Bound">ℓ₁</a> <a id="3039" href="Relation.Binary.Bundles.html#3039" class="Bound">ℓ₂</a> <a id="3042" class="Symbol">:</a> <a id="3044" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3048" class="Symbol">(</a><a id="3049" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="3053" class="Symbol">(</a><a id="3054" href="Relation.Binary.Bundles.html#3034" class="Bound">c</a> <a id="3056" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3058" href="Relation.Binary.Bundles.html#3036" class="Bound">ℓ₁</a> <a id="3061" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3063" href="Relation.Binary.Bundles.html#3039" class="Bound">ℓ₂</a><a id="3065" class="Symbol">))</a> <a id="3068" class="Keyword">where</a>
|
||
<a id="3076" class="Keyword">infix</a> <a id="3082" class="Number">4</a> <a id="3084" href="Relation.Binary.Bundles.html#3131" class="Field Operator">_≈_</a> <a id="3088" href="Relation.Binary.Bundles.html#3167" class="Field Operator">_≤_</a>
|
||
<a id="3094" class="Keyword">field</a>
|
||
<a id="Poset.Carrier"></a><a id="3104" href="Relation.Binary.Bundles.html#3104" class="Field">Carrier</a> <a id="3119" class="Symbol">:</a> <a id="3121" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3125" href="Relation.Binary.Bundles.html#3034" class="Bound">c</a>
|
||
<a id="Poset._≈_"></a><a id="3131" href="Relation.Binary.Bundles.html#3131" class="Field Operator">_≈_</a> <a id="3146" class="Symbol">:</a> <a id="3148" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="3152" href="Relation.Binary.Bundles.html#3104" class="Field">Carrier</a> <a id="3160" href="Relation.Binary.Bundles.html#3036" class="Bound">ℓ₁</a>
|
||
<a id="Poset._≤_"></a><a id="3167" href="Relation.Binary.Bundles.html#3167" class="Field Operator">_≤_</a> <a id="3182" class="Symbol">:</a> <a id="3184" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="3188" href="Relation.Binary.Bundles.html#3104" class="Field">Carrier</a> <a id="3196" href="Relation.Binary.Bundles.html#3039" class="Bound">ℓ₂</a>
|
||
<a id="Poset.isPartialOrder"></a><a id="3203" href="Relation.Binary.Bundles.html#3203" class="Field">isPartialOrder</a> <a id="3218" class="Symbol">:</a> <a id="3220" href="Relation.Binary.Structures.html#3174" class="Record">IsPartialOrder</a> <a id="3235" href="Relation.Binary.Bundles.html#3131" class="Field Operator">_≈_</a> <a id="3239" href="Relation.Binary.Bundles.html#3167" class="Field Operator">_≤_</a>
|
||
|
||
<a id="3246" class="Keyword">open</a> <a id="3251" href="Relation.Binary.Structures.html#3174" class="Module">IsPartialOrder</a> <a id="3266" href="Relation.Binary.Bundles.html#3203" class="Field">isPartialOrder</a> <a id="3281" class="Keyword">public</a>
|
||
<a id="3292" class="Keyword">hiding</a> <a id="3299" class="Symbol">(</a><a id="3300" class="Keyword">module</a> <a id="3307" href="Relation.Binary.Structures.html#2402" class="Module">Eq</a><a id="3309" class="Symbol">)</a>
|
||
|
||
<a id="Poset.preorder"></a><a id="3314" href="Relation.Binary.Bundles.html#3314" class="Function">preorder</a> <a id="3323" class="Symbol">:</a> <a id="3325" href="Relation.Binary.Bundles.html#1920" class="Record">Preorder</a> <a id="3334" href="Relation.Binary.Bundles.html#3034" class="Bound">c</a> <a id="3336" href="Relation.Binary.Bundles.html#3036" class="Bound">ℓ₁</a> <a id="3339" href="Relation.Binary.Bundles.html#3039" class="Bound">ℓ₂</a>
|
||
<a id="3344" href="Relation.Binary.Bundles.html#3314" class="Function">preorder</a> <a id="3353" class="Symbol">=</a> <a id="3355" class="Keyword">record</a>
|
||
<a id="3366" class="Symbol">{</a> <a id="3368" href="Relation.Binary.Bundles.html#2133" class="Field">isPreorder</a> <a id="3379" class="Symbol">=</a> <a id="3381" href="Relation.Binary.Structures.html#3243" class="Function">isPreorder</a>
|
||
<a id="3396" class="Symbol">}</a>
|
||
|
||
<a id="3401" class="Keyword">open</a> <a id="3406" href="Relation.Binary.Bundles.html#1920" class="Module">Preorder</a> <a id="3415" href="Relation.Binary.Bundles.html#3314" class="Function">preorder</a> <a id="3424" class="Keyword">public</a>
|
||
<a id="3435" class="Keyword">using</a> <a id="3441" class="Symbol">(</a><a id="3442" class="Keyword">module</a> <a id="3449" href="Relation.Binary.Bundles.html#2235" class="Module">Eq</a><a id="3451" class="Symbol">)</a>
|
||
|
||
|
||
<a id="3455" class="Keyword">record</a> <a id="DecPoset"></a><a id="3462" href="Relation.Binary.Bundles.html#3462" class="Record">DecPoset</a> <a id="3471" href="Relation.Binary.Bundles.html#3471" class="Bound">c</a> <a id="3473" href="Relation.Binary.Bundles.html#3473" class="Bound">ℓ₁</a> <a id="3476" href="Relation.Binary.Bundles.html#3476" class="Bound">ℓ₂</a> <a id="3479" class="Symbol">:</a> <a id="3481" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3485" class="Symbol">(</a><a id="3486" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="3490" class="Symbol">(</a><a id="3491" href="Relation.Binary.Bundles.html#3471" class="Bound">c</a> <a id="3493" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3495" href="Relation.Binary.Bundles.html#3473" class="Bound">ℓ₁</a> <a id="3498" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3500" href="Relation.Binary.Bundles.html#3476" class="Bound">ℓ₂</a><a id="3502" class="Symbol">))</a> <a id="3505" class="Keyword">where</a>
|
||
<a id="3513" class="Keyword">infix</a> <a id="3519" class="Number">4</a> <a id="3521" href="Relation.Binary.Bundles.html#3571" class="Field Operator">_≈_</a> <a id="3525" href="Relation.Binary.Bundles.html#3610" class="Field Operator">_≤_</a>
|
||
<a id="3531" class="Keyword">field</a>
|
||
<a id="DecPoset.Carrier"></a><a id="3541" href="Relation.Binary.Bundles.html#3541" class="Field">Carrier</a> <a id="3559" class="Symbol">:</a> <a id="3561" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3565" href="Relation.Binary.Bundles.html#3471" class="Bound">c</a>
|
||
<a id="DecPoset._≈_"></a><a id="3571" href="Relation.Binary.Bundles.html#3571" class="Field Operator">_≈_</a> <a id="3589" class="Symbol">:</a> <a id="3591" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="3595" href="Relation.Binary.Bundles.html#3541" class="Field">Carrier</a> <a id="3603" href="Relation.Binary.Bundles.html#3473" class="Bound">ℓ₁</a>
|
||
<a id="DecPoset._≤_"></a><a id="3610" href="Relation.Binary.Bundles.html#3610" class="Field Operator">_≤_</a> <a id="3628" class="Symbol">:</a> <a id="3630" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="3634" href="Relation.Binary.Bundles.html#3541" class="Field">Carrier</a> <a id="3642" href="Relation.Binary.Bundles.html#3476" class="Bound">ℓ₂</a>
|
||
<a id="DecPoset.isDecPartialOrder"></a><a id="3649" href="Relation.Binary.Bundles.html#3649" class="Field">isDecPartialOrder</a> <a id="3667" class="Symbol">:</a> <a id="3669" href="Relation.Binary.Structures.html#3461" class="Record">IsDecPartialOrder</a> <a id="3687" href="Relation.Binary.Bundles.html#3571" class="Field Operator">_≈_</a> <a id="3691" href="Relation.Binary.Bundles.html#3610" class="Field Operator">_≤_</a>
|
||
|
||
<a id="3698" class="Keyword">private</a>
|
||
<a id="3710" class="Keyword">module</a> <a id="DecPoset.DPO"></a><a id="3717" href="Relation.Binary.Bundles.html#3717" class="Module">DPO</a> <a id="3721" class="Symbol">=</a> <a id="3723" href="Relation.Binary.Structures.html#3461" class="Module">IsDecPartialOrder</a> <a id="3741" href="Relation.Binary.Bundles.html#3649" class="Field">isDecPartialOrder</a>
|
||
<a id="3761" class="Keyword">open</a> <a id="3766" href="Relation.Binary.Bundles.html#3717" class="Module">DPO</a> <a id="3770" class="Keyword">public</a> <a id="3777" class="Keyword">hiding</a> <a id="3784" class="Symbol">(</a><a id="3785" class="Keyword">module</a> <a id="3792" href="Relation.Binary.Structures.html#3736" class="Module">Eq</a><a id="3794" class="Symbol">)</a>
|
||
|
||
<a id="DecPoset.poset"></a><a id="3799" href="Relation.Binary.Bundles.html#3799" class="Function">poset</a> <a id="3805" class="Symbol">:</a> <a id="3807" href="Relation.Binary.Bundles.html#3028" class="Record">Poset</a> <a id="3813" href="Relation.Binary.Bundles.html#3471" class="Bound">c</a> <a id="3815" href="Relation.Binary.Bundles.html#3473" class="Bound">ℓ₁</a> <a id="3818" href="Relation.Binary.Bundles.html#3476" class="Bound">ℓ₂</a>
|
||
<a id="3823" href="Relation.Binary.Bundles.html#3799" class="Function">poset</a> <a id="3829" class="Symbol">=</a> <a id="3831" class="Keyword">record</a>
|
||
<a id="3842" class="Symbol">{</a> <a id="3844" href="Relation.Binary.Bundles.html#3203" class="Field">isPartialOrder</a> <a id="3859" class="Symbol">=</a> <a id="3861" href="Relation.Binary.Structures.html#3552" class="Function">isPartialOrder</a>
|
||
<a id="3880" class="Symbol">}</a>
|
||
|
||
<a id="3885" class="Keyword">open</a> <a id="3890" href="Relation.Binary.Bundles.html#3028" class="Module">Poset</a> <a id="3896" href="Relation.Binary.Bundles.html#3799" class="Function">poset</a> <a id="3902" class="Keyword">public</a>
|
||
<a id="3913" class="Keyword">using</a> <a id="3919" class="Symbol">(</a><a id="3920" href="Relation.Binary.Bundles.html#3314" class="Function">preorder</a><a id="3928" class="Symbol">)</a>
|
||
|
||
<a id="3933" class="Keyword">module</a> <a id="DecPoset.Eq"></a><a id="3940" href="Relation.Binary.Bundles.html#3940" class="Module">Eq</a> <a id="3943" class="Keyword">where</a>
|
||
<a id="DecPoset.Eq.decSetoid"></a><a id="3953" href="Relation.Binary.Bundles.html#3953" class="Function">decSetoid</a> <a id="3963" class="Symbol">:</a> <a id="3965" href="Relation.Binary.Bundles.html#1391" class="Record">DecSetoid</a> <a id="3975" href="Relation.Binary.Bundles.html#3471" class="Bound">c</a> <a id="3977" href="Relation.Binary.Bundles.html#3473" class="Bound">ℓ₁</a>
|
||
<a id="3984" href="Relation.Binary.Bundles.html#3953" class="Function">decSetoid</a> <a id="3994" class="Symbol">=</a> <a id="3996" class="Keyword">record</a>
|
||
<a id="4009" class="Symbol">{</a> <a id="4011" href="Relation.Binary.Bundles.html#1523" class="Field">isDecEquivalence</a> <a id="4028" class="Symbol">=</a> <a id="4030" href="Relation.Binary.Structures.html#3750" class="Function">DPO.Eq.isDecEquivalence</a>
|
||
<a id="4060" class="Symbol">}</a>
|
||
|
||
<a id="4067" class="Keyword">open</a> <a id="4072" href="Relation.Binary.Bundles.html#1391" class="Module">DecSetoid</a> <a id="4082" href="Relation.Binary.Bundles.html#3953" class="Function">decSetoid</a> <a id="4092" class="Keyword">public</a>
|
||
|
||
|
||
<a id="4101" class="Keyword">record</a> <a id="StrictPartialOrder"></a><a id="4108" href="Relation.Binary.Bundles.html#4108" class="Record">StrictPartialOrder</a> <a id="4127" href="Relation.Binary.Bundles.html#4127" class="Bound">c</a> <a id="4129" href="Relation.Binary.Bundles.html#4129" class="Bound">ℓ₁</a> <a id="4132" href="Relation.Binary.Bundles.html#4132" class="Bound">ℓ₂</a> <a id="4135" class="Symbol">:</a> <a id="4137" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4141" class="Symbol">(</a><a id="4142" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="4146" class="Symbol">(</a><a id="4147" href="Relation.Binary.Bundles.html#4127" class="Bound">c</a> <a id="4149" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="4151" href="Relation.Binary.Bundles.html#4129" class="Bound">ℓ₁</a> <a id="4154" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="4156" href="Relation.Binary.Bundles.html#4132" class="Bound">ℓ₂</a><a id="4158" class="Symbol">))</a> <a id="4161" class="Keyword">where</a>
|
||
<a id="4169" class="Keyword">infix</a> <a id="4175" class="Number">4</a> <a id="4177" href="Relation.Binary.Bundles.html#4230" class="Field Operator">_≈_</a> <a id="4181" href="Relation.Binary.Bundles.html#4272" class="Field Operator">_<_</a>
|
||
<a id="4187" class="Keyword">field</a>
|
||
<a id="StrictPartialOrder.Carrier"></a><a id="4197" href="Relation.Binary.Bundles.html#4197" class="Field">Carrier</a> <a id="4218" class="Symbol">:</a> <a id="4220" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4224" href="Relation.Binary.Bundles.html#4127" class="Bound">c</a>
|
||
<a id="StrictPartialOrder._≈_"></a><a id="4230" href="Relation.Binary.Bundles.html#4230" class="Field Operator">_≈_</a> <a id="4251" class="Symbol">:</a> <a id="4253" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="4257" href="Relation.Binary.Bundles.html#4197" class="Field">Carrier</a> <a id="4265" href="Relation.Binary.Bundles.html#4129" class="Bound">ℓ₁</a>
|
||
<a id="StrictPartialOrder._<_"></a><a id="4272" href="Relation.Binary.Bundles.html#4272" class="Field Operator">_<_</a> <a id="4293" class="Symbol">:</a> <a id="4295" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="4299" href="Relation.Binary.Bundles.html#4197" class="Field">Carrier</a> <a id="4307" href="Relation.Binary.Bundles.html#4132" class="Bound">ℓ₂</a>
|
||
<a id="StrictPartialOrder.isStrictPartialOrder"></a><a id="4314" href="Relation.Binary.Bundles.html#4314" class="Field">isStrictPartialOrder</a> <a id="4335" class="Symbol">:</a> <a id="4337" href="Relation.Binary.Structures.html#3950" class="Record">IsStrictPartialOrder</a> <a id="4358" href="Relation.Binary.Bundles.html#4230" class="Field Operator">_≈_</a> <a id="4362" href="Relation.Binary.Bundles.html#4272" class="Field Operator">_<_</a>
|
||
|
||
<a id="4369" class="Keyword">open</a> <a id="4374" href="Relation.Binary.Structures.html#3950" class="Module">IsStrictPartialOrder</a> <a id="4395" href="Relation.Binary.Bundles.html#4314" class="Field">isStrictPartialOrder</a> <a id="4416" class="Keyword">public</a>
|
||
<a id="4427" class="Keyword">hiding</a> <a id="4434" class="Symbol">(</a><a id="4435" class="Keyword">module</a> <a id="4442" href="Relation.Binary.Structures.html#4178" class="Module">Eq</a><a id="4444" class="Symbol">)</a>
|
||
|
||
<a id="4449" class="Keyword">module</a> <a id="StrictPartialOrder.Eq"></a><a id="4456" href="Relation.Binary.Bundles.html#4456" class="Module">Eq</a> <a id="4459" class="Keyword">where</a>
|
||
<a id="StrictPartialOrder.Eq.setoid"></a><a id="4469" href="Relation.Binary.Bundles.html#4469" class="Function">setoid</a> <a id="4476" class="Symbol">:</a> <a id="4478" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="4485" href="Relation.Binary.Bundles.html#4127" class="Bound">c</a> <a id="4487" href="Relation.Binary.Bundles.html#4129" class="Bound">ℓ₁</a>
|
||
<a id="4494" href="Relation.Binary.Bundles.html#4469" class="Function">setoid</a> <a id="4501" class="Symbol">=</a> <a id="4503" class="Keyword">record</a>
|
||
<a id="4516" class="Symbol">{</a> <a id="4518" href="Relation.Binary.Bundles.html#1132" class="Field">isEquivalence</a> <a id="4532" class="Symbol">=</a> <a id="4534" href="Relation.Binary.Structures.html#4025" class="Function">isEquivalence</a>
|
||
<a id="4554" class="Symbol">}</a>
|
||
|
||
<a id="4561" class="Keyword">open</a> <a id="4566" href="Relation.Binary.Bundles.html#1009" class="Module">Setoid</a> <a id="4573" href="Relation.Binary.Bundles.html#4469" class="Function">setoid</a> <a id="4580" class="Keyword">public</a>
|
||
|
||
|
||
<a id="4589" class="Keyword">record</a> <a id="DecStrictPartialOrder"></a><a id="4596" href="Relation.Binary.Bundles.html#4596" class="Record">DecStrictPartialOrder</a> <a id="4618" href="Relation.Binary.Bundles.html#4618" class="Bound">c</a> <a id="4620" href="Relation.Binary.Bundles.html#4620" class="Bound">ℓ₁</a> <a id="4623" href="Relation.Binary.Bundles.html#4623" class="Bound">ℓ₂</a> <a id="4626" class="Symbol">:</a> <a id="4628" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4632" class="Symbol">(</a><a id="4633" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="4637" class="Symbol">(</a><a id="4638" href="Relation.Binary.Bundles.html#4618" class="Bound">c</a> <a id="4640" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="4642" href="Relation.Binary.Bundles.html#4620" class="Bound">ℓ₁</a> <a id="4645" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="4647" href="Relation.Binary.Bundles.html#4623" class="Bound">ℓ₂</a><a id="4649" class="Symbol">))</a> <a id="4652" class="Keyword">where</a>
|
||
<a id="4660" class="Keyword">infix</a> <a id="4666" class="Number">4</a> <a id="4668" href="Relation.Binary.Bundles.html#4724" class="Field Operator">_≈_</a> <a id="4672" href="Relation.Binary.Bundles.html#4769" class="Field Operator">_<_</a>
|
||
<a id="4678" class="Keyword">field</a>
|
||
<a id="DecStrictPartialOrder.Carrier"></a><a id="4688" href="Relation.Binary.Bundles.html#4688" class="Field">Carrier</a> <a id="4712" class="Symbol">:</a> <a id="4714" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4718" href="Relation.Binary.Bundles.html#4618" class="Bound">c</a>
|
||
<a id="DecStrictPartialOrder._≈_"></a><a id="4724" href="Relation.Binary.Bundles.html#4724" class="Field Operator">_≈_</a> <a id="4748" class="Symbol">:</a> <a id="4750" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="4754" href="Relation.Binary.Bundles.html#4688" class="Field">Carrier</a> <a id="4762" href="Relation.Binary.Bundles.html#4620" class="Bound">ℓ₁</a>
|
||
<a id="DecStrictPartialOrder._<_"></a><a id="4769" href="Relation.Binary.Bundles.html#4769" class="Field Operator">_<_</a> <a id="4793" class="Symbol">:</a> <a id="4795" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="4799" href="Relation.Binary.Bundles.html#4688" class="Field">Carrier</a> <a id="4807" href="Relation.Binary.Bundles.html#4623" class="Bound">ℓ₂</a>
|
||
<a id="DecStrictPartialOrder.isDecStrictPartialOrder"></a><a id="4814" href="Relation.Binary.Bundles.html#4814" class="Field">isDecStrictPartialOrder</a> <a id="4838" class="Symbol">:</a> <a id="4840" href="Relation.Binary.Structures.html#4571" class="Record">IsDecStrictPartialOrder</a> <a id="4864" href="Relation.Binary.Bundles.html#4724" class="Field Operator">_≈_</a> <a id="4868" href="Relation.Binary.Bundles.html#4769" class="Field Operator">_<_</a>
|
||
|
||
<a id="4875" class="Keyword">private</a>
|
||
<a id="4887" class="Keyword">module</a> <a id="DecStrictPartialOrder.DSPO"></a><a id="4894" href="Relation.Binary.Bundles.html#4894" class="Module">DSPO</a> <a id="4899" class="Symbol">=</a> <a id="4901" href="Relation.Binary.Structures.html#4571" class="Module">IsDecStrictPartialOrder</a> <a id="4925" href="Relation.Binary.Bundles.html#4814" class="Field">isDecStrictPartialOrder</a>
|
||
<a id="4951" class="Keyword">open</a> <a id="4956" href="Relation.Binary.Bundles.html#4894" class="Module">DSPO</a> <a id="4961" class="Keyword">public</a> <a id="4968" class="Keyword">hiding</a> <a id="4975" class="Symbol">(</a><a id="4976" class="Keyword">module</a> <a id="4983" href="Relation.Binary.Structures.html#4916" class="Module">Eq</a><a id="4985" class="Symbol">)</a>
|
||
|
||
<a id="DecStrictPartialOrder.strictPartialOrder"></a><a id="4990" href="Relation.Binary.Bundles.html#4990" class="Function">strictPartialOrder</a> <a id="5009" class="Symbol">:</a> <a id="5011" href="Relation.Binary.Bundles.html#4108" class="Record">StrictPartialOrder</a> <a id="5030" href="Relation.Binary.Bundles.html#4618" class="Bound">c</a> <a id="5032" href="Relation.Binary.Bundles.html#4620" class="Bound">ℓ₁</a> <a id="5035" href="Relation.Binary.Bundles.html#4623" class="Bound">ℓ₂</a>
|
||
<a id="5040" href="Relation.Binary.Bundles.html#4990" class="Function">strictPartialOrder</a> <a id="5059" class="Symbol">=</a> <a id="5061" class="Keyword">record</a>
|
||
<a id="5072" class="Symbol">{</a> <a id="5074" href="Relation.Binary.Bundles.html#4314" class="Field">isStrictPartialOrder</a> <a id="5095" class="Symbol">=</a> <a id="5097" href="Relation.Binary.Structures.html#4668" class="Function">isStrictPartialOrder</a>
|
||
<a id="5122" class="Symbol">}</a>
|
||
|
||
<a id="5127" class="Keyword">module</a> <a id="DecStrictPartialOrder.Eq"></a><a id="5134" href="Relation.Binary.Bundles.html#5134" class="Module">Eq</a> <a id="5137" class="Keyword">where</a>
|
||
|
||
<a id="DecStrictPartialOrder.Eq.decSetoid"></a><a id="5148" href="Relation.Binary.Bundles.html#5148" class="Function">decSetoid</a> <a id="5158" class="Symbol">:</a> <a id="5160" href="Relation.Binary.Bundles.html#1391" class="Record">DecSetoid</a> <a id="5170" href="Relation.Binary.Bundles.html#4618" class="Bound">c</a> <a id="5172" href="Relation.Binary.Bundles.html#4620" class="Bound">ℓ₁</a>
|
||
<a id="5179" href="Relation.Binary.Bundles.html#5148" class="Function">decSetoid</a> <a id="5189" class="Symbol">=</a> <a id="5191" class="Keyword">record</a>
|
||
<a id="5204" class="Symbol">{</a> <a id="5206" href="Relation.Binary.Bundles.html#1523" class="Field">isDecEquivalence</a> <a id="5223" class="Symbol">=</a> <a id="5225" href="Relation.Binary.Structures.html#4930" class="Function">DSPO.Eq.isDecEquivalence</a>
|
||
<a id="5256" class="Symbol">}</a>
|
||
|
||
<a id="5263" class="Keyword">open</a> <a id="5268" href="Relation.Binary.Bundles.html#1391" class="Module">DecSetoid</a> <a id="5278" href="Relation.Binary.Bundles.html#5148" class="Function">decSetoid</a> <a id="5288" class="Keyword">public</a>
|
||
|
||
|
||
<a id="5297" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="5370" class="Comment">-- Total orders</a>
|
||
<a id="5386" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="5460" class="Keyword">record</a> <a id="TotalOrder"></a><a id="5467" href="Relation.Binary.Bundles.html#5467" class="Record">TotalOrder</a> <a id="5478" href="Relation.Binary.Bundles.html#5478" class="Bound">c</a> <a id="5480" href="Relation.Binary.Bundles.html#5480" class="Bound">ℓ₁</a> <a id="5483" href="Relation.Binary.Bundles.html#5483" class="Bound">ℓ₂</a> <a id="5486" class="Symbol">:</a> <a id="5488" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5492" class="Symbol">(</a><a id="5493" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="5497" class="Symbol">(</a><a id="5498" href="Relation.Binary.Bundles.html#5478" class="Bound">c</a> <a id="5500" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="5502" href="Relation.Binary.Bundles.html#5480" class="Bound">ℓ₁</a> <a id="5505" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="5507" href="Relation.Binary.Bundles.html#5483" class="Bound">ℓ₂</a><a id="5509" class="Symbol">))</a> <a id="5512" class="Keyword">where</a>
|
||
<a id="5520" class="Keyword">infix</a> <a id="5526" class="Number">4</a> <a id="5528" href="Relation.Binary.Bundles.html#5573" class="Field Operator">_≈_</a> <a id="5532" href="Relation.Binary.Bundles.html#5607" class="Field Operator">_≤_</a>
|
||
<a id="5538" class="Keyword">field</a>
|
||
<a id="TotalOrder.Carrier"></a><a id="5548" href="Relation.Binary.Bundles.html#5548" class="Field">Carrier</a> <a id="5561" class="Symbol">:</a> <a id="5563" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5567" href="Relation.Binary.Bundles.html#5478" class="Bound">c</a>
|
||
<a id="TotalOrder._≈_"></a><a id="5573" href="Relation.Binary.Bundles.html#5573" class="Field Operator">_≈_</a> <a id="5586" class="Symbol">:</a> <a id="5588" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="5592" href="Relation.Binary.Bundles.html#5548" class="Field">Carrier</a> <a id="5600" href="Relation.Binary.Bundles.html#5480" class="Bound">ℓ₁</a>
|
||
<a id="TotalOrder._≤_"></a><a id="5607" href="Relation.Binary.Bundles.html#5607" class="Field Operator">_≤_</a> <a id="5620" class="Symbol">:</a> <a id="5622" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="5626" href="Relation.Binary.Bundles.html#5548" class="Field">Carrier</a> <a id="5634" href="Relation.Binary.Bundles.html#5483" class="Bound">ℓ₂</a>
|
||
<a id="TotalOrder.isTotalOrder"></a><a id="5641" href="Relation.Binary.Bundles.html#5641" class="Field">isTotalOrder</a> <a id="5654" class="Symbol">:</a> <a id="5656" href="Relation.Binary.Structures.html#5297" class="Record">IsTotalOrder</a> <a id="5669" href="Relation.Binary.Bundles.html#5573" class="Field Operator">_≈_</a> <a id="5673" href="Relation.Binary.Bundles.html#5607" class="Field Operator">_≤_</a>
|
||
|
||
<a id="5680" class="Keyword">open</a> <a id="5685" href="Relation.Binary.Structures.html#5297" class="Module">IsTotalOrder</a> <a id="5698" href="Relation.Binary.Bundles.html#5641" class="Field">isTotalOrder</a> <a id="5711" class="Keyword">public</a>
|
||
<a id="5722" class="Keyword">hiding</a> <a id="5729" class="Symbol">(</a><a id="5730" class="Keyword">module</a> <a id="5737" href="Relation.Binary.Structures.html#2402" class="Module">Eq</a><a id="5739" class="Symbol">)</a>
|
||
|
||
<a id="TotalOrder.poset"></a><a id="5744" href="Relation.Binary.Bundles.html#5744" class="Function">poset</a> <a id="5750" class="Symbol">:</a> <a id="5752" href="Relation.Binary.Bundles.html#3028" class="Record">Poset</a> <a id="5758" href="Relation.Binary.Bundles.html#5478" class="Bound">c</a> <a id="5760" href="Relation.Binary.Bundles.html#5480" class="Bound">ℓ₁</a> <a id="5763" href="Relation.Binary.Bundles.html#5483" class="Bound">ℓ₂</a>
|
||
<a id="5768" href="Relation.Binary.Bundles.html#5744" class="Function">poset</a> <a id="5774" class="Symbol">=</a> <a id="5776" class="Keyword">record</a>
|
||
<a id="5787" class="Symbol">{</a> <a id="5789" href="Relation.Binary.Bundles.html#3203" class="Field">isPartialOrder</a> <a id="5804" class="Symbol">=</a> <a id="5806" href="Relation.Binary.Structures.html#5364" class="Function">isPartialOrder</a>
|
||
<a id="5825" class="Symbol">}</a>
|
||
|
||
<a id="5830" class="Keyword">open</a> <a id="5835" href="Relation.Binary.Bundles.html#3028" class="Module">Poset</a> <a id="5841" href="Relation.Binary.Bundles.html#5744" class="Function">poset</a> <a id="5847" class="Keyword">public</a>
|
||
<a id="5858" class="Keyword">using</a> <a id="5864" class="Symbol">(</a><a id="5865" class="Keyword">module</a> <a id="5872" href="Relation.Binary.Bundles.html#2235" class="Module">Eq</a><a id="5874" class="Symbol">;</a> <a id="5876" href="Relation.Binary.Bundles.html#3314" class="Function">preorder</a><a id="5884" class="Symbol">)</a>
|
||
|
||
<a id="TotalOrder.totalPreorder"></a><a id="5889" href="Relation.Binary.Bundles.html#5889" class="Function">totalPreorder</a> <a id="5903" class="Symbol">:</a> <a id="5905" href="Relation.Binary.Bundles.html#2375" class="Record">TotalPreorder</a> <a id="5919" href="Relation.Binary.Bundles.html#5478" class="Bound">c</a> <a id="5921" href="Relation.Binary.Bundles.html#5480" class="Bound">ℓ₁</a> <a id="5924" href="Relation.Binary.Bundles.html#5483" class="Bound">ℓ₂</a>
|
||
<a id="5929" href="Relation.Binary.Bundles.html#5889" class="Function">totalPreorder</a> <a id="5943" class="Symbol">=</a> <a id="5945" class="Keyword">record</a>
|
||
<a id="5956" class="Symbol">{</a> <a id="5958" href="Relation.Binary.Bundles.html#2608" class="Field">isTotalPreorder</a> <a id="5974" class="Symbol">=</a> <a id="5976" href="Relation.Binary.Structures.html#5479" class="Function">isTotalPreorder</a>
|
||
<a id="5996" class="Symbol">}</a>
|
||
|
||
|
||
<a id="6000" class="Keyword">record</a> <a id="DecTotalOrder"></a><a id="6007" href="Relation.Binary.Bundles.html#6007" class="Record">DecTotalOrder</a> <a id="6021" href="Relation.Binary.Bundles.html#6021" class="Bound">c</a> <a id="6023" href="Relation.Binary.Bundles.html#6023" class="Bound">ℓ₁</a> <a id="6026" href="Relation.Binary.Bundles.html#6026" class="Bound">ℓ₂</a> <a id="6029" class="Symbol">:</a> <a id="6031" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="6035" class="Symbol">(</a><a id="6036" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="6040" class="Symbol">(</a><a id="6041" href="Relation.Binary.Bundles.html#6021" class="Bound">c</a> <a id="6043" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="6045" href="Relation.Binary.Bundles.html#6023" class="Bound">ℓ₁</a> <a id="6048" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="6050" href="Relation.Binary.Bundles.html#6026" class="Bound">ℓ₂</a><a id="6052" class="Symbol">))</a> <a id="6055" class="Keyword">where</a>
|
||
<a id="6063" class="Keyword">infix</a> <a id="6069" class="Number">4</a> <a id="6071" href="Relation.Binary.Bundles.html#6119" class="Field Operator">_≈_</a> <a id="6075" href="Relation.Binary.Bundles.html#6156" class="Field Operator">_≤_</a>
|
||
<a id="6081" class="Keyword">field</a>
|
||
<a id="DecTotalOrder.Carrier"></a><a id="6091" href="Relation.Binary.Bundles.html#6091" class="Field">Carrier</a> <a id="6107" class="Symbol">:</a> <a id="6109" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="6113" href="Relation.Binary.Bundles.html#6021" class="Bound">c</a>
|
||
<a id="DecTotalOrder._≈_"></a><a id="6119" href="Relation.Binary.Bundles.html#6119" class="Field Operator">_≈_</a> <a id="6135" class="Symbol">:</a> <a id="6137" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="6141" href="Relation.Binary.Bundles.html#6091" class="Field">Carrier</a> <a id="6149" href="Relation.Binary.Bundles.html#6023" class="Bound">ℓ₁</a>
|
||
<a id="DecTotalOrder._≤_"></a><a id="6156" href="Relation.Binary.Bundles.html#6156" class="Field Operator">_≤_</a> <a id="6172" class="Symbol">:</a> <a id="6174" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="6178" href="Relation.Binary.Bundles.html#6091" class="Field">Carrier</a> <a id="6186" href="Relation.Binary.Bundles.html#6026" class="Bound">ℓ₂</a>
|
||
<a id="DecTotalOrder.isDecTotalOrder"></a><a id="6193" href="Relation.Binary.Bundles.html#6193" class="Field">isDecTotalOrder</a> <a id="6209" class="Symbol">:</a> <a id="6211" href="Relation.Binary.Structures.html#5614" class="Record">IsDecTotalOrder</a> <a id="6227" href="Relation.Binary.Bundles.html#6119" class="Field Operator">_≈_</a> <a id="6231" href="Relation.Binary.Bundles.html#6156" class="Field Operator">_≤_</a>
|
||
|
||
<a id="6238" class="Keyword">private</a>
|
||
<a id="6250" class="Keyword">module</a> <a id="DecTotalOrder.DTO"></a><a id="6257" href="Relation.Binary.Bundles.html#6257" class="Module">DTO</a> <a id="6261" class="Symbol">=</a> <a id="6263" href="Relation.Binary.Structures.html#5614" class="Module">IsDecTotalOrder</a> <a id="6279" href="Relation.Binary.Bundles.html#6193" class="Field">isDecTotalOrder</a>
|
||
<a id="6297" class="Keyword">open</a> <a id="6302" href="Relation.Binary.Bundles.html#6257" class="Module">DTO</a> <a id="6306" class="Keyword">public</a> <a id="6313" class="Keyword">hiding</a> <a id="6320" class="Symbol">(</a><a id="6321" class="Keyword">module</a> <a id="6328" href="Relation.Binary.Structures.html#6048" class="Module">Eq</a><a id="6330" class="Symbol">)</a>
|
||
|
||
<a id="DecTotalOrder.totalOrder"></a><a id="6335" href="Relation.Binary.Bundles.html#6335" class="Function">totalOrder</a> <a id="6346" class="Symbol">:</a> <a id="6348" href="Relation.Binary.Bundles.html#5467" class="Record">TotalOrder</a> <a id="6359" href="Relation.Binary.Bundles.html#6021" class="Bound">c</a> <a id="6361" href="Relation.Binary.Bundles.html#6023" class="Bound">ℓ₁</a> <a id="6364" href="Relation.Binary.Bundles.html#6026" class="Bound">ℓ₂</a>
|
||
<a id="6369" href="Relation.Binary.Bundles.html#6335" class="Function">totalOrder</a> <a id="6380" class="Symbol">=</a> <a id="6382" class="Keyword">record</a>
|
||
<a id="6393" class="Symbol">{</a> <a id="6395" href="Relation.Binary.Bundles.html#5641" class="Field">isTotalOrder</a> <a id="6408" class="Symbol">=</a> <a id="6410" href="Relation.Binary.Structures.html#5703" class="Function">isTotalOrder</a>
|
||
<a id="6427" class="Symbol">}</a>
|
||
|
||
<a id="6432" class="Keyword">open</a> <a id="6437" href="Relation.Binary.Bundles.html#5467" class="Module">TotalOrder</a> <a id="6448" href="Relation.Binary.Bundles.html#6335" class="Function">totalOrder</a> <a id="6459" class="Keyword">public</a> <a id="6466" class="Keyword">using</a> <a id="6472" class="Symbol">(</a><a id="6473" href="Relation.Binary.Bundles.html#5744" class="Function">poset</a><a id="6478" class="Symbol">;</a> <a id="6480" href="Relation.Binary.Bundles.html#3314" class="Function">preorder</a><a id="6488" class="Symbol">)</a>
|
||
|
||
<a id="DecTotalOrder.decPoset"></a><a id="6493" href="Relation.Binary.Bundles.html#6493" class="Function">decPoset</a> <a id="6502" class="Symbol">:</a> <a id="6504" href="Relation.Binary.Bundles.html#3462" class="Record">DecPoset</a> <a id="6513" href="Relation.Binary.Bundles.html#6021" class="Bound">c</a> <a id="6515" href="Relation.Binary.Bundles.html#6023" class="Bound">ℓ₁</a> <a id="6518" href="Relation.Binary.Bundles.html#6026" class="Bound">ℓ₂</a>
|
||
<a id="6523" href="Relation.Binary.Bundles.html#6493" class="Function">decPoset</a> <a id="6532" class="Symbol">=</a> <a id="6534" class="Keyword">record</a>
|
||
<a id="6545" class="Symbol">{</a> <a id="6547" href="Relation.Binary.Bundles.html#3649" class="Field">isDecPartialOrder</a> <a id="6565" class="Symbol">=</a> <a id="6567" href="Relation.Binary.Structures.html#5868" class="Function">isDecPartialOrder</a>
|
||
<a id="6589" class="Symbol">}</a>
|
||
|
||
<a id="6594" class="Keyword">open</a> <a id="6599" href="Relation.Binary.Bundles.html#3462" class="Module">DecPoset</a> <a id="6608" href="Relation.Binary.Bundles.html#6493" class="Function">decPoset</a> <a id="6617" class="Keyword">public</a> <a id="6624" class="Keyword">using</a> <a id="6630" class="Symbol">(</a><a id="6631" class="Keyword">module</a> <a id="6638" href="Relation.Binary.Bundles.html#3940" class="Module">Eq</a><a id="6640" class="Symbol">)</a>
|
||
|
||
|
||
<a id="6644" class="Comment">-- Note that these orders are decidable. The current implementation</a>
|
||
<a id="6712" class="Comment">-- of `Trichotomous` subsumes irreflexivity and asymmetry. Any reasonable</a>
|
||
<a id="6786" class="Comment">-- definition capturing these three properties implies decidability</a>
|
||
<a id="6854" class="Comment">-- as `Trichotomous` necessarily separates out the equality case.</a>
|
||
|
||
<a id="6921" class="Keyword">record</a> <a id="StrictTotalOrder"></a><a id="6928" href="Relation.Binary.Bundles.html#6928" class="Record">StrictTotalOrder</a> <a id="6945" href="Relation.Binary.Bundles.html#6945" class="Bound">c</a> <a id="6947" href="Relation.Binary.Bundles.html#6947" class="Bound">ℓ₁</a> <a id="6950" href="Relation.Binary.Bundles.html#6950" class="Bound">ℓ₂</a> <a id="6953" class="Symbol">:</a> <a id="6955" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="6959" class="Symbol">(</a><a id="6960" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="6964" class="Symbol">(</a><a id="6965" href="Relation.Binary.Bundles.html#6945" class="Bound">c</a> <a id="6967" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="6969" href="Relation.Binary.Bundles.html#6947" class="Bound">ℓ₁</a> <a id="6972" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="6974" href="Relation.Binary.Bundles.html#6950" class="Bound">ℓ₂</a><a id="6976" class="Symbol">))</a> <a id="6979" class="Keyword">where</a>
|
||
<a id="6987" class="Keyword">infix</a> <a id="6993" class="Number">4</a> <a id="6995" href="Relation.Binary.Bundles.html#7046" class="Field Operator">_≈_</a> <a id="6999" href="Relation.Binary.Bundles.html#7086" class="Field Operator">_<_</a>
|
||
<a id="7005" class="Keyword">field</a>
|
||
<a id="StrictTotalOrder.Carrier"></a><a id="7015" href="Relation.Binary.Bundles.html#7015" class="Field">Carrier</a> <a id="7034" class="Symbol">:</a> <a id="7036" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="7040" href="Relation.Binary.Bundles.html#6945" class="Bound">c</a>
|
||
<a id="StrictTotalOrder._≈_"></a><a id="7046" href="Relation.Binary.Bundles.html#7046" class="Field Operator">_≈_</a> <a id="7065" class="Symbol">:</a> <a id="7067" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="7071" href="Relation.Binary.Bundles.html#7015" class="Field">Carrier</a> <a id="7079" href="Relation.Binary.Bundles.html#6947" class="Bound">ℓ₁</a>
|
||
<a id="StrictTotalOrder._<_"></a><a id="7086" href="Relation.Binary.Bundles.html#7086" class="Field Operator">_<_</a> <a id="7105" class="Symbol">:</a> <a id="7107" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="7111" href="Relation.Binary.Bundles.html#7015" class="Field">Carrier</a> <a id="7119" href="Relation.Binary.Bundles.html#6950" class="Bound">ℓ₂</a>
|
||
<a id="StrictTotalOrder.isStrictTotalOrder"></a><a id="7126" href="Relation.Binary.Bundles.html#7126" class="Field">isStrictTotalOrder</a> <a id="7145" class="Symbol">:</a> <a id="7147" href="Relation.Binary.Structures.html#6539" class="Record">IsStrictTotalOrder</a> <a id="7166" href="Relation.Binary.Bundles.html#7046" class="Field Operator">_≈_</a> <a id="7170" href="Relation.Binary.Bundles.html#7086" class="Field Operator">_<_</a>
|
||
|
||
<a id="7177" class="Keyword">open</a> <a id="7182" href="Relation.Binary.Structures.html#6539" class="Module">IsStrictTotalOrder</a> <a id="7201" href="Relation.Binary.Bundles.html#7126" class="Field">isStrictTotalOrder</a> <a id="7220" class="Keyword">public</a>
|
||
<a id="7231" class="Keyword">hiding</a> <a id="7238" class="Symbol">(</a><a id="7239" class="Keyword">module</a> <a id="7246" href="Relation.Binary.Structures.html#6981" class="Module">Eq</a><a id="7248" class="Symbol">)</a>
|
||
|
||
<a id="StrictTotalOrder.strictPartialOrder"></a><a id="7253" href="Relation.Binary.Bundles.html#7253" class="Function">strictPartialOrder</a> <a id="7272" class="Symbol">:</a> <a id="7274" href="Relation.Binary.Bundles.html#4108" class="Record">StrictPartialOrder</a> <a id="7293" href="Relation.Binary.Bundles.html#6945" class="Bound">c</a> <a id="7295" href="Relation.Binary.Bundles.html#6947" class="Bound">ℓ₁</a> <a id="7298" href="Relation.Binary.Bundles.html#6950" class="Bound">ℓ₂</a>
|
||
<a id="7303" href="Relation.Binary.Bundles.html#7253" class="Function">strictPartialOrder</a> <a id="7322" class="Symbol">=</a> <a id="7324" class="Keyword">record</a>
|
||
<a id="7335" class="Symbol">{</a> <a id="7337" href="Relation.Binary.Bundles.html#4314" class="Field">isStrictPartialOrder</a> <a id="7358" class="Symbol">=</a> <a id="7360" href="Relation.Binary.Structures.html#7023" class="Function">isStrictPartialOrder</a>
|
||
<a id="7385" class="Symbol">}</a>
|
||
|
||
<a id="7390" class="Keyword">open</a> <a id="7395" href="Relation.Binary.Bundles.html#4108" class="Module">StrictPartialOrder</a> <a id="7414" href="Relation.Binary.Bundles.html#7253" class="Function">strictPartialOrder</a> <a id="7433" class="Keyword">public</a>
|
||
<a id="7444" class="Keyword">using</a> <a id="7450" class="Symbol">(</a><a id="7451" class="Keyword">module</a> <a id="7458" href="Relation.Binary.Bundles.html#4456" class="Module">Eq</a><a id="7460" class="Symbol">)</a>
|
||
|
||
<a id="StrictTotalOrder.decSetoid"></a><a id="7465" href="Relation.Binary.Bundles.html#7465" class="Function">decSetoid</a> <a id="7475" class="Symbol">:</a> <a id="7477" href="Relation.Binary.Bundles.html#1391" class="Record">DecSetoid</a> <a id="7487" href="Relation.Binary.Bundles.html#6945" class="Bound">c</a> <a id="7489" href="Relation.Binary.Bundles.html#6947" class="Bound">ℓ₁</a>
|
||
<a id="7494" href="Relation.Binary.Bundles.html#7465" class="Function">decSetoid</a> <a id="7504" class="Symbol">=</a> <a id="7506" class="Keyword">record</a>
|
||
<a id="7517" class="Symbol">{</a> <a id="7519" href="Relation.Binary.Bundles.html#1523" class="Field">isDecEquivalence</a> <a id="7536" class="Symbol">=</a> <a id="7538" href="Relation.Binary.Structures.html#6839" class="Function">isDecEquivalence</a>
|
||
<a id="7559" class="Symbol">}</a>
|
||
<a id="7563" class="Symbol">{-#</a> <a id="7567" class="Keyword">WARNING_ON_USAGE</a> <a id="7584" class="Pragma">decSetoid</a>
|
||
<a id="7596" class="String">"Warning: decSetoid was deprecated in v1.3.
|
||
Please use Eq.decSetoid instead."</a>
|
||
<a id="7678" class="Symbol">#-}</a>
|
||
</pre></body></html> |