299 lines
84 KiB
HTML
299 lines
84 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Relation.Unary</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">-- Unary relations</a>
|
||
<a id="125" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="199" class="Symbol">{-#</a> <a id="203" class="Keyword">OPTIONS</a> <a id="211" class="Pragma">--without-K</a> <a id="223" class="Pragma">--safe</a> <a id="230" class="Symbol">#-}</a>
|
||
|
||
<a id="235" class="Keyword">module</a> <a id="242" href="Relation.Unary.html" class="Module">Relation.Unary</a> <a id="257" class="Keyword">where</a>
|
||
|
||
<a id="264" class="Keyword">open</a> <a id="269" class="Keyword">import</a> <a id="276" href="Data.Empty.html" class="Module">Data.Empty</a>
|
||
<a id="287" class="Keyword">open</a> <a id="292" class="Keyword">import</a> <a id="299" href="Data.Unit.Base.html" class="Module">Data.Unit.Base</a> <a id="314" class="Keyword">using</a> <a id="320" class="Symbol">(</a><a id="321" href="Agda.Builtin.Unit.html#164" class="Record">⊤</a><a id="322" class="Symbol">)</a>
|
||
<a id="324" class="Keyword">open</a> <a id="329" class="Keyword">import</a> <a id="336" href="Data.Product.html" class="Module">Data.Product</a>
|
||
<a id="349" class="Keyword">open</a> <a id="354" class="Keyword">import</a> <a id="361" href="Data.Sum.Base.html" class="Module">Data.Sum.Base</a> <a id="375" class="Keyword">using</a> <a id="381" class="Symbol">(</a><a id="382" href="Data.Sum.Base.html#734" class="Datatype Operator">_⊎_</a><a id="385" class="Symbol">;</a> <a id="387" href="Data.Sum.Base.html#920" class="Function Operator">[_,_]</a><a id="392" class="Symbol">)</a>
|
||
<a id="394" class="Keyword">open</a> <a id="399" class="Keyword">import</a> <a id="406" href="Function.Base.html" class="Module">Function.Base</a>
|
||
<a id="420" class="Keyword">open</a> <a id="425" class="Keyword">import</a> <a id="432" href="Level.html" class="Module">Level</a>
|
||
<a id="438" class="Keyword">open</a> <a id="443" class="Keyword">import</a> <a id="450" href="Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="467" class="Keyword">hiding</a> <a id="474" class="Symbol">(</a><a id="475" href="Relation.Nullary.html#2040" class="Function">Irrelevant</a><a id="485" class="Symbol">)</a>
|
||
<a id="487" class="Keyword">open</a> <a id="492" class="Keyword">import</a> <a id="499" href="Relation.Nullary.Decidable.Core.html" class="Module">Relation.Nullary.Decidable.Core</a> <a id="531" class="Keyword">using</a> <a id="537" class="Symbol">(</a><a id="538" href="Relation.Nullary.Decidable.Core.html#1365" class="Function">True</a><a id="542" class="Symbol">)</a>
|
||
<a id="544" class="Keyword">open</a> <a id="549" class="Keyword">import</a> <a id="556" href="Relation.Binary.PropositionalEquality.Core.html" class="Module">Relation.Binary.PropositionalEquality.Core</a> <a id="599" class="Keyword">using</a> <a id="605" class="Symbol">(</a><a id="606" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a><a id="609" class="Symbol">)</a>
|
||
|
||
<a id="612" class="Keyword">private</a>
|
||
<a id="622" class="Keyword">variable</a>
|
||
<a id="635" href="Relation.Unary.html#635" class="Generalizable">a</a> <a id="637" href="Relation.Unary.html#637" class="Generalizable">b</a> <a id="639" href="Relation.Unary.html#639" class="Generalizable">c</a> <a id="641" href="Relation.Unary.html#641" class="Generalizable">ℓ</a> <a id="643" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="646" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="649" class="Symbol">:</a> <a id="651" href="Agda.Primitive.html#597" class="Postulate">Level</a>
|
||
<a id="661" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="663" class="Symbol">:</a> <a id="665" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="669" href="Relation.Unary.html#635" class="Generalizable">a</a>
|
||
<a id="675" href="Relation.Unary.html#675" class="Generalizable">B</a> <a id="677" class="Symbol">:</a> <a id="679" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="683" href="Relation.Unary.html#637" class="Generalizable">b</a>
|
||
<a id="689" href="Relation.Unary.html#689" class="Generalizable">C</a> <a id="691" class="Symbol">:</a> <a id="693" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="697" href="Relation.Unary.html#639" class="Generalizable">c</a>
|
||
|
||
<a id="700" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="773" class="Comment">-- Definition</a>
|
||
|
||
<a id="788" class="Comment">-- Unary relations are known as predicates and `Pred A ℓ` can be viewed</a>
|
||
<a id="860" class="Comment">-- as some property that elements of type A might satisfy.</a>
|
||
|
||
<a id="920" class="Comment">-- Consequently `P : Pred A ℓ` can also be seen as a subset of A</a>
|
||
<a id="985" class="Comment">-- containing all the elements of A that satisfy property P. This view</a>
|
||
<a id="1056" class="Comment">-- informs much of the notation used below.</a>
|
||
|
||
<a id="Pred"></a><a id="1101" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1106" class="Symbol">:</a> <a id="1108" class="Symbol">∀</a> <a id="1110" class="Symbol">{</a><a id="1111" href="Relation.Unary.html#1111" class="Bound">a</a><a id="1112" class="Symbol">}</a> <a id="1114" class="Symbol">→</a> <a id="1116" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1120" href="Relation.Unary.html#1111" class="Bound">a</a> <a id="1122" class="Symbol">→</a> <a id="1124" class="Symbol">(</a><a id="1125" href="Relation.Unary.html#1125" class="Bound">ℓ</a> <a id="1127" class="Symbol">:</a> <a id="1129" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="1134" class="Symbol">)</a> <a id="1136" class="Symbol">→</a> <a id="1138" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1142" class="Symbol">(</a><a id="1143" href="Relation.Unary.html#1111" class="Bound">a</a> <a id="1145" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1147" href="Agda.Primitive.html#780" class="Primitive">suc</a> <a id="1151" href="Relation.Unary.html#1125" class="Bound">ℓ</a><a id="1152" class="Symbol">)</a>
|
||
<a id="1154" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1159" href="Relation.Unary.html#1159" class="Bound">A</a> <a id="1161" href="Relation.Unary.html#1161" class="Bound">ℓ</a> <a id="1163" class="Symbol">=</a> <a id="1165" href="Relation.Unary.html#1159" class="Bound">A</a> <a id="1167" class="Symbol">→</a> <a id="1169" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1173" href="Relation.Unary.html#1161" class="Bound">ℓ</a>
|
||
|
||
<a id="1176" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="1249" class="Comment">-- Special sets</a>
|
||
|
||
<a id="1266" class="Comment">-- The empty set.</a>
|
||
|
||
<a id="∅"></a><a id="1285" href="Relation.Unary.html#1285" class="Function">∅</a> <a id="1287" class="Symbol">:</a> <a id="1289" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1294" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1296" href="Level.html#512" class="Function">0ℓ</a>
|
||
<a id="1299" href="Relation.Unary.html#1285" class="Function">∅</a> <a id="1301" class="Symbol">=</a> <a id="1303" class="Symbol">λ</a> <a id="1305" href="Relation.Unary.html#1305" class="Bound">_</a> <a id="1307" class="Symbol">→</a> <a id="1309" href="Data.Empty.html#526" class="Datatype">⊥</a>
|
||
|
||
<a id="1312" class="Comment">-- The singleton set.</a>
|
||
|
||
<a id="｛_｝"></a><a id="1335" href="Relation.Unary.html#1335" class="Function Operator">｛_｝</a> <a id="1339" class="Symbol">:</a> <a id="1341" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1343" class="Symbol">→</a> <a id="1345" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1350" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1352" class="Symbol">_</a>
|
||
<a id="1354" href="Relation.Unary.html#1335" class="Function Operator">｛</a> <a id="1356" href="Relation.Unary.html#1356" class="Bound">x</a> <a id="1358" href="Relation.Unary.html#1335" class="Function Operator">｝</a> <a id="1360" class="Symbol">=</a> <a id="1362" href="Relation.Unary.html#1356" class="Bound">x</a> <a id="1364" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡_</a>
|
||
|
||
<a id="1368" class="Comment">-- The universal set.</a>
|
||
|
||
<a id="U"></a><a id="1391" href="Relation.Unary.html#1391" class="Function">U</a> <a id="1393" class="Symbol">:</a> <a id="1395" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1400" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1402" href="Level.html#512" class="Function">0ℓ</a>
|
||
<a id="1405" href="Relation.Unary.html#1391" class="Function">U</a> <a id="1407" class="Symbol">=</a> <a id="1409" class="Symbol">λ</a> <a id="1411" href="Relation.Unary.html#1411" class="Bound">_</a> <a id="1413" class="Symbol">→</a> <a id="1415" href="Agda.Builtin.Unit.html#164" class="Record">⊤</a>
|
||
|
||
<a id="1418" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="1491" class="Comment">-- Membership</a>
|
||
|
||
<a id="1506" class="Keyword">infix</a> <a id="1512" class="Number">4</a> <a id="1514" href="Relation.Unary.html#1523" class="Function Operator">_∈_</a> <a id="1518" href="Relation.Unary.html#1563" class="Function Operator">_∉_</a>
|
||
|
||
<a id="_∈_"></a><a id="1523" href="Relation.Unary.html#1523" class="Function Operator">_∈_</a> <a id="1527" class="Symbol">:</a> <a id="1529" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1531" class="Symbol">→</a> <a id="1533" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1538" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1540" href="Relation.Unary.html#641" class="Generalizable">ℓ</a> <a id="1542" class="Symbol">→</a> <a id="1544" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1548" class="Symbol">_</a>
|
||
<a id="1550" href="Relation.Unary.html#1550" class="Bound">x</a> <a id="1552" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="1554" href="Relation.Unary.html#1554" class="Bound">P</a> <a id="1556" class="Symbol">=</a> <a id="1558" href="Relation.Unary.html#1554" class="Bound">P</a> <a id="1560" href="Relation.Unary.html#1550" class="Bound">x</a>
|
||
|
||
<a id="_∉_"></a><a id="1563" href="Relation.Unary.html#1563" class="Function Operator">_∉_</a> <a id="1567" class="Symbol">:</a> <a id="1569" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1571" class="Symbol">→</a> <a id="1573" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1578" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1580" href="Relation.Unary.html#641" class="Generalizable">ℓ</a> <a id="1582" class="Symbol">→</a> <a id="1584" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1588" class="Symbol">_</a>
|
||
<a id="1590" href="Relation.Unary.html#1590" class="Bound">x</a> <a id="1592" href="Relation.Unary.html#1563" class="Function Operator">∉</a> <a id="1594" href="Relation.Unary.html#1594" class="Bound">P</a> <a id="1596" class="Symbol">=</a> <a id="1598" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="1600" href="Relation.Unary.html#1590" class="Bound">x</a> <a id="1602" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="1604" href="Relation.Unary.html#1594" class="Bound">P</a>
|
||
|
||
<a id="1607" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="1680" class="Comment">-- Subset relations</a>
|
||
|
||
<a id="1701" class="Keyword">infix</a> <a id="1707" class="Number">4</a> <a id="1709" href="Relation.Unary.html#1742" class="Function Operator">_⊆_</a> <a id="1713" href="Relation.Unary.html#1809" class="Function Operator">_⊇_</a> <a id="1717" href="Relation.Unary.html#1860" class="Function Operator">_⊈_</a> <a id="1721" href="Relation.Unary.html#1915" class="Function Operator">_⊉_</a> <a id="1725" href="Relation.Unary.html#1970" class="Function Operator">_⊂_</a> <a id="1729" href="Relation.Unary.html#2029" class="Function Operator">_⊃_</a> <a id="1733" href="Relation.Unary.html#2080" class="Function Operator">_⊄_</a> <a id="1737" href="Relation.Unary.html#2135" class="Function Operator">_⊅_</a>
|
||
|
||
<a id="_⊆_"></a><a id="1742" href="Relation.Unary.html#1742" class="Function Operator">_⊆_</a> <a id="1746" class="Symbol">:</a> <a id="1748" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1753" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1755" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="1758" class="Symbol">→</a> <a id="1760" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1765" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1767" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="1770" class="Symbol">→</a> <a id="1772" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1776" class="Symbol">_</a>
|
||
<a id="1778" href="Relation.Unary.html#1778" class="Bound">P</a> <a id="1780" href="Relation.Unary.html#1742" class="Function Operator">⊆</a> <a id="1782" href="Relation.Unary.html#1782" class="Bound">Q</a> <a id="1784" class="Symbol">=</a> <a id="1786" class="Symbol">∀</a> <a id="1788" class="Symbol">{</a><a id="1789" href="Relation.Unary.html#1789" class="Bound">x</a><a id="1790" class="Symbol">}</a> <a id="1792" class="Symbol">→</a> <a id="1794" href="Relation.Unary.html#1789" class="Bound">x</a> <a id="1796" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="1798" href="Relation.Unary.html#1778" class="Bound">P</a> <a id="1800" class="Symbol">→</a> <a id="1802" href="Relation.Unary.html#1789" class="Bound">x</a> <a id="1804" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="1806" href="Relation.Unary.html#1782" class="Bound">Q</a>
|
||
|
||
<a id="_⊇_"></a><a id="1809" href="Relation.Unary.html#1809" class="Function Operator">_⊇_</a> <a id="1813" class="Symbol">:</a> <a id="1815" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1820" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1822" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="1825" class="Symbol">→</a> <a id="1827" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1832" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1834" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="1837" class="Symbol">→</a> <a id="1839" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1843" class="Symbol">_</a>
|
||
<a id="1845" href="Relation.Unary.html#1845" class="Bound">P</a> <a id="1847" href="Relation.Unary.html#1809" class="Function Operator">⊇</a> <a id="1849" href="Relation.Unary.html#1849" class="Bound">Q</a> <a id="1851" class="Symbol">=</a> <a id="1853" href="Relation.Unary.html#1849" class="Bound">Q</a> <a id="1855" href="Relation.Unary.html#1742" class="Function Operator">⊆</a> <a id="1857" href="Relation.Unary.html#1845" class="Bound">P</a>
|
||
|
||
<a id="_⊈_"></a><a id="1860" href="Relation.Unary.html#1860" class="Function Operator">_⊈_</a> <a id="1864" class="Symbol">:</a> <a id="1866" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1871" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1873" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="1876" class="Symbol">→</a> <a id="1878" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1883" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1885" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="1888" class="Symbol">→</a> <a id="1890" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1894" class="Symbol">_</a>
|
||
<a id="1896" href="Relation.Unary.html#1896" class="Bound">P</a> <a id="1898" href="Relation.Unary.html#1860" class="Function Operator">⊈</a> <a id="1900" href="Relation.Unary.html#1900" class="Bound">Q</a> <a id="1902" class="Symbol">=</a> <a id="1904" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="1906" class="Symbol">(</a><a id="1907" href="Relation.Unary.html#1896" class="Bound">P</a> <a id="1909" href="Relation.Unary.html#1742" class="Function Operator">⊆</a> <a id="1911" href="Relation.Unary.html#1900" class="Bound">Q</a><a id="1912" class="Symbol">)</a>
|
||
|
||
<a id="_⊉_"></a><a id="1915" href="Relation.Unary.html#1915" class="Function Operator">_⊉_</a> <a id="1919" class="Symbol">:</a> <a id="1921" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1926" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1928" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="1931" class="Symbol">→</a> <a id="1933" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1938" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1940" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="1943" class="Symbol">→</a> <a id="1945" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1949" class="Symbol">_</a>
|
||
<a id="1951" href="Relation.Unary.html#1951" class="Bound">P</a> <a id="1953" href="Relation.Unary.html#1915" class="Function Operator">⊉</a> <a id="1955" href="Relation.Unary.html#1955" class="Bound">Q</a> <a id="1957" class="Symbol">=</a> <a id="1959" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="1961" class="Symbol">(</a><a id="1962" href="Relation.Unary.html#1951" class="Bound">P</a> <a id="1964" href="Relation.Unary.html#1809" class="Function Operator">⊇</a> <a id="1966" href="Relation.Unary.html#1955" class="Bound">Q</a><a id="1967" class="Symbol">)</a>
|
||
|
||
<a id="_⊂_"></a><a id="1970" href="Relation.Unary.html#1970" class="Function Operator">_⊂_</a> <a id="1974" class="Symbol">:</a> <a id="1976" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1981" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1983" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="1986" class="Symbol">→</a> <a id="1988" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="1993" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="1995" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="1998" class="Symbol">→</a> <a id="2000" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2004" class="Symbol">_</a>
|
||
<a id="2006" href="Relation.Unary.html#2006" class="Bound">P</a> <a id="2008" href="Relation.Unary.html#1970" class="Function Operator">⊂</a> <a id="2010" href="Relation.Unary.html#2010" class="Bound">Q</a> <a id="2012" class="Symbol">=</a> <a id="2014" href="Relation.Unary.html#2006" class="Bound">P</a> <a id="2016" href="Relation.Unary.html#1742" class="Function Operator">⊆</a> <a id="2018" href="Relation.Unary.html#2010" class="Bound">Q</a> <a id="2020" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="2022" href="Relation.Unary.html#2010" class="Bound">Q</a> <a id="2024" href="Relation.Unary.html#1860" class="Function Operator">⊈</a> <a id="2026" href="Relation.Unary.html#2006" class="Bound">P</a>
|
||
|
||
<a id="_⊃_"></a><a id="2029" href="Relation.Unary.html#2029" class="Function Operator">_⊃_</a> <a id="2033" class="Symbol">:</a> <a id="2035" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2040" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2042" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="2045" class="Symbol">→</a> <a id="2047" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2052" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2054" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="2057" class="Symbol">→</a> <a id="2059" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2063" class="Symbol">_</a>
|
||
<a id="2065" href="Relation.Unary.html#2065" class="Bound">P</a> <a id="2067" href="Relation.Unary.html#2029" class="Function Operator">⊃</a> <a id="2069" href="Relation.Unary.html#2069" class="Bound">Q</a> <a id="2071" class="Symbol">=</a> <a id="2073" href="Relation.Unary.html#2069" class="Bound">Q</a> <a id="2075" href="Relation.Unary.html#1970" class="Function Operator">⊂</a> <a id="2077" href="Relation.Unary.html#2065" class="Bound">P</a>
|
||
|
||
<a id="_⊄_"></a><a id="2080" href="Relation.Unary.html#2080" class="Function Operator">_⊄_</a> <a id="2084" class="Symbol">:</a> <a id="2086" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2091" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2093" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="2096" class="Symbol">→</a> <a id="2098" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2103" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2105" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="2108" class="Symbol">→</a> <a id="2110" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2114" class="Symbol">_</a>
|
||
<a id="2116" href="Relation.Unary.html#2116" class="Bound">P</a> <a id="2118" href="Relation.Unary.html#2080" class="Function Operator">⊄</a> <a id="2120" href="Relation.Unary.html#2120" class="Bound">Q</a> <a id="2122" class="Symbol">=</a> <a id="2124" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="2126" class="Symbol">(</a><a id="2127" href="Relation.Unary.html#2116" class="Bound">P</a> <a id="2129" href="Relation.Unary.html#1970" class="Function Operator">⊂</a> <a id="2131" href="Relation.Unary.html#2120" class="Bound">Q</a><a id="2132" class="Symbol">)</a>
|
||
|
||
<a id="_⊅_"></a><a id="2135" href="Relation.Unary.html#2135" class="Function Operator">_⊅_</a> <a id="2139" class="Symbol">:</a> <a id="2141" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2146" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2148" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="2151" class="Symbol">→</a> <a id="2153" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2158" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2160" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="2163" class="Symbol">→</a> <a id="2165" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2169" class="Symbol">_</a>
|
||
<a id="2171" href="Relation.Unary.html#2171" class="Bound">P</a> <a id="2173" href="Relation.Unary.html#2135" class="Function Operator">⊅</a> <a id="2175" href="Relation.Unary.html#2175" class="Bound">Q</a> <a id="2177" class="Symbol">=</a> <a id="2179" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="2181" class="Symbol">(</a><a id="2182" href="Relation.Unary.html#2171" class="Bound">P</a> <a id="2184" href="Relation.Unary.html#2029" class="Function Operator">⊃</a> <a id="2186" href="Relation.Unary.html#2175" class="Bound">Q</a><a id="2187" class="Symbol">)</a>
|
||
|
||
<a id="2190" class="Comment">-- The following primed variants of _⊆_ can be used when 'x' can't</a>
|
||
<a id="2257" class="Comment">-- be inferred from 'x ∈ P'.</a>
|
||
|
||
<a id="2287" class="Keyword">infix</a> <a id="2293" class="Number">4</a> <a id="2295" href="Relation.Unary.html#2336" class="Function Operator">_⊆′_</a> <a id="2300" href="Relation.Unary.html#2403" class="Function Operator">_⊇′_</a> <a id="2305" href="Relation.Unary.html#2457" class="Function Operator">_⊈′_</a> <a id="2310" href="Relation.Unary.html#2515" class="Function Operator">_⊉′_</a> <a id="2315" href="Relation.Unary.html#2573" class="Function Operator">_⊂′_</a> <a id="2320" href="Relation.Unary.html#2636" class="Function Operator">_⊃′_</a> <a id="2325" href="Relation.Unary.html#2690" class="Function Operator">_⊄′_</a> <a id="2330" href="Relation.Unary.html#2748" class="Function Operator">_⊅′_</a>
|
||
|
||
<a id="_⊆′_"></a><a id="2336" href="Relation.Unary.html#2336" class="Function Operator">_⊆′_</a> <a id="2341" class="Symbol">:</a> <a id="2343" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2348" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2350" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="2353" class="Symbol">→</a> <a id="2355" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2360" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2362" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="2365" class="Symbol">→</a> <a id="2367" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2371" class="Symbol">_</a>
|
||
<a id="2373" href="Relation.Unary.html#2373" class="Bound">P</a> <a id="2375" href="Relation.Unary.html#2336" class="Function Operator">⊆′</a> <a id="2378" href="Relation.Unary.html#2378" class="Bound">Q</a> <a id="2380" class="Symbol">=</a> <a id="2382" class="Symbol">∀</a> <a id="2384" href="Relation.Unary.html#2384" class="Bound">x</a> <a id="2386" class="Symbol">→</a> <a id="2388" href="Relation.Unary.html#2384" class="Bound">x</a> <a id="2390" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="2392" href="Relation.Unary.html#2373" class="Bound">P</a> <a id="2394" class="Symbol">→</a> <a id="2396" href="Relation.Unary.html#2384" class="Bound">x</a> <a id="2398" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="2400" href="Relation.Unary.html#2378" class="Bound">Q</a>
|
||
|
||
<a id="_⊇′_"></a><a id="2403" href="Relation.Unary.html#2403" class="Function Operator">_⊇′_</a> <a id="2408" class="Symbol">:</a> <a id="2410" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2415" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2417" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="2420" class="Symbol">→</a> <a id="2422" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2427" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2429" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="2432" class="Symbol">→</a> <a id="2434" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2438" class="Symbol">_</a>
|
||
<a id="2440" href="Relation.Unary.html#2440" class="Bound">Q</a> <a id="2442" href="Relation.Unary.html#2403" class="Function Operator">⊇′</a> <a id="2445" href="Relation.Unary.html#2445" class="Bound">P</a> <a id="2447" class="Symbol">=</a> <a id="2449" href="Relation.Unary.html#2445" class="Bound">P</a> <a id="2451" href="Relation.Unary.html#2336" class="Function Operator">⊆′</a> <a id="2454" href="Relation.Unary.html#2440" class="Bound">Q</a>
|
||
|
||
<a id="_⊈′_"></a><a id="2457" href="Relation.Unary.html#2457" class="Function Operator">_⊈′_</a> <a id="2462" class="Symbol">:</a> <a id="2464" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2469" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2471" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="2474" class="Symbol">→</a> <a id="2476" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2481" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2483" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="2486" class="Symbol">→</a> <a id="2488" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2492" class="Symbol">_</a>
|
||
<a id="2494" href="Relation.Unary.html#2494" class="Bound">P</a> <a id="2496" href="Relation.Unary.html#2457" class="Function Operator">⊈′</a> <a id="2499" href="Relation.Unary.html#2499" class="Bound">Q</a> <a id="2501" class="Symbol">=</a> <a id="2503" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="2505" class="Symbol">(</a><a id="2506" href="Relation.Unary.html#2494" class="Bound">P</a> <a id="2508" href="Relation.Unary.html#2336" class="Function Operator">⊆′</a> <a id="2511" href="Relation.Unary.html#2499" class="Bound">Q</a><a id="2512" class="Symbol">)</a>
|
||
|
||
<a id="_⊉′_"></a><a id="2515" href="Relation.Unary.html#2515" class="Function Operator">_⊉′_</a> <a id="2520" class="Symbol">:</a> <a id="2522" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2527" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2529" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="2532" class="Symbol">→</a> <a id="2534" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2539" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2541" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="2544" class="Symbol">→</a> <a id="2546" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2550" class="Symbol">_</a>
|
||
<a id="2552" href="Relation.Unary.html#2552" class="Bound">P</a> <a id="2554" href="Relation.Unary.html#2515" class="Function Operator">⊉′</a> <a id="2557" href="Relation.Unary.html#2557" class="Bound">Q</a> <a id="2559" class="Symbol">=</a> <a id="2561" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="2563" class="Symbol">(</a><a id="2564" href="Relation.Unary.html#2552" class="Bound">P</a> <a id="2566" href="Relation.Unary.html#2403" class="Function Operator">⊇′</a> <a id="2569" href="Relation.Unary.html#2557" class="Bound">Q</a><a id="2570" class="Symbol">)</a>
|
||
|
||
<a id="_⊂′_"></a><a id="2573" href="Relation.Unary.html#2573" class="Function Operator">_⊂′_</a> <a id="2578" class="Symbol">:</a> <a id="2580" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2585" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2587" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="2590" class="Symbol">→</a> <a id="2592" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2597" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2599" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="2602" class="Symbol">→</a> <a id="2604" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2608" class="Symbol">_</a>
|
||
<a id="2610" href="Relation.Unary.html#2610" class="Bound">P</a> <a id="2612" href="Relation.Unary.html#2573" class="Function Operator">⊂′</a> <a id="2615" href="Relation.Unary.html#2615" class="Bound">Q</a> <a id="2617" class="Symbol">=</a> <a id="2619" href="Relation.Unary.html#2610" class="Bound">P</a> <a id="2621" href="Relation.Unary.html#2336" class="Function Operator">⊆′</a> <a id="2624" href="Relation.Unary.html#2615" class="Bound">Q</a> <a id="2626" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="2628" href="Relation.Unary.html#2615" class="Bound">Q</a> <a id="2630" href="Relation.Unary.html#2457" class="Function Operator">⊈′</a> <a id="2633" href="Relation.Unary.html#2610" class="Bound">P</a>
|
||
|
||
<a id="_⊃′_"></a><a id="2636" href="Relation.Unary.html#2636" class="Function Operator">_⊃′_</a> <a id="2641" class="Symbol">:</a> <a id="2643" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2648" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2650" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="2653" class="Symbol">→</a> <a id="2655" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2660" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2662" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="2665" class="Symbol">→</a> <a id="2667" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2671" class="Symbol">_</a>
|
||
<a id="2673" href="Relation.Unary.html#2673" class="Bound">P</a> <a id="2675" href="Relation.Unary.html#2636" class="Function Operator">⊃′</a> <a id="2678" href="Relation.Unary.html#2678" class="Bound">Q</a> <a id="2680" class="Symbol">=</a> <a id="2682" href="Relation.Unary.html#2678" class="Bound">Q</a> <a id="2684" href="Relation.Unary.html#2573" class="Function Operator">⊂′</a> <a id="2687" href="Relation.Unary.html#2673" class="Bound">P</a>
|
||
|
||
<a id="_⊄′_"></a><a id="2690" href="Relation.Unary.html#2690" class="Function Operator">_⊄′_</a> <a id="2695" class="Symbol">:</a> <a id="2697" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2702" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2704" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="2707" class="Symbol">→</a> <a id="2709" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2714" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2716" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="2719" class="Symbol">→</a> <a id="2721" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2725" class="Symbol">_</a>
|
||
<a id="2727" href="Relation.Unary.html#2727" class="Bound">P</a> <a id="2729" href="Relation.Unary.html#2690" class="Function Operator">⊄′</a> <a id="2732" href="Relation.Unary.html#2732" class="Bound">Q</a> <a id="2734" class="Symbol">=</a> <a id="2736" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="2738" class="Symbol">(</a><a id="2739" href="Relation.Unary.html#2727" class="Bound">P</a> <a id="2741" href="Relation.Unary.html#2573" class="Function Operator">⊂′</a> <a id="2744" href="Relation.Unary.html#2732" class="Bound">Q</a><a id="2745" class="Symbol">)</a>
|
||
|
||
<a id="_⊅′_"></a><a id="2748" href="Relation.Unary.html#2748" class="Function Operator">_⊅′_</a> <a id="2753" class="Symbol">:</a> <a id="2755" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2760" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2762" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="2765" class="Symbol">→</a> <a id="2767" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2772" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="2774" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="2777" class="Symbol">→</a> <a id="2779" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2783" class="Symbol">_</a>
|
||
<a id="2785" href="Relation.Unary.html#2785" class="Bound">P</a> <a id="2787" href="Relation.Unary.html#2748" class="Function Operator">⊅′</a> <a id="2790" href="Relation.Unary.html#2790" class="Bound">Q</a> <a id="2792" class="Symbol">=</a> <a id="2794" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="2796" class="Symbol">(</a><a id="2797" href="Relation.Unary.html#2785" class="Bound">P</a> <a id="2799" href="Relation.Unary.html#2636" class="Function Operator">⊃′</a> <a id="2802" href="Relation.Unary.html#2790" class="Bound">Q</a><a id="2803" class="Symbol">)</a>
|
||
|
||
<a id="2806" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="2879" class="Comment">-- Properties of sets</a>
|
||
|
||
<a id="2902" class="Keyword">infix</a> <a id="2908" class="Number">10</a> <a id="2911" href="Relation.Unary.html#3085" class="Function">Satisfiable</a> <a id="2923" href="Relation.Unary.html#3221" class="Function">Universal</a> <a id="2933" href="Relation.Unary.html#3359" class="Function">IUniversal</a>
|
||
|
||
<a id="2945" class="Comment">-- Emptiness - no element satisfies P.</a>
|
||
|
||
<a id="Empty"></a><a id="2985" href="Relation.Unary.html#2985" class="Function">Empty</a> <a id="2991" class="Symbol">:</a> <a id="2993" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="2998" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="3000" href="Relation.Unary.html#641" class="Generalizable">ℓ</a> <a id="3002" class="Symbol">→</a> <a id="3004" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3008" class="Symbol">_</a>
|
||
<a id="3010" href="Relation.Unary.html#2985" class="Function">Empty</a> <a id="3016" href="Relation.Unary.html#3016" class="Bound">P</a> <a id="3018" class="Symbol">=</a> <a id="3020" class="Symbol">∀</a> <a id="3022" href="Relation.Unary.html#3022" class="Bound">x</a> <a id="3024" class="Symbol">→</a> <a id="3026" href="Relation.Unary.html#3022" class="Bound">x</a> <a id="3028" href="Relation.Unary.html#1563" class="Function Operator">∉</a> <a id="3030" href="Relation.Unary.html#3016" class="Bound">P</a>
|
||
|
||
<a id="3033" class="Comment">-- Satisfiable - at least one element satisfies P.</a>
|
||
|
||
<a id="Satisfiable"></a><a id="3085" href="Relation.Unary.html#3085" class="Function">Satisfiable</a> <a id="3097" class="Symbol">:</a> <a id="3099" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="3104" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="3106" href="Relation.Unary.html#641" class="Generalizable">ℓ</a> <a id="3108" class="Symbol">→</a> <a id="3110" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3114" class="Symbol">_</a>
|
||
<a id="3116" href="Relation.Unary.html#3085" class="Function">Satisfiable</a> <a id="3128" href="Relation.Unary.html#3128" class="Bound">P</a> <a id="3130" class="Symbol">=</a> <a id="3132" href="Data.Product.html#1369" class="Function">∃</a> <a id="3134" class="Symbol">λ</a> <a id="3136" href="Relation.Unary.html#3136" class="Bound">x</a> <a id="3138" class="Symbol">→</a> <a id="3140" href="Relation.Unary.html#3136" class="Bound">x</a> <a id="3142" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="3144" href="Relation.Unary.html#3128" class="Bound">P</a>
|
||
|
||
<a id="3147" class="Keyword">syntax</a> <a id="3154" href="Relation.Unary.html#3085" class="Function">Satisfiable</a> <a id="3166" class="Bound">P</a> <a id="3168" class="Symbol">=</a> <a id="3170" class="Function">∃⟨</a> <a id="3173" class="Bound">P</a> <a id="3175" class="Function">⟩</a>
|
||
|
||
<a id="3178" class="Comment">-- Universality - all elements satisfy P.</a>
|
||
|
||
<a id="Universal"></a><a id="3221" href="Relation.Unary.html#3221" class="Function">Universal</a> <a id="3231" class="Symbol">:</a> <a id="3233" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="3238" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="3240" href="Relation.Unary.html#641" class="Generalizable">ℓ</a> <a id="3242" class="Symbol">→</a> <a id="3244" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3248" class="Symbol">_</a>
|
||
<a id="3250" href="Relation.Unary.html#3221" class="Function">Universal</a> <a id="3260" href="Relation.Unary.html#3260" class="Bound">P</a> <a id="3262" class="Symbol">=</a> <a id="3264" class="Symbol">∀</a> <a id="3266" href="Relation.Unary.html#3266" class="Bound">x</a> <a id="3268" class="Symbol">→</a> <a id="3270" href="Relation.Unary.html#3266" class="Bound">x</a> <a id="3272" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="3274" href="Relation.Unary.html#3260" class="Bound">P</a>
|
||
|
||
<a id="3277" class="Keyword">syntax</a> <a id="3284" href="Relation.Unary.html#3221" class="Function">Universal</a> <a id="3295" class="Bound">P</a> <a id="3297" class="Symbol">=</a> <a id="3299" class="Function">Π[</a> <a id="3302" class="Bound">P</a> <a id="3304" class="Function">]</a>
|
||
|
||
<a id="3307" class="Comment">-- Implicit universality - all elements satisfy P.</a>
|
||
|
||
<a id="IUniversal"></a><a id="3359" href="Relation.Unary.html#3359" class="Function">IUniversal</a> <a id="3370" class="Symbol">:</a> <a id="3372" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="3377" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="3379" href="Relation.Unary.html#641" class="Generalizable">ℓ</a> <a id="3381" class="Symbol">→</a> <a id="3383" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3387" class="Symbol">_</a>
|
||
<a id="3389" href="Relation.Unary.html#3359" class="Function">IUniversal</a> <a id="3400" href="Relation.Unary.html#3400" class="Bound">P</a> <a id="3402" class="Symbol">=</a> <a id="3404" class="Symbol">∀</a> <a id="3406" class="Symbol">{</a><a id="3407" href="Relation.Unary.html#3407" class="Bound">x</a><a id="3408" class="Symbol">}</a> <a id="3410" class="Symbol">→</a> <a id="3412" href="Relation.Unary.html#3407" class="Bound">x</a> <a id="3414" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="3416" href="Relation.Unary.html#3400" class="Bound">P</a>
|
||
|
||
<a id="3419" class="Keyword">syntax</a> <a id="3426" href="Relation.Unary.html#3359" class="Function">IUniversal</a> <a id="3437" class="Bound">P</a> <a id="3439" class="Symbol">=</a> <a id="3441" class="Function">∀[</a> <a id="3444" class="Bound">P</a> <a id="3446" class="Function">]</a>
|
||
|
||
<a id="3449" class="Comment">-- Decidability - it is possible to determine if an arbitrary element</a>
|
||
<a id="3519" class="Comment">-- satisfies P.</a>
|
||
|
||
<a id="Decidable"></a><a id="3536" href="Relation.Unary.html#3536" class="Function">Decidable</a> <a id="3546" class="Symbol">:</a> <a id="3548" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="3553" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="3555" href="Relation.Unary.html#641" class="Generalizable">ℓ</a> <a id="3557" class="Symbol">→</a> <a id="3559" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3563" class="Symbol">_</a>
|
||
<a id="3565" href="Relation.Unary.html#3536" class="Function">Decidable</a> <a id="3575" href="Relation.Unary.html#3575" class="Bound">P</a> <a id="3577" class="Symbol">=</a> <a id="3579" class="Symbol">∀</a> <a id="3581" href="Relation.Unary.html#3581" class="Bound">x</a> <a id="3583" class="Symbol">→</a> <a id="3585" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="3589" class="Symbol">(</a><a id="3590" href="Relation.Unary.html#3575" class="Bound">P</a> <a id="3592" href="Relation.Unary.html#3581" class="Bound">x</a><a id="3593" class="Symbol">)</a>
|
||
|
||
<a id="3596" class="Comment">-- Erasure: A decidable predicate gives rise to another one, more</a>
|
||
<a id="3662" class="Comment">-- amenable to η-expansion</a>
|
||
|
||
<a id="⌊_⌋"></a><a id="3690" href="Relation.Unary.html#3690" class="Function Operator">⌊_⌋</a> <a id="3694" class="Symbol">:</a> <a id="3696" class="Symbol">{</a><a id="3697" href="Relation.Unary.html#3697" class="Bound">P</a> <a id="3699" class="Symbol">:</a> <a id="3701" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="3706" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="3708" href="Relation.Unary.html#641" class="Generalizable">ℓ</a><a id="3709" class="Symbol">}</a> <a id="3711" class="Symbol">→</a> <a id="3713" href="Relation.Unary.html#3536" class="Function">Decidable</a> <a id="3723" href="Relation.Unary.html#3697" class="Bound">P</a> <a id="3725" class="Symbol">→</a> <a id="3727" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="3732" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="3734" href="Relation.Unary.html#641" class="Generalizable">ℓ</a>
|
||
<a id="3736" href="Relation.Unary.html#3690" class="Function Operator">⌊</a> <a id="3738" href="Relation.Unary.html#3738" class="Bound">P?</a> <a id="3741" href="Relation.Unary.html#3690" class="Function Operator">⌋</a> <a id="3743" href="Relation.Unary.html#3743" class="Bound">a</a> <a id="3745" class="Symbol">=</a> <a id="3747" href="Level.html#400" class="Record">Lift</a> <a id="3752" class="Symbol">_</a> <a id="3754" class="Symbol">(</a><a id="3755" href="Relation.Nullary.Decidable.Core.html#1365" class="Function">True</a> <a id="3760" class="Symbol">(</a><a id="3761" href="Relation.Unary.html#3738" class="Bound">P?</a> <a id="3764" href="Relation.Unary.html#3743" class="Bound">a</a><a id="3765" class="Symbol">))</a>
|
||
|
||
<a id="3769" class="Comment">-- Irrelevance - any two proofs that an element satifies P are</a>
|
||
<a id="3832" class="Comment">-- indistinguishable.</a>
|
||
|
||
<a id="Irrelevant"></a><a id="3855" href="Relation.Unary.html#3855" class="Function">Irrelevant</a> <a id="3866" class="Symbol">:</a> <a id="3868" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="3873" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="3875" href="Relation.Unary.html#641" class="Generalizable">ℓ</a> <a id="3877" class="Symbol">→</a> <a id="3879" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3883" class="Symbol">_</a>
|
||
<a id="3885" href="Relation.Unary.html#3855" class="Function">Irrelevant</a> <a id="3896" href="Relation.Unary.html#3896" class="Bound">P</a> <a id="3898" class="Symbol">=</a> <a id="3900" class="Symbol">∀</a> <a id="3902" class="Symbol">{</a><a id="3903" href="Relation.Unary.html#3903" class="Bound">x</a><a id="3904" class="Symbol">}</a> <a id="3906" class="Symbol">(</a><a id="3907" href="Relation.Unary.html#3907" class="Bound">a</a> <a id="3909" class="Symbol">:</a> <a id="3911" href="Relation.Unary.html#3896" class="Bound">P</a> <a id="3913" href="Relation.Unary.html#3903" class="Bound">x</a><a id="3914" class="Symbol">)</a> <a id="3916" class="Symbol">(</a><a id="3917" href="Relation.Unary.html#3917" class="Bound">b</a> <a id="3919" class="Symbol">:</a> <a id="3921" href="Relation.Unary.html#3896" class="Bound">P</a> <a id="3923" href="Relation.Unary.html#3903" class="Bound">x</a><a id="3924" class="Symbol">)</a> <a id="3926" class="Symbol">→</a> <a id="3928" href="Relation.Unary.html#3907" class="Bound">a</a> <a id="3930" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="3932" href="Relation.Unary.html#3917" class="Bound">b</a>
|
||
|
||
<a id="3935" class="Comment">-- Recomputability - we can rebuild a relevant proof given an</a>
|
||
<a id="3997" class="Comment">-- irrelevant one.</a>
|
||
|
||
<a id="Recomputable"></a><a id="4017" href="Relation.Unary.html#4017" class="Function">Recomputable</a> <a id="4030" class="Symbol">:</a> <a id="4032" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4037" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4039" href="Relation.Unary.html#641" class="Generalizable">ℓ</a> <a id="4041" class="Symbol">→</a> <a id="4043" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4047" class="Symbol">_</a>
|
||
<a id="4049" href="Relation.Unary.html#4017" class="Function">Recomputable</a> <a id="4062" href="Relation.Unary.html#4062" class="Bound">P</a> <a id="4064" class="Symbol">=</a> <a id="4066" class="Symbol">∀</a> <a id="4068" class="Symbol">{</a><a id="4069" href="Relation.Unary.html#4069" class="Bound">x</a><a id="4070" class="Symbol">}</a> <a id="4072" class="Symbol">→</a> <a id="4074" class="Symbol">.(</a><a id="4076" href="Relation.Unary.html#4062" class="Bound">P</a> <a id="4078" href="Relation.Unary.html#4069" class="Bound">x</a><a id="4079" class="Symbol">)</a> <a id="4081" class="Symbol">→</a> <a id="4083" href="Relation.Unary.html#4062" class="Bound">P</a> <a id="4085" href="Relation.Unary.html#4069" class="Bound">x</a>
|
||
|
||
<a id="4088" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="4161" class="Comment">-- Operations on sets</a>
|
||
|
||
<a id="4184" class="Keyword">infix</a> <a id="4190" class="Number">10</a> <a id="4193" href="Relation.Unary.html#4593" class="Function">⋃</a> <a id="4195" href="Relation.Unary.html#4741" class="Function">⋂</a>
|
||
<a id="4197" class="Keyword">infixr</a> <a id="4204" class="Number">9</a> <a id="4206" href="Relation.Unary.html#4999" class="Function Operator">_⊢_</a>
|
||
<a id="4210" class="Keyword">infixr</a> <a id="4217" class="Number">8</a> <a id="4219" href="Relation.Unary.html#4338" class="Function Operator">_⇒_</a>
|
||
<a id="4223" class="Keyword">infixr</a> <a id="4230" class="Number">7</a> <a id="4232" href="Relation.Unary.html#4503" class="Function Operator">_∩_</a>
|
||
<a id="4236" class="Keyword">infixr</a> <a id="4243" class="Number">6</a> <a id="4245" href="Relation.Unary.html#4417" class="Function Operator">_∪_</a>
|
||
<a id="4249" class="Keyword">infix</a> <a id="4255" class="Number">4</a> <a id="4257" href="Relation.Unary.html#4920" class="Function Operator">_≬_</a>
|
||
|
||
<a id="4262" class="Comment">-- Complement.</a>
|
||
|
||
<a id="∁"></a><a id="4278" href="Relation.Unary.html#4278" class="Function">∁</a> <a id="4280" class="Symbol">:</a> <a id="4282" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4287" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4289" href="Relation.Unary.html#641" class="Generalizable">ℓ</a> <a id="4291" class="Symbol">→</a> <a id="4293" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4298" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4300" href="Relation.Unary.html#641" class="Generalizable">ℓ</a>
|
||
<a id="4302" href="Relation.Unary.html#4278" class="Function">∁</a> <a id="4304" href="Relation.Unary.html#4304" class="Bound">P</a> <a id="4306" class="Symbol">=</a> <a id="4308" class="Symbol">λ</a> <a id="4310" href="Relation.Unary.html#4310" class="Bound">x</a> <a id="4312" class="Symbol">→</a> <a id="4314" href="Relation.Unary.html#4310" class="Bound">x</a> <a id="4316" href="Relation.Unary.html#1563" class="Function Operator">∉</a> <a id="4318" href="Relation.Unary.html#4304" class="Bound">P</a>
|
||
|
||
<a id="4321" class="Comment">-- Implication.</a>
|
||
|
||
<a id="_⇒_"></a><a id="4338" href="Relation.Unary.html#4338" class="Function Operator">_⇒_</a> <a id="4342" class="Symbol">:</a> <a id="4344" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4349" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4351" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="4354" class="Symbol">→</a> <a id="4356" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4361" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4363" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="4366" class="Symbol">→</a> <a id="4368" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4373" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4375" class="Symbol">_</a>
|
||
<a id="4377" href="Relation.Unary.html#4377" class="Bound">P</a> <a id="4379" href="Relation.Unary.html#4338" class="Function Operator">⇒</a> <a id="4381" href="Relation.Unary.html#4381" class="Bound">Q</a> <a id="4383" class="Symbol">=</a> <a id="4385" class="Symbol">λ</a> <a id="4387" href="Relation.Unary.html#4387" class="Bound">x</a> <a id="4389" class="Symbol">→</a> <a id="4391" href="Relation.Unary.html#4387" class="Bound">x</a> <a id="4393" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="4395" href="Relation.Unary.html#4377" class="Bound">P</a> <a id="4397" class="Symbol">→</a> <a id="4399" href="Relation.Unary.html#4387" class="Bound">x</a> <a id="4401" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="4403" href="Relation.Unary.html#4381" class="Bound">Q</a>
|
||
|
||
<a id="4406" class="Comment">-- Union.</a>
|
||
|
||
<a id="_∪_"></a><a id="4417" href="Relation.Unary.html#4417" class="Function Operator">_∪_</a> <a id="4421" class="Symbol">:</a> <a id="4423" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4428" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4430" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="4433" class="Symbol">→</a> <a id="4435" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4440" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4442" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="4445" class="Symbol">→</a> <a id="4447" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4452" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4454" class="Symbol">_</a>
|
||
<a id="4456" href="Relation.Unary.html#4456" class="Bound">P</a> <a id="4458" href="Relation.Unary.html#4417" class="Function Operator">∪</a> <a id="4460" href="Relation.Unary.html#4460" class="Bound">Q</a> <a id="4462" class="Symbol">=</a> <a id="4464" class="Symbol">λ</a> <a id="4466" href="Relation.Unary.html#4466" class="Bound">x</a> <a id="4468" class="Symbol">→</a> <a id="4470" href="Relation.Unary.html#4466" class="Bound">x</a> <a id="4472" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="4474" href="Relation.Unary.html#4456" class="Bound">P</a> <a id="4476" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="4478" href="Relation.Unary.html#4466" class="Bound">x</a> <a id="4480" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="4482" href="Relation.Unary.html#4460" class="Bound">Q</a>
|
||
|
||
<a id="4485" class="Comment">-- Intersection.</a>
|
||
|
||
<a id="_∩_"></a><a id="4503" href="Relation.Unary.html#4503" class="Function Operator">_∩_</a> <a id="4507" class="Symbol">:</a> <a id="4509" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4514" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4516" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="4519" class="Symbol">→</a> <a id="4521" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4526" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4528" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="4531" class="Symbol">→</a> <a id="4533" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4538" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4540" class="Symbol">_</a>
|
||
<a id="4542" href="Relation.Unary.html#4542" class="Bound">P</a> <a id="4544" href="Relation.Unary.html#4503" class="Function Operator">∩</a> <a id="4546" href="Relation.Unary.html#4546" class="Bound">Q</a> <a id="4548" class="Symbol">=</a> <a id="4550" class="Symbol">λ</a> <a id="4552" href="Relation.Unary.html#4552" class="Bound">x</a> <a id="4554" class="Symbol">→</a> <a id="4556" href="Relation.Unary.html#4552" class="Bound">x</a> <a id="4558" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="4560" href="Relation.Unary.html#4542" class="Bound">P</a> <a id="4562" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="4564" href="Relation.Unary.html#4552" class="Bound">x</a> <a id="4566" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="4568" href="Relation.Unary.html#4546" class="Bound">Q</a>
|
||
|
||
<a id="4571" class="Comment">-- Infinitary union.</a>
|
||
|
||
<a id="⋃"></a><a id="4593" href="Relation.Unary.html#4593" class="Function">⋃</a> <a id="4595" class="Symbol">:</a> <a id="4597" class="Symbol">∀</a> <a id="4599" class="Symbol">{</a><a id="4600" href="Relation.Unary.html#4600" class="Bound">i</a><a id="4601" class="Symbol">}</a> <a id="4603" class="Symbol">(</a><a id="4604" href="Relation.Unary.html#4604" class="Bound">I</a> <a id="4606" class="Symbol">:</a> <a id="4608" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4612" href="Relation.Unary.html#4600" class="Bound">i</a><a id="4613" class="Symbol">)</a> <a id="4615" class="Symbol">→</a> <a id="4617" class="Symbol">(</a><a id="4618" href="Relation.Unary.html#4604" class="Bound">I</a> <a id="4620" class="Symbol">→</a> <a id="4622" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4627" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4629" href="Relation.Unary.html#641" class="Generalizable">ℓ</a><a id="4630" class="Symbol">)</a> <a id="4632" class="Symbol">→</a> <a id="4634" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4639" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4641" class="Symbol">_</a>
|
||
<a id="4643" href="Relation.Unary.html#4593" class="Function">⋃</a> <a id="4645" href="Relation.Unary.html#4645" class="Bound">I</a> <a id="4647" href="Relation.Unary.html#4647" class="Bound">P</a> <a id="4649" class="Symbol">=</a> <a id="4651" class="Symbol">λ</a> <a id="4653" href="Relation.Unary.html#4653" class="Bound">x</a> <a id="4655" class="Symbol">→</a> <a id="4657" href="Data.Product.html#916" class="Function">Σ[</a> <a id="4660" href="Relation.Unary.html#4660" class="Bound">i</a> <a id="4662" href="Data.Product.html#916" class="Function">∈</a> <a id="4664" href="Relation.Unary.html#4645" class="Bound">I</a> <a id="4666" href="Data.Product.html#916" class="Function">]</a> <a id="4668" href="Relation.Unary.html#4647" class="Bound">P</a> <a id="4670" href="Relation.Unary.html#4660" class="Bound">i</a> <a id="4672" href="Relation.Unary.html#4653" class="Bound">x</a>
|
||
|
||
<a id="4675" class="Keyword">syntax</a> <a id="4682" href="Relation.Unary.html#4593" class="Function">⋃</a> <a id="4684" class="Bound">I</a> <a id="4686" class="Symbol">(λ</a> <a id="4689" class="Bound">i</a> <a id="4691" class="Symbol">→</a> <a id="4693" class="Bound">P</a><a id="4694" class="Symbol">)</a> <a id="4696" class="Symbol">=</a> <a id="4698" class="Function">⋃[</a> <a id="4701" class="Bound">i</a> <a id="4703" class="Function">∶</a> <a id="4705" class="Bound">I</a> <a id="4707" class="Function">]</a> <a id="4709" class="Bound">P</a>
|
||
|
||
<a id="4712" class="Comment">-- Infinitary intersection.</a>
|
||
|
||
<a id="⋂"></a><a id="4741" href="Relation.Unary.html#4741" class="Function">⋂</a> <a id="4743" class="Symbol">:</a> <a id="4745" class="Symbol">∀</a> <a id="4747" class="Symbol">{</a><a id="4748" href="Relation.Unary.html#4748" class="Bound">i</a><a id="4749" class="Symbol">}</a> <a id="4751" class="Symbol">(</a><a id="4752" href="Relation.Unary.html#4752" class="Bound">I</a> <a id="4754" class="Symbol">:</a> <a id="4756" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4760" href="Relation.Unary.html#4748" class="Bound">i</a><a id="4761" class="Symbol">)</a> <a id="4763" class="Symbol">→</a> <a id="4765" class="Symbol">(</a><a id="4766" href="Relation.Unary.html#4752" class="Bound">I</a> <a id="4768" class="Symbol">→</a> <a id="4770" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4775" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4777" href="Relation.Unary.html#641" class="Generalizable">ℓ</a><a id="4778" class="Symbol">)</a> <a id="4780" class="Symbol">→</a> <a id="4782" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4787" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4789" class="Symbol">_</a>
|
||
<a id="4791" href="Relation.Unary.html#4741" class="Function">⋂</a> <a id="4793" href="Relation.Unary.html#4793" class="Bound">I</a> <a id="4795" href="Relation.Unary.html#4795" class="Bound">P</a> <a id="4797" class="Symbol">=</a> <a id="4799" class="Symbol">λ</a> <a id="4801" href="Relation.Unary.html#4801" class="Bound">x</a> <a id="4803" class="Symbol">→</a> <a id="4805" class="Symbol">(</a><a id="4806" href="Relation.Unary.html#4806" class="Bound">i</a> <a id="4808" class="Symbol">:</a> <a id="4810" href="Relation.Unary.html#4793" class="Bound">I</a><a id="4811" class="Symbol">)</a> <a id="4813" class="Symbol">→</a> <a id="4815" href="Relation.Unary.html#4795" class="Bound">P</a> <a id="4817" href="Relation.Unary.html#4806" class="Bound">i</a> <a id="4819" href="Relation.Unary.html#4801" class="Bound">x</a>
|
||
|
||
<a id="4822" class="Keyword">syntax</a> <a id="4829" href="Relation.Unary.html#4741" class="Function">⋂</a> <a id="4831" class="Bound">I</a> <a id="4833" class="Symbol">(λ</a> <a id="4836" class="Bound">i</a> <a id="4838" class="Symbol">→</a> <a id="4840" class="Bound">P</a><a id="4841" class="Symbol">)</a> <a id="4843" class="Symbol">=</a> <a id="4845" class="Function">⋂[</a> <a id="4848" class="Bound">i</a> <a id="4850" class="Function">∶</a> <a id="4852" class="Bound">I</a> <a id="4854" class="Function">]</a> <a id="4856" class="Bound">P</a>
|
||
|
||
<a id="4859" class="Comment">-- Positive version of non-disjointness, dual to inclusion.</a>
|
||
|
||
<a id="_≬_"></a><a id="4920" href="Relation.Unary.html#4920" class="Function Operator">_≬_</a> <a id="4924" class="Symbol">:</a> <a id="4926" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4931" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4933" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="4936" class="Symbol">→</a> <a id="4938" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="4943" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="4945" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="4948" class="Symbol">→</a> <a id="4950" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="4954" class="Symbol">_</a>
|
||
<a id="4956" href="Relation.Unary.html#4956" class="Bound">P</a> <a id="4958" href="Relation.Unary.html#4920" class="Function Operator">≬</a> <a id="4960" href="Relation.Unary.html#4960" class="Bound">Q</a> <a id="4962" class="Symbol">=</a> <a id="4964" href="Data.Product.html#1369" class="Function">∃</a> <a id="4966" class="Symbol">λ</a> <a id="4968" href="Relation.Unary.html#4968" class="Bound">x</a> <a id="4970" class="Symbol">→</a> <a id="4972" href="Relation.Unary.html#4968" class="Bound">x</a> <a id="4974" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="4976" href="Relation.Unary.html#4956" class="Bound">P</a> <a id="4978" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="4980" href="Relation.Unary.html#4968" class="Bound">x</a> <a id="4982" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="4984" href="Relation.Unary.html#4960" class="Bound">Q</a>
|
||
|
||
<a id="4987" class="Comment">-- Update.</a>
|
||
|
||
<a id="_⊢_"></a><a id="4999" href="Relation.Unary.html#4999" class="Function Operator">_⊢_</a> <a id="5003" class="Symbol">:</a> <a id="5005" class="Symbol">(</a><a id="5006" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="5008" class="Symbol">→</a> <a id="5010" href="Relation.Unary.html#675" class="Generalizable">B</a><a id="5011" class="Symbol">)</a> <a id="5013" class="Symbol">→</a> <a id="5015" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5020" href="Relation.Unary.html#675" class="Generalizable">B</a> <a id="5022" href="Relation.Unary.html#641" class="Generalizable">ℓ</a> <a id="5024" class="Symbol">→</a> <a id="5026" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5031" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="5033" href="Relation.Unary.html#641" class="Generalizable">ℓ</a>
|
||
<a id="5035" href="Relation.Unary.html#5035" class="Bound">f</a> <a id="5037" href="Relation.Unary.html#4999" class="Function Operator">⊢</a> <a id="5039" href="Relation.Unary.html#5039" class="Bound">P</a> <a id="5041" class="Symbol">=</a> <a id="5043" class="Symbol">λ</a> <a id="5045" href="Relation.Unary.html#5045" class="Bound">x</a> <a id="5047" class="Symbol">→</a> <a id="5049" href="Relation.Unary.html#5039" class="Bound">P</a> <a id="5051" class="Symbol">(</a><a id="5052" href="Relation.Unary.html#5035" class="Bound">f</a> <a id="5054" href="Relation.Unary.html#5045" class="Bound">x</a><a id="5055" class="Symbol">)</a>
|
||
|
||
<a id="5058" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="5131" class="Comment">-- Predicate combinators</a>
|
||
|
||
<a id="5157" class="Comment">-- These differ from the set operations above, as the carrier set of the</a>
|
||
<a id="5230" class="Comment">-- resulting predicates are not the same as the carrier set of the</a>
|
||
<a id="5297" class="Comment">-- component predicates.</a>
|
||
|
||
<a id="5323" class="Keyword">infixr</a> <a id="5331" class="Number">2</a> <a id="5333" href="Relation.Unary.html#5466" class="Function Operator">_⟨×⟩_</a>
|
||
<a id="5339" class="Keyword">infixr</a> <a id="5347" class="Number">2</a> <a id="5349" href="Relation.Unary.html#5667" class="Function Operator">_⟨⊙⟩_</a>
|
||
<a id="5355" class="Keyword">infixr</a> <a id="5363" class="Number">1</a> <a id="5365" href="Relation.Unary.html#5574" class="Function Operator">_⟨⊎⟩_</a>
|
||
<a id="5371" class="Keyword">infixr</a> <a id="5379" class="Number">0</a> <a id="5381" href="Relation.Unary.html#5766" class="Function Operator">_⟨→⟩_</a>
|
||
<a id="5387" class="Keyword">infixl</a> <a id="5395" class="Number">9</a> <a id="5397" href="Relation.Unary.html#5851" class="Function Operator">_⟨·⟩_</a>
|
||
<a id="5403" class="Keyword">infix</a> <a id="5410" class="Number">10</a> <a id="5413" href="Relation.Unary.html#5983" class="Function Operator">_~</a>
|
||
<a id="5416" class="Keyword">infixr</a> <a id="5424" class="Number">9</a> <a id="5426" href="Relation.Unary.html#6053" class="Function Operator">_⟨∘⟩_</a>
|
||
<a id="5432" class="Keyword">infixr</a> <a id="5440" class="Number">2</a> <a id="5442" href="Relation.Unary.html#6186" class="Function Operator">_//_</a> <a id="5447" href="Relation.Unary.html#6306" class="Function Operator">_\\_</a>
|
||
|
||
<a id="5453" class="Comment">-- Product.</a>
|
||
|
||
<a id="_⟨×⟩_"></a><a id="5466" href="Relation.Unary.html#5466" class="Function Operator">_⟨×⟩_</a> <a id="5472" class="Symbol">:</a> <a id="5474" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5479" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="5481" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="5484" class="Symbol">→</a> <a id="5486" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5491" href="Relation.Unary.html#675" class="Generalizable">B</a> <a id="5493" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="5496" class="Symbol">→</a> <a id="5498" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5503" class="Symbol">(</a><a id="5504" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="5506" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5508" href="Relation.Unary.html#675" class="Generalizable">B</a><a id="5509" class="Symbol">)</a> <a id="5511" class="Symbol">_</a>
|
||
<a id="5513" class="Symbol">(</a><a id="5514" href="Relation.Unary.html#5514" class="Bound">P</a> <a id="5516" href="Relation.Unary.html#5466" class="Function Operator">⟨×⟩</a> <a id="5520" href="Relation.Unary.html#5520" class="Bound">Q</a><a id="5521" class="Symbol">)</a> <a id="5523" class="Symbol">(</a><a id="5524" href="Relation.Unary.html#5524" class="Bound">x</a> <a id="5526" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5528" href="Relation.Unary.html#5528" class="Bound">y</a><a id="5529" class="Symbol">)</a> <a id="5531" class="Symbol">=</a> <a id="5533" href="Relation.Unary.html#5524" class="Bound">x</a> <a id="5535" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="5537" href="Relation.Unary.html#5514" class="Bound">P</a> <a id="5539" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5541" href="Relation.Unary.html#5528" class="Bound">y</a> <a id="5543" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="5545" href="Relation.Unary.html#5520" class="Bound">Q</a>
|
||
|
||
<a id="5548" class="Comment">-- Sum over one element.</a>
|
||
|
||
<a id="_⟨⊎⟩_"></a><a id="5574" href="Relation.Unary.html#5574" class="Function Operator">_⟨⊎⟩_</a> <a id="5580" class="Symbol">:</a> <a id="5582" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5587" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="5589" href="Relation.Unary.html#641" class="Generalizable">ℓ</a> <a id="5591" class="Symbol">→</a> <a id="5593" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5598" href="Relation.Unary.html#675" class="Generalizable">B</a> <a id="5600" href="Relation.Unary.html#641" class="Generalizable">ℓ</a> <a id="5602" class="Symbol">→</a> <a id="5604" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5609" class="Symbol">(</a><a id="5610" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="5612" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="5614" href="Relation.Unary.html#675" class="Generalizable">B</a><a id="5615" class="Symbol">)</a> <a id="5617" class="Symbol">_</a>
|
||
<a id="5619" href="Relation.Unary.html#5619" class="Bound">P</a> <a id="5621" href="Relation.Unary.html#5574" class="Function Operator">⟨⊎⟩</a> <a id="5625" href="Relation.Unary.html#5625" class="Bound">Q</a> <a id="5627" class="Symbol">=</a> <a id="5629" href="Data.Sum.Base.html#920" class="Function Operator">[</a> <a id="5631" href="Relation.Unary.html#5619" class="Bound">P</a> <a id="5633" href="Data.Sum.Base.html#920" class="Function Operator">,</a> <a id="5635" href="Relation.Unary.html#5625" class="Bound">Q</a> <a id="5637" href="Data.Sum.Base.html#920" class="Function Operator">]</a>
|
||
|
||
<a id="5640" class="Comment">-- Sum over two elements.</a>
|
||
|
||
<a id="_⟨⊙⟩_"></a><a id="5667" href="Relation.Unary.html#5667" class="Function Operator">_⟨⊙⟩_</a> <a id="5673" class="Symbol">:</a> <a id="5675" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5680" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="5682" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="5685" class="Symbol">→</a> <a id="5687" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5692" href="Relation.Unary.html#675" class="Generalizable">B</a> <a id="5694" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="5697" class="Symbol">→</a> <a id="5699" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5704" class="Symbol">(</a><a id="5705" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="5707" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5709" href="Relation.Unary.html#675" class="Generalizable">B</a><a id="5710" class="Symbol">)</a> <a id="5712" class="Symbol">_</a>
|
||
<a id="5714" class="Symbol">(</a><a id="5715" href="Relation.Unary.html#5715" class="Bound">P</a> <a id="5717" href="Relation.Unary.html#5667" class="Function Operator">⟨⊙⟩</a> <a id="5721" href="Relation.Unary.html#5721" class="Bound">Q</a><a id="5722" class="Symbol">)</a> <a id="5724" class="Symbol">(</a><a id="5725" href="Relation.Unary.html#5725" class="Bound">x</a> <a id="5727" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5729" href="Relation.Unary.html#5729" class="Bound">y</a><a id="5730" class="Symbol">)</a> <a id="5732" class="Symbol">=</a> <a id="5734" href="Relation.Unary.html#5725" class="Bound">x</a> <a id="5736" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="5738" href="Relation.Unary.html#5715" class="Bound">P</a> <a id="5740" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="5742" href="Relation.Unary.html#5729" class="Bound">y</a> <a id="5744" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="5746" href="Relation.Unary.html#5721" class="Bound">Q</a>
|
||
|
||
<a id="5749" class="Comment">-- Implication.</a>
|
||
|
||
<a id="_⟨→⟩_"></a><a id="5766" href="Relation.Unary.html#5766" class="Function Operator">_⟨→⟩_</a> <a id="5772" class="Symbol">:</a> <a id="5774" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5779" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="5781" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="5784" class="Symbol">→</a> <a id="5786" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5791" href="Relation.Unary.html#675" class="Generalizable">B</a> <a id="5793" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="5796" class="Symbol">→</a> <a id="5798" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5803" class="Symbol">(</a><a id="5804" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="5806" class="Symbol">→</a> <a id="5808" href="Relation.Unary.html#675" class="Generalizable">B</a><a id="5809" class="Symbol">)</a> <a id="5811" class="Symbol">_</a>
|
||
<a id="5813" class="Symbol">(</a><a id="5814" href="Relation.Unary.html#5814" class="Bound">P</a> <a id="5816" href="Relation.Unary.html#5766" class="Function Operator">⟨→⟩</a> <a id="5820" href="Relation.Unary.html#5820" class="Bound">Q</a><a id="5821" class="Symbol">)</a> <a id="5823" href="Relation.Unary.html#5823" class="Bound">f</a> <a id="5825" class="Symbol">=</a> <a id="5827" href="Relation.Unary.html#5814" class="Bound">P</a> <a id="5829" href="Relation.Unary.html#1742" class="Function Operator">⊆</a> <a id="5831" href="Relation.Unary.html#5820" class="Bound">Q</a> <a id="5833" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="5835" href="Relation.Unary.html#5823" class="Bound">f</a>
|
||
|
||
<a id="5838" class="Comment">-- Product.</a>
|
||
|
||
<a id="_⟨·⟩_"></a><a id="5851" href="Relation.Unary.html#5851" class="Function Operator">_⟨·⟩_</a> <a id="5857" class="Symbol">:</a> <a id="5859" class="Symbol">(</a><a id="5860" href="Relation.Unary.html#5860" class="Bound">P</a> <a id="5862" class="Symbol">:</a> <a id="5864" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5869" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="5871" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a><a id="5873" class="Symbol">)</a> <a id="5875" class="Symbol">(</a><a id="5876" href="Relation.Unary.html#5876" class="Bound">Q</a> <a id="5878" class="Symbol">:</a> <a id="5880" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5885" href="Relation.Unary.html#675" class="Generalizable">B</a> <a id="5887" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a><a id="5889" class="Symbol">)</a> <a id="5891" class="Symbol">→</a>
|
||
<a id="5901" class="Symbol">(</a><a id="5902" href="Relation.Unary.html#5860" class="Bound">P</a> <a id="5904" href="Relation.Unary.html#5466" class="Function Operator">⟨×⟩</a> <a id="5908" class="Symbol">(</a><a id="5909" href="Relation.Unary.html#5860" class="Bound">P</a> <a id="5911" href="Relation.Unary.html#5766" class="Function Operator">⟨→⟩</a> <a id="5915" href="Relation.Unary.html#5876" class="Bound">Q</a><a id="5916" class="Symbol">))</a> <a id="5919" href="Relation.Unary.html#1742" class="Function Operator">⊆</a> <a id="5921" href="Relation.Unary.html#5876" class="Bound">Q</a> <a id="5923" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="5925" href="Data.Product.html#3422" class="Function">uncurry</a> <a id="5933" class="Symbol">(</a><a id="5934" href="Function.Base.html#1554" class="Function">flip</a> <a id="5939" href="Function.Base.html#1919" class="Function Operator">_$_</a><a id="5942" class="Symbol">)</a>
|
||
<a id="5944" class="Symbol">(</a><a id="5945" href="Relation.Unary.html#5945" class="Bound">P</a> <a id="5947" href="Relation.Unary.html#5851" class="Function Operator">⟨·⟩</a> <a id="5951" href="Relation.Unary.html#5951" class="Bound">Q</a><a id="5952" class="Symbol">)</a> <a id="5954" class="Symbol">(</a><a id="5955" href="Relation.Unary.html#5955" class="Bound">p</a> <a id="5957" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="5959" href="Relation.Unary.html#5959" class="Bound">f</a><a id="5960" class="Symbol">)</a> <a id="5962" class="Symbol">=</a> <a id="5964" href="Relation.Unary.html#5959" class="Bound">f</a> <a id="5966" href="Relation.Unary.html#5955" class="Bound">p</a>
|
||
|
||
<a id="5969" class="Comment">-- Converse.</a>
|
||
|
||
<a id="_~"></a><a id="5983" href="Relation.Unary.html#5983" class="Function Operator">_~</a> <a id="5986" class="Symbol">:</a> <a id="5988" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="5993" class="Symbol">(</a><a id="5994" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="5996" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="5998" href="Relation.Unary.html#675" class="Generalizable">B</a><a id="5999" class="Symbol">)</a> <a id="6001" href="Relation.Unary.html#641" class="Generalizable">ℓ</a> <a id="6003" class="Symbol">→</a> <a id="6005" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="6010" class="Symbol">(</a><a id="6011" href="Relation.Unary.html#675" class="Generalizable">B</a> <a id="6013" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="6015" href="Relation.Unary.html#661" class="Generalizable">A</a><a id="6016" class="Symbol">)</a> <a id="6018" href="Relation.Unary.html#641" class="Generalizable">ℓ</a>
|
||
<a id="6020" href="Relation.Unary.html#6020" class="Bound">P</a> <a id="6022" href="Relation.Unary.html#5983" class="Function Operator">~</a> <a id="6024" class="Symbol">=</a> <a id="6026" href="Relation.Unary.html#6020" class="Bound">P</a> <a id="6028" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="6030" href="Data.Product.html#5317" class="Function">swap</a>
|
||
|
||
<a id="6036" class="Comment">-- Composition.</a>
|
||
|
||
<a id="_⟨∘⟩_"></a><a id="6053" href="Relation.Unary.html#6053" class="Function Operator">_⟨∘⟩_</a> <a id="6059" class="Symbol">:</a> <a id="6061" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="6066" class="Symbol">(</a><a id="6067" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="6069" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="6071" href="Relation.Unary.html#675" class="Generalizable">B</a><a id="6072" class="Symbol">)</a> <a id="6074" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="6077" class="Symbol">→</a> <a id="6079" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="6084" class="Symbol">(</a><a id="6085" href="Relation.Unary.html#675" class="Generalizable">B</a> <a id="6087" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="6089" href="Relation.Unary.html#689" class="Generalizable">C</a><a id="6090" class="Symbol">)</a> <a id="6092" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="6095" class="Symbol">→</a> <a id="6097" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="6102" class="Symbol">(</a><a id="6103" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="6105" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="6107" href="Relation.Unary.html#689" class="Generalizable">C</a><a id="6108" class="Symbol">)</a> <a id="6110" class="Symbol">_</a>
|
||
<a id="6112" class="Symbol">(</a><a id="6113" href="Relation.Unary.html#6113" class="Bound">P</a> <a id="6115" href="Relation.Unary.html#6053" class="Function Operator">⟨∘⟩</a> <a id="6119" href="Relation.Unary.html#6119" class="Bound">Q</a><a id="6120" class="Symbol">)</a> <a id="6122" class="Symbol">(</a><a id="6123" href="Relation.Unary.html#6123" class="Bound">x</a> <a id="6125" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="6127" href="Relation.Unary.html#6127" class="Bound">z</a><a id="6128" class="Symbol">)</a> <a id="6130" class="Symbol">=</a> <a id="6132" href="Data.Product.html#1369" class="Function">∃</a> <a id="6134" class="Symbol">λ</a> <a id="6136" href="Relation.Unary.html#6136" class="Bound">y</a> <a id="6138" class="Symbol">→</a> <a id="6140" class="Symbol">(</a><a id="6141" href="Relation.Unary.html#6123" class="Bound">x</a> <a id="6143" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="6145" href="Relation.Unary.html#6136" class="Bound">y</a><a id="6146" class="Symbol">)</a> <a id="6148" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="6150" href="Relation.Unary.html#6113" class="Bound">P</a> <a id="6152" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="6154" class="Symbol">(</a><a id="6155" href="Relation.Unary.html#6136" class="Bound">y</a> <a id="6157" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="6159" href="Relation.Unary.html#6127" class="Bound">z</a><a id="6160" class="Symbol">)</a> <a id="6162" href="Relation.Unary.html#1523" class="Function Operator">∈</a> <a id="6164" href="Relation.Unary.html#6119" class="Bound">Q</a>
|
||
|
||
<a id="6167" class="Comment">-- Post-division.</a>
|
||
|
||
<a id="_//_"></a><a id="6186" href="Relation.Unary.html#6186" class="Function Operator">_//_</a> <a id="6191" class="Symbol">:</a> <a id="6193" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="6198" class="Symbol">(</a><a id="6199" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="6201" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="6203" href="Relation.Unary.html#689" class="Generalizable">C</a><a id="6204" class="Symbol">)</a> <a id="6206" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="6209" class="Symbol">→</a> <a id="6211" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="6216" class="Symbol">(</a><a id="6217" href="Relation.Unary.html#675" class="Generalizable">B</a> <a id="6219" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="6221" href="Relation.Unary.html#689" class="Generalizable">C</a><a id="6222" class="Symbol">)</a> <a id="6224" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="6227" class="Symbol">→</a> <a id="6229" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="6234" class="Symbol">(</a><a id="6235" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="6237" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="6239" href="Relation.Unary.html#675" class="Generalizable">B</a><a id="6240" class="Symbol">)</a> <a id="6242" class="Symbol">_</a>
|
||
<a id="6244" class="Symbol">(</a><a id="6245" href="Relation.Unary.html#6245" class="Bound">P</a> <a id="6247" href="Relation.Unary.html#6186" class="Function Operator">//</a> <a id="6250" href="Relation.Unary.html#6250" class="Bound">Q</a><a id="6251" class="Symbol">)</a> <a id="6253" class="Symbol">(</a><a id="6254" href="Relation.Unary.html#6254" class="Bound">x</a> <a id="6256" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="6258" href="Relation.Unary.html#6258" class="Bound">y</a><a id="6259" class="Symbol">)</a> <a id="6261" class="Symbol">=</a> <a id="6263" href="Relation.Unary.html#6250" class="Bound">Q</a> <a id="6265" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="6267" class="Symbol">(</a><a id="6268" href="Relation.Unary.html#6258" class="Bound">y</a> <a id="6270" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,_</a><a id="6272" class="Symbol">)</a> <a id="6274" href="Relation.Unary.html#1742" class="Function Operator">⊆</a> <a id="6276" href="Relation.Unary.html#6245" class="Bound">P</a> <a id="6278" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="6280" class="Symbol">(</a><a id="6281" href="Relation.Unary.html#6254" class="Bound">x</a> <a id="6283" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,_</a><a id="6285" class="Symbol">)</a>
|
||
|
||
<a id="6288" class="Comment">-- Pre-division.</a>
|
||
|
||
<a id="_\\_"></a><a id="6306" href="Relation.Unary.html#6306" class="Function Operator">_\\_</a> <a id="6311" class="Symbol">:</a> <a id="6313" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="6318" class="Symbol">(</a><a id="6319" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="6321" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="6323" href="Relation.Unary.html#689" class="Generalizable">C</a><a id="6324" class="Symbol">)</a> <a id="6326" href="Relation.Unary.html#643" class="Generalizable">ℓ₁</a> <a id="6329" class="Symbol">→</a> <a id="6331" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="6336" class="Symbol">(</a><a id="6337" href="Relation.Unary.html#661" class="Generalizable">A</a> <a id="6339" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="6341" href="Relation.Unary.html#675" class="Generalizable">B</a><a id="6342" class="Symbol">)</a> <a id="6344" href="Relation.Unary.html#646" class="Generalizable">ℓ₂</a> <a id="6347" class="Symbol">→</a> <a id="6349" href="Relation.Unary.html#1101" class="Function">Pred</a> <a id="6354" class="Symbol">(</a><a id="6355" href="Relation.Unary.html#675" class="Generalizable">B</a> <a id="6357" href="Data.Product.html#1167" class="Function Operator">×</a> <a id="6359" href="Relation.Unary.html#689" class="Generalizable">C</a><a id="6360" class="Symbol">)</a> <a id="6362" class="Symbol">_</a>
|
||
<a id="6364" href="Relation.Unary.html#6364" class="Bound">P</a> <a id="6366" href="Relation.Unary.html#6306" class="Function Operator">\\</a> <a id="6369" href="Relation.Unary.html#6369" class="Bound">Q</a> <a id="6371" class="Symbol">=</a> <a id="6373" class="Symbol">(</a><a id="6374" href="Relation.Unary.html#6364" class="Bound">P</a> <a id="6376" href="Relation.Unary.html#5983" class="Function Operator">~</a> <a id="6378" href="Relation.Unary.html#6186" class="Function Operator">//</a> <a id="6381" href="Relation.Unary.html#6369" class="Bound">Q</a> <a id="6383" href="Relation.Unary.html#5983" class="Function Operator">~</a><a id="6384" class="Symbol">)</a> <a id="6386" href="Relation.Unary.html#5983" class="Function Operator">~</a>
|
||
</pre></body></html> |