88 lines
31 KiB
HTML
88 lines
31 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>Data.Sum.Base</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">-- Sums (disjoint unions)</a>
|
||
<a id="132" class="Comment">------------------------------------------------------------------------</a>
|
||
|
||
<a id="206" class="Symbol">{-#</a> <a id="210" class="Keyword">OPTIONS</a> <a id="218" class="Pragma">--without-K</a> <a id="230" class="Pragma">--safe</a> <a id="237" class="Symbol">#-}</a>
|
||
|
||
<a id="242" class="Keyword">module</a> <a id="249" href="Data.Sum.Base.html" class="Module">Data.Sum.Base</a> <a id="263" class="Keyword">where</a>
|
||
|
||
<a id="270" class="Keyword">open</a> <a id="275" class="Keyword">import</a> <a id="282" href="Data.Bool.Base.html" class="Module">Data.Bool.Base</a> <a id="297" class="Keyword">using</a> <a id="303" class="Symbol">(</a><a id="304" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a><a id="308" class="Symbol">;</a> <a id="310" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a><a id="315" class="Symbol">)</a>
|
||
<a id="317" class="Keyword">open</a> <a id="322" class="Keyword">import</a> <a id="329" href="Function.Base.html" class="Module">Function.Base</a> <a id="343" class="Keyword">using</a> <a id="349" class="Symbol">(</a><a id="350" href="Function.Base.html#1031" class="Function Operator">_∘_</a><a id="353" class="Symbol">;</a> <a id="355" href="Function.Base.html#3706" class="Function Operator">_∘′_</a><a id="359" class="Symbol">;</a> <a id="361" href="Function.Base.html#5115" class="Function Operator">_-⟪_⟫-_</a> <a id="369" class="Symbol">;</a> <a id="371" href="Function.Base.html#615" class="Function">id</a><a id="373" class="Symbol">)</a>
|
||
<a id="375" class="Keyword">open</a> <a id="380" class="Keyword">import</a> <a id="387" href="Relation.Nullary.Reflects.html" class="Module">Relation.Nullary.Reflects</a> <a id="413" class="Keyword">using</a> <a id="419" class="Symbol">(</a><a id="420" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a><a id="426" class="Symbol">)</a>
|
||
<a id="428" class="Keyword">open</a> <a id="433" class="Keyword">import</a> <a id="440" href="Relation.Nullary.html" class="Module">Relation.Nullary</a> <a id="457" class="Keyword">using</a> <a id="463" class="Symbol">(</a><a id="464" href="Relation.Nullary.html#1511" class="Record">Dec</a><a id="467" class="Symbol">;</a> <a id="469" href="Relation.Nullary.html#1648" class="InductiveConstructor">yes</a><a id="472" class="Symbol">;</a> <a id="474" href="Relation.Nullary.html#1685" class="InductiveConstructor">no</a><a id="476" class="Symbol">;</a> <a id="478" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">_because_</a><a id="487" class="Symbol">;</a> <a id="489" href="Relation.Nullary.html#656" class="Function Operator">¬_</a><a id="491" class="Symbol">)</a>
|
||
<a id="493" class="Keyword">open</a> <a id="498" class="Keyword">import</a> <a id="505" href="Level.html" class="Module">Level</a> <a id="511" class="Keyword">using</a> <a id="517" class="Symbol">(</a><a id="518" href="Agda.Primitive.html#597" class="Postulate">Level</a><a id="523" class="Symbol">;</a> <a id="525" href="Agda.Primitive.html#810" class="Primitive Operator">_⊔_</a><a id="528" class="Symbol">)</a>
|
||
|
||
<a id="531" class="Keyword">private</a>
|
||
<a id="541" class="Keyword">variable</a>
|
||
<a id="554" href="Data.Sum.Base.html#554" class="Generalizable">a</a> <a id="556" href="Data.Sum.Base.html#556" class="Generalizable">b</a> <a id="558" href="Data.Sum.Base.html#558" class="Generalizable">c</a> <a id="560" href="Data.Sum.Base.html#560" class="Generalizable">d</a> <a id="562" class="Symbol">:</a> <a id="564" href="Agda.Primitive.html#597" class="Postulate">Level</a>
|
||
<a id="574" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="576" class="Symbol">:</a> <a id="578" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="582" href="Data.Sum.Base.html#554" class="Generalizable">a</a>
|
||
<a id="588" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="590" class="Symbol">:</a> <a id="592" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="596" href="Data.Sum.Base.html#556" class="Generalizable">b</a>
|
||
<a id="602" href="Data.Sum.Base.html#602" class="Generalizable">C</a> <a id="604" class="Symbol">:</a> <a id="606" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="610" href="Data.Sum.Base.html#558" class="Generalizable">c</a>
|
||
<a id="616" href="Data.Sum.Base.html#616" class="Generalizable">D</a> <a id="618" class="Symbol">:</a> <a id="620" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="624" href="Data.Sum.Base.html#560" class="Generalizable">d</a>
|
||
|
||
<a id="627" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="700" class="Comment">-- Definition</a>
|
||
|
||
<a id="715" class="Keyword">infixr</a> <a id="722" class="Number">1</a> <a id="724" href="Data.Sum.Base.html#734" class="Datatype Operator">_⊎_</a>
|
||
|
||
<a id="729" class="Keyword">data</a> <a id="_⊎_"></a><a id="734" href="Data.Sum.Base.html#734" class="Datatype Operator">_⊎_</a> <a id="738" class="Symbol">(</a><a id="739" href="Data.Sum.Base.html#739" class="Bound">A</a> <a id="741" class="Symbol">:</a> <a id="743" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="747" href="Data.Sum.Base.html#554" class="Generalizable">a</a><a id="748" class="Symbol">)</a> <a id="750" class="Symbol">(</a><a id="751" href="Data.Sum.Base.html#751" class="Bound">B</a> <a id="753" class="Symbol">:</a> <a id="755" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="759" href="Data.Sum.Base.html#556" class="Generalizable">b</a><a id="760" class="Symbol">)</a> <a id="762" class="Symbol">:</a> <a id="764" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="768" class="Symbol">(</a><a id="769" href="Data.Sum.Base.html#747" class="Bound">a</a> <a id="771" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="773" href="Data.Sum.Base.html#759" class="Bound">b</a><a id="774" class="Symbol">)</a> <a id="776" class="Keyword">where</a>
|
||
<a id="_⊎_.inj₁"></a><a id="784" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="789" class="Symbol">:</a> <a id="791" class="Symbol">(</a><a id="792" href="Data.Sum.Base.html#792" class="Bound">x</a> <a id="794" class="Symbol">:</a> <a id="796" href="Data.Sum.Base.html#739" class="Bound">A</a><a id="797" class="Symbol">)</a> <a id="799" class="Symbol">→</a> <a id="801" href="Data.Sum.Base.html#739" class="Bound">A</a> <a id="803" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="805" href="Data.Sum.Base.html#751" class="Bound">B</a>
|
||
<a id="_⊎_.inj₂"></a><a id="809" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="814" class="Symbol">:</a> <a id="816" class="Symbol">(</a><a id="817" href="Data.Sum.Base.html#817" class="Bound">y</a> <a id="819" class="Symbol">:</a> <a id="821" href="Data.Sum.Base.html#751" class="Bound">B</a><a id="822" class="Symbol">)</a> <a id="824" class="Symbol">→</a> <a id="826" href="Data.Sum.Base.html#739" class="Bound">A</a> <a id="828" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="830" href="Data.Sum.Base.html#751" class="Bound">B</a>
|
||
|
||
<a id="833" class="Comment">------------------------------------------------------------------------</a>
|
||
<a id="906" class="Comment">-- Functions</a>
|
||
|
||
<a id="[_,_]"></a><a id="920" href="Data.Sum.Base.html#920" class="Function Operator">[_,_]</a> <a id="926" class="Symbol">:</a> <a id="928" class="Symbol">∀</a> <a id="930" class="Symbol">{</a><a id="931" href="Data.Sum.Base.html#931" class="Bound">C</a> <a id="933" class="Symbol">:</a> <a id="935" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="937" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="939" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="941" class="Symbol">→</a> <a id="943" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="947" href="Data.Sum.Base.html#558" class="Generalizable">c</a><a id="948" class="Symbol">}</a> <a id="950" class="Symbol">→</a>
|
||
<a id="960" class="Symbol">((</a><a id="962" href="Data.Sum.Base.html#962" class="Bound">x</a> <a id="964" class="Symbol">:</a> <a id="966" href="Data.Sum.Base.html#574" class="Generalizable">A</a><a id="967" class="Symbol">)</a> <a id="969" class="Symbol">→</a> <a id="971" href="Data.Sum.Base.html#931" class="Bound">C</a> <a id="973" class="Symbol">(</a><a id="974" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="979" href="Data.Sum.Base.html#962" class="Bound">x</a><a id="980" class="Symbol">))</a> <a id="983" class="Symbol">→</a> <a id="985" class="Symbol">((</a><a id="987" href="Data.Sum.Base.html#987" class="Bound">x</a> <a id="989" class="Symbol">:</a> <a id="991" href="Data.Sum.Base.html#588" class="Generalizable">B</a><a id="992" class="Symbol">)</a> <a id="994" class="Symbol">→</a> <a id="996" href="Data.Sum.Base.html#931" class="Bound">C</a> <a id="998" class="Symbol">(</a><a id="999" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="1004" href="Data.Sum.Base.html#987" class="Bound">x</a><a id="1005" class="Symbol">))</a> <a id="1008" class="Symbol">→</a>
|
||
<a id="1018" class="Symbol">((</a><a id="1020" href="Data.Sum.Base.html#1020" class="Bound">x</a> <a id="1022" class="Symbol">:</a> <a id="1024" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1026" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1028" href="Data.Sum.Base.html#588" class="Generalizable">B</a><a id="1029" class="Symbol">)</a> <a id="1031" class="Symbol">→</a> <a id="1033" href="Data.Sum.Base.html#931" class="Bound">C</a> <a id="1035" href="Data.Sum.Base.html#1020" class="Bound">x</a><a id="1036" class="Symbol">)</a>
|
||
<a id="1038" href="Data.Sum.Base.html#920" class="Function Operator">[</a> <a id="1040" href="Data.Sum.Base.html#1040" class="Bound">f</a> <a id="1042" href="Data.Sum.Base.html#920" class="Function Operator">,</a> <a id="1044" href="Data.Sum.Base.html#1044" class="Bound">g</a> <a id="1046" href="Data.Sum.Base.html#920" class="Function Operator">]</a> <a id="1048" class="Symbol">(</a><a id="1049" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="1054" href="Data.Sum.Base.html#1054" class="Bound">x</a><a id="1055" class="Symbol">)</a> <a id="1057" class="Symbol">=</a> <a id="1059" href="Data.Sum.Base.html#1040" class="Bound">f</a> <a id="1061" href="Data.Sum.Base.html#1054" class="Bound">x</a>
|
||
<a id="1063" href="Data.Sum.Base.html#920" class="Function Operator">[</a> <a id="1065" href="Data.Sum.Base.html#1065" class="Bound">f</a> <a id="1067" href="Data.Sum.Base.html#920" class="Function Operator">,</a> <a id="1069" href="Data.Sum.Base.html#1069" class="Bound">g</a> <a id="1071" href="Data.Sum.Base.html#920" class="Function Operator">]</a> <a id="1073" class="Symbol">(</a><a id="1074" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="1079" href="Data.Sum.Base.html#1079" class="Bound">y</a><a id="1080" class="Symbol">)</a> <a id="1082" class="Symbol">=</a> <a id="1084" href="Data.Sum.Base.html#1069" class="Bound">g</a> <a id="1086" href="Data.Sum.Base.html#1079" class="Bound">y</a>
|
||
|
||
<a id="[_,_]′"></a><a id="1089" href="Data.Sum.Base.html#1089" class="Function Operator">[_,_]′</a> <a id="1096" class="Symbol">:</a> <a id="1098" class="Symbol">(</a><a id="1099" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1101" class="Symbol">→</a> <a id="1103" href="Data.Sum.Base.html#602" class="Generalizable">C</a><a id="1104" class="Symbol">)</a> <a id="1106" class="Symbol">→</a> <a id="1108" class="Symbol">(</a><a id="1109" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1111" class="Symbol">→</a> <a id="1113" href="Data.Sum.Base.html#602" class="Generalizable">C</a><a id="1114" class="Symbol">)</a> <a id="1116" class="Symbol">→</a> <a id="1118" class="Symbol">(</a><a id="1119" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1121" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1123" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1125" class="Symbol">→</a> <a id="1127" href="Data.Sum.Base.html#602" class="Generalizable">C</a><a id="1128" class="Symbol">)</a>
|
||
<a id="1130" href="Data.Sum.Base.html#1089" class="Function Operator">[_,_]′</a> <a id="1137" class="Symbol">=</a> <a id="1139" href="Data.Sum.Base.html#920" class="Function Operator">[_,_]</a>
|
||
|
||
<a id="fromInj₁"></a><a id="1146" href="Data.Sum.Base.html#1146" class="Function">fromInj₁</a> <a id="1155" class="Symbol">:</a> <a id="1157" class="Symbol">(</a><a id="1158" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1160" class="Symbol">→</a> <a id="1162" href="Data.Sum.Base.html#574" class="Generalizable">A</a><a id="1163" class="Symbol">)</a> <a id="1165" class="Symbol">→</a> <a id="1167" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1169" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1171" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1173" class="Symbol">→</a> <a id="1175" href="Data.Sum.Base.html#574" class="Generalizable">A</a>
|
||
<a id="1177" href="Data.Sum.Base.html#1146" class="Function">fromInj₁</a> <a id="1186" class="Symbol">=</a> <a id="1188" href="Data.Sum.Base.html#1089" class="Function Operator">[</a> <a id="1190" href="Function.Base.html#615" class="Function">id</a> <a id="1193" href="Data.Sum.Base.html#1089" class="Function Operator">,_]′</a>
|
||
|
||
<a id="fromInj₂"></a><a id="1199" href="Data.Sum.Base.html#1199" class="Function">fromInj₂</a> <a id="1208" class="Symbol">:</a> <a id="1210" class="Symbol">(</a><a id="1211" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1213" class="Symbol">→</a> <a id="1215" href="Data.Sum.Base.html#588" class="Generalizable">B</a><a id="1216" class="Symbol">)</a> <a id="1218" class="Symbol">→</a> <a id="1220" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1222" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1224" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1226" class="Symbol">→</a> <a id="1228" href="Data.Sum.Base.html#588" class="Generalizable">B</a>
|
||
<a id="1230" href="Data.Sum.Base.html#1199" class="Function">fromInj₂</a> <a id="1239" class="Symbol">=</a> <a id="1241" href="Data.Sum.Base.html#1089" class="Function Operator">[_,</a> <a id="1245" href="Function.Base.html#615" class="Function">id</a> <a id="1248" href="Data.Sum.Base.html#1089" class="Function Operator">]′</a>
|
||
|
||
<a id="reduce"></a><a id="1252" href="Data.Sum.Base.html#1252" class="Function">reduce</a> <a id="1259" class="Symbol">:</a> <a id="1261" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1263" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1265" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1267" class="Symbol">→</a> <a id="1269" href="Data.Sum.Base.html#574" class="Generalizable">A</a>
|
||
<a id="1271" href="Data.Sum.Base.html#1252" class="Function">reduce</a> <a id="1278" class="Symbol">=</a> <a id="1280" href="Data.Sum.Base.html#1089" class="Function Operator">[</a> <a id="1282" href="Function.Base.html#615" class="Function">id</a> <a id="1285" href="Data.Sum.Base.html#1089" class="Function Operator">,</a> <a id="1287" href="Function.Base.html#615" class="Function">id</a> <a id="1290" href="Data.Sum.Base.html#1089" class="Function Operator">]′</a>
|
||
|
||
<a id="swap"></a><a id="1294" href="Data.Sum.Base.html#1294" class="Function">swap</a> <a id="1299" class="Symbol">:</a> <a id="1301" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1303" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1305" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1307" class="Symbol">→</a> <a id="1309" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1311" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1313" href="Data.Sum.Base.html#574" class="Generalizable">A</a>
|
||
<a id="1315" href="Data.Sum.Base.html#1294" class="Function">swap</a> <a id="1320" class="Symbol">(</a><a id="1321" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="1326" href="Data.Sum.Base.html#1326" class="Bound">x</a><a id="1327" class="Symbol">)</a> <a id="1329" class="Symbol">=</a> <a id="1331" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="1336" href="Data.Sum.Base.html#1326" class="Bound">x</a>
|
||
<a id="1338" href="Data.Sum.Base.html#1294" class="Function">swap</a> <a id="1343" class="Symbol">(</a><a id="1344" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="1349" href="Data.Sum.Base.html#1349" class="Bound">x</a><a id="1350" class="Symbol">)</a> <a id="1352" class="Symbol">=</a> <a id="1354" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="1359" href="Data.Sum.Base.html#1349" class="Bound">x</a>
|
||
|
||
<a id="map"></a><a id="1362" href="Data.Sum.Base.html#1362" class="Function">map</a> <a id="1366" class="Symbol">:</a> <a id="1368" class="Symbol">(</a><a id="1369" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1371" class="Symbol">→</a> <a id="1373" href="Data.Sum.Base.html#602" class="Generalizable">C</a><a id="1374" class="Symbol">)</a> <a id="1376" class="Symbol">→</a> <a id="1378" class="Symbol">(</a><a id="1379" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1381" class="Symbol">→</a> <a id="1383" href="Data.Sum.Base.html#616" class="Generalizable">D</a><a id="1384" class="Symbol">)</a> <a id="1386" class="Symbol">→</a> <a id="1388" class="Symbol">(</a><a id="1389" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1391" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1393" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1395" class="Symbol">→</a> <a id="1397" href="Data.Sum.Base.html#602" class="Generalizable">C</a> <a id="1399" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1401" href="Data.Sum.Base.html#616" class="Generalizable">D</a><a id="1402" class="Symbol">)</a>
|
||
<a id="1404" href="Data.Sum.Base.html#1362" class="Function">map</a> <a id="1408" href="Data.Sum.Base.html#1408" class="Bound">f</a> <a id="1410" href="Data.Sum.Base.html#1410" class="Bound">g</a> <a id="1412" class="Symbol">=</a> <a id="1414" href="Data.Sum.Base.html#1089" class="Function Operator">[</a> <a id="1416" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="1421" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="1423" href="Data.Sum.Base.html#1408" class="Bound">f</a> <a id="1425" href="Data.Sum.Base.html#1089" class="Function Operator">,</a> <a id="1427" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="1432" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="1434" href="Data.Sum.Base.html#1410" class="Bound">g</a> <a id="1436" href="Data.Sum.Base.html#1089" class="Function Operator">]′</a>
|
||
|
||
<a id="map₁"></a><a id="1440" href="Data.Sum.Base.html#1440" class="Function">map₁</a> <a id="1445" class="Symbol">:</a> <a id="1447" class="Symbol">(</a><a id="1448" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1450" class="Symbol">→</a> <a id="1452" href="Data.Sum.Base.html#602" class="Generalizable">C</a><a id="1453" class="Symbol">)</a> <a id="1455" class="Symbol">→</a> <a id="1457" class="Symbol">(</a><a id="1458" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1460" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1462" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1464" class="Symbol">→</a> <a id="1466" href="Data.Sum.Base.html#602" class="Generalizable">C</a> <a id="1468" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1470" href="Data.Sum.Base.html#588" class="Generalizable">B</a><a id="1471" class="Symbol">)</a>
|
||
<a id="1473" href="Data.Sum.Base.html#1440" class="Function">map₁</a> <a id="1478" href="Data.Sum.Base.html#1478" class="Bound">f</a> <a id="1480" class="Symbol">=</a> <a id="1482" href="Data.Sum.Base.html#1362" class="Function">map</a> <a id="1486" href="Data.Sum.Base.html#1478" class="Bound">f</a> <a id="1488" href="Function.Base.html#615" class="Function">id</a>
|
||
|
||
<a id="map₂"></a><a id="1492" href="Data.Sum.Base.html#1492" class="Function">map₂</a> <a id="1497" class="Symbol">:</a> <a id="1499" class="Symbol">(</a><a id="1500" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1502" class="Symbol">→</a> <a id="1504" href="Data.Sum.Base.html#616" class="Generalizable">D</a><a id="1505" class="Symbol">)</a> <a id="1507" class="Symbol">→</a> <a id="1509" class="Symbol">(</a><a id="1510" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1512" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1514" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1516" class="Symbol">→</a> <a id="1518" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1520" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1522" href="Data.Sum.Base.html#616" class="Generalizable">D</a><a id="1523" class="Symbol">)</a>
|
||
<a id="1525" href="Data.Sum.Base.html#1492" class="Function">map₂</a> <a id="1530" class="Symbol">=</a> <a id="1532" href="Data.Sum.Base.html#1362" class="Function">map</a> <a id="1536" href="Function.Base.html#615" class="Function">id</a>
|
||
|
||
<a id="assocʳ"></a><a id="1540" href="Data.Sum.Base.html#1540" class="Function">assocʳ</a> <a id="1547" class="Symbol">:</a> <a id="1549" class="Symbol">(</a><a id="1550" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1552" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1554" href="Data.Sum.Base.html#588" class="Generalizable">B</a><a id="1555" class="Symbol">)</a> <a id="1557" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1559" href="Data.Sum.Base.html#602" class="Generalizable">C</a> <a id="1561" class="Symbol">→</a> <a id="1563" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1565" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1567" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1569" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1571" href="Data.Sum.Base.html#602" class="Generalizable">C</a>
|
||
<a id="1573" href="Data.Sum.Base.html#1540" class="Function">assocʳ</a> <a id="1580" class="Symbol">=</a> <a id="1582" href="Data.Sum.Base.html#1089" class="Function Operator">[</a> <a id="1584" href="Data.Sum.Base.html#1492" class="Function">map₂</a> <a id="1589" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="1594" href="Data.Sum.Base.html#1089" class="Function Operator">,</a> <a id="1596" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="1601" href="Function.Base.html#3706" class="Function Operator">∘′</a> <a id="1604" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="1609" href="Data.Sum.Base.html#1089" class="Function Operator">]′</a>
|
||
|
||
<a id="assocˡ"></a><a id="1613" href="Data.Sum.Base.html#1613" class="Function">assocˡ</a> <a id="1620" class="Symbol">:</a> <a id="1622" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1624" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1626" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1628" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1630" href="Data.Sum.Base.html#602" class="Generalizable">C</a> <a id="1632" class="Symbol">→</a> <a id="1634" class="Symbol">(</a><a id="1635" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1637" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1639" href="Data.Sum.Base.html#588" class="Generalizable">B</a><a id="1640" class="Symbol">)</a> <a id="1642" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1644" href="Data.Sum.Base.html#602" class="Generalizable">C</a>
|
||
<a id="1646" href="Data.Sum.Base.html#1613" class="Function">assocˡ</a> <a id="1653" class="Symbol">=</a> <a id="1655" href="Data.Sum.Base.html#1089" class="Function Operator">[</a> <a id="1657" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="1662" href="Function.Base.html#3706" class="Function Operator">∘′</a> <a id="1665" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="1670" href="Data.Sum.Base.html#1089" class="Function Operator">,</a> <a id="1672" href="Data.Sum.Base.html#1440" class="Function">map₁</a> <a id="1677" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="1682" href="Data.Sum.Base.html#1089" class="Function Operator">]′</a>
|
||
|
||
<a id="1686" class="Keyword">infixr</a> <a id="1693" class="Number">1</a> <a id="1695" href="Data.Sum.Base.html#1701" class="Function Operator">_-⊎-_</a>
|
||
<a id="_-⊎-_"></a><a id="1701" href="Data.Sum.Base.html#1701" class="Function Operator">_-⊎-_</a> <a id="1707" class="Symbol">:</a> <a id="1709" class="Symbol">(</a><a id="1710" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1712" class="Symbol">→</a> <a id="1714" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1716" class="Symbol">→</a> <a id="1718" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1722" href="Data.Sum.Base.html#558" class="Generalizable">c</a><a id="1723" class="Symbol">)</a> <a id="1725" class="Symbol">→</a> <a id="1727" class="Symbol">(</a><a id="1728" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1730" class="Symbol">→</a> <a id="1732" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1734" class="Symbol">→</a> <a id="1736" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1740" href="Data.Sum.Base.html#560" class="Generalizable">d</a><a id="1741" class="Symbol">)</a> <a id="1743" class="Symbol">→</a> <a id="1745" class="Symbol">(</a><a id="1746" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1748" class="Symbol">→</a> <a id="1750" href="Data.Sum.Base.html#588" class="Generalizable">B</a> <a id="1752" class="Symbol">→</a> <a id="1754" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="1758" class="Symbol">(</a><a id="1759" href="Data.Sum.Base.html#558" class="Generalizable">c</a> <a id="1761" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="1763" href="Data.Sum.Base.html#560" class="Generalizable">d</a><a id="1764" class="Symbol">))</a>
|
||
<a id="1767" href="Data.Sum.Base.html#1767" class="Bound">f</a> <a id="1769" href="Data.Sum.Base.html#1701" class="Function Operator">-⊎-</a> <a id="1773" href="Data.Sum.Base.html#1773" class="Bound">g</a> <a id="1775" class="Symbol">=</a> <a id="1777" href="Data.Sum.Base.html#1767" class="Bound">f</a> <a id="1779" href="Function.Base.html#5115" class="Function Operator">-⟪</a> <a id="1782" href="Data.Sum.Base.html#734" class="Datatype Operator">_⊎_</a> <a id="1786" href="Function.Base.html#5115" class="Function Operator">⟫-</a> <a id="1789" href="Data.Sum.Base.html#1773" class="Bound">g</a>
|
||
|
||
<a id="1792" class="Comment">-- Conversion back and forth with Dec</a>
|
||
|
||
<a id="fromDec"></a><a id="1831" href="Data.Sum.Base.html#1831" class="Function">fromDec</a> <a id="1839" class="Symbol">:</a> <a id="1841" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="1845" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1847" class="Symbol">→</a> <a id="1849" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1851" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1853" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="1855" href="Data.Sum.Base.html#574" class="Generalizable">A</a>
|
||
<a id="1857" href="Data.Sum.Base.html#1831" class="Function">fromDec</a> <a id="1865" class="Symbol">(</a> <a id="1867" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="1872" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="1881" href="Data.Sum.Base.html#1881" class="Bound">[p]</a><a id="1884" class="Symbol">)</a> <a id="1886" class="Symbol">=</a> <a id="1888" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="1893" class="Symbol">(</a><a id="1894" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a> <a id="1902" href="Data.Sum.Base.html#1881" class="Bound">[p]</a><a id="1905" class="Symbol">)</a>
|
||
<a id="1907" href="Data.Sum.Base.html#1831" class="Function">fromDec</a> <a id="1915" class="Symbol">(</a><a id="1916" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a> <a id="1922" href="Relation.Nullary.html#1559" class="InductiveConstructor Operator">because</a> <a id="1930" href="Data.Sum.Base.html#1930" class="Bound">[¬p]</a><a id="1934" class="Symbol">)</a> <a id="1936" class="Symbol">=</a> <a id="1938" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="1943" class="Symbol">(</a><a id="1944" href="Relation.Nullary.Reflects.html#1031" class="Function">invert</a> <a id="1951" href="Data.Sum.Base.html#1930" class="Bound">[¬p]</a><a id="1955" class="Symbol">)</a>
|
||
|
||
<a id="toDec"></a><a id="1958" href="Data.Sum.Base.html#1958" class="Function">toDec</a> <a id="1964" class="Symbol">:</a> <a id="1966" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1968" href="Data.Sum.Base.html#734" class="Datatype Operator">⊎</a> <a id="1970" href="Relation.Nullary.html#656" class="Function Operator">¬</a> <a id="1972" href="Data.Sum.Base.html#574" class="Generalizable">A</a> <a id="1974" class="Symbol">→</a> <a id="1976" href="Relation.Nullary.html#1511" class="Record">Dec</a> <a id="1980" href="Data.Sum.Base.html#574" class="Generalizable">A</a>
|
||
<a id="1982" href="Data.Sum.Base.html#1958" class="Function">toDec</a> <a id="1988" class="Symbol">(</a><a id="1989" href="Data.Sum.Base.html#784" class="InductiveConstructor">inj₁</a> <a id="1994" href="Data.Sum.Base.html#1994" class="Bound">p</a><a id="1995" class="Symbol">)</a> <a id="1998" class="Symbol">=</a> <a id="2000" href="Relation.Nullary.html#1648" class="InductiveConstructor">yes</a> <a id="2004" href="Data.Sum.Base.html#1994" class="Bound">p</a>
|
||
<a id="2006" href="Data.Sum.Base.html#1958" class="Function">toDec</a> <a id="2012" class="Symbol">(</a><a id="2013" href="Data.Sum.Base.html#809" class="InductiveConstructor">inj₂</a> <a id="2018" href="Data.Sum.Base.html#2018" class="Bound">¬p</a><a id="2020" class="Symbol">)</a> <a id="2022" class="Symbol">=</a> <a id="2024" href="Relation.Nullary.html#1685" class="InductiveConstructor">no</a> <a id="2027" href="Data.Sum.Base.html#2018" class="Bound">¬p</a>
|
||
</pre></body></html> |