126 lines
39 KiB
HTML
126 lines
39 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Function.Equality</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">-- Function setoids and related constructions</a>
|
||
<a id="152" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="226" class="Symbol">{-#</a> <a id="230" class="Keyword">OPTIONS</a> <a id="238" class="Pragma">--without-K</a> <a id="250" class="Pragma">--safe</a> <a id="257" class="Symbol">#-}</a>
|
||
|
||
<a id="262" class="Comment">-- Note: use of the standard function hierarchy is encouraged. The</a>
|
||
<a id="329" class="Comment">-- module `Function` re-exports `Congruent`, `IsBijection` and</a>
|
||
<a id="392" class="Comment">-- `Bijection`. The alternative definitions found in this file will</a>
|
||
<a id="460" class="Comment">-- eventually be deprecated.</a>
|
||
|
||
<a id="490" class="Keyword">module</a> <a id="497" href="Function.Equality.html" class="Module">Function.Equality</a> <a id="515" class="Keyword">where</a>
|
||
|
||
<a id="522" class="Keyword">import</a> <a id="529" href="Function.Base.html" class="Module">Function.Base</a> <a id="543" class="Symbol">as</a> <a id="546" class="Module">Fun</a>
|
||
<a id="550" class="Keyword">open</a> <a id="555" class="Keyword">import</a> <a id="562" href="Level.html" class="Module">Level</a>
|
||
<a id="568" class="Keyword">open</a> <a id="573" class="Keyword">import</a> <a id="580" href="Relation.Binary.html" class="Module">Relation.Binary</a> <a id="596" class="Keyword">using</a> <a id="602" class="Symbol">(</a><a id="603" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a><a id="609" class="Symbol">)</a>
|
||
<a id="611" class="Keyword">open</a> <a id="616" class="Keyword">import</a> <a id="623" href="Relation.Binary.Indexed.Heterogeneous.html" class="Module">Relation.Binary.Indexed.Heterogeneous</a>
|
||
<a id="663" class="Keyword">using</a> <a id="669" class="Symbol">(</a><a id="670" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#789" class="Record">IndexedSetoid</a><a id="683" class="Symbol">;</a> <a id="685" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1062" class="Function Operator">_=[_]⇒_</a><a id="692" class="Symbol">)</a>
|
||
<a id="694" class="Keyword">import</a> <a id="701" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html" class="Module">Relation.Binary.Indexed.Heterogeneous.Construct.Trivial</a>
|
||
<a id="759" class="Symbol">as</a> <a id="762" class="Module">Trivial</a>
|
||
|
||
<a id="771" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="844" class="Comment">-- Functions which preserve equality</a>
|
||
|
||
<a id="882" class="Keyword">record</a> <a id="Π"></a><a id="889" href="Function.Equality.html#889" class="Record">Π</a> <a id="891" class="Symbol">{</a><a id="892" href="Function.Equality.html#892" class="Bound">f₁</a> <a id="895" href="Function.Equality.html#895" class="Bound">f₂</a> <a id="898" href="Function.Equality.html#898" class="Bound">t₁</a> <a id="901" href="Function.Equality.html#901" class="Bound">t₂</a><a id="903" class="Symbol">}</a>
|
||
<a id="914" class="Symbol">(</a><a id="915" href="Function.Equality.html#915" class="Bound">From</a> <a id="920" class="Symbol">:</a> <a id="922" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="929" href="Function.Equality.html#892" class="Bound">f₁</a> <a id="932" href="Function.Equality.html#895" class="Bound">f₂</a><a id="934" class="Symbol">)</a>
|
||
<a id="945" class="Symbol">(</a><a id="946" href="Function.Equality.html#946" class="Bound">To</a> <a id="949" class="Symbol">:</a> <a id="951" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#789" class="Record">IndexedSetoid</a> <a id="965" class="Symbol">(</a><a id="966" href="Relation.Binary.Bundles.html#1072" class="Field">Setoid.Carrier</a> <a id="981" href="Function.Equality.html#915" class="Bound">From</a><a id="985" class="Symbol">)</a> <a id="987" href="Function.Equality.html#898" class="Bound">t₁</a> <a id="990" href="Function.Equality.html#901" class="Bound">t₂</a><a id="992" class="Symbol">)</a> <a id="994" class="Symbol">:</a>
|
||
<a id="1005" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1009" class="Symbol">(</a><a id="1010" href="Function.Equality.html#892" class="Bound">f₁</a> <a id="1013" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1015" href="Function.Equality.html#895" class="Bound">f₂</a> <a id="1018" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1020" href="Function.Equality.html#898" class="Bound">t₁</a> <a id="1023" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1025" href="Function.Equality.html#901" class="Bound">t₂</a><a id="1027" class="Symbol">)</a> <a id="1029" class="Keyword">where</a>
|
||
<a id="1037" class="Keyword">infixl</a> <a id="1044" class="Number">5</a> <a id="1046" href="Function.Equality.html#1064" class="Field Operator">_⟨$⟩_</a>
|
||
<a id="1054" class="Keyword">field</a>
|
||
<a id="Π._⟨$⟩_"></a><a id="1064" href="Function.Equality.html#1064" class="Field Operator">_⟨$⟩_</a> <a id="1070" class="Symbol">:</a> <a id="1072" class="Symbol">(</a><a id="1073" href="Function.Equality.html#1073" class="Bound">x</a> <a id="1075" class="Symbol">:</a> <a id="1077" href="Relation.Binary.Bundles.html#1072" class="Field">Setoid.Carrier</a> <a id="1092" href="Function.Equality.html#915" class="Bound">From</a><a id="1096" class="Symbol">)</a> <a id="1098" class="Symbol">→</a> <a id="1100" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#879" class="Field">IndexedSetoid.Carrier</a> <a id="1122" href="Function.Equality.html#946" class="Bound">To</a> <a id="1125" href="Function.Equality.html#1073" class="Bound">x</a>
|
||
<a id="Π.cong"></a><a id="1131" href="Function.Equality.html#1131" class="Field">cong</a> <a id="1137" class="Symbol">:</a> <a id="1139" href="Relation.Binary.Bundles.html#1098" class="Field Operator">Setoid._≈_</a> <a id="1150" href="Function.Equality.html#915" class="Bound">From</a> <a id="1155" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1062" class="Function Operator">=[</a> <a id="1158" href="Function.Equality.html#1064" class="Field Operator">_⟨$⟩_</a> <a id="1164" href="Relation.Binary.Indexed.Heterogeneous.Core.html#1062" class="Function Operator">]⇒</a> <a id="1167" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#909" class="Field Operator">IndexedSetoid._≈_</a> <a id="1185" href="Function.Equality.html#946" class="Bound">To</a>
|
||
|
||
<a id="1189" class="Keyword">open</a> <a id="1194" href="Function.Equality.html#889" class="Module">Π</a> <a id="1196" class="Keyword">public</a>
|
||
|
||
<a id="1204" class="Keyword">infixr</a> <a id="1211" class="Number">0</a> <a id="1213" href="Function.Equality.html#1218" class="Function Operator">_⟶_</a>
|
||
|
||
<a id="_⟶_"></a><a id="1218" href="Function.Equality.html#1218" class="Function Operator">_⟶_</a> <a id="1222" class="Symbol">:</a> <a id="1224" class="Symbol">∀</a> <a id="1226" class="Symbol">{</a><a id="1227" href="Function.Equality.html#1227" class="Bound">f₁</a> <a id="1230" href="Function.Equality.html#1230" class="Bound">f₂</a> <a id="1233" href="Function.Equality.html#1233" class="Bound">t₁</a> <a id="1236" href="Function.Equality.html#1236" class="Bound">t₂</a><a id="1238" class="Symbol">}</a> <a id="1240" class="Symbol">→</a> <a id="1242" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1249" href="Function.Equality.html#1227" class="Bound">f₁</a> <a id="1252" href="Function.Equality.html#1230" class="Bound">f₂</a> <a id="1255" class="Symbol">→</a> <a id="1257" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1264" href="Function.Equality.html#1233" class="Bound">t₁</a> <a id="1267" href="Function.Equality.html#1236" class="Bound">t₂</a> <a id="1270" class="Symbol">→</a> <a id="1272" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1276" class="Symbol">_</a>
|
||
<a id="1278" href="Function.Equality.html#1278" class="Bound">From</a> <a id="1283" href="Function.Equality.html#1218" class="Function Operator">⟶</a> <a id="1285" href="Function.Equality.html#1285" class="Bound">To</a> <a id="1288" class="Symbol">=</a> <a id="1290" href="Function.Equality.html#889" class="Record">Π</a> <a id="1292" href="Function.Equality.html#1278" class="Bound">From</a> <a id="1297" class="Symbol">(</a><a id="1298" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1370" class="Function">Trivial.indexedSetoid</a> <a id="1320" href="Function.Equality.html#1285" class="Bound">To</a><a id="1322" class="Symbol">)</a>
|
||
|
||
<a id="1325" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="1398" class="Comment">-- Identity and composition.</a>
|
||
|
||
<a id="id"></a><a id="1428" href="Function.Equality.html#1428" class="Function">id</a> <a id="1431" class="Symbol">:</a> <a id="1433" class="Symbol">∀</a> <a id="1435" class="Symbol">{</a><a id="1436" href="Function.Equality.html#1436" class="Bound">a₁</a> <a id="1439" href="Function.Equality.html#1439" class="Bound">a₂</a><a id="1441" class="Symbol">}</a> <a id="1443" class="Symbol">{</a><a id="1444" href="Function.Equality.html#1444" class="Bound">A</a> <a id="1446" class="Symbol">:</a> <a id="1448" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1455" href="Function.Equality.html#1436" class="Bound">a₁</a> <a id="1458" href="Function.Equality.html#1439" class="Bound">a₂</a><a id="1460" class="Symbol">}</a> <a id="1462" class="Symbol">→</a> <a id="1464" href="Function.Equality.html#1444" class="Bound">A</a> <a id="1466" href="Function.Equality.html#1218" class="Function Operator">⟶</a> <a id="1468" href="Function.Equality.html#1444" class="Bound">A</a>
|
||
<a id="1470" href="Function.Equality.html#1428" class="Function">id</a> <a id="1473" class="Symbol">=</a> <a id="1475" class="Keyword">record</a> <a id="1482" class="Symbol">{</a> <a id="1484" href="Function.Equality.html#1064" class="Field Operator">_⟨$⟩_</a> <a id="1490" class="Symbol">=</a> <a id="1492" href="Function.Base.html#615" class="Function">Fun.id</a><a id="1498" class="Symbol">;</a> <a id="1500" href="Function.Equality.html#1131" class="Field">cong</a> <a id="1505" class="Symbol">=</a> <a id="1507" href="Function.Base.html#615" class="Function">Fun.id</a> <a id="1514" class="Symbol">}</a>
|
||
|
||
<a id="1517" class="Keyword">infixr</a> <a id="1524" class="Number">9</a> <a id="1526" href="Function.Equality.html#1531" class="Function Operator">_∘_</a>
|
||
|
||
<a id="_∘_"></a><a id="1531" href="Function.Equality.html#1531" class="Function Operator">_∘_</a> <a id="1535" class="Symbol">:</a> <a id="1537" class="Symbol">∀</a> <a id="1539" class="Symbol">{</a><a id="1540" href="Function.Equality.html#1540" class="Bound">a₁</a> <a id="1543" href="Function.Equality.html#1543" class="Bound">a₂</a><a id="1545" class="Symbol">}</a> <a id="1547" class="Symbol">{</a><a id="1548" href="Function.Equality.html#1548" class="Bound">A</a> <a id="1550" class="Symbol">:</a> <a id="1552" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1559" href="Function.Equality.html#1540" class="Bound">a₁</a> <a id="1562" href="Function.Equality.html#1543" class="Bound">a₂</a><a id="1564" class="Symbol">}</a>
|
||
<a id="1574" class="Symbol">{</a><a id="1575" href="Function.Equality.html#1575" class="Bound">b₁</a> <a id="1578" href="Function.Equality.html#1578" class="Bound">b₂</a><a id="1580" class="Symbol">}</a> <a id="1582" class="Symbol">{</a><a id="1583" href="Function.Equality.html#1583" class="Bound">B</a> <a id="1585" class="Symbol">:</a> <a id="1587" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1594" href="Function.Equality.html#1575" class="Bound">b₁</a> <a id="1597" href="Function.Equality.html#1578" class="Bound">b₂</a><a id="1599" class="Symbol">}</a>
|
||
<a id="1609" class="Symbol">{</a><a id="1610" href="Function.Equality.html#1610" class="Bound">c₁</a> <a id="1613" href="Function.Equality.html#1613" class="Bound">c₂</a><a id="1615" class="Symbol">}</a> <a id="1617" class="Symbol">{</a><a id="1618" href="Function.Equality.html#1618" class="Bound">C</a> <a id="1620" class="Symbol">:</a> <a id="1622" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1629" href="Function.Equality.html#1610" class="Bound">c₁</a> <a id="1632" href="Function.Equality.html#1613" class="Bound">c₂</a><a id="1634" class="Symbol">}</a> <a id="1636" class="Symbol">→</a>
|
||
<a id="1644" href="Function.Equality.html#1583" class="Bound">B</a> <a id="1646" href="Function.Equality.html#1218" class="Function Operator">⟶</a> <a id="1648" href="Function.Equality.html#1618" class="Bound">C</a> <a id="1650" class="Symbol">→</a> <a id="1652" href="Function.Equality.html#1548" class="Bound">A</a> <a id="1654" href="Function.Equality.html#1218" class="Function Operator">⟶</a> <a id="1656" href="Function.Equality.html#1583" class="Bound">B</a> <a id="1658" class="Symbol">→</a> <a id="1660" href="Function.Equality.html#1548" class="Bound">A</a> <a id="1662" href="Function.Equality.html#1218" class="Function Operator">⟶</a> <a id="1664" href="Function.Equality.html#1618" class="Bound">C</a>
|
||
<a id="1666" href="Function.Equality.html#1666" class="Bound">f</a> <a id="1668" href="Function.Equality.html#1531" class="Function Operator">∘</a> <a id="1670" href="Function.Equality.html#1670" class="Bound">g</a> <a id="1672" class="Symbol">=</a> <a id="1674" class="Keyword">record</a>
|
||
<a id="1683" class="Symbol">{</a> <a id="1685" href="Function.Equality.html#1064" class="Field Operator">_⟨$⟩_</a> <a id="1691" class="Symbol">=</a> <a id="1693" href="Function.Base.html#1031" class="Function Operator">Fun._∘_</a> <a id="1701" class="Symbol">(</a><a id="1702" href="Function.Equality.html#1064" class="Field Operator">_⟨$⟩_</a> <a id="1708" href="Function.Equality.html#1666" class="Bound">f</a><a id="1709" class="Symbol">)</a> <a id="1711" class="Symbol">(</a><a id="1712" href="Function.Equality.html#1064" class="Field Operator">_⟨$⟩_</a> <a id="1718" href="Function.Equality.html#1670" class="Bound">g</a><a id="1719" class="Symbol">)</a>
|
||
<a id="1723" class="Symbol">;</a> <a id="1725" href="Function.Equality.html#1131" class="Field">cong</a> <a id="1731" class="Symbol">=</a> <a id="1733" href="Function.Base.html#1031" class="Function Operator">Fun._∘_</a> <a id="1741" class="Symbol">(</a><a id="1742" href="Function.Equality.html#1131" class="Field">cong</a> <a id="1748" href="Function.Equality.html#1666" class="Bound">f</a><a id="1749" class="Symbol">)</a> <a id="1751" class="Symbol">(</a><a id="1752" href="Function.Equality.html#1131" class="Field">cong</a> <a id="1758" href="Function.Equality.html#1670" class="Bound">g</a><a id="1759" class="Symbol">)</a>
|
||
<a id="1763" class="Symbol">}</a>
|
||
|
||
<a id="1766" class="Comment">-- Constant equality-preserving function.</a>
|
||
|
||
<a id="const"></a><a id="1809" href="Function.Equality.html#1809" class="Function">const</a> <a id="1815" class="Symbol">:</a> <a id="1817" class="Symbol">∀</a> <a id="1819" class="Symbol">{</a><a id="1820" href="Function.Equality.html#1820" class="Bound">a₁</a> <a id="1823" href="Function.Equality.html#1823" class="Bound">a₂</a><a id="1825" class="Symbol">}</a> <a id="1827" class="Symbol">{</a><a id="1828" href="Function.Equality.html#1828" class="Bound">A</a> <a id="1830" class="Symbol">:</a> <a id="1832" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1839" href="Function.Equality.html#1820" class="Bound">a₁</a> <a id="1842" href="Function.Equality.html#1823" class="Bound">a₂</a><a id="1844" class="Symbol">}</a>
|
||
<a id="1856" class="Symbol">{</a><a id="1857" href="Function.Equality.html#1857" class="Bound">b₁</a> <a id="1860" href="Function.Equality.html#1860" class="Bound">b₂</a><a id="1862" class="Symbol">}</a> <a id="1864" class="Symbol">{</a><a id="1865" href="Function.Equality.html#1865" class="Bound">B</a> <a id="1867" class="Symbol">:</a> <a id="1869" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1876" href="Function.Equality.html#1857" class="Bound">b₁</a> <a id="1879" href="Function.Equality.html#1860" class="Bound">b₂</a><a id="1881" class="Symbol">}</a> <a id="1883" class="Symbol">→</a>
|
||
<a id="1893" href="Relation.Binary.Bundles.html#1072" class="Field">Setoid.Carrier</a> <a id="1908" href="Function.Equality.html#1865" class="Bound">B</a> <a id="1910" class="Symbol">→</a> <a id="1912" href="Function.Equality.html#1828" class="Bound">A</a> <a id="1914" href="Function.Equality.html#1218" class="Function Operator">⟶</a> <a id="1916" href="Function.Equality.html#1865" class="Bound">B</a>
|
||
<a id="1918" href="Function.Equality.html#1809" class="Function">const</a> <a id="1924" class="Symbol">{</a><a id="1925" class="Argument">B</a> <a id="1927" class="Symbol">=</a> <a id="1929" href="Function.Equality.html#1929" class="Bound">B</a><a id="1930" class="Symbol">}</a> <a id="1932" href="Function.Equality.html#1932" class="Bound">b</a> <a id="1934" class="Symbol">=</a> <a id="1936" class="Keyword">record</a>
|
||
<a id="1945" class="Symbol">{</a> <a id="1947" href="Function.Equality.html#1064" class="Field Operator">_⟨$⟩_</a> <a id="1953" class="Symbol">=</a> <a id="1955" href="Function.Base.html#636" class="Function">Fun.const</a> <a id="1965" href="Function.Equality.html#1932" class="Bound">b</a>
|
||
<a id="1969" class="Symbol">;</a> <a id="1971" href="Function.Equality.html#1131" class="Field">cong</a> <a id="1977" class="Symbol">=</a> <a id="1979" href="Function.Base.html#636" class="Function">Fun.const</a> <a id="1989" class="Symbol">(</a><a id="1990" href="Relation.Binary.Structures.html#1568" class="Function">Setoid.refl</a> <a id="2002" href="Function.Equality.html#1929" class="Bound">B</a><a id="2003" class="Symbol">)</a>
|
||
<a id="2007" class="Symbol">}</a>
|
||
|
||
<a id="2010" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="2083" class="Comment">-- Function setoids</a>
|
||
|
||
<a id="2104" class="Comment">-- Dependent.</a>
|
||
|
||
<a id="setoid"></a><a id="2119" href="Function.Equality.html#2119" class="Function">setoid</a> <a id="2126" class="Symbol">:</a> <a id="2128" class="Symbol">∀</a> <a id="2130" class="Symbol">{</a><a id="2131" href="Function.Equality.html#2131" class="Bound">f₁</a> <a id="2134" href="Function.Equality.html#2134" class="Bound">f₂</a> <a id="2137" href="Function.Equality.html#2137" class="Bound">t₁</a> <a id="2140" href="Function.Equality.html#2140" class="Bound">t₂</a><a id="2142" class="Symbol">}</a>
|
||
<a id="2153" class="Symbol">(</a><a id="2154" href="Function.Equality.html#2154" class="Bound">From</a> <a id="2159" class="Symbol">:</a> <a id="2161" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="2168" href="Function.Equality.html#2131" class="Bound">f₁</a> <a id="2171" href="Function.Equality.html#2134" class="Bound">f₂</a><a id="2173" class="Symbol">)</a> <a id="2175" class="Symbol">→</a>
|
||
<a id="2186" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#789" class="Record">IndexedSetoid</a> <a id="2200" class="Symbol">(</a><a id="2201" href="Relation.Binary.Bundles.html#1072" class="Field">Setoid.Carrier</a> <a id="2216" href="Function.Equality.html#2154" class="Bound">From</a><a id="2220" class="Symbol">)</a> <a id="2222" href="Function.Equality.html#2137" class="Bound">t₁</a> <a id="2225" href="Function.Equality.html#2140" class="Bound">t₂</a> <a id="2228" class="Symbol">→</a>
|
||
<a id="2239" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="2246" class="Symbol">_</a> <a id="2248" class="Symbol">_</a>
|
||
<a id="2250" href="Function.Equality.html#2119" class="Function">setoid</a> <a id="2257" href="Function.Equality.html#2257" class="Bound">From</a> <a id="2262" href="Function.Equality.html#2262" class="Bound">To</a> <a id="2265" class="Symbol">=</a> <a id="2267" class="Keyword">record</a>
|
||
<a id="2276" class="Symbol">{</a> <a id="2278" href="Relation.Binary.Bundles.html#1072" class="Field">Carrier</a> <a id="2292" class="Symbol">=</a> <a id="2294" href="Function.Equality.html#889" class="Record">Π</a> <a id="2296" href="Function.Equality.html#2257" class="Bound">From</a> <a id="2301" href="Function.Equality.html#2262" class="Bound">To</a>
|
||
<a id="2306" class="Symbol">;</a> <a id="2308" href="Relation.Binary.Bundles.html#1098" class="Field Operator">_≈_</a> <a id="2322" class="Symbol">=</a> <a id="2324" class="Symbol">λ</a> <a id="2326" href="Function.Equality.html#2326" class="Bound">f</a> <a id="2328" href="Function.Equality.html#2328" class="Bound">g</a> <a id="2330" class="Symbol">→</a> <a id="2332" class="Symbol">∀</a> <a id="2334" class="Symbol">{</a><a id="2335" href="Function.Equality.html#2335" class="Bound">x</a> <a id="2337" href="Function.Equality.html#2337" class="Bound">y</a><a id="2338" class="Symbol">}</a> <a id="2340" class="Symbol">→</a> <a id="2342" href="Function.Equality.html#2335" class="Bound">x</a> <a id="2344" href="Function.Equality.html#2622" class="Function Operator">≈₁</a> <a id="2347" href="Function.Equality.html#2337" class="Bound">y</a> <a id="2349" class="Symbol">→</a> <a id="2351" href="Function.Equality.html#2326" class="Bound">f</a> <a id="2353" href="Function.Equality.html#1064" class="Field Operator">⟨$⟩</a> <a id="2357" href="Function.Equality.html#2335" class="Bound">x</a> <a id="2359" href="Function.Equality.html#2692" class="Field Operator">≈₂</a> <a id="2362" href="Function.Equality.html#2328" class="Bound">g</a> <a id="2364" href="Function.Equality.html#1064" class="Field Operator">⟨$⟩</a> <a id="2368" href="Function.Equality.html#2337" class="Bound">y</a>
|
||
<a id="2372" class="Symbol">;</a> <a id="2374" href="Relation.Binary.Bundles.html#1132" class="Field">isEquivalence</a> <a id="2388" class="Symbol">=</a> <a id="2390" class="Keyword">record</a>
|
||
<a id="2401" class="Symbol">{</a> <a id="2403" href="Relation.Binary.Structures.html#1568" class="Field">refl</a> <a id="2409" class="Symbol">=</a> <a id="2411" class="Symbol">λ</a> <a id="2413" class="Symbol">{</a><a id="2414" href="Function.Equality.html#2414" class="Bound">f</a><a id="2415" class="Symbol">}</a> <a id="2417" class="Symbol">→</a> <a id="2419" href="Function.Equality.html#1131" class="Field">cong</a> <a id="2424" href="Function.Equality.html#2414" class="Bound">f</a>
|
||
<a id="2430" class="Symbol">;</a> <a id="2432" href="Relation.Binary.Structures.html#1594" class="Field">sym</a> <a id="2438" class="Symbol">=</a> <a id="2440" class="Symbol">λ</a> <a id="2442" href="Function.Equality.html#2442" class="Bound">f∼g</a> <a id="2446" href="Function.Equality.html#2446" class="Bound">x∼y</a> <a id="2450" class="Symbol">→</a> <a id="2452" href="Relation.Binary.Indexed.Heterogeneous.Structures.html#938" class="Function">To.sym</a> <a id="2459" class="Symbol">(</a><a id="2460" href="Function.Equality.html#2442" class="Bound">f∼g</a> <a id="2464" class="Symbol">(</a><a id="2465" href="Relation.Binary.Structures.html#1594" class="Function">From.sym</a> <a id="2474" href="Function.Equality.html#2446" class="Bound">x∼y</a><a id="2477" class="Symbol">))</a>
|
||
<a id="2484" class="Symbol">;</a> <a id="2486" href="Relation.Binary.Structures.html#1620" class="Field">trans</a> <a id="2492" class="Symbol">=</a> <a id="2494" class="Symbol">λ</a> <a id="2496" href="Function.Equality.html#2496" class="Bound">f∼g</a> <a id="2500" href="Function.Equality.html#2500" class="Bound">g∼h</a> <a id="2504" href="Function.Equality.html#2504" class="Bound">x∼y</a> <a id="2508" class="Symbol">→</a> <a id="2510" href="Relation.Binary.Indexed.Heterogeneous.Structures.html#967" class="Function">To.trans</a> <a id="2519" class="Symbol">(</a><a id="2520" href="Function.Equality.html#2496" class="Bound">f∼g</a> <a id="2524" href="Relation.Binary.Structures.html#1568" class="Function">From.refl</a><a id="2533" class="Symbol">)</a> <a id="2535" class="Symbol">(</a><a id="2536" href="Function.Equality.html#2500" class="Bound">g∼h</a> <a id="2540" href="Function.Equality.html#2504" class="Bound">x∼y</a><a id="2543" class="Symbol">)</a>
|
||
<a id="2549" class="Symbol">}</a>
|
||
<a id="2553" class="Symbol">}</a>
|
||
<a id="2557" class="Keyword">where</a>
|
||
<a id="2565" class="Keyword">open</a> <a id="2570" class="Keyword">module</a> <a id="2577" href="Function.Equality.html#2577" class="Module">From</a> <a id="2582" class="Symbol">=</a> <a id="2584" href="Relation.Binary.Bundles.html#1009" class="Module">Setoid</a> <a id="2591" href="Function.Equality.html#2257" class="Bound">From</a> <a id="2596" class="Keyword">using</a> <a id="2602" class="Symbol">()</a> <a id="2605" class="Keyword">renaming</a> <a id="2614" class="Symbol">(</a><a id="2615" href="Relation.Binary.Bundles.html#1098" class="Function Operator">_≈_</a> <a id="2619" class="Symbol">to</a> <a id="2622" class="Function Operator">_≈₁_</a><a id="2626" class="Symbol">)</a>
|
||
<a id="2630" class="Keyword">open</a> <a id="2635" class="Keyword">module</a> <a id="2642" href="Function.Equality.html#2642" class="Module">To</a> <a id="2645" class="Symbol">=</a> <a id="2647" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#789" class="Module">IndexedSetoid</a> <a id="2661" href="Function.Equality.html#2262" class="Bound">To</a> <a id="2666" class="Keyword">using</a> <a id="2672" class="Symbol">()</a> <a id="2675" class="Keyword">renaming</a> <a id="2684" class="Symbol">(</a><a id="2685" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#909" class="Field Operator">_≈_</a> <a id="2689" class="Symbol">to</a> <a id="2692" class="Field Operator">_≈₂_</a><a id="2696" class="Symbol">)</a>
|
||
|
||
<a id="2699" class="Comment">-- Non-dependent.</a>
|
||
|
||
<a id="2718" class="Keyword">infixr</a> <a id="2725" class="Number">0</a> <a id="2727" href="Function.Equality.html#2732" class="Function Operator">_⇨_</a>
|
||
|
||
<a id="_⇨_"></a><a id="2732" href="Function.Equality.html#2732" class="Function Operator">_⇨_</a> <a id="2736" class="Symbol">:</a> <a id="2738" class="Symbol">∀</a> <a id="2740" class="Symbol">{</a><a id="2741" href="Function.Equality.html#2741" class="Bound">f₁</a> <a id="2744" href="Function.Equality.html#2744" class="Bound">f₂</a> <a id="2747" href="Function.Equality.html#2747" class="Bound">t₁</a> <a id="2750" href="Function.Equality.html#2750" class="Bound">t₂</a><a id="2752" class="Symbol">}</a> <a id="2754" class="Symbol">→</a> <a id="2756" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="2763" href="Function.Equality.html#2741" class="Bound">f₁</a> <a id="2766" href="Function.Equality.html#2744" class="Bound">f₂</a> <a id="2769" class="Symbol">→</a> <a id="2771" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="2778" href="Function.Equality.html#2747" class="Bound">t₁</a> <a id="2781" href="Function.Equality.html#2750" class="Bound">t₂</a> <a id="2784" class="Symbol">→</a> <a id="2786" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="2793" class="Symbol">_</a> <a id="2795" class="Symbol">_</a>
|
||
<a id="2797" href="Function.Equality.html#2797" class="Bound">From</a> <a id="2802" href="Function.Equality.html#2732" class="Function Operator">⇨</a> <a id="2804" href="Function.Equality.html#2804" class="Bound">To</a> <a id="2807" class="Symbol">=</a> <a id="2809" href="Function.Equality.html#2119" class="Function">setoid</a> <a id="2816" href="Function.Equality.html#2797" class="Bound">From</a> <a id="2821" class="Symbol">(</a><a id="2822" href="Relation.Binary.Indexed.Heterogeneous.Construct.Trivial.html#1370" class="Function">Trivial.indexedSetoid</a> <a id="2844" href="Function.Equality.html#2804" class="Bound">To</a><a id="2846" class="Symbol">)</a>
|
||
|
||
<a id="2849" class="Comment">-- A variant of setoid which uses the propositional equality setoid</a>
|
||
<a id="2917" class="Comment">-- for the domain, and a more convenient definition of _≈_.</a>
|
||
|
||
<a id="≡-setoid"></a><a id="2978" href="Function.Equality.html#2978" class="Function">≡-setoid</a> <a id="2987" class="Symbol">:</a> <a id="2989" class="Symbol">∀</a> <a id="2991" class="Symbol">{</a><a id="2992" href="Function.Equality.html#2992" class="Bound">f</a> <a id="2994" href="Function.Equality.html#2994" class="Bound">t₁</a> <a id="2997" href="Function.Equality.html#2997" class="Bound">t₂</a><a id="2999" class="Symbol">}</a> <a id="3001" class="Symbol">(</a><a id="3002" href="Function.Equality.html#3002" class="Bound">From</a> <a id="3007" class="Symbol">:</a> <a id="3009" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3013" href="Function.Equality.html#2992" class="Bound">f</a><a id="3014" class="Symbol">)</a> <a id="3016" class="Symbol">→</a> <a id="3018" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#789" class="Record">IndexedSetoid</a> <a id="3032" href="Function.Equality.html#3002" class="Bound">From</a> <a id="3037" href="Function.Equality.html#2994" class="Bound">t₁</a> <a id="3040" href="Function.Equality.html#2997" class="Bound">t₂</a> <a id="3043" class="Symbol">→</a> <a id="3045" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="3052" class="Symbol">_</a> <a id="3054" class="Symbol">_</a>
|
||
<a id="3056" href="Function.Equality.html#2978" class="Function">≡-setoid</a> <a id="3065" href="Function.Equality.html#3065" class="Bound">From</a> <a id="3070" href="Function.Equality.html#3070" class="Bound">To</a> <a id="3073" class="Symbol">=</a> <a id="3075" class="Keyword">record</a>
|
||
<a id="3084" class="Symbol">{</a> <a id="3086" href="Relation.Binary.Bundles.html#1072" class="Field">Carrier</a> <a id="3100" class="Symbol">=</a> <a id="3102" class="Symbol">(</a><a id="3103" href="Function.Equality.html#3103" class="Bound">x</a> <a id="3105" class="Symbol">:</a> <a id="3107" href="Function.Equality.html#3065" class="Bound">From</a><a id="3111" class="Symbol">)</a> <a id="3113" class="Symbol">→</a> <a id="3115" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#879" class="Field">Carrier</a> <a id="3123" href="Function.Equality.html#3103" class="Bound">x</a>
|
||
<a id="3127" class="Symbol">;</a> <a id="3129" href="Relation.Binary.Bundles.html#1098" class="Field Operator">_≈_</a> <a id="3143" class="Symbol">=</a> <a id="3145" class="Symbol">λ</a> <a id="3147" href="Function.Equality.html#3147" class="Bound">f</a> <a id="3149" href="Function.Equality.html#3149" class="Bound">g</a> <a id="3151" class="Symbol">→</a> <a id="3153" class="Symbol">∀</a> <a id="3155" href="Function.Equality.html#3155" class="Bound">x</a> <a id="3157" class="Symbol">→</a> <a id="3159" href="Function.Equality.html#3147" class="Bound">f</a> <a id="3161" href="Function.Equality.html#3155" class="Bound">x</a> <a id="3163" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#909" class="Field Operator">≈</a> <a id="3165" href="Function.Equality.html#3149" class="Bound">g</a> <a id="3167" href="Function.Equality.html#3155" class="Bound">x</a>
|
||
<a id="3171" class="Symbol">;</a> <a id="3173" href="Relation.Binary.Bundles.html#1132" class="Field">isEquivalence</a> <a id="3187" class="Symbol">=</a> <a id="3189" class="Keyword">record</a>
|
||
<a id="3200" class="Symbol">{</a> <a id="3202" href="Relation.Binary.Structures.html#1568" class="Field">refl</a> <a id="3208" class="Symbol">=</a> <a id="3210" class="Symbol">λ</a> <a id="3212" class="Symbol">{</a><a id="3213" href="Function.Equality.html#3213" class="Bound">f</a><a id="3214" class="Symbol">}</a> <a id="3216" href="Function.Equality.html#3216" class="Bound">x</a> <a id="3218" class="Symbol">→</a> <a id="3220" href="Relation.Binary.Indexed.Heterogeneous.Structures.html#909" class="Function">refl</a>
|
||
<a id="3229" class="Symbol">;</a> <a id="3231" href="Relation.Binary.Structures.html#1594" class="Field">sym</a> <a id="3237" class="Symbol">=</a> <a id="3239" class="Symbol">λ</a> <a id="3241" href="Function.Equality.html#3241" class="Bound">f∼g</a> <a id="3245" href="Function.Equality.html#3245" class="Bound">x</a> <a id="3247" class="Symbol">→</a> <a id="3249" href="Relation.Binary.Indexed.Heterogeneous.Structures.html#938" class="Function">sym</a> <a id="3253" class="Symbol">(</a><a id="3254" href="Function.Equality.html#3241" class="Bound">f∼g</a> <a id="3258" href="Function.Equality.html#3245" class="Bound">x</a><a id="3259" class="Symbol">)</a>
|
||
<a id="3265" class="Symbol">;</a> <a id="3267" href="Relation.Binary.Structures.html#1620" class="Field">trans</a> <a id="3273" class="Symbol">=</a> <a id="3275" class="Symbol">λ</a> <a id="3277" href="Function.Equality.html#3277" class="Bound">f∼g</a> <a id="3281" href="Function.Equality.html#3281" class="Bound">g∼h</a> <a id="3285" href="Function.Equality.html#3285" class="Bound">x</a> <a id="3287" class="Symbol">→</a> <a id="3289" href="Relation.Binary.Indexed.Heterogeneous.Structures.html#967" class="Function">trans</a> <a id="3295" class="Symbol">(</a><a id="3296" href="Function.Equality.html#3277" class="Bound">f∼g</a> <a id="3300" href="Function.Equality.html#3285" class="Bound">x</a><a id="3301" class="Symbol">)</a> <a id="3303" class="Symbol">(</a><a id="3304" href="Function.Equality.html#3281" class="Bound">g∼h</a> <a id="3308" href="Function.Equality.html#3285" class="Bound">x</a><a id="3309" class="Symbol">)</a>
|
||
<a id="3315" class="Symbol">}</a>
|
||
<a id="3319" class="Symbol">}</a> <a id="3321" class="Keyword">where</a> <a id="3327" class="Keyword">open</a> <a id="3332" href="Relation.Binary.Indexed.Heterogeneous.Bundles.html#789" class="Module">IndexedSetoid</a> <a id="3346" href="Function.Equality.html#3070" class="Bound">To</a>
|
||
|
||
<a id="3350" class="Comment">-- Parameter swapping function.</a>
|
||
|
||
<a id="flip"></a><a id="3383" href="Function.Equality.html#3383" class="Function">flip</a> <a id="3388" class="Symbol">:</a> <a id="3390" class="Symbol">∀</a> <a id="3392" class="Symbol">{</a><a id="3393" href="Function.Equality.html#3393" class="Bound">a₁</a> <a id="3396" href="Function.Equality.html#3396" class="Bound">a₂</a><a id="3398" class="Symbol">}</a> <a id="3400" class="Symbol">{</a><a id="3401" href="Function.Equality.html#3401" class="Bound">A</a> <a id="3403" class="Symbol">:</a> <a id="3405" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="3412" href="Function.Equality.html#3393" class="Bound">a₁</a> <a id="3415" href="Function.Equality.html#3396" class="Bound">a₂</a><a id="3417" class="Symbol">}</a>
|
||
<a id="3428" class="Symbol">{</a><a id="3429" href="Function.Equality.html#3429" class="Bound">b₁</a> <a id="3432" href="Function.Equality.html#3432" class="Bound">b₂</a><a id="3434" class="Symbol">}</a> <a id="3436" class="Symbol">{</a><a id="3437" href="Function.Equality.html#3437" class="Bound">B</a> <a id="3439" class="Symbol">:</a> <a id="3441" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="3448" href="Function.Equality.html#3429" class="Bound">b₁</a> <a id="3451" href="Function.Equality.html#3432" class="Bound">b₂</a><a id="3453" class="Symbol">}</a>
|
||
<a id="3464" class="Symbol">{</a><a id="3465" href="Function.Equality.html#3465" class="Bound">c₁</a> <a id="3468" href="Function.Equality.html#3468" class="Bound">c₂</a><a id="3470" class="Symbol">}</a> <a id="3472" class="Symbol">{</a><a id="3473" href="Function.Equality.html#3473" class="Bound">C</a> <a id="3475" class="Symbol">:</a> <a id="3477" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="3484" href="Function.Equality.html#3465" class="Bound">c₁</a> <a id="3487" href="Function.Equality.html#3468" class="Bound">c₂</a><a id="3489" class="Symbol">}</a> <a id="3491" class="Symbol">→</a>
|
||
<a id="3500" href="Function.Equality.html#3401" class="Bound">A</a> <a id="3502" href="Function.Equality.html#1218" class="Function Operator">⟶</a> <a id="3504" href="Function.Equality.html#3437" class="Bound">B</a> <a id="3506" href="Function.Equality.html#2732" class="Function Operator">⇨</a> <a id="3508" href="Function.Equality.html#3473" class="Bound">C</a> <a id="3510" class="Symbol">→</a> <a id="3512" href="Function.Equality.html#3437" class="Bound">B</a> <a id="3514" href="Function.Equality.html#1218" class="Function Operator">⟶</a> <a id="3516" href="Function.Equality.html#3401" class="Bound">A</a> <a id="3518" href="Function.Equality.html#2732" class="Function Operator">⇨</a> <a id="3520" href="Function.Equality.html#3473" class="Bound">C</a>
|
||
<a id="3522" href="Function.Equality.html#3383" class="Function">flip</a> <a id="3527" class="Symbol">{</a><a id="3528" class="Argument">B</a> <a id="3530" class="Symbol">=</a> <a id="3532" href="Function.Equality.html#3532" class="Bound">B</a><a id="3533" class="Symbol">}</a> <a id="3535" href="Function.Equality.html#3535" class="Bound">f</a> <a id="3537" class="Symbol">=</a> <a id="3539" class="Keyword">record</a>
|
||
<a id="3548" class="Symbol">{</a> <a id="3550" href="Function.Equality.html#1064" class="Field Operator">_⟨$⟩_</a> <a id="3556" class="Symbol">=</a> <a id="3558" class="Symbol">λ</a> <a id="3560" href="Function.Equality.html#3560" class="Bound">b</a> <a id="3562" class="Symbol">→</a> <a id="3564" class="Keyword">record</a>
|
||
<a id="3575" class="Symbol">{</a> <a id="3577" href="Function.Equality.html#1064" class="Field Operator">_⟨$⟩_</a> <a id="3583" class="Symbol">=</a> <a id="3585" class="Symbol">λ</a> <a id="3587" href="Function.Equality.html#3587" class="Bound">a</a> <a id="3589" class="Symbol">→</a> <a id="3591" href="Function.Equality.html#3535" class="Bound">f</a> <a id="3593" href="Function.Equality.html#1064" class="Field Operator">⟨$⟩</a> <a id="3597" href="Function.Equality.html#3587" class="Bound">a</a> <a id="3599" href="Function.Equality.html#1064" class="Field Operator">⟨$⟩</a> <a id="3603" href="Function.Equality.html#3560" class="Bound">b</a>
|
||
<a id="3609" class="Symbol">;</a> <a id="3611" href="Function.Equality.html#1131" class="Field">cong</a> <a id="3617" class="Symbol">=</a> <a id="3619" class="Symbol">λ</a> <a id="3621" href="Function.Equality.html#3621" class="Bound">a₁≈a₂</a> <a id="3627" class="Symbol">→</a> <a id="3629" href="Function.Equality.html#1131" class="Field">cong</a> <a id="3634" href="Function.Equality.html#3535" class="Bound">f</a> <a id="3636" href="Function.Equality.html#3621" class="Bound">a₁≈a₂</a> <a id="3642" class="Symbol">(</a><a id="3643" href="Relation.Binary.Structures.html#1568" class="Function">Setoid.refl</a> <a id="3655" href="Function.Equality.html#3532" class="Bound">B</a><a id="3656" class="Symbol">)</a> <a id="3658" class="Symbol">}</a>
|
||
<a id="3662" class="Symbol">;</a> <a id="3664" href="Function.Equality.html#1131" class="Field">cong</a> <a id="3670" class="Symbol">=</a> <a id="3672" class="Symbol">λ</a> <a id="3674" href="Function.Equality.html#3674" class="Bound">b₁≈b₂</a> <a id="3680" href="Function.Equality.html#3680" class="Bound">a₁≈a₂</a> <a id="3686" class="Symbol">→</a> <a id="3688" href="Function.Equality.html#1131" class="Field">cong</a> <a id="3693" href="Function.Equality.html#3535" class="Bound">f</a> <a id="3695" href="Function.Equality.html#3680" class="Bound">a₁≈a₂</a> <a id="3701" href="Function.Equality.html#3674" class="Bound">b₁≈b₂</a>
|
||
<a id="3709" class="Symbol">}</a>
|
||
</pre></body></html> |