rachel/rachel.cafe
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
f69b6e6959
rachel.cafe/misc/Function.Structures.html

154 lines
38 KiB
HTML
Raw Normal View History

add some agda stuff
2022-06-23 22:12:24 +02:00
<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Function.Structures</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">------------------------------------------------------------------------</a>
<a id="74" class="Comment">-- The Agda standard library</a>
<a id="103" class="Comment">--</a>
<a id="106" class="Comment">-- Structures for types of functions</a>
<a id="143" class="Comment">------------------------------------------------------------------------</a>
<a id="217" class="Comment">-- The contents of this file should usually be accessed from `Function`.</a>
<a id="291" class="Symbol">{-#</a> <a id="295" class="Keyword">OPTIONS</a> <a id="303" class="Pragma">--without-K</a> <a id="315" class="Pragma">--safe</a> <a id="322" class="Symbol">#-}</a>
<a id="327" class="Keyword">open</a> <a id="332" class="Keyword">import</a> <a id="339" href="Relation.Binary.html" class="Module">Relation.Binary</a>
<a id="356" class="Keyword">module</a> <a id="363" href="Function.Structures.html" class="Module">Function.Structures</a> <a id="383" class="Symbol">{</a><a id="384" href="Function.Structures.html#384" class="Bound">a</a> <a id="386" href="Function.Structures.html#386" class="Bound">b</a> <a id="388" href="Function.Structures.html#388" class="Bound">ℓ₁</a> <a id="391" href="Function.Structures.html#391" class="Bound">ℓ₂</a><a id="393" class="Symbol">}</a>
<a id="397" class="Symbol">{</a><a id="398" href="Function.Structures.html#398" class="Bound">A</a> <a id="400" class="Symbol">:</a> <a id="402" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="406" href="Function.Structures.html#384" class="Bound">a</a><a id="407" class="Symbol">}</a> <a id="409" class="Symbol">(</a><a id="410" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="415" class="Symbol">:</a> <a id="417" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="421" href="Function.Structures.html#398" class="Bound">A</a> <a id="423" href="Function.Structures.html#388" class="Bound">ℓ₁</a><a id="425" class="Symbol">)</a> <a id="427" class="Comment">-- Equality over the domain</a>
<a id="457" class="Symbol">{</a><a id="458" href="Function.Structures.html#458" class="Bound">B</a> <a id="460" class="Symbol">:</a> <a id="462" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="466" href="Function.Structures.html#386" class="Bound">b</a><a id="467" class="Symbol">}</a> <a id="469" class="Symbol">(</a><a id="470" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="475" class="Symbol">:</a> <a id="477" href="Relation.Binary.Core.html#882" class="Function">Rel</a> <a id="481" href="Function.Structures.html#458" class="Bound">B</a> <a id="483" href="Function.Structures.html#391" class="Bound">ℓ₂</a><a id="485" class="Symbol">)</a> <a id="487" class="Comment">-- Equality over the codomain</a>
<a id="519" class="Keyword">where</a>
<a id="526" class="Keyword">open</a> <a id="531" class="Keyword">import</a> <a id="538" href="Data.Product.html" class="Module">Data.Product</a> <a id="551" class="Keyword">using</a> <a id="557" class="Symbol">(</a><a id="558" href="Data.Product.html#1369" class="Function">∃</a><a id="559" class="Symbol">;</a> <a id="561" href="Data.Product.html#1167" class="Function Operator">_×_</a><a id="564" class="Symbol">;</a> <a id="566" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">_,_</a><a id="569" class="Symbol">)</a>
<a id="571" class="Keyword">open</a> <a id="576" class="Keyword">import</a> <a id="583" href="Function.Base.html" class="Module">Function.Base</a>
<a id="597" class="Keyword">open</a> <a id="602" class="Keyword">import</a> <a id="609" href="Function.Definitions.html" class="Module">Function.Definitions</a>
<a id="630" class="Keyword">open</a> <a id="635" class="Keyword">import</a> <a id="642" href="Level.html" class="Module">Level</a> <a id="648" class="Keyword">using</a> <a id="654" class="Symbol">(</a><a id="655" href="Agda.Primitive.html#810" class="Primitive Operator">_⊔_</a><a id="658" class="Symbol">)</a>
<a id="661" class="Comment">------------------------------------------------------------------------</a>
<a id="734" class="Comment">-- One element structures</a>
<a id="760" class="Comment">------------------------------------------------------------------------</a>
<a id="834" class="Keyword">record</a> <a id="IsCongruent"></a><a id="841" href="Function.Structures.html#841" class="Record">IsCongruent</a> <a id="853" class="Symbol">(</a><a id="854" href="Function.Structures.html#854" class="Bound">f</a> <a id="856" class="Symbol">:</a> <a id="858" href="Function.Structures.html#398" class="Bound">A</a> <a id="860" class="Symbol">→</a> <a id="862" href="Function.Structures.html#458" class="Bound">B</a><a id="863" class="Symbol">)</a> <a id="865" class="Symbol">:</a> <a id="867" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="871" class="Symbol">(</a><a id="872" href="Function.Structures.html#384" class="Bound">a</a> <a id="874" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="876" href="Function.Structures.html#386" class="Bound">b</a> <a id="878" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="880" href="Function.Structures.html#388" class="Bound">ℓ₁</a> <a id="883" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="885" href="Function.Structures.html#391" class="Bound">ℓ₂</a><a id="887" class="Symbol">)</a> <a id="889" class="Keyword">where</a>
<a id="897" class="Keyword">field</a>
<a id="IsCongruent.cong"></a><a id="907" href="Function.Structures.html#907" class="Field">cong</a> <a id="922" class="Symbol">:</a> <a id="924" href="Function.Definitions.html#803" class="Function">Congruent</a> <a id="934" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="939" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="944" href="Function.Structures.html#854" class="Bound">f</a>
<a id="IsCongruent.isEquivalence₁"></a><a id="950" href="Function.Structures.html#950" class="Field">isEquivalence₁</a> <a id="965" class="Symbol">:</a> <a id="967" href="Relation.Binary.Structures.html#1522" class="Record">IsEquivalence</a> <a id="981" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a>
<a id="IsCongruent.isEquivalence₂"></a><a id="990" href="Function.Structures.html#990" class="Field">isEquivalence₂</a> <a id="1005" class="Symbol">:</a> <a id="1007" href="Relation.Binary.Structures.html#1522" class="Record">IsEquivalence</a> <a id="1021" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a>
<a id="1029" class="Keyword">module</a> <a id="IsCongruent.Eq₁"></a><a id="1036" href="Function.Structures.html#1036" class="Module">Eq₁</a> <a id="1040" class="Keyword">where</a>
<a id="IsCongruent.Eq₁.setoid"></a><a id="1051" href="Function.Structures.html#1051" class="Function">setoid</a> <a id="1058" class="Symbol">:</a> <a id="1060" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1067" href="Function.Structures.html#384" class="Bound">a</a> <a id="1069" href="Function.Structures.html#388" class="Bound">ℓ₁</a>
<a id="1076" href="Function.Structures.html#1051" class="Function">setoid</a> <a id="1083" class="Symbol">=</a> <a id="1085" class="Keyword">record</a>
<a id="1098" class="Symbol">{</a> <a id="1100" href="Relation.Binary.Bundles.html#1132" class="Field">isEquivalence</a> <a id="1114" class="Symbol">=</a> <a id="1116" href="Function.Structures.html#950" class="Field">isEquivalence₁</a>
<a id="1137" class="Symbol">}</a>
<a id="1144" class="Keyword">open</a> <a id="1149" href="Relation.Binary.Bundles.html#1009" class="Module">Setoid</a> <a id="1156" href="Function.Structures.html#1051" class="Function">setoid</a> <a id="1163" class="Keyword">public</a>
<a id="1173" class="Keyword">module</a> <a id="IsCongruent.Eq₂"></a><a id="1180" href="Function.Structures.html#1180" class="Module">Eq₂</a> <a id="1184" class="Keyword">where</a>
<a id="IsCongruent.Eq₂.setoid"></a><a id="1195" href="Function.Structures.html#1195" class="Function">setoid</a> <a id="1202" class="Symbol">:</a> <a id="1204" href="Relation.Binary.Bundles.html#1009" class="Record">Setoid</a> <a id="1211" href="Function.Structures.html#386" class="Bound">b</a> <a id="1213" href="Function.Structures.html#391" class="Bound">ℓ₂</a>
<a id="1220" href="Function.Structures.html#1195" class="Function">setoid</a> <a id="1227" class="Symbol">=</a> <a id="1229" class="Keyword">record</a>
<a id="1242" class="Symbol">{</a> <a id="1244" href="Relation.Binary.Bundles.html#1132" class="Field">isEquivalence</a> <a id="1258" class="Symbol">=</a> <a id="1260" href="Function.Structures.html#990" class="Field">isEquivalence₂</a>
<a id="1281" class="Symbol">}</a>
<a id="1288" class="Keyword">open</a> <a id="1293" href="Relation.Binary.Bundles.html#1009" class="Module">Setoid</a> <a id="1300" href="Function.Structures.html#1195" class="Function">setoid</a> <a id="1307" class="Keyword">public</a>
<a id="1316" class="Keyword">record</a> <a id="IsInjection"></a><a id="1323" href="Function.Structures.html#1323" class="Record">IsInjection</a> <a id="1335" class="Symbol">(</a><a id="1336" href="Function.Structures.html#1336" class="Bound">f</a> <a id="1338" class="Symbol">:</a> <a id="1340" href="Function.Structures.html#398" class="Bound">A</a> <a id="1342" class="Symbol">→</a> <a id="1344" href="Function.Structures.html#458" class="Bound">B</a><a id="1345" class="Symbol">)</a> <a id="1347" class="Symbol">:</a> <a id="1349" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1353" class="Symbol">(</a><a id="1354" href="Function.Structures.html#384" class="Bound">a</a> <a id="1356" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1358" href="Function.Structures.html#386" class="Bound">b</a> <a id="1360" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1362" href="Function.Structures.html#388" class="Bound">ℓ₁</a> <a id="1365" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1367" href="Function.Structures.html#391" class="Bound">ℓ₂</a><a id="1369" class="Symbol">)</a> <a id="1371" class="Keyword">where</a>
<a id="1379" class="Keyword">field</a>
<a id="IsInjection.isCongruent"></a><a id="1389" href="Function.Structures.html#1389" class="Field">isCongruent</a> <a id="1401" class="Symbol">:</a> <a id="1403" href="Function.Structures.html#841" class="Record">IsCongruent</a> <a id="1415" href="Function.Structures.html#1336" class="Bound">f</a>
<a id="IsInjection.injective"></a><a id="1421" href="Function.Structures.html#1421" class="Field">injective</a> <a id="1433" class="Symbol">:</a> <a id="1435" href="Function.Definitions.html#889" class="Function">Injective</a> <a id="1445" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="1450" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="1455" href="Function.Structures.html#1336" class="Bound">f</a>
<a id="1460" class="Keyword">open</a> <a id="1465" href="Function.Structures.html#841" class="Module">IsCongruent</a> <a id="1477" href="Function.Structures.html#1389" class="Field">isCongruent</a> <a id="1489" class="Keyword">public</a>
<a id="1498" class="Keyword">record</a> <a id="IsSurjection"></a><a id="1505" href="Function.Structures.html#1505" class="Record">IsSurjection</a> <a id="1518" class="Symbol">(</a><a id="1519" href="Function.Structures.html#1519" class="Bound">f</a> <a id="1521" class="Symbol">:</a> <a id="1523" href="Function.Structures.html#398" class="Bound">A</a> <a id="1525" class="Symbol">→</a> <a id="1527" href="Function.Structures.html#458" class="Bound">B</a><a id="1528" class="Symbol">)</a> <a id="1530" class="Symbol">:</a> <a id="1532" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1536" class="Symbol">(</a><a id="1537" href="Function.Structures.html#384" class="Bound">a</a> <a id="1539" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1541" href="Function.Structures.html#386" class="Bound">b</a> <a id="1543" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1545" href="Function.Structures.html#388" class="Bound">ℓ₁</a> <a id="1548" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1550" href="Function.Structures.html#391" class="Bound">ℓ₂</a><a id="1552" class="Symbol">)</a> <a id="1554" class="Keyword">where</a>
<a id="1562" class="Keyword">field</a>
<a id="IsSurjection.isCongruent"></a><a id="1572" href="Function.Structures.html#1572" class="Field">isCongruent</a> <a id="1584" class="Symbol">:</a> <a id="1586" href="Function.Structures.html#841" class="Record">IsCongruent</a> <a id="1598" href="Function.Structures.html#1519" class="Bound">f</a>
<a id="IsSurjection.surjective"></a><a id="1604" href="Function.Structures.html#1604" class="Field">surjective</a> <a id="1616" class="Symbol">:</a> <a id="1618" href="Function.Definitions.Core2.html#663" class="Function">Surjective</a> <a id="1629" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="1634" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="1639" href="Function.Structures.html#1519" class="Bound">f</a>
<a id="1644" class="Keyword">open</a> <a id="1649" href="Function.Structures.html#841" class="Module">IsCongruent</a> <a id="1661" href="Function.Structures.html#1572" class="Field">isCongruent</a> <a id="1673" class="Keyword">public</a>
<a id="1682" class="Keyword">record</a> <a id="IsBijection"></a><a id="1689" href="Function.Structures.html#1689" class="Record">IsBijection</a> <a id="1701" class="Symbol">(</a><a id="1702" href="Function.Structures.html#1702" class="Bound">f</a> <a id="1704" class="Symbol">:</a> <a id="1706" href="Function.Structures.html#398" class="Bound">A</a> <a id="1708" class="Symbol">→</a> <a id="1710" href="Function.Structures.html#458" class="Bound">B</a><a id="1711" class="Symbol">)</a> <a id="1713" class="Symbol">:</a> <a id="1715" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1719" class="Symbol">(</a><a id="1720" href="Function.Structures.html#384" class="Bound">a</a> <a id="1722" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1724" href="Function.Structures.html#386" class="Bound">b</a> <a id="1726" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1728" href="Function.Structures.html#388" class="Bound">ℓ₁</a> <a id="1731" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1733" href="Function.Structures.html#391" class="Bound">ℓ₂</a><a id="1735" class="Symbol">)</a> <a id="1737" class="Keyword">where</a>
<a id="1745" class="Keyword">field</a>
<a id="IsBijection.isInjection"></a><a id="1755" href="Function.Structures.html#1755" class="Field">isInjection</a> <a id="1767" class="Symbol">:</a> <a id="1769" href="Function.Structures.html#1323" class="Record">IsInjection</a> <a id="1781" href="Function.Structures.html#1702" class="Bound">f</a>
<a id="IsBijection.surjective"></a><a id="1787" href="Function.Structures.html#1787" class="Field">surjective</a> <a id="1799" class="Symbol">:</a> <a id="1801" href="Function.Definitions.Core2.html#663" class="Function">Surjective</a> <a id="1812" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="1817" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="1822" href="Function.Structures.html#1702" class="Bound">f</a>
<a id="1827" class="Keyword">open</a> <a id="1832" href="Function.Structures.html#1323" class="Module">IsInjection</a> <a id="1844" href="Function.Structures.html#1755" class="Field">isInjection</a> <a id="1856" class="Keyword">public</a>
<a id="IsBijection.bijective"></a><a id="1866" href="Function.Structures.html#1866" class="Function">bijective</a> <a id="1876" class="Symbol">:</a> <a id="1878" href="Function.Definitions.html#1019" class="Function">Bijective</a> <a id="1888" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="1893" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="1898" href="Function.Structures.html#1702" class="Bound">f</a>
<a id="1902" href="Function.Structures.html#1866" class="Function">bijective</a> <a id="1912" class="Symbol">=</a> <a id="1914" href="Function.Structures.html#1421" class="Function">injective</a> <a id="1924" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="1926" href="Function.Structures.html#1787" class="Field">surjective</a>
<a id="IsBijection.isSurjection"></a><a id="1940" href="Function.Structures.html#1940" class="Function">isSurjection</a> <a id="1953" class="Symbol">:</a> <a id="1955" href="Function.Structures.html#1505" class="Record">IsSurjection</a> <a id="1968" href="Function.Structures.html#1702" class="Bound">f</a>
<a id="1972" href="Function.Structures.html#1940" class="Function">isSurjection</a> <a id="1985" class="Symbol">=</a> <a id="1987" class="Keyword">record</a>
<a id="1998" class="Symbol">{</a> <a id="2000" href="Function.Structures.html#1572" class="Field">isCongruent</a> <a id="2012" class="Symbol">=</a> <a id="2014" href="Function.Structures.html#1389" class="Function">isCongruent</a>
<a id="2030" class="Symbol">;</a> <a id="2032" href="Function.Structures.html#1604" class="Field">surjective</a> <a id="2044" class="Symbol">=</a> <a id="2046" href="Function.Structures.html#1787" class="Field">surjective</a>
<a id="2061" class="Symbol">}</a>
<a id="2065" class="Comment">------------------------------------------------------------------------</a>
<a id="2138" class="Comment">-- Two element structures</a>
<a id="2164" class="Comment">------------------------------------------------------------------------</a>
<a id="2238" class="Keyword">record</a> <a id="IsLeftInverse"></a><a id="2245" href="Function.Structures.html#2245" class="Record">IsLeftInverse</a> <a id="2259" class="Symbol">(</a><a id="2260" href="Function.Structures.html#2260" class="Bound">f</a> <a id="2262" class="Symbol">:</a> <a id="2264" href="Function.Structures.html#398" class="Bound">A</a> <a id="2266" class="Symbol">→</a> <a id="2268" href="Function.Structures.html#458" class="Bound">B</a><a id="2269" class="Symbol">)</a> <a id="2271" class="Symbol">(</a><a id="2272" href="Function.Structures.html#2272" class="Bound">g</a> <a id="2274" class="Symbol">:</a> <a id="2276" href="Function.Structures.html#458" class="Bound">B</a> <a id="2278" class="Symbol">→</a> <a id="2280" href="Function.Structures.html#398" class="Bound">A</a><a id="2281" class="Symbol">)</a> <a id="2283" class="Symbol">:</a> <a id="2285" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2289" class="Symbol">(</a><a id="2290" href="Function.Structures.html#384" class="Bound">a</a> <a id="2292" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2294" href="Function.Structures.html#386" class="Bound">b</a> <a id="2296" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2298" href="Function.Structures.html#388" class="Bound">ℓ₁</a> <a id="2301" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2303" href="Function.Structures.html#391" class="Bound">ℓ₂</a><a id="2305" class="Symbol">)</a> <a id="2307" class="Keyword">where</a>
<a id="2315" class="Keyword">field</a>
<a id="IsLeftInverse.isCongruent"></a><a id="2325" href="Function.Structures.html#2325" class="Field">isCongruent</a> <a id="2338" class="Symbol">:</a> <a id="2340" href="Function.Structures.html#841" class="Record">IsCongruent</a> <a id="2352" href="Function.Structures.html#2260" class="Bound">f</a>
<a id="IsLeftInverse.cong₂"></a><a id="2358" href="Function.Structures.html#2358" class="Field">cong₂</a> <a id="2371" class="Symbol">:</a> <a id="2373" href="Function.Definitions.html#803" class="Function">Congruent</a> <a id="2383" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="2388" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="2393" href="Function.Structures.html#2272" class="Bound">g</a>
<a id="IsLeftInverse.inverseˡ"></a><a id="2399" href="Function.Structures.html#2399" class="Field">inverseˡ</a> <a id="2412" class="Symbol">:</a> <a id="2414" href="Function.Definitions.Core2.html#818" class="Function">Inverseˡ</a> <a id="2423" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="2428" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="2433" href="Function.Structures.html#2260" class="Bound">f</a> <a id="2435" href="Function.Structures.html#2272" class="Bound">g</a>
<a id="2440" class="Keyword">open</a> <a id="2445" href="Function.Structures.html#841" class="Module">IsCongruent</a> <a id="2457" href="Function.Structures.html#2325" class="Field">isCongruent</a> <a id="2469" class="Keyword">public</a>
<a id="2480" class="Keyword">renaming</a> <a id="2489" class="Symbol">(</a><a id="2490" href="Function.Structures.html#907" class="Field">cong</a> <a id="2495" class="Symbol">to</a> <a id="2498" class="Field">cong₁</a><a id="2503" class="Symbol">)</a>
<a id="2507" class="Keyword">record</a> <a id="IsRightInverse"></a><a id="2514" href="Function.Structures.html#2514" class="Record">IsRightInverse</a> <a id="2529" class="Symbol">(</a><a id="2530" href="Function.Structures.html#2530" class="Bound">f</a> <a id="2532" class="Symbol">:</a> <a id="2534" href="Function.Structures.html#398" class="Bound">A</a> <a id="2536" class="Symbol">→</a> <a id="2538" href="Function.Structures.html#458" class="Bound">B</a><a id="2539" class="Symbol">)</a> <a id="2541" class="Symbol">(</a><a id="2542" href="Function.Structures.html#2542" class="Bound">g</a> <a id="2544" class="Symbol">:</a> <a id="2546" href="Function.Structures.html#458" class="Bound">B</a> <a id="2548" class="Symbol">→</a> <a id="2550" href="Function.Structures.html#398" class="Bound">A</a><a id="2551" class="Symbol">)</a> <a id="2553" class="Symbol">:</a> <a id="2555" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2559" class="Symbol">(</a><a id="2560" href="Function.Structures.html#384" class="Bound">a</a> <a id="2562" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2564" href="Function.Structures.html#386" class="Bound">b</a> <a id="2566" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2568" href="Function.Structures.html#388" class="Bound">ℓ₁</a> <a id="2571" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2573" href="Function.Structures.html#391" class="Bound">ℓ₂</a><a id="2575" class="Symbol">)</a> <a id="2577" class="Keyword">where</a>
<a id="2585" class="Keyword">field</a>
<a id="IsRightInverse.isCongruent"></a><a id="2595" href="Function.Structures.html#2595" class="Field">isCongruent</a> <a id="2607" class="Symbol">:</a> <a id="2609" href="Function.Structures.html#841" class="Record">IsCongruent</a> <a id="2621" href="Function.Structures.html#2530" class="Bound">f</a>
<a id="IsRightInverse.cong₂"></a><a id="2627" href="Function.Structures.html#2627" class="Field">cong₂</a> <a id="2639" class="Symbol">:</a> <a id="2641" href="Function.Definitions.html#803" class="Function">Congruent</a> <a id="2651" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="2656" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="2661" href="Function.Structures.html#2542" class="Bound">g</a>
<a id="IsRightInverse.inverseʳ"></a><a id="2667" href="Function.Structures.html#2667" class="Field">inverseʳ</a> <a id="2679" class="Symbol">:</a> <a id="2681" href="Function.Definitions.Core1.html#675" class="Function">Inverseʳ</a> <a id="2690" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="2695" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="2700" href="Function.Structures.html#2530" class="Bound">f</a> <a id="2702" href="Function.Structures.html#2542" class="Bound">g</a>
<a id="2707" class="Keyword">open</a> <a id="2712" href="Function.Structures.html#841" class="Module">IsCongruent</a> <a id="2724" href="Function.Structures.html#2595" class="Field">isCongruent</a> <a id="2736" class="Keyword">public</a>
<a id="2747" class="Keyword">renaming</a> <a id="2756" class="Symbol">(</a><a id="2757" href="Function.Structures.html#907" class="Field">cong</a> <a id="2762" class="Symbol">to</a> <a id="2765" class="Field">cong₁</a><a id="2770" class="Symbol">)</a>
<a id="2774" class="Keyword">record</a> <a id="IsInverse"></a><a id="2781" href="Function.Structures.html#2781" class="Record">IsInverse</a> <a id="2791" class="Symbol">(</a><a id="2792" href="Function.Structures.html#2792" class="Bound">f</a> <a id="2794" class="Symbol">:</a> <a id="2796" href="Function.Structures.html#398" class="Bound">A</a> <a id="2798" class="Symbol">→</a> <a id="2800" href="Function.Structures.html#458" class="Bound">B</a><a id="2801" class="Symbol">)</a> <a id="2803" class="Symbol">(</a><a id="2804" href="Function.Structures.html#2804" class="Bound">g</a> <a id="2806" class="Symbol">:</a> <a id="2808" href="Function.Structures.html#458" class="Bound">B</a> <a id="2810" class="Symbol">→</a> <a id="2812" href="Function.Structures.html#398" class="Bound">A</a><a id="2813" class="Symbol">)</a> <a id="2815" class="Symbol">:</a> <a id="2817" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="2821" class="Symbol">(</a><a id="2822" href="Function.Structures.html#384" class="Bound">a</a> <a id="2824" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2826" href="Function.Structures.html#386" class="Bound">b</a> <a id="2828" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2830" href="Function.Structures.html#388" class="Bound">ℓ₁</a> <a id="2833" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="2835" href="Function.Structures.html#391" class="Bound">ℓ₂</a><a id="2837" class="Symbol">)</a> <a id="2839" class="Keyword">where</a>
<a id="2847" class="Keyword">field</a>
<a id="IsInverse.isLeftInverse"></a><a id="2857" href="Function.Structures.html#2857" class="Field">isLeftInverse</a> <a id="2871" class="Symbol">:</a> <a id="2873" href="Function.Structures.html#2245" class="Record">IsLeftInverse</a> <a id="2887" href="Function.Structures.html#2792" class="Bound">f</a> <a id="2889" href="Function.Structures.html#2804" class="Bound">g</a>
<a id="IsInverse.inverseʳ"></a><a id="2895" href="Function.Structures.html#2895" class="Field">inverseʳ</a> <a id="2909" class="Symbol">:</a> <a id="2911" href="Function.Definitions.Core1.html#675" class="Function">Inverseʳ</a> <a id="2920" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="2925" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="2930" href="Function.Structures.html#2792" class="Bound">f</a> <a id="2932" href="Function.Structures.html#2804" class="Bound">g</a>
<a id="2937" class="Keyword">open</a> <a id="2942" href="Function.Structures.html#2245" class="Module">IsLeftInverse</a> <a id="2956" href="Function.Structures.html#2857" class="Field">isLeftInverse</a> <a id="2970" class="Keyword">public</a>
<a id="IsInverse.isRightInverse"></a><a id="2980" href="Function.Structures.html#2980" class="Function">isRightInverse</a> <a id="2995" class="Symbol">:</a> <a id="2997" href="Function.Structures.html#2514" class="Record">IsRightInverse</a> <a id="3012" href="Function.Structures.html#2792" class="Bound">f</a> <a id="3014" href="Function.Structures.html#2804" class="Bound">g</a>
<a id="3018" href="Function.Structures.html#2980" class="Function">isRightInverse</a> <a id="3033" class="Symbol">=</a> <a id="3035" class="Keyword">record</a>
<a id="3046" class="Symbol">{</a> <a id="3048" href="Function.Structures.html#2595" class="Field">isCongruent</a> <a id="3060" class="Symbol">=</a> <a id="3062" href="Function.Structures.html#2325" class="Function">isCongruent</a>
<a id="3078" class="Symbol">;</a> <a id="3080" href="Function.Structures.html#2627" class="Field">cong₂</a> <a id="3092" class="Symbol">=</a> <a id="3094" href="Function.Structures.html#2358" class="Function">cong₂</a>
<a id="3104" class="Symbol">;</a> <a id="3106" href="Function.Structures.html#2667" class="Field">inverseʳ</a> <a id="3118" class="Symbol">=</a> <a id="3120" href="Function.Structures.html#2895" class="Field">inverseʳ</a>
<a id="3133" class="Symbol">}</a>
<a id="IsInverse.inverse"></a><a id="3138" href="Function.Structures.html#3138" class="Function">inverse</a> <a id="3146" class="Symbol">:</a> <a id="3148" href="Function.Definitions.html#1191" class="Function">Inverseᵇ</a> <a id="3157" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="3162" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="3167" href="Function.Structures.html#2792" class="Bound">f</a> <a id="3169" href="Function.Structures.html#2804" class="Bound">g</a>
<a id="3173" href="Function.Structures.html#3138" class="Function">inverse</a> <a id="3181" class="Symbol">=</a> <a id="3183" href="Function.Structures.html#2399" class="Function">inverseˡ</a> <a id="3192" href="Agda.Builtin.Sigma.html#236" class="InductiveConstructor Operator">,</a> <a id="3194" href="Function.Structures.html#2895" class="Field">inverseʳ</a>
<a id="3205" class="Comment">------------------------------------------------------------------------</a>
<a id="3278" class="Comment">-- Three element structures</a>
<a id="3306" class="Comment">------------------------------------------------------------------------</a>
<a id="3380" class="Keyword">record</a> <a id="IsBiEquivalence"></a><a id="3387" href="Function.Structures.html#3387" class="Record">IsBiEquivalence</a>
<a id="3405" class="Symbol">(</a><a id="3406" href="Function.Structures.html#3406" class="Bound">f</a> <a id="3408" class="Symbol">:</a> <a id="3410" href="Function.Structures.html#398" class="Bound">A</a> <a id="3412" class="Symbol">→</a> <a id="3414" href="Function.Structures.html#458" class="Bound">B</a><a id="3415" class="Symbol">)</a> <a id="3417" class="Symbol">(</a><a id="3418" href="Function.Structures.html#3418" class="Bound">g₁</a> <a id="3421" class="Symbol">:</a> <a id="3423" href="Function.Structures.html#458" class="Bound">B</a> <a id="3425" class="Symbol">→</a> <a id="3427" href="Function.Structures.html#398" class="Bound">A</a><a id="3428" class="Symbol">)</a> <a id="3430" class="Symbol">(</a><a id="3431" href="Function.Structures.html#3431" class="Bound">g₂</a> <a id="3434" class="Symbol">:</a> <a id="3436" href="Function.Structures.html#458" class="Bound">B</a> <a id="3438" class="Symbol">→</a> <a id="3440" href="Function.Structures.html#398" class="Bound">A</a><a id="3441" class="Symbol">)</a> <a id="3443" class="Symbol">:</a> <a id="3445" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3449" class="Symbol">(</a><a id="3450" href="Function.Structures.html#384" class="Bound">a</a> <a id="3452" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3454" href="Function.Structures.html#386" class="Bound">b</a> <a id="3456" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3458" href="Function.Structures.html#388" class="Bound">ℓ₁</a> <a id="3461" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3463" href="Function.Structures.html#391" class="Bound">ℓ₂</a><a id="3465" class="Symbol">)</a> <a id="3467" class="Keyword">where</a>
<a id="3475" class="Keyword">field</a>
<a id="IsBiEquivalence.f-isCongruent"></a><a id="3485" href="Function.Structures.html#3485" class="Field">f-isCongruent</a> <a id="3499" class="Symbol">:</a> <a id="3501" href="Function.Structures.html#841" class="Record">IsCongruent</a> <a id="3513" href="Function.Structures.html#3406" class="Bound">f</a>
<a id="IsBiEquivalence.cong₂"></a><a id="3519" href="Function.Structures.html#3519" class="Field">cong₂</a> <a id="3533" class="Symbol">:</a> <a id="3535" href="Function.Definitions.html#803" class="Function">Congruent</a> <a id="3545" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="3550" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="3555" href="Function.Structures.html#3418" class="Bound">g₁</a>
<a id="IsBiEquivalence.cong₃"></a><a id="3562" href="Function.Structures.html#3562" class="Field">cong₃</a> <a id="3576" class="Symbol">:</a> <a id="3578" href="Function.Definitions.html#803" class="Function">Congruent</a> <a id="3588" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="3593" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="3598" href="Function.Structures.html#3431" class="Bound">g₂</a>
<a id="3604" class="Keyword">open</a> <a id="3609" href="Function.Structures.html#841" class="Module">IsCongruent</a> <a id="3621" href="Function.Structures.html#3485" class="Field">f-isCongruent</a> <a id="3635" class="Keyword">public</a>
<a id="3646" class="Keyword">renaming</a> <a id="3655" class="Symbol">(</a><a id="3656" href="Function.Structures.html#907" class="Field">cong</a> <a id="3661" class="Symbol">to</a> <a id="3664" class="Field">cong₁</a><a id="3669" class="Symbol">)</a>
<a id="3673" class="Keyword">record</a> <a id="IsBiInverse"></a><a id="3680" href="Function.Structures.html#3680" class="Record">IsBiInverse</a>
<a id="3694" class="Symbol">(</a><a id="3695" href="Function.Structures.html#3695" class="Bound">f</a> <a id="3697" class="Symbol">:</a> <a id="3699" href="Function.Structures.html#398" class="Bound">A</a> <a id="3701" class="Symbol">→</a> <a id="3703" href="Function.Structures.html#458" class="Bound">B</a><a id="3704" class="Symbol">)</a> <a id="3706" class="Symbol">(</a><a id="3707" href="Function.Structures.html#3707" class="Bound">g₁</a> <a id="3710" class="Symbol">:</a> <a id="3712" href="Function.Structures.html#458" class="Bound">B</a> <a id="3714" class="Symbol">→</a> <a id="3716" href="Function.Structures.html#398" class="Bound">A</a><a id="3717" class="Symbol">)</a> <a id="3719" class="Symbol">(</a><a id="3720" href="Function.Structures.html#3720" class="Bound">g₂</a> <a id="3723" class="Symbol">:</a> <a id="3725" href="Function.Structures.html#458" class="Bound">B</a> <a id="3727" class="Symbol">→</a> <a id="3729" href="Function.Structures.html#398" class="Bound">A</a><a id="3730" class="Symbol">)</a> <a id="3732" class="Symbol">:</a> <a id="3734" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="3738" class="Symbol">(</a><a id="3739" href="Function.Structures.html#384" class="Bound">a</a> <a id="3741" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3743" href="Function.Structures.html#386" class="Bound">b</a> <a id="3745" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3747" href="Function.Structures.html#388" class="Bound">ℓ₁</a> <a id="3750" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="3752" href="Function.Structures.html#391" class="Bound">ℓ₂</a><a id="3754" class="Symbol">)</a> <a id="3756" class="Keyword">where</a>
<a id="3764" class="Keyword">field</a>
<a id="IsBiInverse.f-isCongruent"></a><a id="3774" href="Function.Structures.html#3774" class="Field">f-isCongruent</a> <a id="3788" class="Symbol">:</a> <a id="3790" href="Function.Structures.html#841" class="Record">IsCongruent</a> <a id="3802" href="Function.Structures.html#3695" class="Bound">f</a>
<a id="IsBiInverse.cong₂"></a><a id="3808" href="Function.Structures.html#3808" class="Field">cong₂</a> <a id="3822" class="Symbol">:</a> <a id="3824" href="Function.Definitions.html#803" class="Function">Congruent</a> <a id="3834" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="3839" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="3844" href="Function.Structures.html#3707" class="Bound">g₁</a>
<a id="IsBiInverse.inverseˡ"></a><a id="3851" href="Function.Structures.html#3851" class="Field">inverseˡ</a> <a id="3865" class="Symbol">:</a> <a id="3867" href="Function.Definitions.Core2.html#818" class="Function">Inverseˡ</a> <a id="3876" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="3881" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="3886" href="Function.Structures.html#3695" class="Bound">f</a> <a id="3888" href="Function.Structures.html#3707" class="Bound">g₁</a>
<a id="IsBiInverse.cong₃"></a><a id="3895" href="Function.Structures.html#3895" class="Field">cong₃</a> <a id="3909" class="Symbol">:</a> <a id="3911" href="Function.Definitions.html#803" class="Function">Congruent</a> <a id="3921" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="3926" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="3931" href="Function.Structures.html#3720" class="Bound">g₂</a>
<a id="IsBiInverse.inverseʳ"></a><a id="3938" href="Function.Structures.html#3938" class="Field">inverseʳ</a> <a id="3952" class="Symbol">:</a> <a id="3954" href="Function.Definitions.Core1.html#675" class="Function">Inverseʳ</a> <a id="3963" href="Function.Structures.html#410" class="Bound Operator">_≈₁_</a> <a id="3968" href="Function.Structures.html#470" class="Bound Operator">_≈₂_</a> <a id="3973" href="Function.Structures.html#3695" class="Bound">f</a> <a id="3975" href="Function.Structures.html#3720" class="Bound">g₂</a>
<a id="3981" class="Keyword">open</a> <a id="3986" href="Function.Structures.html#841" class="Module">IsCongruent</a> <a id="3998" href="Function.Structures.html#3774" class="Field">f-isCongruent</a> <a id="4012" class="Keyword">public</a>
<a id="4023" class="Keyword">renaming</a> <a id="4032" class="Symbol">(</a><a id="4033" href="Function.Structures.html#907" class="Field">cong</a> <a id="4038" class="Symbol">to</a> <a id="4041" class="Field">cong₁</a><a id="4046" class="Symbol">)</a>
</pre></body></html>
Reference in New Issue Copy Permalink