225 lines
68 KiB
HTML
225 lines
68 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Relation.Binary.Definitions</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="74" class="Comment">-- The Agda standard library</a>
|
||
<a id="103" class="Comment">--</a>
|
||
<a id="106" class="Comment">-- Properties of binary relations</a>
|
||
<a id="140" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="214" class="Comment">-- The contents of this module should be accessed via `Relation.Binary`.</a>
|
||
|
||
<a id="288" class="Symbol">{-#</a> <a id="292" class="Keyword">OPTIONS</a> <a id="300" class="Pragma">--without-K</a> <a id="312" class="Pragma">--safe</a> <a id="319" class="Symbol">#-}</a>
|
||
|
||
<a id="324" class="Keyword">module</a> <a id="331" href="Relation.Binary.Definitions.html" class="Module">Relation.Binary.Definitions</a> <a id="359" class="Keyword">where</a>
|
||
|
||
<a id="366" class="Keyword">open</a> <a id="371" class="Keyword">import</a> <a id="378" href="Agda.Builtin.Equality.html" class="Module">Agda.Builtin.Equality</a> <a id="400" class="Keyword">using</a> <a id="406" class="Symbol">(</a><a id="407" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a><a id="410" class="Symbol">)</a>
|
||
|
||
<a id="413" class="Keyword">open</a> <a id="418" class="Keyword">import</a> <a id="425" href="Data.Maybe.Base.html" class="Module">Data.Maybe.Base</a> <a id="441" class="Keyword">using</a> <a id="447" class="Symbol">(</a><a id="448" href="Agda.Builtin.Maybe.html#136" class="Datatype">Maybe</a><a id="453" class="Symbol">)</a>
|
||
<a id="455" class="Keyword">open</a> <a id="460" class="Keyword">import</a> <a id="467" href="Data.Product.html" class="Module">Data.Product</a> <a id="480" class="Keyword">using</a> <a id="486" class="Symbol">(</a><a id="487" href="Data.Product.html#1167" class="Function Operator">_×_</a><a id="490" class="Symbol">)</a>
|
||
<a id="492" class="Keyword">open</a> <a id="497" class="Keyword">import</a> <a id="504" href="Data.Sum.Base.html" class="Module">Data.Sum.Base</a> <a id="518" class="Keyword">using</a> <a id="524" class="Symbol">(</a><a id="525" href="Data.Sum.Base.html#734" class="Datatype Operator">_⊎_</a><a id="528" class="Symbol">)</a>
|
||
<a id="530" class="Keyword">open</a> <a id="535" class="Keyword">import</a> <a id="542" href="Function.Base.html" class="Module">Function.Base</a> <a id="556" class="Keyword">using</a> <a id="562" class="Symbol">(</a><a id="563" href="Function.Base.html#6285" class="Function Operator">_on_</a><a id="567" class="Symbol">;</a> <a id="569" href="Function.Base.html#1554" class="Function">flip</a><a id="573" class="Symbol">)</a>
|
||
<a id="575" class="Keyword">open</a> <a id="580" class="Keyword">import</a> <a id="587" href="Level.html" class="Module">Level</a>
|
||
<a id="593" class="Keyword">open</a> <a id="598" class="Keyword">import</a> <a id="605" href="Relation.Binary.Core.html" class="Module">Relation.Binary.Core</a>
|
||
<a id="626" class="Keyword">open</a> <a id="631" class="Keyword">import</a> <a id="638" href="Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="655" class="Keyword">using</a> <a id="661" class="Symbol">(</a><a id="662" href="Relation.Nullary.html#1511" class="Record">Dec</a><a id="665" class="Symbol">;</a> <a id="667" href="Relation.Nullary.html#656" class="Function Operator">¬_</a><a id="669" class="Symbol">)</a>
|
||
|
||
<a id="672" class="Keyword">private</a>
|
||
<a id="682" class="Keyword">variable</a>
|
||
<a id="695" href="Relation.Binary.Definitions.html#695" class="Generalizable">a</a> <a id="697" href="Relation.Binary.Definitions.html#697" class="Generalizable">b</a> <a id="699" href="Relation.Binary.Definitions.html#699" class="Generalizable">c</a> <a id="701" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a> <a id="703" href="Relation.Binary.Definitions.html#703" class="Generalizable">ℓ₁</a> <a id="706" href="Relation.Binary.Definitions.html#706" class="Generalizable">ℓ₂</a> <a id="709" href="Relation.Binary.Definitions.html#709" class="Generalizable">ℓ₃</a> <a id="712" class="Symbol">:</a> <a id="714" href="Agda.Primitive.html#597" class="Postulate">Level</a>
|
||
<a id="724" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="726" class="Symbol">:</a> <a id="728" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="732" href="Relation.Binary.Definitions.html#695" class="Generalizable">a</a>
|
||
<a id="738" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="740" class="Symbol">:</a> <a id="742" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="746" href="Relation.Binary.Definitions.html#697" class="Generalizable">b</a>
|
||
<a id="752" href="Relation.Binary.Definitions.html#752" class="Generalizable">C</a> <a id="754" class="Symbol">:</a> <a id="756" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="760" href="Relation.Binary.Definitions.html#699" class="Generalizable">c</a>
|
||
|
||
<a id="763" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="836" class="Comment">-- Definitions</a>
|
||
<a id="851" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="925" class="Comment">-- Reflexivity - defined without an underlying equality. It could</a>
|
||
<a id="991" class="Comment">-- alternatively be defined as `_≈_ ⇒ _∼_` for some equality `_≈_`.</a>
|
||
|
||
<a id="1060" class="Comment">-- Confusingly the convention in the library is to use the name "refl"</a>
|
||
<a id="1131" class="Comment">-- for proofs of Reflexive and `reflexive` for proofs of type `_≈_ ⇒ _∼_`,</a>
|
||
<a id="1206" class="Comment">-- e.g. in the definition of `IsEquivalence` later in this file. This</a>
|
||
<a id="1276" class="Comment">-- convention is a legacy from the early days of the library.</a>
|
||
|
||
<a id="Reflexive"></a><a id="1339" href="Relation.Binary.Definitions.html#1339" class="Function">Reflexive</a> <a id="1349" class="Symbol">:</a> <a id="1351" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="1355" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="1357" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a> <a id="1359" class="Symbol">→</a> <a id="1361" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1365" class="Symbol">_</a>
|
||
<a id="1367" href="Relation.Binary.Definitions.html#1339" class="Function">Reflexive</a> <a id="1377" href="Relation.Binary.Definitions.html#1377" class="Bound Operator">_∼_</a> <a id="1381" class="Symbol">=</a> <a id="1383" class="Symbol">∀</a> <a id="1385" class="Symbol">{</a><a id="1386" href="Relation.Binary.Definitions.html#1386" class="Bound">x</a><a id="1387" class="Symbol">}</a> <a id="1389" class="Symbol">→</a> <a id="1391" href="Relation.Binary.Definitions.html#1386" class="Bound">x</a> <a id="1393" href="Relation.Binary.Definitions.html#1377" class="Bound Operator">∼</a> <a id="1395" href="Relation.Binary.Definitions.html#1386" class="Bound">x</a>
|
||
|
||
<a id="1398" class="Comment">-- Generalised symmetry.</a>
|
||
|
||
<a id="Sym"></a><a id="1424" href="Relation.Binary.Definitions.html#1424" class="Function">Sym</a> <a id="1428" class="Symbol">:</a> <a id="1430" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="1434" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="1436" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="1438" href="Relation.Binary.Definitions.html#703" class="Generalizable">ℓ₁</a> <a id="1441" class="Symbol">→</a> <a id="1443" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="1447" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="1449" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="1451" href="Relation.Binary.Definitions.html#706" class="Generalizable">ℓ₂</a> <a id="1454" class="Symbol">→</a> <a id="1456" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1460" class="Symbol">_</a>
|
||
<a id="1462" href="Relation.Binary.Definitions.html#1424" class="Function">Sym</a> <a id="1466" href="Relation.Binary.Definitions.html#1466" class="Bound">P</a> <a id="1468" href="Relation.Binary.Definitions.html#1468" class="Bound">Q</a> <a id="1470" class="Symbol">=</a> <a id="1472" href="Relation.Binary.Definitions.html#1466" class="Bound">P</a> <a id="1474" href="Relation.Binary.Core.html#1254" class="Function Operator">⇒</a> <a id="1476" href="Function.Base.html#1554" class="Function">flip</a> <a id="1481" href="Relation.Binary.Definitions.html#1468" class="Bound">Q</a>
|
||
|
||
<a id="1484" class="Comment">-- Symmetry.</a>
|
||
|
||
<a id="Symmetric"></a><a id="1498" href="Relation.Binary.Definitions.html#1498" class="Function">Symmetric</a> <a id="1508" class="Symbol">:</a> <a id="1510" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="1514" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="1516" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a> <a id="1518" class="Symbol">→</a> <a id="1520" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1524" class="Symbol">_</a>
|
||
<a id="1526" href="Relation.Binary.Definitions.html#1498" class="Function">Symmetric</a> <a id="1536" href="Relation.Binary.Definitions.html#1536" class="Bound Operator">_∼_</a> <a id="1540" class="Symbol">=</a> <a id="1542" href="Relation.Binary.Definitions.html#1424" class="Function">Sym</a> <a id="1546" href="Relation.Binary.Definitions.html#1536" class="Bound Operator">_∼_</a> <a id="1550" href="Relation.Binary.Definitions.html#1536" class="Bound Operator">_∼_</a>
|
||
|
||
<a id="1555" class="Comment">-- Generalised transitivity.</a>
|
||
|
||
<a id="Trans"></a><a id="1585" href="Relation.Binary.Definitions.html#1585" class="Function">Trans</a> <a id="1591" class="Symbol">:</a> <a id="1593" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="1597" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="1599" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="1601" href="Relation.Binary.Definitions.html#703" class="Generalizable">ℓ₁</a> <a id="1604" class="Symbol">→</a> <a id="1606" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="1610" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="1612" href="Relation.Binary.Definitions.html#752" class="Generalizable">C</a> <a id="1614" href="Relation.Binary.Definitions.html#706" class="Generalizable">ℓ₂</a> <a id="1617" class="Symbol">→</a> <a id="1619" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="1623" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="1625" href="Relation.Binary.Definitions.html#752" class="Generalizable">C</a> <a id="1627" href="Relation.Binary.Definitions.html#709" class="Generalizable">ℓ₃</a> <a id="1630" class="Symbol">→</a> <a id="1632" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1636" class="Symbol">_</a>
|
||
<a id="1638" href="Relation.Binary.Definitions.html#1585" class="Function">Trans</a> <a id="1644" href="Relation.Binary.Definitions.html#1644" class="Bound">P</a> <a id="1646" href="Relation.Binary.Definitions.html#1646" class="Bound">Q</a> <a id="1648" href="Relation.Binary.Definitions.html#1648" class="Bound">R</a> <a id="1650" class="Symbol">=</a> <a id="1652" class="Symbol">∀</a> <a id="1654" class="Symbol">{</a><a id="1655" href="Relation.Binary.Definitions.html#1655" class="Bound">i</a> <a id="1657" href="Relation.Binary.Definitions.html#1657" class="Bound">j</a> <a id="1659" href="Relation.Binary.Definitions.html#1659" class="Bound">k</a><a id="1660" class="Symbol">}</a> <a id="1662" class="Symbol">→</a> <a id="1664" href="Relation.Binary.Definitions.html#1644" class="Bound">P</a> <a id="1666" href="Relation.Binary.Definitions.html#1655" class="Bound">i</a> <a id="1668" href="Relation.Binary.Definitions.html#1657" class="Bound">j</a> <a id="1670" class="Symbol">→</a> <a id="1672" href="Relation.Binary.Definitions.html#1646" class="Bound">Q</a> <a id="1674" href="Relation.Binary.Definitions.html#1657" class="Bound">j</a> <a id="1676" href="Relation.Binary.Definitions.html#1659" class="Bound">k</a> <a id="1678" class="Symbol">→</a> <a id="1680" href="Relation.Binary.Definitions.html#1648" class="Bound">R</a> <a id="1682" href="Relation.Binary.Definitions.html#1655" class="Bound">i</a> <a id="1684" href="Relation.Binary.Definitions.html#1659" class="Bound">k</a>
|
||
|
||
<a id="1687" class="Comment">-- A flipped variant of generalised transitivity.</a>
|
||
|
||
<a id="TransFlip"></a><a id="1738" href="Relation.Binary.Definitions.html#1738" class="Function">TransFlip</a> <a id="1748" class="Symbol">:</a> <a id="1750" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="1754" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="1756" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="1758" href="Relation.Binary.Definitions.html#703" class="Generalizable">ℓ₁</a> <a id="1761" class="Symbol">→</a> <a id="1763" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="1767" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="1769" href="Relation.Binary.Definitions.html#752" class="Generalizable">C</a> <a id="1771" href="Relation.Binary.Definitions.html#706" class="Generalizable">ℓ₂</a> <a id="1774" class="Symbol">→</a> <a id="1776" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="1780" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="1782" href="Relation.Binary.Definitions.html#752" class="Generalizable">C</a> <a id="1784" href="Relation.Binary.Definitions.html#709" class="Generalizable">ℓ₃</a> <a id="1787" class="Symbol">→</a> <a id="1789" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1793" class="Symbol">_</a>
|
||
<a id="1795" href="Relation.Binary.Definitions.html#1738" class="Function">TransFlip</a> <a id="1805" href="Relation.Binary.Definitions.html#1805" class="Bound">P</a> <a id="1807" href="Relation.Binary.Definitions.html#1807" class="Bound">Q</a> <a id="1809" href="Relation.Binary.Definitions.html#1809" class="Bound">R</a> <a id="1811" class="Symbol">=</a> <a id="1813" class="Symbol">∀</a> <a id="1815" class="Symbol">{</a><a id="1816" href="Relation.Binary.Definitions.html#1816" class="Bound">i</a> <a id="1818" href="Relation.Binary.Definitions.html#1818" class="Bound">j</a> <a id="1820" href="Relation.Binary.Definitions.html#1820" class="Bound">k</a><a id="1821" class="Symbol">}</a> <a id="1823" class="Symbol">→</a> <a id="1825" href="Relation.Binary.Definitions.html#1807" class="Bound">Q</a> <a id="1827" href="Relation.Binary.Definitions.html#1818" class="Bound">j</a> <a id="1829" href="Relation.Binary.Definitions.html#1820" class="Bound">k</a> <a id="1831" class="Symbol">→</a> <a id="1833" href="Relation.Binary.Definitions.html#1805" class="Bound">P</a> <a id="1835" href="Relation.Binary.Definitions.html#1816" class="Bound">i</a> <a id="1837" href="Relation.Binary.Definitions.html#1818" class="Bound">j</a> <a id="1839" class="Symbol">→</a> <a id="1841" href="Relation.Binary.Definitions.html#1809" class="Bound">R</a> <a id="1843" href="Relation.Binary.Definitions.html#1816" class="Bound">i</a> <a id="1845" href="Relation.Binary.Definitions.html#1820" class="Bound">k</a>
|
||
|
||
<a id="1848" class="Comment">-- Transitivity.</a>
|
||
|
||
<a id="Transitive"></a><a id="1866" href="Relation.Binary.Definitions.html#1866" class="Function">Transitive</a> <a id="1877" class="Symbol">:</a> <a id="1879" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="1883" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="1885" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a> <a id="1887" class="Symbol">→</a> <a id="1889" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1893" class="Symbol">_</a>
|
||
<a id="1895" href="Relation.Binary.Definitions.html#1866" class="Function">Transitive</a> <a id="1906" href="Relation.Binary.Definitions.html#1906" class="Bound Operator">_∼_</a> <a id="1910" class="Symbol">=</a> <a id="1912" href="Relation.Binary.Definitions.html#1585" class="Function">Trans</a> <a id="1918" href="Relation.Binary.Definitions.html#1906" class="Bound Operator">_∼_</a> <a id="1922" href="Relation.Binary.Definitions.html#1906" class="Bound Operator">_∼_</a> <a id="1926" href="Relation.Binary.Definitions.html#1906" class="Bound Operator">_∼_</a>
|
||
|
||
<a id="1931" class="Comment">-- Generalised antisymmetry</a>
|
||
|
||
<a id="Antisym"></a><a id="1960" href="Relation.Binary.Definitions.html#1960" class="Function">Antisym</a> <a id="1968" class="Symbol">:</a> <a id="1970" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="1974" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="1976" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="1978" href="Relation.Binary.Definitions.html#703" class="Generalizable">ℓ₁</a> <a id="1981" class="Symbol">→</a> <a id="1983" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="1987" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="1989" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="1991" href="Relation.Binary.Definitions.html#706" class="Generalizable">ℓ₂</a> <a id="1994" class="Symbol">→</a> <a id="1996" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="2000" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="2002" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="2004" href="Relation.Binary.Definitions.html#709" class="Generalizable">ℓ₃</a> <a id="2007" class="Symbol">→</a> <a id="2009" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2013" class="Symbol">_</a>
|
||
<a id="2015" href="Relation.Binary.Definitions.html#1960" class="Function">Antisym</a> <a id="2023" href="Relation.Binary.Definitions.html#2023" class="Bound">R</a> <a id="2025" href="Relation.Binary.Definitions.html#2025" class="Bound">S</a> <a id="2027" href="Relation.Binary.Definitions.html#2027" class="Bound">E</a> <a id="2029" class="Symbol">=</a> <a id="2031" class="Symbol">∀</a> <a id="2033" class="Symbol">{</a><a id="2034" href="Relation.Binary.Definitions.html#2034" class="Bound">i</a> <a id="2036" href="Relation.Binary.Definitions.html#2036" class="Bound">j</a><a id="2037" class="Symbol">}</a> <a id="2039" class="Symbol">→</a> <a id="2041" href="Relation.Binary.Definitions.html#2023" class="Bound">R</a> <a id="2043" href="Relation.Binary.Definitions.html#2034" class="Bound">i</a> <a id="2045" href="Relation.Binary.Definitions.html#2036" class="Bound">j</a> <a id="2047" class="Symbol">→</a> <a id="2049" href="Relation.Binary.Definitions.html#2025" class="Bound">S</a> <a id="2051" href="Relation.Binary.Definitions.html#2036" class="Bound">j</a> <a id="2053" href="Relation.Binary.Definitions.html#2034" class="Bound">i</a> <a id="2055" class="Symbol">→</a> <a id="2057" href="Relation.Binary.Definitions.html#2027" class="Bound">E</a> <a id="2059" href="Relation.Binary.Definitions.html#2034" class="Bound">i</a> <a id="2061" href="Relation.Binary.Definitions.html#2036" class="Bound">j</a>
|
||
|
||
<a id="2064" class="Comment">-- Antisymmetry.</a>
|
||
|
||
<a id="Antisymmetric"></a><a id="2082" href="Relation.Binary.Definitions.html#2082" class="Function">Antisymmetric</a> <a id="2096" class="Symbol">:</a> <a id="2098" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="2102" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="2104" href="Relation.Binary.Definitions.html#703" class="Generalizable">ℓ₁</a> <a id="2107" class="Symbol">→</a> <a id="2109" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="2113" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="2115" href="Relation.Binary.Definitions.html#706" class="Generalizable">ℓ₂</a> <a id="2118" class="Symbol">→</a> <a id="2120" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2124" class="Symbol">_</a>
|
||
<a id="2126" href="Relation.Binary.Definitions.html#2082" class="Function">Antisymmetric</a> <a id="2140" href="Relation.Binary.Definitions.html#2140" class="Bound Operator">_≈_</a> <a id="2144" href="Relation.Binary.Definitions.html#2144" class="Bound Operator">_≤_</a> <a id="2148" class="Symbol">=</a> <a id="2150" href="Relation.Binary.Definitions.html#1960" class="Function">Antisym</a> <a id="2158" href="Relation.Binary.Definitions.html#2144" class="Bound Operator">_≤_</a> <a id="2162" href="Relation.Binary.Definitions.html#2144" class="Bound Operator">_≤_</a> <a id="2166" href="Relation.Binary.Definitions.html#2140" class="Bound Operator">_≈_</a>
|
||
|
||
<a id="2171" class="Comment">-- Irreflexivity - this is defined terms of the underlying equality.</a>
|
||
|
||
<a id="Irreflexive"></a><a id="2241" href="Relation.Binary.Definitions.html#2241" class="Function">Irreflexive</a> <a id="2253" class="Symbol">:</a> <a id="2255" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="2259" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="2261" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="2263" href="Relation.Binary.Definitions.html#703" class="Generalizable">ℓ₁</a> <a id="2266" class="Symbol">→</a> <a id="2268" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="2272" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="2274" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="2276" href="Relation.Binary.Definitions.html#706" class="Generalizable">ℓ₂</a> <a id="2279" class="Symbol">→</a> <a id="2281" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2285" class="Symbol">_</a>
|
||
<a id="2287" href="Relation.Binary.Definitions.html#2241" class="Function">Irreflexive</a> <a id="2299" href="Relation.Binary.Definitions.html#2299" class="Bound Operator">_≈_</a> <a id="2303" href="Relation.Binary.Definitions.html#2303" class="Bound Operator">_<_</a> <a id="2307" class="Symbol">=</a> <a id="2309" class="Symbol">∀</a> <a id="2311" class="Symbol">{</a><a id="2312" href="Relation.Binary.Definitions.html#2312" class="Bound">x</a> <a id="2314" href="Relation.Binary.Definitions.html#2314" class="Bound">y</a><a id="2315" class="Symbol">}</a> <a id="2317" class="Symbol">→</a> <a id="2319" href="Relation.Binary.Definitions.html#2312" class="Bound">x</a> <a id="2321" href="Relation.Binary.Definitions.html#2299" class="Bound Operator">≈</a> <a id="2323" href="Relation.Binary.Definitions.html#2314" class="Bound">y</a> <a id="2325" class="Symbol">→</a> <a id="2327" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="2329" class="Symbol">(</a><a id="2330" href="Relation.Binary.Definitions.html#2312" class="Bound">x</a> <a id="2332" href="Relation.Binary.Definitions.html#2303" class="Bound Operator"><</a> <a id="2334" href="Relation.Binary.Definitions.html#2314" class="Bound">y</a><a id="2335" class="Symbol">)</a>
|
||
|
||
<a id="2338" class="Comment">-- Asymmetry.</a>
|
||
|
||
<a id="Asymmetric"></a><a id="2353" href="Relation.Binary.Definitions.html#2353" class="Function">Asymmetric</a> <a id="2364" class="Symbol">:</a> <a id="2366" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="2370" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="2372" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a> <a id="2374" class="Symbol">→</a> <a id="2376" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2380" class="Symbol">_</a>
|
||
<a id="2382" href="Relation.Binary.Definitions.html#2353" class="Function">Asymmetric</a> <a id="2393" href="Relation.Binary.Definitions.html#2393" class="Bound Operator">_<_</a> <a id="2397" class="Symbol">=</a> <a id="2399" class="Symbol">∀</a> <a id="2401" class="Symbol">{</a><a id="2402" href="Relation.Binary.Definitions.html#2402" class="Bound">x</a> <a id="2404" href="Relation.Binary.Definitions.html#2404" class="Bound">y</a><a id="2405" class="Symbol">}</a> <a id="2407" class="Symbol">→</a> <a id="2409" href="Relation.Binary.Definitions.html#2402" class="Bound">x</a> <a id="2411" href="Relation.Binary.Definitions.html#2393" class="Bound Operator"><</a> <a id="2413" href="Relation.Binary.Definitions.html#2404" class="Bound">y</a> <a id="2415" class="Symbol">→</a> <a id="2417" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="2419" class="Symbol">(</a><a id="2420" href="Relation.Binary.Definitions.html#2404" class="Bound">y</a> <a id="2422" href="Relation.Binary.Definitions.html#2393" class="Bound Operator"><</a> <a id="2424" href="Relation.Binary.Definitions.html#2402" class="Bound">x</a><a id="2425" class="Symbol">)</a>
|
||
|
||
<a id="2428" class="Comment">-- Generalised connex - exactly one of the two relations holds.</a>
|
||
|
||
<a id="Connex"></a><a id="2493" href="Relation.Binary.Definitions.html#2493" class="Function">Connex</a> <a id="2500" class="Symbol">:</a> <a id="2502" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="2506" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="2508" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="2510" href="Relation.Binary.Definitions.html#703" class="Generalizable">ℓ₁</a> <a id="2513" class="Symbol">→</a> <a id="2515" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="2519" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="2521" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="2523" href="Relation.Binary.Definitions.html#706" class="Generalizable">ℓ₂</a> <a id="2526" class="Symbol">→</a> <a id="2528" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2532" class="Symbol">_</a>
|
||
<a id="2534" href="Relation.Binary.Definitions.html#2493" class="Function">Connex</a> <a id="2541" href="Relation.Binary.Definitions.html#2541" class="Bound">P</a> <a id="2543" href="Relation.Binary.Definitions.html#2543" class="Bound">Q</a> <a id="2545" class="Symbol">=</a> <a id="2547" class="Symbol">∀</a> <a id="2549" href="Relation.Binary.Definitions.html#2549" class="Bound">x</a> <a id="2551" href="Relation.Binary.Definitions.html#2551" class="Bound">y</a> <a id="2553" class="Symbol">→</a> <a id="2555" href="Relation.Binary.Definitions.html#2541" class="Bound">P</a> <a id="2557" href="Relation.Binary.Definitions.html#2549" class="Bound">x</a> <a id="2559" href="Relation.Binary.Definitions.html#2551" class="Bound">y</a> <a id="2561" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="2563" href="Relation.Binary.Definitions.html#2543" class="Bound">Q</a> <a id="2565" href="Relation.Binary.Definitions.html#2551" class="Bound">y</a> <a id="2567" href="Relation.Binary.Definitions.html#2549" class="Bound">x</a>
|
||
|
||
<a id="2570" class="Comment">-- Totality.</a>
|
||
|
||
<a id="Total"></a><a id="2584" href="Relation.Binary.Definitions.html#2584" class="Function">Total</a> <a id="2590" class="Symbol">:</a> <a id="2592" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="2596" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="2598" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a> <a id="2600" class="Symbol">→</a> <a id="2602" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2606" class="Symbol">_</a>
|
||
<a id="2608" href="Relation.Binary.Definitions.html#2584" class="Function">Total</a> <a id="2614" href="Relation.Binary.Definitions.html#2614" class="Bound Operator">_∼_</a> <a id="2618" class="Symbol">=</a> <a id="2620" href="Relation.Binary.Definitions.html#2493" class="Function">Connex</a> <a id="2627" href="Relation.Binary.Definitions.html#2614" class="Bound Operator">_∼_</a> <a id="2631" href="Relation.Binary.Definitions.html#2614" class="Bound Operator">_∼_</a>
|
||
|
||
<a id="2636" class="Comment">-- Generalised trichotomy - exactly one of three types has a witness.</a>
|
||
|
||
<a id="2707" class="Keyword">data</a> <a id="Tri"></a><a id="2712" href="Relation.Binary.Definitions.html#2712" class="Datatype">Tri</a> <a id="2716" class="Symbol">(</a><a id="2717" href="Relation.Binary.Definitions.html#2717" class="Bound">A</a> <a id="2719" class="Symbol">:</a> <a id="2721" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2725" href="Relation.Binary.Definitions.html#695" class="Generalizable">a</a><a id="2726" class="Symbol">)</a> <a id="2728" class="Symbol">(</a><a id="2729" href="Relation.Binary.Definitions.html#2729" class="Bound">B</a> <a id="2731" class="Symbol">:</a> <a id="2733" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2737" href="Relation.Binary.Definitions.html#697" class="Generalizable">b</a><a id="2738" class="Symbol">)</a> <a id="2740" class="Symbol">(</a><a id="2741" href="Relation.Binary.Definitions.html#2741" class="Bound">C</a> <a id="2743" class="Symbol">:</a> <a id="2745" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2749" href="Relation.Binary.Definitions.html#699" class="Generalizable">c</a><a id="2750" class="Symbol">)</a> <a id="2752" class="Symbol">:</a> <a id="2754" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2758" class="Symbol">(</a><a id="2759" href="Relation.Binary.Definitions.html#2725" class="Bound">a</a> <a id="2761" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2763" href="Relation.Binary.Definitions.html#2737" class="Bound">b</a> <a id="2765" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2767" href="Relation.Binary.Definitions.html#2749" class="Bound">c</a><a id="2768" class="Symbol">)</a> <a id="2770" class="Keyword">where</a>
|
||
<a id="Tri.tri<"></a><a id="2778" href="Relation.Binary.Definitions.html#2778" class="InductiveConstructor">tri<</a> <a id="2783" class="Symbol">:</a> <a id="2785" class="Symbol">(</a> <a id="2787" href="Relation.Binary.Definitions.html#2787" class="Bound">a</a> <a id="2789" class="Symbol">:</a> <a id="2793" href="Relation.Binary.Definitions.html#2717" class="Bound">A</a><a id="2794" class="Symbol">)</a> <a id="2796" class="Symbol">(</a><a id="2797" href="Relation.Binary.Definitions.html#2797" class="Bound">¬b</a> <a id="2800" class="Symbol">:</a> <a id="2802" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="2804" href="Relation.Binary.Definitions.html#2729" class="Bound">B</a><a id="2805" class="Symbol">)</a> <a id="2807" class="Symbol">(</a><a id="2808" href="Relation.Binary.Definitions.html#2808" class="Bound">¬c</a> <a id="2811" class="Symbol">:</a> <a id="2813" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="2815" href="Relation.Binary.Definitions.html#2741" class="Bound">C</a><a id="2816" class="Symbol">)</a> <a id="2818" class="Symbol">→</a> <a id="2820" href="Relation.Binary.Definitions.html#2712" class="Datatype">Tri</a> <a id="2824" href="Relation.Binary.Definitions.html#2717" class="Bound">A</a> <a id="2826" href="Relation.Binary.Definitions.html#2729" class="Bound">B</a> <a id="2828" href="Relation.Binary.Definitions.html#2741" class="Bound">C</a>
|
||
<a id="Tri.tri≈"></a><a id="2832" href="Relation.Binary.Definitions.html#2832" class="InductiveConstructor">tri≈</a> <a id="2837" class="Symbol">:</a> <a id="2839" class="Symbol">(</a><a id="2840" href="Relation.Binary.Definitions.html#2840" class="Bound">¬a</a> <a id="2843" class="Symbol">:</a> <a id="2845" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="2847" href="Relation.Binary.Definitions.html#2717" class="Bound">A</a><a id="2848" class="Symbol">)</a> <a id="2850" class="Symbol">(</a> <a id="2852" href="Relation.Binary.Definitions.html#2852" class="Bound">b</a> <a id="2854" class="Symbol">:</a> <a id="2858" href="Relation.Binary.Definitions.html#2729" class="Bound">B</a><a id="2859" class="Symbol">)</a> <a id="2861" class="Symbol">(</a><a id="2862" href="Relation.Binary.Definitions.html#2862" class="Bound">¬c</a> <a id="2865" class="Symbol">:</a> <a id="2867" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="2869" href="Relation.Binary.Definitions.html#2741" class="Bound">C</a><a id="2870" class="Symbol">)</a> <a id="2872" class="Symbol">→</a> <a id="2874" href="Relation.Binary.Definitions.html#2712" class="Datatype">Tri</a> <a id="2878" href="Relation.Binary.Definitions.html#2717" class="Bound">A</a> <a id="2880" href="Relation.Binary.Definitions.html#2729" class="Bound">B</a> <a id="2882" href="Relation.Binary.Definitions.html#2741" class="Bound">C</a>
|
||
<a id="Tri.tri>"></a><a id="2886" href="Relation.Binary.Definitions.html#2886" class="InductiveConstructor">tri></a> <a id="2891" class="Symbol">:</a> <a id="2893" class="Symbol">(</a><a id="2894" href="Relation.Binary.Definitions.html#2894" class="Bound">¬a</a> <a id="2897" class="Symbol">:</a> <a id="2899" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="2901" href="Relation.Binary.Definitions.html#2717" class="Bound">A</a><a id="2902" class="Symbol">)</a> <a id="2904" class="Symbol">(</a><a id="2905" href="Relation.Binary.Definitions.html#2905" class="Bound">¬b</a> <a id="2908" class="Symbol">:</a> <a id="2910" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="2912" href="Relation.Binary.Definitions.html#2729" class="Bound">B</a><a id="2913" class="Symbol">)</a> <a id="2915" class="Symbol">(</a> <a id="2917" href="Relation.Binary.Definitions.html#2917" class="Bound">c</a> <a id="2919" class="Symbol">:</a> <a id="2923" href="Relation.Binary.Definitions.html#2741" class="Bound">C</a><a id="2924" class="Symbol">)</a> <a id="2926" class="Symbol">→</a> <a id="2928" href="Relation.Binary.Definitions.html#2712" class="Datatype">Tri</a> <a id="2932" href="Relation.Binary.Definitions.html#2717" class="Bound">A</a> <a id="2934" href="Relation.Binary.Definitions.html#2729" class="Bound">B</a> <a id="2936" href="Relation.Binary.Definitions.html#2741" class="Bound">C</a>
|
||
|
||
<a id="2939" class="Comment">-- Trichotomy.</a>
|
||
|
||
<a id="Trichotomous"></a><a id="2955" href="Relation.Binary.Definitions.html#2955" class="Function">Trichotomous</a> <a id="2968" class="Symbol">:</a> <a id="2970" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="2974" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="2976" href="Relation.Binary.Definitions.html#703" class="Generalizable">ℓ₁</a> <a id="2979" class="Symbol">→</a> <a id="2981" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="2985" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="2987" href="Relation.Binary.Definitions.html#706" class="Generalizable">ℓ₂</a> <a id="2990" class="Symbol">→</a> <a id="2992" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2996" class="Symbol">_</a>
|
||
<a id="2998" href="Relation.Binary.Definitions.html#2955" class="Function">Trichotomous</a> <a id="3011" href="Relation.Binary.Definitions.html#3011" class="Bound Operator">_≈_</a> <a id="3015" href="Relation.Binary.Definitions.html#3015" class="Bound Operator">_<_</a> <a id="3019" class="Symbol">=</a> <a id="3021" class="Symbol">∀</a> <a id="3023" href="Relation.Binary.Definitions.html#3023" class="Bound">x</a> <a id="3025" href="Relation.Binary.Definitions.html#3025" class="Bound">y</a> <a id="3027" class="Symbol">→</a> <a id="3029" href="Relation.Binary.Definitions.html#2712" class="Datatype">Tri</a> <a id="3033" class="Symbol">(</a><a id="3034" href="Relation.Binary.Definitions.html#3023" class="Bound">x</a> <a id="3036" href="Relation.Binary.Definitions.html#3015" class="Bound Operator"><</a> <a id="3038" href="Relation.Binary.Definitions.html#3025" class="Bound">y</a><a id="3039" class="Symbol">)</a> <a id="3041" class="Symbol">(</a><a id="3042" href="Relation.Binary.Definitions.html#3023" class="Bound">x</a> <a id="3044" href="Relation.Binary.Definitions.html#3011" class="Bound Operator">≈</a> <a id="3046" href="Relation.Binary.Definitions.html#3025" class="Bound">y</a><a id="3047" class="Symbol">)</a> <a id="3049" class="Symbol">(</a><a id="3050" href="Relation.Binary.Definitions.html#3023" class="Bound">x</a> <a id="3052" href="Relation.Binary.Definitions.html#3065" class="Function Operator">></a> <a id="3054" href="Relation.Binary.Definitions.html#3025" class="Bound">y</a><a id="3055" class="Symbol">)</a>
|
||
<a id="3059" class="Keyword">where</a> <a id="3065" href="Relation.Binary.Definitions.html#3065" class="Function Operator">_>_</a> <a id="3069" class="Symbol">=</a> <a id="3071" href="Function.Base.html#1554" class="Function">flip</a> <a id="3076" href="Relation.Binary.Definitions.html#3015" class="Bound Operator">_<_</a>
|
||
|
||
<a id="3081" class="Comment">-- Generalised maximum element.</a>
|
||
|
||
<a id="Max"></a><a id="3114" href="Relation.Binary.Definitions.html#3114" class="Function">Max</a> <a id="3118" class="Symbol">:</a> <a id="3120" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="3124" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="3126" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="3128" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a> <a id="3130" class="Symbol">→</a> <a id="3132" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="3134" class="Symbol">→</a> <a id="3136" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3140" class="Symbol">_</a>
|
||
<a id="3142" href="Relation.Binary.Definitions.html#3114" class="Function">Max</a> <a id="3146" href="Relation.Binary.Definitions.html#3146" class="Bound Operator">_≤_</a> <a id="3150" href="Relation.Binary.Definitions.html#3150" class="Bound">T</a> <a id="3152" class="Symbol">=</a> <a id="3154" class="Symbol">∀</a> <a id="3156" href="Relation.Binary.Definitions.html#3156" class="Bound">x</a> <a id="3158" class="Symbol">→</a> <a id="3160" href="Relation.Binary.Definitions.html#3156" class="Bound">x</a> <a id="3162" href="Relation.Binary.Definitions.html#3146" class="Bound Operator">≤</a> <a id="3164" href="Relation.Binary.Definitions.html#3150" class="Bound">T</a>
|
||
|
||
<a id="3167" class="Comment">-- Maximum element.</a>
|
||
|
||
<a id="Maximum"></a><a id="3188" href="Relation.Binary.Definitions.html#3188" class="Function">Maximum</a> <a id="3196" class="Symbol">:</a> <a id="3198" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="3202" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="3204" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a> <a id="3206" class="Symbol">→</a> <a id="3208" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="3210" class="Symbol">→</a> <a id="3212" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3216" class="Symbol">_</a>
|
||
<a id="3218" href="Relation.Binary.Definitions.html#3188" class="Function">Maximum</a> <a id="3226" class="Symbol">=</a> <a id="3228" href="Relation.Binary.Definitions.html#3114" class="Function">Max</a>
|
||
|
||
<a id="3233" class="Comment">-- Generalised minimum element.</a>
|
||
|
||
<a id="Min"></a><a id="3266" href="Relation.Binary.Definitions.html#3266" class="Function">Min</a> <a id="3270" class="Symbol">:</a> <a id="3272" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="3276" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="3278" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="3280" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a> <a id="3282" class="Symbol">→</a> <a id="3284" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="3286" class="Symbol">→</a> <a id="3288" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3292" class="Symbol">_</a>
|
||
<a id="3294" href="Relation.Binary.Definitions.html#3266" class="Function">Min</a> <a id="3298" href="Relation.Binary.Definitions.html#3298" class="Bound">R</a> <a id="3300" class="Symbol">=</a> <a id="3302" href="Relation.Binary.Definitions.html#3114" class="Function">Max</a> <a id="3306" class="Symbol">(</a><a id="3307" href="Function.Base.html#1554" class="Function">flip</a> <a id="3312" href="Relation.Binary.Definitions.html#3298" class="Bound">R</a><a id="3313" class="Symbol">)</a>
|
||
|
||
<a id="3316" class="Comment">-- Minimum element.</a>
|
||
|
||
<a id="Minimum"></a><a id="3337" href="Relation.Binary.Definitions.html#3337" class="Function">Minimum</a> <a id="3345" class="Symbol">:</a> <a id="3347" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="3351" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="3353" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a> <a id="3355" class="Symbol">→</a> <a id="3357" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="3359" class="Symbol">→</a> <a id="3361" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3365" class="Symbol">_</a>
|
||
<a id="3367" href="Relation.Binary.Definitions.html#3337" class="Function">Minimum</a> <a id="3375" class="Symbol">=</a> <a id="3377" href="Relation.Binary.Definitions.html#3266" class="Function">Min</a>
|
||
|
||
<a id="3382" class="Comment">-- Unary relations respecting a binary relation.</a>
|
||
|
||
<a id="_⟶_Respects_"></a><a id="3432" href="Relation.Binary.Definitions.html#3432" class="Function Operator">_⟶_Respects_</a> <a id="3445" class="Symbol">:</a> <a id="3447" class="Symbol">(</a><a id="3448" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="3450" class="Symbol">→</a> <a id="3452" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3456" href="Relation.Binary.Definitions.html#703" class="Generalizable">ℓ₁</a><a id="3458" class="Symbol">)</a> <a id="3460" class="Symbol">→</a> <a id="3462" class="Symbol">(</a><a id="3463" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="3465" class="Symbol">→</a> <a id="3467" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3471" href="Relation.Binary.Definitions.html#706" class="Generalizable">ℓ₂</a><a id="3473" class="Symbol">)</a> <a id="3475" class="Symbol">→</a> <a id="3477" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="3481" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="3483" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="3485" href="Relation.Binary.Definitions.html#709" class="Generalizable">ℓ₃</a> <a id="3488" class="Symbol">→</a> <a id="3490" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3494" class="Symbol">_</a>
|
||
<a id="3496" href="Relation.Binary.Definitions.html#3496" class="Bound">P</a> <a id="3498" href="Relation.Binary.Definitions.html#3432" class="Function Operator">⟶</a> <a id="3500" href="Relation.Binary.Definitions.html#3500" class="Bound">Q</a> <a id="3502" href="Relation.Binary.Definitions.html#3432" class="Function Operator">Respects</a> <a id="3511" href="Relation.Binary.Definitions.html#3511" class="Bound Operator">_∼_</a> <a id="3515" class="Symbol">=</a> <a id="3517" class="Symbol">∀</a> <a id="3519" class="Symbol">{</a><a id="3520" href="Relation.Binary.Definitions.html#3520" class="Bound">x</a> <a id="3522" href="Relation.Binary.Definitions.html#3522" class="Bound">y</a><a id="3523" class="Symbol">}</a> <a id="3525" class="Symbol">→</a> <a id="3527" href="Relation.Binary.Definitions.html#3520" class="Bound">x</a> <a id="3529" href="Relation.Binary.Definitions.html#3511" class="Bound Operator">∼</a> <a id="3531" href="Relation.Binary.Definitions.html#3522" class="Bound">y</a> <a id="3533" class="Symbol">→</a> <a id="3535" href="Relation.Binary.Definitions.html#3496" class="Bound">P</a> <a id="3537" href="Relation.Binary.Definitions.html#3520" class="Bound">x</a> <a id="3539" class="Symbol">→</a> <a id="3541" href="Relation.Binary.Definitions.html#3500" class="Bound">Q</a> <a id="3543" href="Relation.Binary.Definitions.html#3522" class="Bound">y</a>
|
||
|
||
<a id="3546" class="Comment">-- Unary relation respects a binary relation.</a>
|
||
|
||
<a id="_Respects_"></a><a id="3593" href="Relation.Binary.Definitions.html#3593" class="Function Operator">_Respects_</a> <a id="3604" class="Symbol">:</a> <a id="3606" class="Symbol">(</a><a id="3607" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="3609" class="Symbol">→</a> <a id="3611" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3615" href="Relation.Binary.Definitions.html#703" class="Generalizable">ℓ₁</a><a id="3617" class="Symbol">)</a> <a id="3619" class="Symbol">→</a> <a id="3621" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="3625" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="3627" href="Relation.Binary.Definitions.html#706" class="Generalizable">ℓ₂</a> <a id="3630" class="Symbol">→</a> <a id="3632" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3636" class="Symbol">_</a>
|
||
<a id="3638" href="Relation.Binary.Definitions.html#3638" class="Bound">P</a> <a id="3640" href="Relation.Binary.Definitions.html#3593" class="Function Operator">Respects</a> <a id="3649" href="Relation.Binary.Definitions.html#3649" class="Bound Operator">_∼_</a> <a id="3653" class="Symbol">=</a> <a id="3655" href="Relation.Binary.Definitions.html#3638" class="Bound">P</a> <a id="3657" href="Relation.Binary.Definitions.html#3432" class="Function Operator">⟶</a> <a id="3659" href="Relation.Binary.Definitions.html#3638" class="Bound">P</a> <a id="3661" href="Relation.Binary.Definitions.html#3432" class="Function Operator">Respects</a> <a id="3670" href="Relation.Binary.Definitions.html#3649" class="Bound Operator">_∼_</a>
|
||
|
||
<a id="3675" class="Comment">-- Right respecting - relatedness is preserved on the right by equality.</a>
|
||
|
||
<a id="_Respectsʳ_"></a><a id="3749" href="Relation.Binary.Definitions.html#3749" class="Function Operator">_Respectsʳ_</a> <a id="3761" class="Symbol">:</a> <a id="3763" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="3767" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="3769" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="3771" href="Relation.Binary.Definitions.html#703" class="Generalizable">ℓ₁</a> <a id="3774" class="Symbol">→</a> <a id="3776" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="3780" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="3782" href="Relation.Binary.Definitions.html#706" class="Generalizable">ℓ₂</a> <a id="3785" class="Symbol">→</a> <a id="3787" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3791" class="Symbol">_</a>
|
||
<a id="3793" href="Relation.Binary.Definitions.html#3793" class="Bound Operator">_∼_</a> <a id="3797" href="Relation.Binary.Definitions.html#3749" class="Function Operator">Respectsʳ</a> <a id="3807" href="Relation.Binary.Definitions.html#3807" class="Bound Operator">_≈_</a> <a id="3811" class="Symbol">=</a> <a id="3813" class="Symbol">∀</a> <a id="3815" class="Symbol">{</a><a id="3816" href="Relation.Binary.Definitions.html#3816" class="Bound">x</a><a id="3817" class="Symbol">}</a> <a id="3819" class="Symbol">→</a> <a id="3821" class="Symbol">(</a><a id="3822" href="Relation.Binary.Definitions.html#3816" class="Bound">x</a> <a id="3824" href="Relation.Binary.Definitions.html#3793" class="Bound Operator">∼_</a><a id="3826" class="Symbol">)</a> <a id="3828" href="Relation.Binary.Definitions.html#3593" class="Function Operator">Respects</a> <a id="3837" href="Relation.Binary.Definitions.html#3807" class="Bound Operator">_≈_</a>
|
||
|
||
<a id="3842" class="Comment">-- Left respecting - relatedness is preserved on the left by equality.</a>
|
||
|
||
<a id="_Respectsˡ_"></a><a id="3914" href="Relation.Binary.Definitions.html#3914" class="Function Operator">_Respectsˡ_</a> <a id="3926" class="Symbol">:</a> <a id="3928" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="3932" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="3934" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="3936" href="Relation.Binary.Definitions.html#703" class="Generalizable">ℓ₁</a> <a id="3939" class="Symbol">→</a> <a id="3941" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="3945" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="3947" href="Relation.Binary.Definitions.html#706" class="Generalizable">ℓ₂</a> <a id="3950" class="Symbol">→</a> <a id="3952" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3956" class="Symbol">_</a>
|
||
<a id="3958" href="Relation.Binary.Definitions.html#3958" class="Bound">P</a> <a id="3960" href="Relation.Binary.Definitions.html#3914" class="Function Operator">Respectsˡ</a> <a id="3970" href="Relation.Binary.Definitions.html#3970" class="Bound Operator">_∼_</a> <a id="3974" class="Symbol">=</a> <a id="3976" class="Symbol">∀</a> <a id="3978" class="Symbol">{</a><a id="3979" href="Relation.Binary.Definitions.html#3979" class="Bound">y</a><a id="3980" class="Symbol">}</a> <a id="3982" class="Symbol">→</a> <a id="3984" class="Symbol">(</a><a id="3985" href="Function.Base.html#1554" class="Function">flip</a> <a id="3990" href="Relation.Binary.Definitions.html#3958" class="Bound">P</a> <a id="3992" href="Relation.Binary.Definitions.html#3979" class="Bound">y</a><a id="3993" class="Symbol">)</a> <a id="3995" href="Relation.Binary.Definitions.html#3593" class="Function Operator">Respects</a> <a id="4004" href="Relation.Binary.Definitions.html#3970" class="Bound Operator">_∼_</a>
|
||
|
||
<a id="4009" class="Comment">-- Respecting - relatedness is preserved on both sides by equality</a>
|
||
|
||
<a id="_Respects₂_"></a><a id="4077" href="Relation.Binary.Definitions.html#4077" class="Function Operator">_Respects₂_</a> <a id="4089" class="Symbol">:</a> <a id="4091" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="4095" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="4097" href="Relation.Binary.Definitions.html#703" class="Generalizable">ℓ₁</a> <a id="4100" class="Symbol">→</a> <a id="4102" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="4106" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="4108" href="Relation.Binary.Definitions.html#706" class="Generalizable">ℓ₂</a> <a id="4111" class="Symbol">→</a> <a id="4113" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4117" class="Symbol">_</a>
|
||
<a id="4119" href="Relation.Binary.Definitions.html#4119" class="Bound">P</a> <a id="4121" href="Relation.Binary.Definitions.html#4077" class="Function Operator">Respects₂</a> <a id="4131" href="Relation.Binary.Definitions.html#4131" class="Bound Operator">_∼_</a> <a id="4135" class="Symbol">=</a> <a id="4137" class="Symbol">(</a><a id="4138" href="Relation.Binary.Definitions.html#4119" class="Bound">P</a> <a id="4140" href="Relation.Binary.Definitions.html#3749" class="Function Operator">Respectsʳ</a> <a id="4150" href="Relation.Binary.Definitions.html#4131" class="Bound Operator">_∼_</a><a id="4153" class="Symbol">)</a> <a id="4155" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="4157" class="Symbol">(</a><a id="4158" href="Relation.Binary.Definitions.html#4119" class="Bound">P</a> <a id="4160" href="Relation.Binary.Definitions.html#3914" class="Function Operator">Respectsˡ</a> <a id="4170" href="Relation.Binary.Definitions.html#4131" class="Bound Operator">_∼_</a><a id="4173" class="Symbol">)</a>
|
||
|
||
<a id="4176" class="Comment">-- Substitutivity - any two related elements satisfy exactly the same</a>
|
||
<a id="4246" class="Comment">-- set of unary relations. Note that only the various derivatives</a>
|
||
<a id="4312" class="Comment">-- of propositional equality can satisfy this property.</a>
|
||
|
||
<a id="Substitutive"></a><a id="4369" href="Relation.Binary.Definitions.html#4369" class="Function">Substitutive</a> <a id="4382" class="Symbol">:</a> <a id="4384" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="4388" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="4390" href="Relation.Binary.Definitions.html#703" class="Generalizable">ℓ₁</a> <a id="4393" class="Symbol">→</a> <a id="4395" class="Symbol">(</a><a id="4396" href="Relation.Binary.Definitions.html#4396" class="Bound">ℓ₂</a> <a id="4399" class="Symbol">:</a> <a id="4401" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="4406" class="Symbol">)</a> <a id="4408" class="Symbol">→</a> <a id="4410" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4414" class="Symbol">_</a>
|
||
<a id="4416" href="Relation.Binary.Definitions.html#4369" class="Function">Substitutive</a> <a id="4429" class="Symbol">{</a><a id="4430" class="Argument">A</a> <a id="4432" class="Symbol">=</a> <a id="4434" href="Relation.Binary.Definitions.html#4434" class="Bound">A</a><a id="4435" class="Symbol">}</a> <a id="4437" href="Relation.Binary.Definitions.html#4437" class="Bound Operator">_∼_</a> <a id="4441" href="Relation.Binary.Definitions.html#4441" class="Bound">p</a> <a id="4443" class="Symbol">=</a> <a id="4445" class="Symbol">(</a><a id="4446" href="Relation.Binary.Definitions.html#4446" class="Bound">P</a> <a id="4448" class="Symbol">:</a> <a id="4450" href="Relation.Binary.Definitions.html#4434" class="Bound">A</a> <a id="4452" class="Symbol">→</a> <a id="4454" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4458" href="Relation.Binary.Definitions.html#4441" class="Bound">p</a><a id="4459" class="Symbol">)</a> <a id="4461" class="Symbol">→</a> <a id="4463" href="Relation.Binary.Definitions.html#4446" class="Bound">P</a> <a id="4465" href="Relation.Binary.Definitions.html#3593" class="Function Operator">Respects</a> <a id="4474" href="Relation.Binary.Definitions.html#4437" class="Bound Operator">_∼_</a>
|
||
|
||
<a id="4479" class="Comment">-- Decidability - it is possible to determine whether a given pair of</a>
|
||
<a id="4549" class="Comment">-- elements are related.</a>
|
||
|
||
<a id="Decidable"></a><a id="4575" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="4585" class="Symbol">:</a> <a id="4587" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="4591" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="4593" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="4595" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a> <a id="4597" class="Symbol">→</a> <a id="4599" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4603" class="Symbol">_</a>
|
||
<a id="4605" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="4615" href="Relation.Binary.Definitions.html#4615" class="Bound Operator">_∼_</a> <a id="4619" class="Symbol">=</a> <a id="4621" class="Symbol">∀</a> <a id="4623" href="Relation.Binary.Definitions.html#4623" class="Bound">x</a> <a id="4625" href="Relation.Binary.Definitions.html#4625" class="Bound">y</a> <a id="4627" class="Symbol">→</a> <a id="4629" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="4633" class="Symbol">(</a><a id="4634" href="Relation.Binary.Definitions.html#4623" class="Bound">x</a> <a id="4636" href="Relation.Binary.Definitions.html#4615" class="Bound Operator">∼</a> <a id="4638" href="Relation.Binary.Definitions.html#4625" class="Bound">y</a><a id="4639" class="Symbol">)</a>
|
||
|
||
<a id="4642" class="Comment">-- Weak decidability - it is sometimes possible to determine if a given</a>
|
||
<a id="4714" class="Comment">-- pair of elements are related.</a>
|
||
|
||
<a id="WeaklyDecidable"></a><a id="4748" href="Relation.Binary.Definitions.html#4748" class="Function">WeaklyDecidable</a> <a id="4764" class="Symbol">:</a> <a id="4766" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="4770" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="4772" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="4774" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a> <a id="4776" class="Symbol">→</a> <a id="4778" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4782" class="Symbol">_</a>
|
||
<a id="4784" href="Relation.Binary.Definitions.html#4748" class="Function">WeaklyDecidable</a> <a id="4800" href="Relation.Binary.Definitions.html#4800" class="Bound Operator">_∼_</a> <a id="4804" class="Symbol">=</a> <a id="4806" class="Symbol">∀</a> <a id="4808" href="Relation.Binary.Definitions.html#4808" class="Bound">x</a> <a id="4810" href="Relation.Binary.Definitions.html#4810" class="Bound">y</a> <a id="4812" class="Symbol">→</a> <a id="4814" href="Agda.Builtin.Maybe.html#136" class="Datatype">Maybe</a> <a id="4820" class="Symbol">(</a><a id="4821" href="Relation.Binary.Definitions.html#4808" class="Bound">x</a> <a id="4823" href="Relation.Binary.Definitions.html#4800" class="Bound Operator">∼</a> <a id="4825" href="Relation.Binary.Definitions.html#4810" class="Bound">y</a><a id="4826" class="Symbol">)</a>
|
||
|
||
<a id="4829" class="Comment">-- Propositional equality is decidable for the type.</a>
|
||
|
||
<a id="DecidableEquality"></a><a id="4883" href="Relation.Binary.Definitions.html#4883" class="Function">DecidableEquality</a> <a id="4901" class="Symbol">:</a> <a id="4903" class="Symbol">(</a><a id="4904" href="Relation.Binary.Definitions.html#4904" class="Bound">A</a> <a id="4906" class="Symbol">:</a> <a id="4908" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4912" href="Relation.Binary.Definitions.html#695" class="Generalizable">a</a><a id="4913" class="Symbol">)</a> <a id="4915" class="Symbol">→</a> <a id="4917" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4921" class="Symbol">_</a>
|
||
<a id="4923" href="Relation.Binary.Definitions.html#4883" class="Function">DecidableEquality</a> <a id="4941" href="Relation.Binary.Definitions.html#4941" class="Bound">A</a> <a id="4943" class="Symbol">=</a> <a id="4945" href="Relation.Binary.Definitions.html#4575" class="Function">Decidable</a> <a id="4955" class="Symbol">{</a><a id="4956" class="Argument">A</a> <a id="4958" class="Symbol">=</a> <a id="4960" href="Relation.Binary.Definitions.html#4941" class="Bound">A</a><a id="4961" class="Symbol">}</a> <a id="4963" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a>
|
||
|
||
<a id="4968" class="Comment">-- Irrelevancy - all proofs that a given pair of elements are related</a>
|
||
<a id="5038" class="Comment">-- are indistinguishable.</a>
|
||
|
||
<a id="Irrelevant"></a><a id="5065" href="Relation.Binary.Definitions.html#5065" class="Function">Irrelevant</a> <a id="5076" class="Symbol">:</a> <a id="5078" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="5082" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="5084" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="5086" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a> <a id="5088" class="Symbol">→</a> <a id="5090" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5094" class="Symbol">_</a>
|
||
<a id="5096" href="Relation.Binary.Definitions.html#5065" class="Function">Irrelevant</a> <a id="5107" href="Relation.Binary.Definitions.html#5107" class="Bound Operator">_∼_</a> <a id="5111" class="Symbol">=</a> <a id="5113" class="Symbol">∀</a> <a id="5115" class="Symbol">{</a><a id="5116" href="Relation.Binary.Definitions.html#5116" class="Bound">x</a> <a id="5118" href="Relation.Binary.Definitions.html#5118" class="Bound">y</a><a id="5119" class="Symbol">}</a> <a id="5121" class="Symbol">(</a><a id="5122" href="Relation.Binary.Definitions.html#5122" class="Bound">a</a> <a id="5124" href="Relation.Binary.Definitions.html#5124" class="Bound">b</a> <a id="5126" class="Symbol">:</a> <a id="5128" href="Relation.Binary.Definitions.html#5116" class="Bound">x</a> <a id="5130" href="Relation.Binary.Definitions.html#5107" class="Bound Operator">∼</a> <a id="5132" href="Relation.Binary.Definitions.html#5118" class="Bound">y</a><a id="5133" class="Symbol">)</a> <a id="5135" class="Symbol">→</a> <a id="5137" href="Relation.Binary.Definitions.html#5122" class="Bound">a</a> <a id="5139" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="5141" href="Relation.Binary.Definitions.html#5124" class="Bound">b</a>
|
||
|
||
<a id="5144" class="Comment">-- Recomputability - we can rebuild a relevant proof given an</a>
|
||
<a id="5206" class="Comment">-- irrelevant one.</a>
|
||
|
||
<a id="Recomputable"></a><a id="5226" href="Relation.Binary.Definitions.html#5226" class="Function">Recomputable</a> <a id="5239" class="Symbol">:</a> <a id="5241" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="5245" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="5247" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="5249" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a> <a id="5251" class="Symbol">→</a> <a id="5253" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5257" class="Symbol">_</a>
|
||
<a id="5259" href="Relation.Binary.Definitions.html#5226" class="Function">Recomputable</a> <a id="5272" href="Relation.Binary.Definitions.html#5272" class="Bound Operator">_∼_</a> <a id="5276" class="Symbol">=</a> <a id="5278" class="Symbol">∀</a> <a id="5280" class="Symbol">{</a><a id="5281" href="Relation.Binary.Definitions.html#5281" class="Bound">x</a> <a id="5283" href="Relation.Binary.Definitions.html#5283" class="Bound">y</a><a id="5284" class="Symbol">}</a> <a id="5286" class="Symbol">→</a> <a id="5288" class="Symbol">.(</a><a id="5290" href="Relation.Binary.Definitions.html#5281" class="Bound">x</a> <a id="5292" href="Relation.Binary.Definitions.html#5272" class="Bound Operator">∼</a> <a id="5294" href="Relation.Binary.Definitions.html#5283" class="Bound">y</a><a id="5295" class="Symbol">)</a> <a id="5297" class="Symbol">→</a> <a id="5299" href="Relation.Binary.Definitions.html#5281" class="Bound">x</a> <a id="5301" href="Relation.Binary.Definitions.html#5272" class="Bound Operator">∼</a> <a id="5303" href="Relation.Binary.Definitions.html#5283" class="Bound">y</a>
|
||
|
||
<a id="5306" class="Comment">-- Universal - all pairs of elements are related</a>
|
||
|
||
<a id="Universal"></a><a id="5356" href="Relation.Binary.Definitions.html#5356" class="Function">Universal</a> <a id="5366" class="Symbol">:</a> <a id="5368" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="5372" href="Relation.Binary.Definitions.html#724" class="Generalizable">A</a> <a id="5374" href="Relation.Binary.Definitions.html#738" class="Generalizable">B</a> <a id="5376" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a> <a id="5378" class="Symbol">→</a> <a id="5380" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5384" class="Symbol">_</a>
|
||
<a id="5386" href="Relation.Binary.Definitions.html#5356" class="Function">Universal</a> <a id="5396" href="Relation.Binary.Definitions.html#5396" class="Bound Operator">_∼_</a> <a id="5400" class="Symbol">=</a> <a id="5402" class="Symbol">∀</a> <a id="5404" href="Relation.Binary.Definitions.html#5404" class="Bound">x</a> <a id="5406" href="Relation.Binary.Definitions.html#5406" class="Bound">y</a> <a id="5408" class="Symbol">→</a> <a id="5410" href="Relation.Binary.Definitions.html#5404" class="Bound">x</a> <a id="5412" href="Relation.Binary.Definitions.html#5396" class="Bound Operator">∼</a> <a id="5414" href="Relation.Binary.Definitions.html#5406" class="Bound">y</a>
|
||
|
||
<a id="5417" class="Comment">-- Non-emptiness - at least one pair of elements are related.</a>
|
||
|
||
<a id="5480" class="Keyword">record</a> <a id="NonEmpty"></a><a id="5487" href="Relation.Binary.Definitions.html#5487" class="Record">NonEmpty</a> <a id="5496" class="Symbol">{</a><a id="5497" href="Relation.Binary.Definitions.html#5497" class="Bound">A</a> <a id="5499" class="Symbol">:</a> <a id="5501" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5505" href="Relation.Binary.Definitions.html#695" class="Generalizable">a</a><a id="5506" class="Symbol">}</a> <a id="5508" class="Symbol">{</a><a id="5509" href="Relation.Binary.Definitions.html#5509" class="Bound">B</a> <a id="5511" class="Symbol">:</a> <a id="5513" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5517" href="Relation.Binary.Definitions.html#697" class="Generalizable">b</a><a id="5518" class="Symbol">}</a>
|
||
<a id="5536" class="Symbol">(</a><a id="5537" href="Relation.Binary.Definitions.html#5537" class="Bound">T</a> <a id="5539" class="Symbol">:</a> <a id="5541" href="Relation.Binary.Core.html#766" class="Function">REL</a> <a id="5545" href="Relation.Binary.Definitions.html#5497" class="Bound">A</a> <a id="5547" href="Relation.Binary.Definitions.html#5509" class="Bound">B</a> <a id="5549" href="Relation.Binary.Definitions.html#701" class="Generalizable">ℓ</a><a id="5550" class="Symbol">)</a> <a id="5552" class="Symbol">:</a> <a id="5554" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="5558" class="Symbol">(</a><a id="5559" href="Relation.Binary.Definitions.html#5505" class="Bound">a</a> <a id="5561" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="5563" href="Relation.Binary.Definitions.html#5517" class="Bound">b</a> <a id="5565" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="5567" href="Relation.Binary.Definitions.html#5549" class="Bound">ℓ</a><a id="5568" class="Symbol">)</a> <a id="5570" class="Keyword">where</a>
|
||
<a id="5578" class="Keyword">constructor</a> <a id="nonEmpty"></a><a id="5590" href="Relation.Binary.Definitions.html#5590" class="InductiveConstructor">nonEmpty</a>
|
||
<a id="5601" class="Keyword">field</a>
|
||
<a id="5611" class="Symbol">{</a><a id="NonEmpty.x"></a><a id="5612" href="Relation.Binary.Definitions.html#5612" class="Field">x</a><a id="5613" class="Symbol">}</a> <a id="5617" class="Symbol">:</a> <a id="5619" href="Relation.Binary.Definitions.html#5497" class="Bound">A</a>
|
||
<a id="5625" class="Symbol">{</a><a id="NonEmpty.y"></a><a id="5626" href="Relation.Binary.Definitions.html#5626" class="Field">y</a><a id="5627" class="Symbol">}</a> <a id="5631" class="Symbol">:</a> <a id="5633" href="Relation.Binary.Definitions.html#5509" class="Bound">B</a>
|
||
<a id="NonEmpty.proof"></a><a id="5639" href="Relation.Binary.Definitions.html#5639" class="Field">proof</a> <a id="5645" class="Symbol">:</a> <a id="5647" href="Relation.Binary.Definitions.html#5537" class="Bound">T</a> <a id="5649" href="Relation.Binary.Definitions.html#5612" class="Field">x</a> <a id="5651" href="Relation.Binary.Definitions.html#5626" class="Field">y</a>
|
||
|
||
|
||
|
||
<a id="5656" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="5729" class="Comment">-- DEPRECATED NAMES</a>
|
||
<a id="5749" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="5822" class="Comment">-- Please use the new names as continuing support for the old names is</a>
|
||
<a id="5893" class="Comment">-- not guaranteed.</a>
|
||
|
||
<a id="5913" class="Comment">-- Version 1.1</a>
|
||
|
||
<a id="Conn"></a><a id="5929" href="Relation.Binary.Definitions.html#5929" class="Function">Conn</a> <a id="5934" class="Symbol">=</a> <a id="5936" href="Relation.Binary.Definitions.html#2493" class="Function">Connex</a>
|
||
<a id="5943" class="Symbol">{-#</a> <a id="5947" class="Keyword">WARNING_ON_USAGE</a> <a id="5964" class="Pragma">Conn</a>
|
||
<a id="5969" class="String">"Warning: Conn was deprecated in v1.1.
|
||
Please use Connex instead."</a>
|
||
<a id="6036" class="Symbol">#-}</a>
|
||
</pre></body></html> |