/usr/share/doc/agda-stdlib-doc/html/Function.LeftInverse.html is in agda-stdlib-doc 0.14-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 | <!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Function.LeftInverse</title><link rel="stylesheet" href="Agda.css"></head><body><pre><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">-- Left inverses</a>
<a id="123" class="Comment">------------------------------------------------------------------------</a>
<a id="197" class="Keyword">module</a> <a id="204" href="Function.LeftInverse.html" class="Module">Function.LeftInverse</a> <a id="225" class="Keyword">where</a>
<a id="232" class="Keyword">open</a> <a id="237" class="Keyword">import</a> <a id="244" href="Data.Product.html" class="Module">Data.Product</a>
<a id="257" class="Keyword">open</a> <a id="262" class="Keyword">import</a> <a id="269" href="Level.html" class="Module">Level</a>
<a id="275" class="Keyword">import</a> <a id="282" href="Relation.Binary.EqReasoning.html" class="Module">Relation.Binary.EqReasoning</a> <a id="310" class="Symbol">as</a> <a id="313" class="Module">EqReasoning</a>
<a id="325" class="Keyword">open</a> <a id="330" class="Keyword">import</a> <a id="337" href="Relation.Binary.html" class="Module">Relation.Binary</a>
<a id="353" class="Keyword">open</a> <a id="358" class="Keyword">import</a> <a id="365" href="Function.Equality.html" class="Module">Function.Equality</a> <a id="383" class="Symbol">as</a> <a id="386" class="Module">Eq</a>
<a id="391" class="Keyword">using</a> <a id="397" class="Symbol">(</a><a id="398" href="Function.Equality.html#_%E2%9F%B6_" class="Function Operator">_⟶_</a><a id="401" class="Symbol">;</a> <a id="403" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">_⟨$⟩_</a><a id="408" class="Symbol">)</a> <a id="410" class="Keyword">renaming</a> <a id="419" class="Symbol">(</a><a id="420" href="Function.Equality.html#_%E2%88%98_" class="Function Operator">_∘_</a> <a id="424" class="Symbol">to</a> <a id="427" href="Function.Equality.html#_%E2%88%98_" class="Function Operator">_⟪∘⟫_</a><a id="432" class="Symbol">)</a>
<a id="434" class="Keyword">open</a> <a id="439" class="Keyword">import</a> <a id="446" href="Function.Equivalence.html" class="Module">Function.Equivalence</a> <a id="467" class="Keyword">using</a> <a id="473" class="Symbol">(</a><a id="474" href="Function.Equivalence.html#Equivalence" class="Record">Equivalence</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="Function.Injection.html" class="Module">Function.Injection</a> <a id="518" class="Keyword">using</a> <a id="524" class="Symbol">(</a><a id="525" href="Function.Injection.html#Injective" class="Function">Injective</a><a id="534" class="Symbol">;</a> <a id="536" href="Function.Injection.html#Injection" class="Record">Injection</a><a id="545" class="Symbol">)</a>
<a id="547" class="Keyword">import</a> <a id="554" href="Relation.Binary.PropositionalEquality.html" class="Module">Relation.Binary.PropositionalEquality</a> <a id="592" class="Symbol">as</a> <a id="595" class="Module">P</a>
<a id="598" class="Comment">-- Left and right inverses.</a>
<a id="_LeftInverseOf_" href="Function.LeftInverse.html#_LeftInverseOf_" class="Function Operator">_LeftInverseOf_</a> <a id="643" class="Symbol">:</a>
<a id="647" class="Symbol">∀</a> <a id="649" class="Symbol">{</a><a id="650" href="Function.LeftInverse.html#650" class="Bound">f₁</a> <a id="653" href="Function.LeftInverse.html#653" class="Bound">f₂</a> <a id="656" href="Function.LeftInverse.html#656" class="Bound">t₁</a> <a id="659" href="Function.LeftInverse.html#659" class="Bound">t₂</a><a id="661" class="Symbol">}</a> <a id="663" class="Symbol">{</a><a id="664" href="Function.LeftInverse.html#664" class="Bound">From</a> <a id="669" class="Symbol">:</a> <a id="671" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="678" href="Function.LeftInverse.html#650" class="Bound">f₁</a> <a id="681" href="Function.LeftInverse.html#653" class="Bound">f₂</a><a id="683" class="Symbol">}</a> <a id="685" class="Symbol">{</a><a id="686" href="Function.LeftInverse.html#686" class="Bound">To</a> <a id="689" class="Symbol">:</a> <a id="691" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="698" href="Function.LeftInverse.html#656" class="Bound">t₁</a> <a id="701" href="Function.LeftInverse.html#659" class="Bound">t₂</a><a id="703" class="Symbol">}</a> <a id="705" class="Symbol">→</a>
<a id="709" href="Function.LeftInverse.html#686" class="Bound">To</a> <a id="712" href="Function.Equality.html#_%E2%9F%B6_" class="Function Operator">⟶</a> <a id="714" href="Function.LeftInverse.html#664" class="Bound">From</a> <a id="719" class="Symbol">→</a> <a id="721" href="Function.LeftInverse.html#664" class="Bound">From</a> <a id="726" href="Function.Equality.html#_%E2%9F%B6_" class="Function Operator">⟶</a> <a id="728" href="Function.LeftInverse.html#686" class="Bound">To</a> <a id="731" class="Symbol">→</a> <a id="733" class="PrimitiveType">Set</a> <a id="737" class="Symbol">_</a>
<a id="739" href="Function.LeftInverse.html#_LeftInverseOf_" class="Function Operator">_LeftInverseOf_</a> <a id="755" class="Symbol">{</a><a id="756" class="Argument">From</a> <a id="761" class="Symbol">=</a> <a id="763" href="Function.LeftInverse.html#763" class="Bound">From</a><a id="767" class="Symbol">}</a> <a id="769" href="Function.LeftInverse.html#769" class="Bound">f</a> <a id="771" href="Function.LeftInverse.html#771" class="Bound">g</a> <a id="773" class="Symbol">=</a> <a id="775" class="Symbol">∀</a> <a id="777" href="Function.LeftInverse.html#777" class="Bound">x</a> <a id="779" class="Symbol">→</a> <a id="781" href="Function.LeftInverse.html#769" class="Bound">f</a> <a id="783" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="787" class="Symbol">(</a><a id="788" href="Function.LeftInverse.html#771" class="Bound">g</a> <a id="790" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="794" href="Function.LeftInverse.html#777" class="Bound">x</a><a id="795" class="Symbol">)</a> <a id="797" href="Relation.Binary.html#1997" class="Function Operator">≈</a> <a id="799" href="Function.LeftInverse.html#777" class="Bound">x</a>
<a id="803" class="Keyword">where</a> <a id="809" class="Keyword">open</a> <a id="814" href="Relation.Binary.html#Setoid" class="Module">Setoid</a> <a id="821" href="Function.LeftInverse.html#763" class="Bound">From</a>
<a id="_RightInverseOf_" href="Function.LeftInverse.html#_RightInverseOf_" class="Function Operator">_RightInverseOf_</a> <a id="844" class="Symbol">:</a>
<a id="848" class="Symbol">∀</a> <a id="850" class="Symbol">{</a><a id="851" href="Function.LeftInverse.html#851" class="Bound">f₁</a> <a id="854" href="Function.LeftInverse.html#854" class="Bound">f₂</a> <a id="857" href="Function.LeftInverse.html#857" class="Bound">t₁</a> <a id="860" href="Function.LeftInverse.html#860" class="Bound">t₂</a><a id="862" class="Symbol">}</a> <a id="864" class="Symbol">{</a><a id="865" href="Function.LeftInverse.html#865" class="Bound">From</a> <a id="870" class="Symbol">:</a> <a id="872" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="879" href="Function.LeftInverse.html#851" class="Bound">f₁</a> <a id="882" href="Function.LeftInverse.html#854" class="Bound">f₂</a><a id="884" class="Symbol">}</a> <a id="886" class="Symbol">{</a><a id="887" href="Function.LeftInverse.html#887" class="Bound">To</a> <a id="890" class="Symbol">:</a> <a id="892" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="899" href="Function.LeftInverse.html#857" class="Bound">t₁</a> <a id="902" href="Function.LeftInverse.html#860" class="Bound">t₂</a><a id="904" class="Symbol">}</a> <a id="906" class="Symbol">→</a>
<a id="910" href="Function.LeftInverse.html#887" class="Bound">To</a> <a id="913" href="Function.Equality.html#_%E2%9F%B6_" class="Function Operator">⟶</a> <a id="915" href="Function.LeftInverse.html#865" class="Bound">From</a> <a id="920" class="Symbol">→</a> <a id="922" href="Function.LeftInverse.html#865" class="Bound">From</a> <a id="927" href="Function.Equality.html#_%E2%9F%B6_" class="Function Operator">⟶</a> <a id="929" href="Function.LeftInverse.html#887" class="Bound">To</a> <a id="932" class="Symbol">→</a> <a id="934" class="PrimitiveType">Set</a> <a id="938" class="Symbol">_</a>
<a id="940" href="Function.LeftInverse.html#940" class="Bound">f</a> <a id="942" href="Function.LeftInverse.html#_RightInverseOf_" class="Function Operator">RightInverseOf</a> <a id="957" href="Function.LeftInverse.html#957" class="Bound">g</a> <a id="959" class="Symbol">=</a> <a id="961" href="Function.LeftInverse.html#957" class="Bound">g</a> <a id="963" href="Function.LeftInverse.html#_LeftInverseOf_" class="Function Operator">LeftInverseOf</a> <a id="977" href="Function.LeftInverse.html#940" class="Bound">f</a>
<a id="980" class="Comment">-- The set of all left inverses between two setoids.</a>
<a id="1034" class="Keyword">record</a> <a id="LeftInverse" href="Function.LeftInverse.html#LeftInverse" class="Record">LeftInverse</a> <a id="1053" class="Symbol">{</a><a id="1054" href="Function.LeftInverse.html#1054" class="Bound">f₁</a> <a id="1057" href="Function.LeftInverse.html#1057" class="Bound">f₂</a> <a id="1060" href="Function.LeftInverse.html#1060" class="Bound">t₁</a> <a id="1063" href="Function.LeftInverse.html#1063" class="Bound">t₂</a><a id="1065" class="Symbol">}</a>
<a id="1086" class="Symbol">(</a><a id="1087" href="Function.LeftInverse.html#1087" class="Bound">From</a> <a id="1092" class="Symbol">:</a> <a id="1094" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="1101" href="Function.LeftInverse.html#1054" class="Bound">f₁</a> <a id="1104" href="Function.LeftInverse.html#1057" class="Bound">f₂</a><a id="1106" class="Symbol">)</a> <a id="1108" class="Symbol">(</a><a id="1109" href="Function.LeftInverse.html#1109" class="Bound">To</a> <a id="1112" class="Symbol">:</a> <a id="1114" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="1121" href="Function.LeftInverse.html#1060" class="Bound">t₁</a> <a id="1124" href="Function.LeftInverse.html#1063" class="Bound">t₂</a><a id="1126" class="Symbol">)</a> <a id="1128" class="Symbol">:</a>
<a id="1149" class="PrimitiveType">Set</a> <a id="1153" class="Symbol">(</a><a id="1154" href="Function.LeftInverse.html#1054" class="Bound">f₁</a> <a id="1157" href="Agda.Primitive.html#_%E2%8A%94_" class="Primitive Operator">⊔</a> <a id="1159" href="Function.LeftInverse.html#1057" class="Bound">f₂</a> <a id="1162" href="Agda.Primitive.html#_%E2%8A%94_" class="Primitive Operator">⊔</a> <a id="1164" href="Function.LeftInverse.html#1060" class="Bound">t₁</a> <a id="1167" href="Agda.Primitive.html#_%E2%8A%94_" class="Primitive Operator">⊔</a> <a id="1169" href="Function.LeftInverse.html#1063" class="Bound">t₂</a><a id="1171" class="Symbol">)</a> <a id="1173" class="Keyword">where</a>
<a id="1181" class="Keyword">field</a>
<a id="LeftInverse.to" href="Function.LeftInverse.html#LeftInverse.to" class="Field">to</a> <a id="1207" class="Symbol">:</a> <a id="1209" href="Function.LeftInverse.html#1087" class="Bound">From</a> <a id="1214" href="Function.Equality.html#_%E2%9F%B6_" class="Function Operator">⟶</a> <a id="1216" href="Function.LeftInverse.html#1109" class="Bound">To</a>
<a id="LeftInverse.from" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a> <a id="1239" class="Symbol">:</a> <a id="1241" href="Function.LeftInverse.html#1109" class="Bound">To</a> <a id="1244" href="Function.Equality.html#_%E2%9F%B6_" class="Function Operator">⟶</a> <a id="1246" href="Function.LeftInverse.html#1087" class="Bound">From</a>
<a id="LeftInverse.left-inverse-of" href="Function.LeftInverse.html#LeftInverse.left-inverse-of" class="Field">left-inverse-of</a> <a id="1271" class="Symbol">:</a> <a id="1273" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a> <a id="1278" href="Function.LeftInverse.html#_LeftInverseOf_" class="Function Operator">LeftInverseOf</a> <a id="1292" href="Function.LeftInverse.html#LeftInverse.to" class="Field">to</a>
<a id="1298" class="Keyword">private</a>
<a id="1310" class="Keyword">open</a> <a id="1315" class="Keyword">module</a> <a id="F" href="Function.LeftInverse.html#F" class="Module">F</a> <a id="1324" class="Symbol">=</a> <a id="1326" href="Relation.Binary.html#Setoid" class="Module">Setoid</a> <a id="1333" href="Function.LeftInverse.html#1087" class="Bound">From</a>
<a id="1342" class="Keyword">open</a> <a id="1347" class="Keyword">module</a> <a id="T" href="Function.LeftInverse.html#T" class="Module">T</a> <a id="1356" class="Symbol">=</a> <a id="1358" href="Relation.Binary.html#Setoid" class="Module">Setoid</a> <a id="1365" href="Function.LeftInverse.html#1109" class="Bound">To</a>
<a id="1370" class="Keyword">open</a> <a id="1375" href="Relation.Binary.EqReasoning.html" class="Module">EqReasoning</a> <a id="1387" href="Function.LeftInverse.html#1087" class="Bound">From</a>
<a id="LeftInverse.injective" href="Function.LeftInverse.html#LeftInverse.injective" class="Function">injective</a> <a id="1405" class="Symbol">:</a> <a id="1407" href="Function.Injection.html#Injective" class="Function">Injective</a> <a id="1417" href="Function.LeftInverse.html#LeftInverse.to" class="Field">to</a>
<a id="1422" href="Function.LeftInverse.html#LeftInverse.injective" class="Function">injective</a> <a id="1432" class="Symbol">{</a><a id="1433" href="Function.LeftInverse.html#1433" class="Bound">x</a><a id="1434" class="Symbol">}</a> <a id="1436" class="Symbol">{</a><a id="1437" href="Function.LeftInverse.html#1437" class="Bound">y</a><a id="1438" class="Symbol">}</a> <a id="1440" href="Function.LeftInverse.html#1440" class="Bound">eq</a> <a id="1443" class="Symbol">=</a> <a id="1445" href="Relation.Binary.PreorderReasoning.html#1154" class="Function Operator">begin</a>
<a id="1455" href="Function.LeftInverse.html#1433" class="Bound">x</a> <a id="1476" href="Relation.Binary.PreorderReasoning.html#1220" class="Function Operator">≈⟨</a> <a id="1479" href="Relation.Binary.Core.html#F.sym" class="Function">F.sym</a> <a id="1485" class="Symbol">(</a><a id="1486" href="Function.LeftInverse.html#LeftInverse.left-inverse-of" class="Field">left-inverse-of</a> <a id="1502" href="Function.LeftInverse.html#1433" class="Bound">x</a><a id="1503" class="Symbol">)</a> <a id="1505" href="Relation.Binary.PreorderReasoning.html#1220" class="Function Operator">⟩</a>
<a id="1511" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a> <a id="1516" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="1520" class="Symbol">(</a><a id="1521" href="Function.LeftInverse.html#LeftInverse.to" class="Field">to</a> <a id="1524" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="1528" href="Function.LeftInverse.html#1433" class="Bound">x</a><a id="1529" class="Symbol">)</a> <a id="1532" href="Relation.Binary.PreorderReasoning.html#1220" class="Function Operator">≈⟨</a> <a id="1535" href="Function.Equality.html#%CE%A0.cong" class="Field">Eq.cong</a> <a id="1543" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a> <a id="1548" href="Function.LeftInverse.html#1440" class="Bound">eq</a> <a id="1551" href="Relation.Binary.PreorderReasoning.html#1220" class="Function Operator">⟩</a>
<a id="1557" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a> <a id="1562" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="1566" class="Symbol">(</a><a id="1567" href="Function.LeftInverse.html#LeftInverse.to" class="Field">to</a> <a id="1570" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="1574" href="Function.LeftInverse.html#1437" class="Bound">y</a><a id="1575" class="Symbol">)</a> <a id="1578" href="Relation.Binary.PreorderReasoning.html#1220" class="Function Operator">≈⟨</a> <a id="1581" href="Function.LeftInverse.html#LeftInverse.left-inverse-of" class="Field">left-inverse-of</a> <a id="1597" href="Function.LeftInverse.html#1437" class="Bound">y</a> <a id="1599" href="Relation.Binary.PreorderReasoning.html#1220" class="Function Operator">⟩</a>
<a id="1605" href="Function.LeftInverse.html#1437" class="Bound">y</a> <a id="1626" href="Relation.Binary.PreorderReasoning.html#1519" class="Function Operator">∎</a>
<a id="LeftInverse.injection" href="Function.LeftInverse.html#LeftInverse.injection" class="Function">injection</a> <a id="1641" class="Symbol">:</a> <a id="1643" href="Function.Injection.html#Injection" class="Record">Injection</a> <a id="1653" href="Function.LeftInverse.html#1087" class="Bound">From</a> <a id="1658" href="Function.LeftInverse.html#1109" class="Bound">To</a>
<a id="1663" href="Function.LeftInverse.html#LeftInverse.injection" class="Function">injection</a> <a id="1673" class="Symbol">=</a> <a id="1675" class="Keyword">record</a> <a id="1682" class="Symbol">{</a> <a id="1684" class="Field">to</a> <a id="1687" class="Symbol">=</a> <a id="1689" href="Function.LeftInverse.html#LeftInverse.to" class="Field">to</a><a id="1691" class="Symbol">;</a> <a id="1693" class="Field">injective</a> <a id="1703" class="Symbol">=</a> <a id="1705" href="Function.LeftInverse.html#LeftInverse.injective" class="Function">injective</a> <a id="1715" class="Symbol">}</a>
<a id="LeftInverse.equivalence" href="Function.LeftInverse.html#LeftInverse.equivalence" class="Function">equivalence</a> <a id="1732" class="Symbol">:</a> <a id="1734" href="Function.Equivalence.html#Equivalence" class="Record">Equivalence</a> <a id="1746" href="Function.LeftInverse.html#1087" class="Bound">From</a> <a id="1751" href="Function.LeftInverse.html#1109" class="Bound">To</a>
<a id="1756" href="Function.LeftInverse.html#LeftInverse.equivalence" class="Function">equivalence</a> <a id="1768" class="Symbol">=</a> <a id="1770" class="Keyword">record</a>
<a id="1781" class="Symbol">{</a> <a id="1783" class="Field">to</a> <a id="1788" class="Symbol">=</a> <a id="1790" href="Function.LeftInverse.html#LeftInverse.to" class="Field">to</a>
<a id="1797" class="Symbol">;</a> <a id="1799" class="Field">from</a> <a id="1804" class="Symbol">=</a> <a id="1806" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a>
<a id="1815" class="Symbol">}</a>
<a id="LeftInverse.to-from" href="Function.LeftInverse.html#LeftInverse.to-from" class="Function">to-from</a> <a id="1828" class="Symbol">:</a> <a id="1830" class="Symbol">∀</a> <a id="1832" class="Symbol">{</a><a id="1833" href="Function.LeftInverse.html#1833" class="Bound">x</a> <a id="1835" href="Function.LeftInverse.html#1835" class="Bound">y</a><a id="1836" class="Symbol">}</a> <a id="1838" class="Symbol">→</a> <a id="1840" href="Function.LeftInverse.html#LeftInverse.to" class="Field">to</a> <a id="1843" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="1847" href="Function.LeftInverse.html#1833" class="Bound">x</a> <a id="1849" href="Relation.Binary.html#LeftInverse.T._%E2%89%88_" class="Function Operator">T.≈</a> <a id="1853" href="Function.LeftInverse.html#1835" class="Bound">y</a> <a id="1855" class="Symbol">→</a> <a id="1857" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a> <a id="1862" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="1866" href="Function.LeftInverse.html#1835" class="Bound">y</a> <a id="1868" href="Relation.Binary.html#LeftInverse.F._%E2%89%88_" class="Function Operator">F.≈</a> <a id="1872" href="Function.LeftInverse.html#1833" class="Bound">x</a>
<a id="1876" href="Function.LeftInverse.html#LeftInverse.to-from" class="Function">to-from</a> <a id="1884" class="Symbol">{</a><a id="1885" href="Function.LeftInverse.html#1885" class="Bound">x</a><a id="1886" class="Symbol">}</a> <a id="1888" class="Symbol">{</a><a id="1889" href="Function.LeftInverse.html#1889" class="Bound">y</a><a id="1890" class="Symbol">}</a> <a id="1892" href="Function.LeftInverse.html#1892" class="Bound">to-x≈y</a> <a id="1899" class="Symbol">=</a> <a id="1901" href="Relation.Binary.PreorderReasoning.html#1154" class="Function Operator">begin</a>
<a id="1911" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a> <a id="1916" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="1920" href="Function.LeftInverse.html#1889" class="Bound">y</a> <a id="1932" href="Relation.Binary.PreorderReasoning.html#1220" class="Function Operator">≈⟨</a> <a id="1935" href="Function.Equality.html#%CE%A0.cong" class="Field">Eq.cong</a> <a id="1943" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a> <a id="1948" class="Symbol">(</a><a id="1949" href="Relation.Binary.Core.html#T.sym" class="Function">T.sym</a> <a id="1955" href="Function.LeftInverse.html#1892" class="Bound">to-x≈y</a><a id="1961" class="Symbol">)</a> <a id="1963" href="Relation.Binary.PreorderReasoning.html#1220" class="Function Operator">⟩</a>
<a id="1969" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a> <a id="1974" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="1978" class="Symbol">(</a><a id="1979" href="Function.LeftInverse.html#LeftInverse.to" class="Field">to</a> <a id="1982" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="1986" href="Function.LeftInverse.html#1885" class="Bound">x</a><a id="1987" class="Symbol">)</a> <a id="1990" href="Relation.Binary.PreorderReasoning.html#1220" class="Function Operator">≈⟨</a> <a id="1993" href="Function.LeftInverse.html#LeftInverse.left-inverse-of" class="Field">left-inverse-of</a> <a id="2009" href="Function.LeftInverse.html#1885" class="Bound">x</a> <a id="2011" href="Relation.Binary.PreorderReasoning.html#1220" class="Function Operator">⟩</a>
<a id="2017" href="Function.LeftInverse.html#1885" class="Bound">x</a> <a id="2038" href="Relation.Binary.PreorderReasoning.html#1519" class="Function Operator">∎</a>
<a id="2041" class="Comment">-- The set of all right inverses between two setoids.</a>
<a id="RightInverse" href="Function.LeftInverse.html#RightInverse" class="Function">RightInverse</a> <a id="2109" class="Symbol">:</a> <a id="2111" class="Symbol">∀</a> <a id="2113" class="Symbol">{</a><a id="2114" href="Function.LeftInverse.html#2114" class="Bound">f₁</a> <a id="2117" href="Function.LeftInverse.html#2117" class="Bound">f₂</a> <a id="2120" href="Function.LeftInverse.html#2120" class="Bound">t₁</a> <a id="2123" href="Function.LeftInverse.html#2123" class="Bound">t₂</a><a id="2125" class="Symbol">}</a>
<a id="2142" class="Symbol">(</a><a id="2143" href="Function.LeftInverse.html#2143" class="Bound">From</a> <a id="2148" class="Symbol">:</a> <a id="2150" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="2157" href="Function.LeftInverse.html#2114" class="Bound">f₁</a> <a id="2160" href="Function.LeftInverse.html#2117" class="Bound">f₂</a><a id="2162" class="Symbol">)</a> <a id="2164" class="Symbol">(</a><a id="2165" href="Function.LeftInverse.html#2165" class="Bound">To</a> <a id="2168" class="Symbol">:</a> <a id="2170" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="2177" href="Function.LeftInverse.html#2120" class="Bound">t₁</a> <a id="2180" href="Function.LeftInverse.html#2123" class="Bound">t₂</a><a id="2182" class="Symbol">)</a> <a id="2184" class="Symbol">→</a> <a id="2186" class="PrimitiveType">Set</a> <a id="2190" class="Symbol">_</a>
<a id="2192" href="Function.LeftInverse.html#RightInverse" class="Function">RightInverse</a> <a id="2205" href="Function.LeftInverse.html#2205" class="Bound">From</a> <a id="2210" href="Function.LeftInverse.html#2210" class="Bound">To</a> <a id="2213" class="Symbol">=</a> <a id="2215" href="Function.LeftInverse.html#LeftInverse" class="Record">LeftInverse</a> <a id="2227" href="Function.LeftInverse.html#2210" class="Bound">To</a> <a id="2230" href="Function.LeftInverse.html#2205" class="Bound">From</a>
<a id="2236" class="Comment">-- The set of all left inverses from one set to another. (Read A ↞ B</a>
<a id="2305" class="Comment">-- as "surjection from B to A".)</a>
<a id="2339" class="Keyword">infix</a> <a id="2345" class="Number">3</a> <a id="2347" href="Function.LeftInverse.html#_%E2%86%9E_" class="Function Operator">_↞_</a>
<a id="_↞_" href="Function.LeftInverse.html#_%E2%86%9E_" class="Function Operator">_↞_</a> <a id="2356" class="Symbol">:</a> <a id="2358" class="Symbol">∀</a> <a id="2360" class="Symbol">{</a><a id="2361" href="Function.LeftInverse.html#2361" class="Bound">f</a> <a id="2363" href="Function.LeftInverse.html#2363" class="Bound">t</a><a id="2364" class="Symbol">}</a> <a id="2366" class="Symbol">→</a> <a id="2368" class="PrimitiveType">Set</a> <a id="2372" href="Function.LeftInverse.html#2361" class="Bound">f</a> <a id="2374" class="Symbol">→</a> <a id="2376" class="PrimitiveType">Set</a> <a id="2380" href="Function.LeftInverse.html#2363" class="Bound">t</a> <a id="2382" class="Symbol">→</a> <a id="2384" class="PrimitiveType">Set</a> <a id="2388" class="Symbol">_</a>
<a id="2390" href="Function.LeftInverse.html#2390" class="Bound">From</a> <a id="2395" href="Function.LeftInverse.html#_%E2%86%9E_" class="Function Operator">↞</a> <a id="2397" href="Function.LeftInverse.html#2397" class="Bound">To</a> <a id="2400" class="Symbol">=</a> <a id="2402" href="Function.LeftInverse.html#LeftInverse" class="Record">LeftInverse</a> <a id="2414" class="Symbol">(</a><a id="2415" href="Relation.Binary.PropositionalEquality.html#setoid" class="Function">P.setoid</a> <a id="2424" href="Function.LeftInverse.html#2390" class="Bound">From</a><a id="2428" class="Symbol">)</a> <a id="2430" class="Symbol">(</a><a id="2431" href="Relation.Binary.PropositionalEquality.html#setoid" class="Function">P.setoid</a> <a id="2440" href="Function.LeftInverse.html#2397" class="Bound">To</a><a id="2442" class="Symbol">)</a>
<a id="2445" class="Comment">-- Identity and composition.</a>
<a id="id" href="Function.LeftInverse.html#id" class="Function">id</a> <a id="2478" class="Symbol">:</a> <a id="2480" class="Symbol">∀</a> <a id="2482" class="Symbol">{</a><a id="2483" href="Function.LeftInverse.html#2483" class="Bound">s₁</a> <a id="2486" href="Function.LeftInverse.html#2486" class="Bound">s₂</a><a id="2488" class="Symbol">}</a> <a id="2490" class="Symbol">{</a><a id="2491" href="Function.LeftInverse.html#2491" class="Bound">S</a> <a id="2493" class="Symbol">:</a> <a id="2495" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="2502" href="Function.LeftInverse.html#2483" class="Bound">s₁</a> <a id="2505" href="Function.LeftInverse.html#2486" class="Bound">s₂</a><a id="2507" class="Symbol">}</a> <a id="2509" class="Symbol">→</a> <a id="2511" href="Function.LeftInverse.html#LeftInverse" class="Record">LeftInverse</a> <a id="2523" href="Function.LeftInverse.html#2491" class="Bound">S</a> <a id="2525" href="Function.LeftInverse.html#2491" class="Bound">S</a>
<a id="2527" href="Function.LeftInverse.html#id" class="Function">id</a> <a id="2530" class="Symbol">{</a><a id="2531" class="Argument">S</a> <a id="2533" class="Symbol">=</a> <a id="2535" href="Function.LeftInverse.html#2535" class="Bound">S</a><a id="2536" class="Symbol">}</a> <a id="2538" class="Symbol">=</a> <a id="2540" class="Keyword">record</a>
<a id="2549" class="Symbol">{</a> <a id="2551" class="Field">to</a> <a id="2567" class="Symbol">=</a> <a id="2569" href="Function.Equality.html#id" class="Function">Eq.id</a>
<a id="2577" class="Symbol">;</a> <a id="2579" class="Field">from</a> <a id="2595" class="Symbol">=</a> <a id="2597" href="Function.Equality.html#id" class="Function">Eq.id</a>
<a id="2605" class="Symbol">;</a> <a id="2607" class="Field">left-inverse-of</a> <a id="2623" class="Symbol">=</a> <a id="2625" class="Symbol">λ</a> <a id="2627" href="Function.LeftInverse.html#2627" class="Bound">_</a> <a id="2629" class="Symbol">→</a> <a id="2631" href="Relation.Binary.Core.html#4934" class="Function">Setoid.refl</a> <a id="2643" href="Function.LeftInverse.html#2535" class="Bound">S</a>
<a id="2647" class="Symbol">}</a>
<a id="2650" class="Keyword">infixr</a> <a id="2657" class="Number">9</a> <a id="2659" href="Function.LeftInverse.html#_%E2%88%98_" class="Function Operator">_∘_</a>
<a id="_∘_" href="Function.LeftInverse.html#_%E2%88%98_" class="Function Operator">_∘_</a> <a id="2668" class="Symbol">:</a> <a id="2670" class="Symbol">∀</a> <a id="2672" class="Symbol">{</a><a id="2673" href="Function.LeftInverse.html#2673" class="Bound">f₁</a> <a id="2676" href="Function.LeftInverse.html#2676" class="Bound">f₂</a> <a id="2679" href="Function.LeftInverse.html#2679" class="Bound">m₁</a> <a id="2682" href="Function.LeftInverse.html#2682" class="Bound">m₂</a> <a id="2685" href="Function.LeftInverse.html#2685" class="Bound">t₁</a> <a id="2688" href="Function.LeftInverse.html#2688" class="Bound">t₂</a><a id="2690" class="Symbol">}</a>
<a id="2700" class="Symbol">{</a><a id="2701" href="Function.LeftInverse.html#2701" class="Bound">F</a> <a id="2703" class="Symbol">:</a> <a id="2705" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="2712" href="Function.LeftInverse.html#2673" class="Bound">f₁</a> <a id="2715" href="Function.LeftInverse.html#2676" class="Bound">f₂</a><a id="2717" class="Symbol">}</a> <a id="2719" class="Symbol">{</a><a id="2720" href="Function.LeftInverse.html#2720" class="Bound">M</a> <a id="2722" class="Symbol">:</a> <a id="2724" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="2731" href="Function.LeftInverse.html#2679" class="Bound">m₁</a> <a id="2734" href="Function.LeftInverse.html#2682" class="Bound">m₂</a><a id="2736" class="Symbol">}</a> <a id="2738" class="Symbol">{</a><a id="2739" href="Function.LeftInverse.html#2739" class="Bound">T</a> <a id="2741" class="Symbol">:</a> <a id="2743" href="Relation.Binary.html#Setoid" class="Record">Setoid</a> <a id="2750" href="Function.LeftInverse.html#2685" class="Bound">t₁</a> <a id="2753" href="Function.LeftInverse.html#2688" class="Bound">t₂</a><a id="2755" class="Symbol">}</a> <a id="2757" class="Symbol">→</a>
<a id="2765" href="Function.LeftInverse.html#LeftInverse" class="Record">LeftInverse</a> <a id="2777" href="Function.LeftInverse.html#2720" class="Bound">M</a> <a id="2779" href="Function.LeftInverse.html#2739" class="Bound">T</a> <a id="2781" class="Symbol">→</a> <a id="2783" href="Function.LeftInverse.html#LeftInverse" class="Record">LeftInverse</a> <a id="2795" href="Function.LeftInverse.html#2701" class="Bound">F</a> <a id="2797" href="Function.LeftInverse.html#2720" class="Bound">M</a> <a id="2799" class="Symbol">→</a> <a id="2801" href="Function.LeftInverse.html#LeftInverse" class="Record">LeftInverse</a> <a id="2813" href="Function.LeftInverse.html#2701" class="Bound">F</a> <a id="2815" href="Function.LeftInverse.html#2739" class="Bound">T</a>
<a id="2817" href="Function.LeftInverse.html#_%E2%88%98_" class="Function Operator">_∘_</a> <a id="2821" class="Symbol">{</a><a id="2822" class="Argument">F</a> <a id="2824" class="Symbol">=</a> <a id="2826" href="Function.LeftInverse.html#2826" class="Bound">F</a><a id="2827" class="Symbol">}</a> <a id="2829" href="Function.LeftInverse.html#2829" class="Bound">f</a> <a id="2831" href="Function.LeftInverse.html#2831" class="Bound">g</a> <a id="2833" class="Symbol">=</a> <a id="2835" class="Keyword">record</a>
<a id="2844" class="Symbol">{</a> <a id="2846" class="Field">to</a> <a id="2862" class="Symbol">=</a> <a id="2864" href="Function.LeftInverse.html#LeftInverse.to" class="Field">to</a> <a id="2869" href="Function.LeftInverse.html#2829" class="Bound">f</a> <a id="2871" href="Function.Equality.html#_%E2%9F%AA%E2%88%98%E2%9F%AB_" class="Function Operator">⟪∘⟫</a> <a id="2875" href="Function.LeftInverse.html#LeftInverse.to" class="Field">to</a> <a id="2880" href="Function.LeftInverse.html#2831" class="Bound">g</a>
<a id="2884" class="Symbol">;</a> <a id="2886" class="Field">from</a> <a id="2902" class="Symbol">=</a> <a id="2904" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a> <a id="2909" href="Function.LeftInverse.html#2831" class="Bound">g</a> <a id="2911" href="Function.Equality.html#_%E2%9F%AA%E2%88%98%E2%9F%AB_" class="Function Operator">⟪∘⟫</a> <a id="2915" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a> <a id="2920" href="Function.LeftInverse.html#2829" class="Bound">f</a>
<a id="2924" class="Symbol">;</a> <a id="2926" class="Field">left-inverse-of</a> <a id="2942" class="Symbol">=</a> <a id="2944" class="Symbol">λ</a> <a id="2946" href="Function.LeftInverse.html#2946" class="Bound">x</a> <a id="2948" class="Symbol">→</a> <a id="2950" href="Relation.Binary.PreorderReasoning.html#1154" class="Function Operator">begin</a>
<a id="2962" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a> <a id="2967" href="Function.LeftInverse.html#2831" class="Bound">g</a> <a id="2969" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="2973" class="Symbol">(</a><a id="2974" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a> <a id="2979" href="Function.LeftInverse.html#2829" class="Bound">f</a> <a id="2981" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="2985" class="Symbol">(</a><a id="2986" href="Function.LeftInverse.html#LeftInverse.to" class="Field">to</a> <a id="2989" href="Function.LeftInverse.html#2829" class="Bound">f</a> <a id="2991" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="2995" class="Symbol">(</a><a id="2996" href="Function.LeftInverse.html#LeftInverse.to" class="Field">to</a> <a id="2999" href="Function.LeftInverse.html#2831" class="Bound">g</a> <a id="3001" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="3005" href="Function.LeftInverse.html#2946" class="Bound">x</a><a id="3006" class="Symbol">)))</a> <a id="3011" href="Relation.Binary.PreorderReasoning.html#1220" class="Function Operator">≈⟨</a> <a id="3014" href="Function.Equality.html#%CE%A0.cong" class="Field">Eq.cong</a> <a id="3022" class="Symbol">(</a><a id="3023" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a> <a id="3028" href="Function.LeftInverse.html#2831" class="Bound">g</a><a id="3029" class="Symbol">)</a> <a id="3031" class="Symbol">(</a><a id="3032" href="Function.LeftInverse.html#LeftInverse.left-inverse-of" class="Field">left-inverse-of</a> <a id="3048" href="Function.LeftInverse.html#2829" class="Bound">f</a> <a id="3050" class="Symbol">(</a><a id="3051" href="Function.LeftInverse.html#LeftInverse.to" class="Field">to</a> <a id="3054" href="Function.LeftInverse.html#2831" class="Bound">g</a> <a id="3056" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="3060" href="Function.LeftInverse.html#2946" class="Bound">x</a><a id="3061" class="Symbol">))</a> <a id="3064" href="Relation.Binary.PreorderReasoning.html#1220" class="Function Operator">⟩</a>
<a id="3072" href="Function.LeftInverse.html#LeftInverse.from" class="Field">from</a> <a id="3077" href="Function.LeftInverse.html#2831" class="Bound">g</a> <a id="3079" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="3083" class="Symbol">(</a><a id="3084" href="Function.LeftInverse.html#LeftInverse.to" class="Field">to</a> <a id="3087" href="Function.LeftInverse.html#2831" class="Bound">g</a> <a id="3089" href="Function.Equality.html#%CE%A0._%E2%9F%A8%24%E2%9F%A9_" class="Field Operator">⟨$⟩</a> <a id="3093" href="Function.LeftInverse.html#2946" class="Bound">x</a><a id="3094" class="Symbol">)</a> <a id="3121" href="Relation.Binary.PreorderReasoning.html#1220" class="Function Operator">≈⟨</a> <a id="3124" href="Function.LeftInverse.html#LeftInverse.left-inverse-of" class="Field">left-inverse-of</a> <a id="3140" href="Function.LeftInverse.html#2831" class="Bound">g</a> <a id="3142" href="Function.LeftInverse.html#2946" class="Bound">x</a> <a id="3144" href="Relation.Binary.PreorderReasoning.html#1220" class="Function Operator">⟩</a>
<a id="3152" href="Function.LeftInverse.html#2946" class="Bound">x</a> <a id="3201" href="Relation.Binary.PreorderReasoning.html#1519" class="Function Operator">∎</a>
<a id="3205" class="Symbol">}</a>
<a id="3209" class="Keyword">where</a>
<a id="3217" class="Keyword">open</a> <a id="3222" href="Function.LeftInverse.html#LeftInverse" class="Module">LeftInverse</a>
<a id="3236" class="Keyword">open</a> <a id="3241" href="Relation.Binary.EqReasoning.html" class="Module">EqReasoning</a> <a id="3253" href="Function.LeftInverse.html#2826" class="Bound">F</a>
</pre></body></html>
|