288 lines
59 KiB
HTML
288 lines
59 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Relation.Binary.Structures</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">-- Structures for homogeneous binary relations</a>
|
||
<a id="153" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="227" class="Comment">-- The contents of this module should be accessed via `Relation.Binary`.</a>
|
||
|
||
<a id="301" class="Symbol">{-#</a> <a id="305" class="Keyword">OPTIONS</a> <a id="313" class="Pragma">--without-K</a> <a id="325" class="Pragma">--safe</a> <a id="332" class="Symbol">#-}</a>
|
||
|
||
<a id="337" class="Keyword">open</a> <a id="342" class="Keyword">import</a> <a id="349" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a>
|
||
|
||
<a id="371" class="Keyword">module</a> <a id="378" href="Relation.Binary.Structures.html" class="Module">Relation.Binary.Structures</a>
|
||
<a id="407" class="Symbol">{</a><a id="408" href="Relation.Binary.Structures.html#408" class="Bound">a</a> <a id="410" href="Relation.Binary.Structures.html#410" class="Bound">ℓ</a><a id="411" class="Symbol">}</a> <a id="413" class="Symbol">{</a><a id="414" href="Relation.Binary.Structures.html#414" class="Bound">A</a> <a id="416" class="Symbol">:</a> <a id="418" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="422" href="Relation.Binary.Structures.html#408" class="Bound">a</a><a id="423" class="Symbol">}</a> <a id="425" class="Comment">-- The underlying set</a>
|
||
<a id="449" class="Symbol">(</a><a id="450" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a> <a id="454" class="Symbol">:</a> <a id="456" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="460" href="Relation.Binary.Structures.html#414" class="Bound">A</a> <a id="462" href="Relation.Binary.Structures.html#410" class="Bound">ℓ</a><a id="463" class="Symbol">)</a> <a id="467" class="Comment">-- The underlying equality relation</a>
|
||
<a id="505" class="Keyword">where</a>
|
||
|
||
<a id="512" class="Keyword">open</a> <a id="517" class="Keyword">import</a> <a id="524" href="Data.Product.html" class="Module">Data.Product</a> <a id="537" class="Keyword">using</a> <a id="543" class="Symbol">(</a><a id="544" href="Agda.Builtin.Sigma.html#252" class="Field">proj₁</a><a id="549" class="Symbol">;</a> <a id="551" href="Agda.Builtin.Sigma.html#264" class="Field">proj₂</a><a id="556" class="Symbol">;</a> <a id="558" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">_,_</a><a id="561" class="Symbol">)</a>
|
||
<a id="563" class="Keyword">open</a> <a id="568" class="Keyword">import</a> <a id="575" href="Level.html" class="Module">Level</a> <a id="581" class="Keyword">using</a> <a id="587" class="Symbol">(</a><a id="588" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="593" class="Symbol">;</a> <a id="595" href="Agda.Primitive.html#810" class="Primitive Operator">_⊔_</a><a id="598" class="Symbol">)</a>
|
||
<a id="600" class="Keyword">open</a> <a id="605" class="Keyword">import</a> <a id="612" href="Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="629" class="Keyword">using</a> <a id="635" class="Symbol">(</a><a id="636" href="Relation.Nullary.html#656" class="Function Operator">¬_</a><a id="638" class="Symbol">)</a>
|
||
<a id="640" class="Keyword">open</a> <a id="645" class="Keyword">import</a> <a id="652" href="Relation.Binary.PropositionalEquality.Core.html" class="Module">Relation.Binary.PropositionalEquality.Core</a> <a id="695" class="Symbol">as</a> <a id="698" class="Module">P</a> <a id="700" class="Keyword">using</a> <a id="706" class="Symbol">(</a><a id="707" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a><a id="710" class="Symbol">)</a>
|
||
<a id="712" class="Keyword">open</a> <a id="717" class="Keyword">import</a> <a id="724" href="Relation.Binary.Consequences.html" class="Module">Relation.Binary.Consequences</a>
|
||
<a id="753" class="Keyword">open</a> <a id="758" class="Keyword">import</a> <a id="765" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a>
|
||
|
||
<a id="794" class="Keyword">private</a>
|
||
<a id="804" class="Keyword">variable</a>
|
||
<a id="817" href="Relation.Binary.Structures.html#817" class="Generalizable">ℓ₂</a> <a id="820" class="Symbol">:</a> <a id="822" href="Agda.Primitive.html#597" class="Postulate">Level</a>
|
||
|
||
<a id="829" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="902" class="Comment">-- Equivalences</a>
|
||
<a id="918" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="991" class="Comment">-- Note all the following equivalences refer to the equality provided</a>
|
||
<a id="1061" class="Comment">-- as a module parameter at the top of this file.</a>
|
||
|
||
<a id="1112" class="Keyword">record</a> <a id="IsPartialEquivalence"></a><a id="1119" href="Relation.Binary.Structures.html#1119" class="Record">IsPartialEquivalence</a> <a id="1140" class="Symbol">:</a> <a id="1142" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1146" class="Symbol">(</a><a id="1147" href="Relation.Binary.Structures.html#408" class="Bound">a</a> <a id="1149" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1151" href="Relation.Binary.Structures.html#410" class="Bound">ℓ</a><a id="1152" class="Symbol">)</a> <a id="1154" class="Keyword">where</a>
|
||
<a id="1162" class="Keyword">field</a>
|
||
<a id="IsPartialEquivalence.sym"></a><a id="1172" href="Relation.Binary.Structures.html#1172" class="Field">sym</a> <a id="1178" class="Symbol">:</a> <a id="1180" href="Relation.Binary.Definitions.html#1498" class="Function">Symmetric</a> <a id="1190" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
<a id="IsPartialEquivalence.trans"></a><a id="1198" href="Relation.Binary.Structures.html#1198" class="Field">trans</a> <a id="1204" class="Symbol">:</a> <a id="1206" href="Relation.Binary.Definitions.html#1866" class="Function">Transitive</a> <a id="1217" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
|
||
<a id="1222" class="Comment">-- The preorders of this library are defined in terms of an underlying</a>
|
||
<a id="1293" class="Comment">-- equivalence relation, and hence equivalence relations are not</a>
|
||
<a id="1358" class="Comment">-- defined in terms of preorders.</a>
|
||
|
||
<a id="1393" class="Comment">-- To preserve backwards compatability, equivalence relations are</a>
|
||
<a id="1459" class="Comment">-- not defined in terms of their partial counterparts.</a>
|
||
|
||
<a id="1515" class="Keyword">record</a> <a id="IsEquivalence"></a><a id="1522" href="Relation.Binary.Structures.html#1522" class="Record">IsEquivalence</a> <a id="1536" class="Symbol">:</a> <a id="1538" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1542" class="Symbol">(</a><a id="1543" href="Relation.Binary.Structures.html#408" class="Bound">a</a> <a id="1545" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1547" href="Relation.Binary.Structures.html#410" class="Bound">ℓ</a><a id="1548" class="Symbol">)</a> <a id="1550" class="Keyword">where</a>
|
||
<a id="1558" class="Keyword">field</a>
|
||
<a id="IsEquivalence.refl"></a><a id="1568" href="Relation.Binary.Structures.html#1568" class="Field">refl</a> <a id="1574" class="Symbol">:</a> <a id="1576" href="Relation.Binary.Definitions.html#1339" class="Function">Reflexive</a> <a id="1586" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
<a id="IsEquivalence.sym"></a><a id="1594" href="Relation.Binary.Structures.html#1594" class="Field">sym</a> <a id="1600" class="Symbol">:</a> <a id="1602" href="Relation.Binary.Definitions.html#1498" class="Function">Symmetric</a> <a id="1612" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
<a id="IsEquivalence.trans"></a><a id="1620" href="Relation.Binary.Structures.html#1620" class="Field">trans</a> <a id="1626" class="Symbol">:</a> <a id="1628" href="Relation.Binary.Definitions.html#1866" class="Function">Transitive</a> <a id="1639" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
|
||
<a id="IsEquivalence.reflexive"></a><a id="1646" href="Relation.Binary.Structures.html#1646" class="Function">reflexive</a> <a id="1656" class="Symbol">:</a> <a id="1658" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a> <a id="1662" href="Relation.Binary.Core.html#1254" class="Function Operator">⇒</a> <a id="1664" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
<a id="1670" href="Relation.Binary.Structures.html#1646" class="Function">reflexive</a> <a id="1680" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">P.refl</a> <a id="1687" class="Symbol">=</a> <a id="1689" href="Relation.Binary.Structures.html#1568" class="Field">refl</a>
|
||
|
||
<a id="IsEquivalence.isPartialEquivalence"></a><a id="1697" href="Relation.Binary.Structures.html#1697" class="Function">isPartialEquivalence</a> <a id="1718" class="Symbol">:</a> <a id="1720" href="Relation.Binary.Structures.html#1119" class="Record">IsPartialEquivalence</a>
|
||
<a id="1743" href="Relation.Binary.Structures.html#1697" class="Function">isPartialEquivalence</a> <a id="1764" class="Symbol">=</a> <a id="1766" class="Keyword">record</a>
|
||
<a id="1777" class="Symbol">{</a> <a id="1779" href="Relation.Binary.Structures.html#1172" class="Field">sym</a> <a id="1783" class="Symbol">=</a> <a id="1785" href="Relation.Binary.Structures.html#1594" class="Field">sym</a>
|
||
<a id="1793" class="Symbol">;</a> <a id="1795" href="Relation.Binary.Structures.html#1198" class="Field">trans</a> <a id="1801" class="Symbol">=</a> <a id="1803" href="Relation.Binary.Structures.html#1620" class="Field">trans</a>
|
||
<a id="1813" class="Symbol">}</a>
|
||
|
||
|
||
<a id="1817" class="Keyword">record</a> <a id="IsDecEquivalence"></a><a id="1824" href="Relation.Binary.Structures.html#1824" class="Record">IsDecEquivalence</a> <a id="1841" class="Symbol">:</a> <a id="1843" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1847" class="Symbol">(</a><a id="1848" href="Relation.Binary.Structures.html#408" class="Bound">a</a> <a id="1850" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1852" href="Relation.Binary.Structures.html#410" class="Bound">ℓ</a><a id="1853" class="Symbol">)</a> <a id="1855" class="Keyword">where</a>
|
||
<a id="1863" class="Keyword">infix</a> <a id="1869" class="Number">4</a> <a id="1871" href="Relation.Binary.Structures.html#1921" class="Field Operator">_≟_</a>
|
||
<a id="1877" class="Keyword">field</a>
|
||
<a id="IsDecEquivalence.isEquivalence"></a><a id="1887" href="Relation.Binary.Structures.html#1887" class="Field">isEquivalence</a> <a id="1901" class="Symbol">:</a> <a id="1903" href="Relation.Binary.Structures.html#1522" class="Record">IsEquivalence</a>
|
||
<a id="IsDecEquivalence._≟_"></a><a id="1921" href="Relation.Binary.Structures.html#1921" class="Field Operator">_≟_</a> <a id="1935" class="Symbol">:</a> <a id="1937" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="1947" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
|
||
<a id="1954" class="Keyword">open</a> <a id="1959" href="Relation.Binary.Structures.html#1522" class="Module">IsEquivalence</a> <a id="1973" href="Relation.Binary.Structures.html#1887" class="Field">isEquivalence</a> <a id="1987" class="Keyword">public</a>
|
||
|
||
|
||
<a id="1996" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="2069" class="Comment">-- Preorders</a>
|
||
<a id="2082" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="2156" class="Keyword">record</a> <a id="IsPreorder"></a><a id="2163" href="Relation.Binary.Structures.html#2163" class="Record">IsPreorder</a> <a id="2174" class="Symbol">(</a><a id="2175" href="Relation.Binary.Structures.html#2175" class="Bound Operator">_∼_</a> <a id="2179" class="Symbol">:</a> <a id="2181" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="2185" href="Relation.Binary.Structures.html#414" class="Bound">A</a> <a id="2187" href="Relation.Binary.Structures.html#817" class="Generalizable">ℓ₂</a><a id="2189" class="Symbol">)</a> <a id="2191" class="Symbol">:</a> <a id="2193" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2197" class="Symbol">(</a><a id="2198" href="Relation.Binary.Structures.html#408" class="Bound">a</a> <a id="2200" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2202" href="Relation.Binary.Structures.html#410" class="Bound">ℓ</a> <a id="2204" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2206" href="Relation.Binary.Structures.html#2187" class="Bound">ℓ₂</a><a id="2208" class="Symbol">)</a> <a id="2210" class="Keyword">where</a>
|
||
<a id="2218" class="Keyword">field</a>
|
||
<a id="IsPreorder.isEquivalence"></a><a id="2228" href="Relation.Binary.Structures.html#2228" class="Field">isEquivalence</a> <a id="2242" class="Symbol">:</a> <a id="2244" href="Relation.Binary.Structures.html#1522" class="Record">IsEquivalence</a>
|
||
<a id="2262" class="Comment">-- Reflexivity is expressed in terms of the underlying equality:</a>
|
||
<a id="IsPreorder.reflexive"></a><a id="2331" href="Relation.Binary.Structures.html#2331" class="Field">reflexive</a> <a id="2345" class="Symbol">:</a> <a id="2347" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a> <a id="2351" href="Relation.Binary.Core.html#1254" class="Function Operator">⇒</a> <a id="2353" href="Relation.Binary.Structures.html#2175" class="Bound Operator">_∼_</a>
|
||
<a id="IsPreorder.trans"></a><a id="2361" href="Relation.Binary.Structures.html#2361" class="Field">trans</a> <a id="2375" class="Symbol">:</a> <a id="2377" href="Relation.Binary.Definitions.html#1866" class="Function">Transitive</a> <a id="2388" href="Relation.Binary.Structures.html#2175" class="Bound Operator">_∼_</a>
|
||
|
||
<a id="2395" class="Keyword">module</a> <a id="IsPreorder.Eq"></a><a id="2402" href="Relation.Binary.Structures.html#2402" class="Module">Eq</a> <a id="2405" class="Symbol">=</a> <a id="2407" href="Relation.Binary.Structures.html#1522" class="Module">IsEquivalence</a> <a id="2421" href="Relation.Binary.Structures.html#2228" class="Field">isEquivalence</a>
|
||
|
||
<a id="IsPreorder.refl"></a><a id="2438" href="Relation.Binary.Structures.html#2438" class="Function">refl</a> <a id="2443" class="Symbol">:</a> <a id="2445" href="Relation.Binary.Definitions.html#1339" class="Function">Reflexive</a> <a id="2455" href="Relation.Binary.Structures.html#2175" class="Bound Operator">_∼_</a>
|
||
<a id="2461" href="Relation.Binary.Structures.html#2438" class="Function">refl</a> <a id="2466" class="Symbol">=</a> <a id="2468" href="Relation.Binary.Structures.html#2331" class="Field">reflexive</a> <a id="2478" href="Relation.Binary.Structures.html#1568" class="Function">Eq.refl</a>
|
||
|
||
<a id="IsPreorder.∼-respˡ-≈"></a><a id="2489" href="Relation.Binary.Structures.html#2489" class="Function">∼-respˡ-≈</a> <a id="2499" class="Symbol">:</a> <a id="2501" href="Relation.Binary.Structures.html#2175" class="Bound Operator">_∼_</a> <a id="2505" href="Relation.Binary.Definitions.html#3914" class="Function Operator">Respectsˡ</a> <a id="2515" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
<a id="2521" href="Relation.Binary.Structures.html#2489" class="Function">∼-respˡ-≈</a> <a id="2531" href="Relation.Binary.Structures.html#2531" class="Bound">x≈y</a> <a id="2535" href="Relation.Binary.Structures.html#2535" class="Bound">x∼z</a> <a id="2539" class="Symbol">=</a> <a id="2541" href="Relation.Binary.Structures.html#2361" class="Field">trans</a> <a id="2547" class="Symbol">(</a><a id="2548" href="Relation.Binary.Structures.html#2331" class="Field">reflexive</a> <a id="2558" class="Symbol">(</a><a id="2559" href="Relation.Binary.Structures.html#1594" class="Function">Eq.sym</a> <a id="2566" href="Relation.Binary.Structures.html#2531" class="Bound">x≈y</a><a id="2569" class="Symbol">))</a> <a id="2572" href="Relation.Binary.Structures.html#2535" class="Bound">x∼z</a>
|
||
|
||
<a id="IsPreorder.∼-respʳ-≈"></a><a id="2579" href="Relation.Binary.Structures.html#2579" class="Function">∼-respʳ-≈</a> <a id="2589" class="Symbol">:</a> <a id="2591" href="Relation.Binary.Structures.html#2175" class="Bound Operator">_∼_</a> <a id="2595" href="Relation.Binary.Definitions.html#3749" class="Function Operator">Respectsʳ</a> <a id="2605" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
<a id="2611" href="Relation.Binary.Structures.html#2579" class="Function">∼-respʳ-≈</a> <a id="2621" href="Relation.Binary.Structures.html#2621" class="Bound">x≈y</a> <a id="2625" href="Relation.Binary.Structures.html#2625" class="Bound">z∼x</a> <a id="2629" class="Symbol">=</a> <a id="2631" href="Relation.Binary.Structures.html#2361" class="Field">trans</a> <a id="2637" href="Relation.Binary.Structures.html#2625" class="Bound">z∼x</a> <a id="2641" class="Symbol">(</a><a id="2642" href="Relation.Binary.Structures.html#2331" class="Field">reflexive</a> <a id="2652" href="Relation.Binary.Structures.html#2621" class="Bound">x≈y</a><a id="2655" class="Symbol">)</a>
|
||
|
||
<a id="IsPreorder.∼-resp-≈"></a><a id="2660" href="Relation.Binary.Structures.html#2660" class="Function">∼-resp-≈</a> <a id="2669" class="Symbol">:</a> <a id="2671" href="Relation.Binary.Structures.html#2175" class="Bound Operator">_∼_</a> <a id="2675" href="Relation.Binary.Definitions.html#4077" class="Function Operator">Respects₂</a> <a id="2685" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
<a id="2691" href="Relation.Binary.Structures.html#2660" class="Function">∼-resp-≈</a> <a id="2700" class="Symbol">=</a> <a id="2702" href="Relation.Binary.Structures.html#2579" class="Function">∼-respʳ-≈</a> <a id="2712" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="2714" href="Relation.Binary.Structures.html#2489" class="Function">∼-respˡ-≈</a>
|
||
|
||
|
||
<a id="2726" class="Keyword">record</a> <a id="IsTotalPreorder"></a><a id="2733" href="Relation.Binary.Structures.html#2733" class="Record">IsTotalPreorder</a> <a id="2749" class="Symbol">(</a><a id="2750" href="Relation.Binary.Structures.html#2750" class="Bound Operator">_≲_</a> <a id="2754" class="Symbol">:</a> <a id="2756" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="2760" href="Relation.Binary.Structures.html#414" class="Bound">A</a> <a id="2762" href="Relation.Binary.Structures.html#817" class="Generalizable">ℓ₂</a><a id="2764" class="Symbol">)</a> <a id="2766" class="Symbol">:</a> <a id="2768" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2772" class="Symbol">(</a><a id="2773" href="Relation.Binary.Structures.html#408" class="Bound">a</a> <a id="2775" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2777" href="Relation.Binary.Structures.html#410" class="Bound">ℓ</a> <a id="2779" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2781" href="Relation.Binary.Structures.html#2762" class="Bound">ℓ₂</a><a id="2783" class="Symbol">)</a> <a id="2785" class="Keyword">where</a>
|
||
<a id="2793" class="Keyword">field</a>
|
||
<a id="IsTotalPreorder.isPreorder"></a><a id="2803" href="Relation.Binary.Structures.html#2803" class="Field">isPreorder</a> <a id="2814" class="Symbol">:</a> <a id="2816" href="Relation.Binary.Structures.html#2163" class="Record">IsPreorder</a> <a id="2827" href="Relation.Binary.Structures.html#2750" class="Bound Operator">_≲_</a>
|
||
<a id="IsTotalPreorder.total"></a><a id="2835" href="Relation.Binary.Structures.html#2835" class="Field">total</a> <a id="2846" class="Symbol">:</a> <a id="2848" href="Relation.Binary.Definitions.html#2584" class="Function">Total</a> <a id="2854" href="Relation.Binary.Structures.html#2750" class="Bound Operator">_≲_</a>
|
||
|
||
<a id="2861" class="Keyword">open</a> <a id="2866" href="Relation.Binary.Structures.html#2163" class="Module">IsPreorder</a> <a id="2877" href="Relation.Binary.Structures.html#2803" class="Field">isPreorder</a> <a id="2888" class="Keyword">public</a>
|
||
<a id="2899" class="Keyword">renaming</a>
|
||
<a id="2912" class="Symbol">(</a> <a id="2914" href="Relation.Binary.Structures.html#2489" class="Function">∼-respˡ-≈</a> <a id="2924" class="Symbol">to</a> <a id="2927" class="Function">≲-respˡ-≈</a>
|
||
<a id="2941" class="Symbol">;</a> <a id="2943" href="Relation.Binary.Structures.html#2579" class="Function">∼-respʳ-≈</a> <a id="2953" class="Symbol">to</a> <a id="2956" class="Function">≲-respʳ-≈</a>
|
||
<a id="2970" class="Symbol">;</a> <a id="2972" href="Relation.Binary.Structures.html#2660" class="Function">∼-resp-≈</a> <a id="2982" class="Symbol">to</a> <a id="2985" class="Function">≲-resp-≈</a>
|
||
<a id="2998" class="Symbol">)</a>
|
||
|
||
|
||
<a id="3002" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="3075" class="Comment">-- Partial orders</a>
|
||
<a id="3093" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="3167" class="Keyword">record</a> <a id="IsPartialOrder"></a><a id="3174" href="Relation.Binary.Structures.html#3174" class="Record">IsPartialOrder</a> <a id="3189" class="Symbol">(</a><a id="3190" href="Relation.Binary.Structures.html#3190" class="Bound Operator">_≤_</a> <a id="3194" class="Symbol">:</a> <a id="3196" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="3200" href="Relation.Binary.Structures.html#414" class="Bound">A</a> <a id="3202" href="Relation.Binary.Structures.html#817" class="Generalizable">ℓ₂</a><a id="3204" class="Symbol">)</a> <a id="3206" class="Symbol">:</a> <a id="3208" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3212" class="Symbol">(</a><a id="3213" href="Relation.Binary.Structures.html#408" class="Bound">a</a> <a id="3215" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3217" href="Relation.Binary.Structures.html#410" class="Bound">ℓ</a> <a id="3219" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3221" href="Relation.Binary.Structures.html#3202" class="Bound">ℓ₂</a><a id="3223" class="Symbol">)</a> <a id="3225" class="Keyword">where</a>
|
||
<a id="3233" class="Keyword">field</a>
|
||
<a id="IsPartialOrder.isPreorder"></a><a id="3243" href="Relation.Binary.Structures.html#3243" class="Field">isPreorder</a> <a id="3254" class="Symbol">:</a> <a id="3256" href="Relation.Binary.Structures.html#2163" class="Record">IsPreorder</a> <a id="3267" href="Relation.Binary.Structures.html#3190" class="Bound Operator">_≤_</a>
|
||
<a id="IsPartialOrder.antisym"></a><a id="3275" href="Relation.Binary.Structures.html#3275" class="Field">antisym</a> <a id="3286" class="Symbol">:</a> <a id="3288" href="Relation.Binary.Definitions.html#2082" class="Function">Antisymmetric</a> <a id="3302" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a> <a id="3306" href="Relation.Binary.Structures.html#3190" class="Bound Operator">_≤_</a>
|
||
|
||
<a id="3313" class="Keyword">open</a> <a id="3318" href="Relation.Binary.Structures.html#2163" class="Module">IsPreorder</a> <a id="3329" href="Relation.Binary.Structures.html#3243" class="Field">isPreorder</a> <a id="3340" class="Keyword">public</a>
|
||
<a id="3351" class="Keyword">renaming</a>
|
||
<a id="3364" class="Symbol">(</a> <a id="3366" href="Relation.Binary.Structures.html#2489" class="Function">∼-respˡ-≈</a> <a id="3376" class="Symbol">to</a> <a id="3379" class="Function">≤-respˡ-≈</a>
|
||
<a id="3393" class="Symbol">;</a> <a id="3395" href="Relation.Binary.Structures.html#2579" class="Function">∼-respʳ-≈</a> <a id="3405" class="Symbol">to</a> <a id="3408" class="Function">≤-respʳ-≈</a>
|
||
<a id="3422" class="Symbol">;</a> <a id="3424" href="Relation.Binary.Structures.html#2660" class="Function">∼-resp-≈</a> <a id="3434" class="Symbol">to</a> <a id="3437" class="Function">≤-resp-≈</a>
|
||
<a id="3450" class="Symbol">)</a>
|
||
|
||
|
||
<a id="3454" class="Keyword">record</a> <a id="IsDecPartialOrder"></a><a id="3461" href="Relation.Binary.Structures.html#3461" class="Record">IsDecPartialOrder</a> <a id="3479" class="Symbol">(</a><a id="3480" href="Relation.Binary.Structures.html#3480" class="Bound Operator">_≤_</a> <a id="3484" class="Symbol">:</a> <a id="3486" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="3490" href="Relation.Binary.Structures.html#414" class="Bound">A</a> <a id="3492" href="Relation.Binary.Structures.html#817" class="Generalizable">ℓ₂</a><a id="3494" class="Symbol">)</a> <a id="3496" class="Symbol">:</a> <a id="3498" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3502" class="Symbol">(</a><a id="3503" href="Relation.Binary.Structures.html#408" class="Bound">a</a> <a id="3505" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3507" href="Relation.Binary.Structures.html#410" class="Bound">ℓ</a> <a id="3509" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3511" href="Relation.Binary.Structures.html#3492" class="Bound">ℓ₂</a><a id="3513" class="Symbol">)</a> <a id="3515" class="Keyword">where</a>
|
||
<a id="3523" class="Keyword">infix</a> <a id="3529" class="Number">4</a> <a id="3531" href="Relation.Binary.Structures.html#3592" class="Field Operator">_≟_</a> <a id="3535" href="Relation.Binary.Structures.html#3627" class="Field Operator">_≤?_</a>
|
||
<a id="3542" class="Keyword">field</a>
|
||
<a id="IsDecPartialOrder.isPartialOrder"></a><a id="3552" href="Relation.Binary.Structures.html#3552" class="Field">isPartialOrder</a> <a id="3567" class="Symbol">:</a> <a id="3569" href="Relation.Binary.Structures.html#3174" class="Record">IsPartialOrder</a> <a id="3584" href="Relation.Binary.Structures.html#3480" class="Bound Operator">_≤_</a>
|
||
<a id="IsDecPartialOrder._≟_"></a><a id="3592" href="Relation.Binary.Structures.html#3592" class="Field Operator">_≟_</a> <a id="3607" class="Symbol">:</a> <a id="3609" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="3619" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
<a id="IsDecPartialOrder._≤?_"></a><a id="3627" href="Relation.Binary.Structures.html#3627" class="Field Operator">_≤?_</a> <a id="3642" class="Symbol">:</a> <a id="3644" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="3654" href="Relation.Binary.Structures.html#3480" class="Bound Operator">_≤_</a>
|
||
|
||
<a id="3661" class="Keyword">open</a> <a id="3666" href="Relation.Binary.Structures.html#3174" class="Module">IsPartialOrder</a> <a id="3681" href="Relation.Binary.Structures.html#3552" class="Field">isPartialOrder</a> <a id="3696" class="Keyword">public</a>
|
||
<a id="3707" class="Keyword">hiding</a> <a id="3714" class="Symbol">(</a><a id="3715" class="Keyword">module</a> <a id="3722" href="Relation.Binary.Structures.html#2402" class="Module">Eq</a><a id="3724" class="Symbol">)</a>
|
||
|
||
<a id="3729" class="Keyword">module</a> <a id="IsDecPartialOrder.Eq"></a><a id="3736" href="Relation.Binary.Structures.html#3736" class="Module">Eq</a> <a id="3739" class="Keyword">where</a>
|
||
|
||
<a id="IsDecPartialOrder.Eq.isDecEquivalence"></a><a id="3750" href="Relation.Binary.Structures.html#3750" class="Function">isDecEquivalence</a> <a id="3767" class="Symbol">:</a> <a id="3769" href="Relation.Binary.Structures.html#1824" class="Record">IsDecEquivalence</a>
|
||
<a id="3790" href="Relation.Binary.Structures.html#3750" class="Function">isDecEquivalence</a> <a id="3807" class="Symbol">=</a> <a id="3809" class="Keyword">record</a>
|
||
<a id="3822" class="Symbol">{</a> <a id="3824" href="Relation.Binary.Structures.html#1887" class="Field">isEquivalence</a> <a id="3838" class="Symbol">=</a> <a id="3840" href="Relation.Binary.Structures.html#2228" class="Function">isEquivalence</a>
|
||
<a id="3860" class="Symbol">;</a> <a id="3862" href="Relation.Binary.Structures.html#1921" class="Field Operator">_≟_</a> <a id="3876" class="Symbol">=</a> <a id="3878" href="Relation.Binary.Structures.html#3592" class="Field Operator">_≟_</a>
|
||
<a id="3888" class="Symbol">}</a>
|
||
|
||
<a id="3895" class="Keyword">open</a> <a id="3900" href="Relation.Binary.Structures.html#1824" class="Module">IsDecEquivalence</a> <a id="3917" href="Relation.Binary.Structures.html#3750" class="Function">isDecEquivalence</a> <a id="3934" class="Keyword">public</a>
|
||
|
||
|
||
<a id="3943" class="Keyword">record</a> <a id="IsStrictPartialOrder"></a><a id="3950" href="Relation.Binary.Structures.html#3950" class="Record">IsStrictPartialOrder</a> <a id="3971" class="Symbol">(</a><a id="3972" href="Relation.Binary.Structures.html#3972" class="Bound Operator">_<_</a> <a id="3976" class="Symbol">:</a> <a id="3978" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="3982" href="Relation.Binary.Structures.html#414" class="Bound">A</a> <a id="3984" href="Relation.Binary.Structures.html#817" class="Generalizable">ℓ₂</a><a id="3986" class="Symbol">)</a> <a id="3988" class="Symbol">:</a> <a id="3990" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3994" class="Symbol">(</a><a id="3995" href="Relation.Binary.Structures.html#408" class="Bound">a</a> <a id="3997" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3999" href="Relation.Binary.Structures.html#410" class="Bound">ℓ</a> <a id="4001" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="4003" href="Relation.Binary.Structures.html#3984" class="Bound">ℓ₂</a><a id="4005" class="Symbol">)</a> <a id="4007" class="Keyword">where</a>
|
||
<a id="4015" class="Keyword">field</a>
|
||
<a id="IsStrictPartialOrder.isEquivalence"></a><a id="4025" href="Relation.Binary.Structures.html#4025" class="Field">isEquivalence</a> <a id="4039" class="Symbol">:</a> <a id="4041" href="Relation.Binary.Structures.html#1522" class="Record">IsEquivalence</a>
|
||
<a id="IsStrictPartialOrder.irrefl"></a><a id="4059" href="Relation.Binary.Structures.html#4059" class="Field">irrefl</a> <a id="4073" class="Symbol">:</a> <a id="4075" href="Relation.Binary.Definitions.html#2241" class="Function">Irreflexive</a> <a id="4087" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a> <a id="4091" href="Relation.Binary.Structures.html#3972" class="Bound Operator">_<_</a>
|
||
<a id="IsStrictPartialOrder.trans"></a><a id="4099" href="Relation.Binary.Structures.html#4099" class="Field">trans</a> <a id="4113" class="Symbol">:</a> <a id="4115" href="Relation.Binary.Definitions.html#1866" class="Function">Transitive</a> <a id="4126" href="Relation.Binary.Structures.html#3972" class="Bound Operator">_<_</a>
|
||
<a id="IsStrictPartialOrder.<-resp-≈"></a><a id="4134" href="Relation.Binary.Structures.html#4134" class="Field"><-resp-≈</a> <a id="4148" class="Symbol">:</a> <a id="4150" href="Relation.Binary.Structures.html#3972" class="Bound Operator">_<_</a> <a id="4154" href="Relation.Binary.Definitions.html#4077" class="Function Operator">Respects₂</a> <a id="4164" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
|
||
<a id="4171" class="Keyword">module</a> <a id="IsStrictPartialOrder.Eq"></a><a id="4178" href="Relation.Binary.Structures.html#4178" class="Module">Eq</a> <a id="4181" class="Symbol">=</a> <a id="4183" href="Relation.Binary.Structures.html#1522" class="Module">IsEquivalence</a> <a id="4197" href="Relation.Binary.Structures.html#4025" class="Field">isEquivalence</a>
|
||
|
||
<a id="IsStrictPartialOrder.asym"></a><a id="4214" href="Relation.Binary.Structures.html#4214" class="Function">asym</a> <a id="4219" class="Symbol">:</a> <a id="4221" href="Relation.Binary.Definitions.html#2353" class="Function">Asymmetric</a> <a id="4232" href="Relation.Binary.Structures.html#3972" class="Bound Operator">_<_</a>
|
||
<a id="4238" href="Relation.Binary.Structures.html#4214" class="Function">asym</a> <a id="4243" class="Symbol">{</a><a id="4244" href="Relation.Binary.Structures.html#4244" class="Bound">x</a><a id="4245" class="Symbol">}</a> <a id="4247" class="Symbol">{</a><a id="4248" href="Relation.Binary.Structures.html#4248" class="Bound">y</a><a id="4249" class="Symbol">}</a> <a id="4251" class="Symbol">=</a> <a id="4253" href="Relation.Binary.Consequences.html#2918" class="Function">trans∧irr⇒asym</a> <a id="4268" href="Relation.Binary.Structures.html#1568" class="Function">Eq.refl</a> <a id="4276" href="Relation.Binary.Structures.html#4099" class="Field">trans</a> <a id="4282" href="Relation.Binary.Structures.html#4059" class="Field">irrefl</a> <a id="4289" class="Symbol">{</a><a id="4290" class="Argument">x</a> <a id="4292" class="Symbol">=</a> <a id="4294" href="Relation.Binary.Structures.html#4244" class="Bound">x</a><a id="4295" class="Symbol">}</a> <a id="4297" class="Symbol">{</a><a id="4298" href="Relation.Binary.Structures.html#4248" class="Bound">y</a><a id="4299" class="Symbol">}</a>
|
||
|
||
<a id="IsStrictPartialOrder.<-respʳ-≈"></a><a id="4304" href="Relation.Binary.Structures.html#4304" class="Function"><-respʳ-≈</a> <a id="4314" class="Symbol">:</a> <a id="4316" href="Relation.Binary.Structures.html#3972" class="Bound Operator">_<_</a> <a id="4320" href="Relation.Binary.Definitions.html#3749" class="Function Operator">Respectsʳ</a> <a id="4330" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
<a id="4336" href="Relation.Binary.Structures.html#4304" class="Function"><-respʳ-≈</a> <a id="4346" class="Symbol">=</a> <a id="4348" href="Agda.Builtin.Sigma.html#252" class="Field">proj₁</a> <a id="4354" href="Relation.Binary.Structures.html#4134" class="Field"><-resp-≈</a>
|
||
|
||
<a id="IsStrictPartialOrder.<-respˡ-≈"></a><a id="4366" href="Relation.Binary.Structures.html#4366" class="Function"><-respˡ-≈</a> <a id="4376" class="Symbol">:</a> <a id="4378" href="Relation.Binary.Structures.html#3972" class="Bound Operator">_<_</a> <a id="4382" href="Relation.Binary.Definitions.html#3914" class="Function Operator">Respectsˡ</a> <a id="4392" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
<a id="4398" href="Relation.Binary.Structures.html#4366" class="Function"><-respˡ-≈</a> <a id="4408" class="Symbol">=</a> <a id="4410" href="Agda.Builtin.Sigma.html#264" class="Field">proj₂</a> <a id="4416" href="Relation.Binary.Structures.html#4134" class="Field"><-resp-≈</a>
|
||
|
||
<a id="IsStrictPartialOrder.asymmetric"></a><a id="4428" href="Relation.Binary.Structures.html#4428" class="Function">asymmetric</a> <a id="4439" class="Symbol">=</a> <a id="4441" href="Relation.Binary.Structures.html#4214" class="Function">asym</a>
|
||
<a id="4448" class="Symbol">{-#</a> <a id="4452" class="Keyword">WARNING_ON_USAGE</a> <a id="4469" class="Pragma">asymmetric</a>
|
||
<a id="4482" class="String">"Warning: asymmetric was deprecated in v0.16.
|
||
Please use asym instead."</a>
|
||
<a id="4558" class="Symbol">#-}</a>
|
||
|
||
|
||
<a id="4564" class="Keyword">record</a> <a id="IsDecStrictPartialOrder"></a><a id="4571" href="Relation.Binary.Structures.html#4571" class="Record">IsDecStrictPartialOrder</a> <a id="4595" class="Symbol">(</a><a id="4596" href="Relation.Binary.Structures.html#4596" class="Bound Operator">_<_</a> <a id="4600" class="Symbol">:</a> <a id="4602" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="4606" href="Relation.Binary.Structures.html#414" class="Bound">A</a> <a id="4608" href="Relation.Binary.Structures.html#817" class="Generalizable">ℓ₂</a><a id="4610" class="Symbol">)</a> <a id="4612" class="Symbol">:</a> <a id="4614" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4618" class="Symbol">(</a><a id="4619" href="Relation.Binary.Structures.html#408" class="Bound">a</a> <a id="4621" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="4623" href="Relation.Binary.Structures.html#410" class="Bound">ℓ</a> <a id="4625" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="4627" href="Relation.Binary.Structures.html#4608" class="Bound">ℓ₂</a><a id="4629" class="Symbol">)</a> <a id="4631" class="Keyword">where</a>
|
||
<a id="4639" class="Keyword">infix</a> <a id="4645" class="Number">4</a> <a id="4647" href="Relation.Binary.Structures.html#4720" class="Field Operator">_≟_</a> <a id="4651" href="Relation.Binary.Structures.html#4761" class="Field Operator">_<?_</a>
|
||
<a id="4658" class="Keyword">field</a>
|
||
<a id="IsDecStrictPartialOrder.isStrictPartialOrder"></a><a id="4668" href="Relation.Binary.Structures.html#4668" class="Field">isStrictPartialOrder</a> <a id="4689" class="Symbol">:</a> <a id="4691" href="Relation.Binary.Structures.html#3950" class="Record">IsStrictPartialOrder</a> <a id="4712" href="Relation.Binary.Structures.html#4596" class="Bound Operator">_<_</a>
|
||
<a id="IsDecStrictPartialOrder._≟_"></a><a id="4720" href="Relation.Binary.Structures.html#4720" class="Field Operator">_≟_</a> <a id="4741" class="Symbol">:</a> <a id="4743" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="4753" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
<a id="IsDecStrictPartialOrder._<?_"></a><a id="4761" href="Relation.Binary.Structures.html#4761" class="Field Operator">_<?_</a> <a id="4782" class="Symbol">:</a> <a id="4784" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="4794" href="Relation.Binary.Structures.html#4596" class="Bound Operator">_<_</a>
|
||
|
||
<a id="4801" class="Keyword">private</a>
|
||
<a id="4813" class="Keyword">module</a> <a id="IsDecStrictPartialOrder.SPO"></a><a id="4820" href="Relation.Binary.Structures.html#4820" class="Module">SPO</a> <a id="4824" class="Symbol">=</a> <a id="4826" href="Relation.Binary.Structures.html#3950" class="Module">IsStrictPartialOrder</a> <a id="4847" href="Relation.Binary.Structures.html#4668" class="Field">isStrictPartialOrder</a>
|
||
|
||
<a id="4871" class="Keyword">open</a> <a id="4876" href="Relation.Binary.Structures.html#4820" class="Module">SPO</a> <a id="4880" class="Keyword">public</a> <a id="4887" class="Keyword">hiding</a> <a id="4894" class="Symbol">(</a><a id="4895" class="Keyword">module</a> <a id="4902" href="Relation.Binary.Structures.html#4178" class="Module">Eq</a><a id="4904" class="Symbol">)</a>
|
||
|
||
<a id="4909" class="Keyword">module</a> <a id="IsDecStrictPartialOrder.Eq"></a><a id="4916" href="Relation.Binary.Structures.html#4916" class="Module">Eq</a> <a id="4919" class="Keyword">where</a>
|
||
|
||
<a id="IsDecStrictPartialOrder.Eq.isDecEquivalence"></a><a id="4930" href="Relation.Binary.Structures.html#4930" class="Function">isDecEquivalence</a> <a id="4947" class="Symbol">:</a> <a id="4949" href="Relation.Binary.Structures.html#1824" class="Record">IsDecEquivalence</a>
|
||
<a id="4970" href="Relation.Binary.Structures.html#4930" class="Function">isDecEquivalence</a> <a id="4987" class="Symbol">=</a> <a id="4989" class="Keyword">record</a>
|
||
<a id="5002" class="Symbol">{</a> <a id="5004" href="Relation.Binary.Structures.html#1887" class="Field">isEquivalence</a> <a id="5018" class="Symbol">=</a> <a id="5020" href="Relation.Binary.Structures.html#4025" class="Function">SPO.isEquivalence</a>
|
||
<a id="5044" class="Symbol">;</a> <a id="5046" href="Relation.Binary.Structures.html#1921" class="Field Operator">_≟_</a> <a id="5060" class="Symbol">=</a> <a id="5062" href="Relation.Binary.Structures.html#4720" class="Field Operator">_≟_</a>
|
||
<a id="5072" class="Symbol">}</a>
|
||
|
||
<a id="5079" class="Keyword">open</a> <a id="5084" href="Relation.Binary.Structures.html#1824" class="Module">IsDecEquivalence</a> <a id="5101" href="Relation.Binary.Structures.html#4930" class="Function">isDecEquivalence</a> <a id="5118" class="Keyword">public</a>
|
||
|
||
|
||
<a id="5127" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="5200" class="Comment">-- Total orders</a>
|
||
<a id="5216" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="5290" class="Keyword">record</a> <a id="IsTotalOrder"></a><a id="5297" href="Relation.Binary.Structures.html#5297" class="Record">IsTotalOrder</a> <a id="5310" class="Symbol">(</a><a id="5311" href="Relation.Binary.Structures.html#5311" class="Bound Operator">_≤_</a> <a id="5315" class="Symbol">:</a> <a id="5317" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="5321" href="Relation.Binary.Structures.html#414" class="Bound">A</a> <a id="5323" href="Relation.Binary.Structures.html#817" class="Generalizable">ℓ₂</a><a id="5325" class="Symbol">)</a> <a id="5327" class="Symbol">:</a> <a id="5329" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5333" class="Symbol">(</a><a id="5334" href="Relation.Binary.Structures.html#408" class="Bound">a</a> <a id="5336" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="5338" href="Relation.Binary.Structures.html#410" class="Bound">ℓ</a> <a id="5340" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="5342" href="Relation.Binary.Structures.html#5323" class="Bound">ℓ₂</a><a id="5344" class="Symbol">)</a> <a id="5346" class="Keyword">where</a>
|
||
<a id="5354" class="Keyword">field</a>
|
||
<a id="IsTotalOrder.isPartialOrder"></a><a id="5364" href="Relation.Binary.Structures.html#5364" class="Field">isPartialOrder</a> <a id="5379" class="Symbol">:</a> <a id="5381" href="Relation.Binary.Structures.html#3174" class="Record">IsPartialOrder</a> <a id="5396" href="Relation.Binary.Structures.html#5311" class="Bound Operator">_≤_</a>
|
||
<a id="IsTotalOrder.total"></a><a id="5404" href="Relation.Binary.Structures.html#5404" class="Field">total</a> <a id="5419" class="Symbol">:</a> <a id="5421" href="Relation.Binary.Definitions.html#2584" class="Function">Total</a> <a id="5427" href="Relation.Binary.Structures.html#5311" class="Bound Operator">_≤_</a>
|
||
|
||
<a id="5434" class="Keyword">open</a> <a id="5439" href="Relation.Binary.Structures.html#3174" class="Module">IsPartialOrder</a> <a id="5454" href="Relation.Binary.Structures.html#5364" class="Field">isPartialOrder</a> <a id="5469" class="Keyword">public</a>
|
||
|
||
<a id="IsTotalOrder.isTotalPreorder"></a><a id="5479" href="Relation.Binary.Structures.html#5479" class="Function">isTotalPreorder</a> <a id="5495" class="Symbol">:</a> <a id="5497" href="Relation.Binary.Structures.html#2733" class="Record">IsTotalPreorder</a> <a id="5513" href="Relation.Binary.Structures.html#5311" class="Bound Operator">_≤_</a>
|
||
<a id="5519" href="Relation.Binary.Structures.html#5479" class="Function">isTotalPreorder</a> <a id="5535" class="Symbol">=</a> <a id="5537" class="Keyword">record</a>
|
||
<a id="5548" class="Symbol">{</a> <a id="5550" href="Relation.Binary.Structures.html#2803" class="Field">isPreorder</a> <a id="5561" class="Symbol">=</a> <a id="5563" href="Relation.Binary.Structures.html#3243" class="Function">isPreorder</a>
|
||
<a id="5578" class="Symbol">;</a> <a id="5580" href="Relation.Binary.Structures.html#2835" class="Field">total</a> <a id="5591" class="Symbol">=</a> <a id="5593" href="Relation.Binary.Structures.html#5404" class="Field">total</a>
|
||
<a id="5603" class="Symbol">}</a>
|
||
|
||
|
||
<a id="5607" class="Keyword">record</a> <a id="IsDecTotalOrder"></a><a id="5614" href="Relation.Binary.Structures.html#5614" class="Record">IsDecTotalOrder</a> <a id="5630" class="Symbol">(</a><a id="5631" href="Relation.Binary.Structures.html#5631" class="Bound Operator">_≤_</a> <a id="5635" class="Symbol">:</a> <a id="5637" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="5641" href="Relation.Binary.Structures.html#414" class="Bound">A</a> <a id="5643" href="Relation.Binary.Structures.html#817" class="Generalizable">ℓ₂</a><a id="5645" class="Symbol">)</a> <a id="5647" class="Symbol">:</a> <a id="5649" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5653" class="Symbol">(</a><a id="5654" href="Relation.Binary.Structures.html#408" class="Bound">a</a> <a id="5656" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="5658" href="Relation.Binary.Structures.html#410" class="Bound">ℓ</a> <a id="5660" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="5662" href="Relation.Binary.Structures.html#5643" class="Bound">ℓ₂</a><a id="5664" class="Symbol">)</a> <a id="5666" class="Keyword">where</a>
|
||
<a id="5674" class="Keyword">infix</a> <a id="5680" class="Number">4</a> <a id="5682" href="Relation.Binary.Structures.html#5739" class="Field Operator">_≟_</a> <a id="5686" href="Relation.Binary.Structures.html#5772" class="Field Operator">_≤?_</a>
|
||
<a id="5693" class="Keyword">field</a>
|
||
<a id="IsDecTotalOrder.isTotalOrder"></a><a id="5703" href="Relation.Binary.Structures.html#5703" class="Field">isTotalOrder</a> <a id="5716" class="Symbol">:</a> <a id="5718" href="Relation.Binary.Structures.html#5297" class="Record">IsTotalOrder</a> <a id="5731" href="Relation.Binary.Structures.html#5631" class="Bound Operator">_≤_</a>
|
||
<a id="IsDecTotalOrder._≟_"></a><a id="5739" href="Relation.Binary.Structures.html#5739" class="Field Operator">_≟_</a> <a id="5752" class="Symbol">:</a> <a id="5754" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="5764" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
<a id="IsDecTotalOrder._≤?_"></a><a id="5772" href="Relation.Binary.Structures.html#5772" class="Field Operator">_≤?_</a> <a id="5785" class="Symbol">:</a> <a id="5787" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="5797" href="Relation.Binary.Structures.html#5631" class="Bound Operator">_≤_</a>
|
||
|
||
<a id="5804" class="Keyword">open</a> <a id="5809" href="Relation.Binary.Structures.html#5297" class="Module">IsTotalOrder</a> <a id="5822" href="Relation.Binary.Structures.html#5703" class="Field">isTotalOrder</a> <a id="5835" class="Keyword">public</a>
|
||
<a id="5846" class="Keyword">hiding</a> <a id="5853" class="Symbol">(</a><a id="5854" class="Keyword">module</a> <a id="5861" href="Relation.Binary.Structures.html#2402" class="Module">Eq</a><a id="5863" class="Symbol">)</a>
|
||
|
||
<a id="IsDecTotalOrder.isDecPartialOrder"></a><a id="5868" href="Relation.Binary.Structures.html#5868" class="Function">isDecPartialOrder</a> <a id="5886" class="Symbol">:</a> <a id="5888" href="Relation.Binary.Structures.html#3461" class="Record">IsDecPartialOrder</a> <a id="5906" href="Relation.Binary.Structures.html#5631" class="Bound Operator">_≤_</a>
|
||
<a id="5912" href="Relation.Binary.Structures.html#5868" class="Function">isDecPartialOrder</a> <a id="5930" class="Symbol">=</a> <a id="5932" class="Keyword">record</a>
|
||
<a id="5943" class="Symbol">{</a> <a id="5945" href="Relation.Binary.Structures.html#3552" class="Field">isPartialOrder</a> <a id="5960" class="Symbol">=</a> <a id="5962" href="Relation.Binary.Structures.html#5364" class="Function">isPartialOrder</a>
|
||
<a id="5981" class="Symbol">;</a> <a id="5983" href="Relation.Binary.Structures.html#3592" class="Field Operator">_≟_</a> <a id="5998" class="Symbol">=</a> <a id="6000" href="Relation.Binary.Structures.html#5739" class="Field Operator">_≟_</a>
|
||
<a id="6008" class="Symbol">;</a> <a id="6010" href="Relation.Binary.Structures.html#3627" class="Field Operator">_≤?_</a> <a id="6025" class="Symbol">=</a> <a id="6027" href="Relation.Binary.Structures.html#5772" class="Field Operator">_≤?_</a>
|
||
<a id="6036" class="Symbol">}</a>
|
||
|
||
<a id="6041" class="Keyword">module</a> <a id="IsDecTotalOrder.Eq"></a><a id="6048" href="Relation.Binary.Structures.html#6048" class="Module">Eq</a> <a id="6051" class="Keyword">where</a>
|
||
|
||
<a id="IsDecTotalOrder.Eq.isDecEquivalence"></a><a id="6062" href="Relation.Binary.Structures.html#6062" class="Function">isDecEquivalence</a> <a id="6079" class="Symbol">:</a> <a id="6081" href="Relation.Binary.Structures.html#1824" class="Record">IsDecEquivalence</a>
|
||
<a id="6102" href="Relation.Binary.Structures.html#6062" class="Function">isDecEquivalence</a> <a id="6119" class="Symbol">=</a> <a id="6121" class="Keyword">record</a>
|
||
<a id="6134" class="Symbol">{</a> <a id="6136" href="Relation.Binary.Structures.html#1887" class="Field">isEquivalence</a> <a id="6150" class="Symbol">=</a> <a id="6152" href="Relation.Binary.Structures.html#2228" class="Function">isEquivalence</a>
|
||
<a id="6172" class="Symbol">;</a> <a id="6174" href="Relation.Binary.Structures.html#1921" class="Field Operator">_≟_</a> <a id="6188" class="Symbol">=</a> <a id="6190" href="Relation.Binary.Structures.html#5739" class="Field Operator">_≟_</a>
|
||
<a id="6200" class="Symbol">}</a>
|
||
|
||
<a id="6207" class="Keyword">open</a> <a id="6212" href="Relation.Binary.Structures.html#1824" class="Module">IsDecEquivalence</a> <a id="6229" href="Relation.Binary.Structures.html#6062" class="Function">isDecEquivalence</a> <a id="6246" class="Keyword">public</a>
|
||
|
||
|
||
<a id="6255" class="Comment">-- Note that these orders are decidable. The current implementation</a>
|
||
<a id="6323" class="Comment">-- of `Trichotomous` subsumes irreflexivity and asymmetry. Any reasonable</a>
|
||
<a id="6397" class="Comment">-- definition capturing these three properties implies decidability</a>
|
||
<a id="6465" class="Comment">-- as `Trichotomous` necessarily separates out the equality case.</a>
|
||
|
||
<a id="6532" class="Keyword">record</a> <a id="IsStrictTotalOrder"></a><a id="6539" href="Relation.Binary.Structures.html#6539" class="Record">IsStrictTotalOrder</a> <a id="6558" class="Symbol">(</a><a id="6559" href="Relation.Binary.Structures.html#6559" class="Bound Operator">_<_</a> <a id="6563" class="Symbol">:</a> <a id="6565" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="6569" href="Relation.Binary.Structures.html#414" class="Bound">A</a> <a id="6571" href="Relation.Binary.Structures.html#817" class="Generalizable">ℓ₂</a><a id="6573" class="Symbol">)</a> <a id="6575" class="Symbol">:</a> <a id="6577" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="6581" class="Symbol">(</a><a id="6582" href="Relation.Binary.Structures.html#408" class="Bound">a</a> <a id="6584" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="6586" href="Relation.Binary.Structures.html#410" class="Bound">ℓ</a> <a id="6588" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="6590" href="Relation.Binary.Structures.html#6571" class="Bound">ℓ₂</a><a id="6592" class="Symbol">)</a> <a id="6594" class="Keyword">where</a>
|
||
<a id="6602" class="Keyword">field</a>
|
||
<a id="IsStrictTotalOrder.isEquivalence"></a><a id="6612" href="Relation.Binary.Structures.html#6612" class="Field">isEquivalence</a> <a id="6626" class="Symbol">:</a> <a id="6628" href="Relation.Binary.Structures.html#1522" class="Record">IsEquivalence</a>
|
||
<a id="IsStrictTotalOrder.trans"></a><a id="6646" href="Relation.Binary.Structures.html#6646" class="Field">trans</a> <a id="6660" class="Symbol">:</a> <a id="6662" href="Relation.Binary.Definitions.html#1866" class="Function">Transitive</a> <a id="6673" href="Relation.Binary.Structures.html#6559" class="Bound Operator">_<_</a>
|
||
<a id="IsStrictTotalOrder.compare"></a><a id="6681" href="Relation.Binary.Structures.html#6681" class="Field">compare</a> <a id="6695" class="Symbol">:</a> <a id="6697" href="Relation.Binary.Definitions.html#2955" class="Function">Trichotomous</a> <a id="6710" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a> <a id="6714" href="Relation.Binary.Structures.html#6559" class="Bound Operator">_<_</a>
|
||
|
||
<a id="6721" class="Keyword">infix</a> <a id="6727" class="Number">4</a> <a id="6729" href="Relation.Binary.Structures.html#6741" class="Function Operator">_≟_</a> <a id="6733" href="Relation.Binary.Structures.html#6789" class="Function Operator">_<?_</a>
|
||
|
||
<a id="IsStrictTotalOrder._≟_"></a><a id="6741" href="Relation.Binary.Structures.html#6741" class="Function Operator">_≟_</a> <a id="6745" class="Symbol">:</a> <a id="6747" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="6757" href="Relation.Binary.Structures.html#450" class="Bound Operator">_≈_</a>
|
||
<a id="6763" href="Relation.Binary.Structures.html#6741" class="Function Operator">_≟_</a> <a id="6767" class="Symbol">=</a> <a id="6769" href="Relation.Binary.Consequences.html#4002" class="Function">tri⇒dec≈</a> <a id="6778" href="Relation.Binary.Structures.html#6681" class="Field">compare</a>
|
||
|
||
<a id="IsStrictTotalOrder._<?_"></a><a id="6789" href="Relation.Binary.Structures.html#6789" class="Function Operator">_<?_</a> <a id="6794" class="Symbol">:</a> <a id="6796" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="6806" href="Relation.Binary.Structures.html#6559" class="Bound Operator">_<_</a>
|
||
<a id="6812" href="Relation.Binary.Structures.html#6789" class="Function Operator">_<?_</a> <a id="6817" class="Symbol">=</a> <a id="6819" href="Relation.Binary.Consequences.html#4186" class="Function">tri⇒dec<</a> <a id="6828" href="Relation.Binary.Structures.html#6681" class="Field">compare</a>
|
||
|
||
<a id="IsStrictTotalOrder.isDecEquivalence"></a><a id="6839" href="Relation.Binary.Structures.html#6839" class="Function">isDecEquivalence</a> <a id="6856" class="Symbol">:</a> <a id="6858" href="Relation.Binary.Structures.html#1824" class="Record">IsDecEquivalence</a>
|
||
<a id="6877" href="Relation.Binary.Structures.html#6839" class="Function">isDecEquivalence</a> <a id="6894" class="Symbol">=</a> <a id="6896" class="Keyword">record</a>
|
||
<a id="6907" class="Symbol">{</a> <a id="6909" href="Relation.Binary.Structures.html#1887" class="Field">isEquivalence</a> <a id="6923" class="Symbol">=</a> <a id="6925" href="Relation.Binary.Structures.html#6612" class="Field">isEquivalence</a>
|
||
<a id="6943" class="Symbol">;</a> <a id="6945" href="Relation.Binary.Structures.html#1921" class="Field Operator">_≟_</a> <a id="6959" class="Symbol">=</a> <a id="6961" href="Relation.Binary.Structures.html#6741" class="Function Operator">_≟_</a>
|
||
<a id="6969" class="Symbol">}</a>
|
||
|
||
<a id="6974" class="Keyword">module</a> <a id="IsStrictTotalOrder.Eq"></a><a id="6981" href="Relation.Binary.Structures.html#6981" class="Module">Eq</a> <a id="6984" class="Symbol">=</a> <a id="6986" href="Relation.Binary.Structures.html#1824" class="Module">IsDecEquivalence</a> <a id="7003" href="Relation.Binary.Structures.html#6839" class="Function">isDecEquivalence</a>
|
||
|
||
<a id="IsStrictTotalOrder.isStrictPartialOrder"></a><a id="7023" href="Relation.Binary.Structures.html#7023" class="Function">isStrictPartialOrder</a> <a id="7044" class="Symbol">:</a> <a id="7046" href="Relation.Binary.Structures.html#3950" class="Record">IsStrictPartialOrder</a> <a id="7067" href="Relation.Binary.Structures.html#6559" class="Bound Operator">_<_</a>
|
||
<a id="7073" href="Relation.Binary.Structures.html#7023" class="Function">isStrictPartialOrder</a> <a id="7094" class="Symbol">=</a> <a id="7096" class="Keyword">record</a>
|
||
<a id="7107" class="Symbol">{</a> <a id="7109" href="Relation.Binary.Structures.html#4025" class="Field">isEquivalence</a> <a id="7123" class="Symbol">=</a> <a id="7125" href="Relation.Binary.Structures.html#6612" class="Field">isEquivalence</a>
|
||
<a id="7143" class="Symbol">;</a> <a id="7145" href="Relation.Binary.Structures.html#4059" class="Field">irrefl</a> <a id="7159" class="Symbol">=</a> <a id="7161" href="Relation.Binary.Consequences.html#3790" class="Function">tri⇒irr</a> <a id="7169" href="Relation.Binary.Structures.html#6681" class="Field">compare</a>
|
||
<a id="7181" class="Symbol">;</a> <a id="7183" href="Relation.Binary.Structures.html#4099" class="Field">trans</a> <a id="7197" class="Symbol">=</a> <a id="7199" href="Relation.Binary.Structures.html#6646" class="Field">trans</a>
|
||
<a id="7209" class="Symbol">;</a> <a id="7211" href="Relation.Binary.Structures.html#4134" class="Field"><-resp-≈</a> <a id="7225" class="Symbol">=</a> <a id="7227" href="Relation.Binary.Consequences.html#5110" class="Function">trans∧tri⇒resp</a> <a id="7242" href="Relation.Binary.Structures.html#1594" class="Function">Eq.sym</a> <a id="7249" href="Relation.Binary.Structures.html#1620" class="Function">Eq.trans</a> <a id="7258" href="Relation.Binary.Structures.html#6646" class="Field">trans</a> <a id="7264" href="Relation.Binary.Structures.html#6681" class="Field">compare</a>
|
||
<a id="7276" class="Symbol">}</a>
|
||
|
||
<a id="IsStrictTotalOrder.isDecStrictPartialOrder"></a><a id="7281" href="Relation.Binary.Structures.html#7281" class="Function">isDecStrictPartialOrder</a> <a id="7305" class="Symbol">:</a> <a id="7307" href="Relation.Binary.Structures.html#4571" class="Record">IsDecStrictPartialOrder</a> <a id="7331" href="Relation.Binary.Structures.html#6559" class="Bound Operator">_<_</a>
|
||
<a id="7337" href="Relation.Binary.Structures.html#7281" class="Function">isDecStrictPartialOrder</a> <a id="7361" class="Symbol">=</a> <a id="7363" class="Keyword">record</a>
|
||
<a id="7374" class="Symbol">{</a> <a id="7376" href="Relation.Binary.Structures.html#4668" class="Field">isStrictPartialOrder</a> <a id="7397" class="Symbol">=</a> <a id="7399" href="Relation.Binary.Structures.html#7023" class="Function">isStrictPartialOrder</a>
|
||
<a id="7424" class="Symbol">;</a> <a id="7426" href="Relation.Binary.Structures.html#4720" class="Field Operator">_≟_</a> <a id="7447" class="Symbol">=</a> <a id="7449" href="Relation.Binary.Structures.html#6741" class="Function Operator">_≟_</a>
|
||
<a id="7457" class="Symbol">;</a> <a id="7459" href="Relation.Binary.Structures.html#4761" class="Field Operator">_<?_</a> <a id="7480" class="Symbol">=</a> <a id="7482" href="Relation.Binary.Structures.html#6789" class="Function Operator">_<?_</a>
|
||
<a id="7491" class="Symbol">}</a>
|
||
|
||
<a id="7496" class="Keyword">open</a> <a id="7501" href="Relation.Binary.Structures.html#3950" class="Module">IsStrictPartialOrder</a> <a id="7522" href="Relation.Binary.Structures.html#7023" class="Function">isStrictPartialOrder</a> <a id="7543" class="Keyword">public</a>
|
||
<a id="7554" class="Keyword">using</a> <a id="7560" class="Symbol">(</a><a id="7561" href="Relation.Binary.Structures.html#4059" class="Field">irrefl</a><a id="7567" class="Symbol">;</a> <a id="7569" href="Relation.Binary.Structures.html#4214" class="Function">asym</a><a id="7573" class="Symbol">;</a> <a id="7575" href="Relation.Binary.Structures.html#4304" class="Function"><-respʳ-≈</a><a id="7584" class="Symbol">;</a> <a id="7586" href="Relation.Binary.Structures.html#4366" class="Function"><-respˡ-≈</a><a id="7595" class="Symbol">;</a> <a id="7597" href="Relation.Binary.Structures.html#4134" class="Field"><-resp-≈</a><a id="7605" class="Symbol">)</a>
|
||
</pre></body></html> |