111 lines
38 KiB
HTML
111 lines
38 KiB
HTML
<!DOCTYPE HTML>
|
||
<html><head><meta charset="utf-8"><title>llpo</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Symbol">{-#</a> <a id="5" class="Keyword">OPTIONS</a> <a id="13" class="Pragma">--safe</a> <a id="20" class="Pragma">--without-K</a> <a id="32" class="Symbol">#-}</a>
|
||
|
||
<a id="37" class="Keyword">open</a> <a id="42" class="Keyword">import</a> <a id="49" href="Agda.Primitive.html" class="Module">Agda.Primitive</a> <a id="64" class="Keyword">renaming</a> <a id="73" class="Symbol">(</a><a id="74" href="Agda.Primitive.html#326" class="Primitive">Set</a> <a id="78" class="Symbol">to</a> <a id="81" class="Primitive">𝒰</a><a id="82" class="Symbol">)</a>
|
||
<a id="84" class="Keyword">open</a> <a id="89" class="Keyword">import</a> <a id="96" href="Agda.Builtin.Nat.html" class="Module">Agda.Builtin.Nat</a> <a id="113" class="Keyword">renaming</a> <a id="122" class="Symbol">(</a><a id="123" href="Agda.Builtin.Nat.html#192" class="Datatype">Nat</a> <a id="127" class="Symbol">to</a> <a id="130" class="Datatype">ℕ</a><a id="131" class="Symbol">)</a> <a id="133" class="Keyword">hiding</a> <a id="140" class="Symbol">(</a><a id="141" href="Agda.Builtin.Nat.html#325" class="Primitive Operator">_+_</a><a id="144" class="Symbol">)</a>
|
||
<a id="146" class="Keyword">open</a> <a id="151" class="Keyword">import</a> <a id="158" href="Agda.Builtin.Bool.html" class="Module">Agda.Builtin.Bool</a> <a id="176" class="Keyword">renaming</a> <a id="185" class="Symbol">(</a><a id="186" href="Agda.Builtin.Bool.html#163" class="Datatype">Bool</a> <a id="191" class="Symbol">to</a> <a id="194" class="Datatype">𝟚</a><a id="195" class="Symbol">;</a> <a id="197" href="Agda.Builtin.Bool.html#182" class="InductiveConstructor">false</a> <a id="203" class="Symbol">to</a> <a id="206" class="InductiveConstructor">𝟘</a><a id="207" class="Symbol">;</a> <a id="209" href="Agda.Builtin.Bool.html#188" class="InductiveConstructor">true</a> <a id="214" class="Symbol">to</a> <a id="217" class="InductiveConstructor">𝟙</a><a id="218" class="Symbol">)</a>
|
||
<a id="220" class="Keyword">open</a> <a id="225" class="Keyword">import</a> <a id="232" href="Agda.Builtin.Equality.html" class="Module">Agda.Builtin.Equality</a> <a id="254" class="Keyword">using</a> <a id="260" class="Symbol">(</a><a id="261" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡_</a><a id="264" class="Symbol">;</a> <a id="266" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a><a id="270" class="Symbol">)</a>
|
||
<a id="272" class="Keyword">open</a> <a id="277" class="Keyword">import</a> <a id="284" href="Function.html" class="Module">Function</a> <a id="293" class="Keyword">using</a> <a id="299" class="Symbol">(</a><a id="300" href="Function.Base.html#1031" class="Function Operator">_∘_</a><a id="303" class="Symbol">;</a> <a id="305" href="Function.Base.html#636" class="Function">const</a><a id="310" class="Symbol">)</a>
|
||
|
||
<a id="313" class="Comment">{- Variables -}</a>
|
||
<a id="329" class="Keyword">variable</a>
|
||
<a id="340" href="llpo.html#340" class="Generalizable">ₙ</a> <a id="342" class="Symbol">:</a> <a id="344" href="Agda.Primitive.html#597" class="Postulate">Level</a>
|
||
<a id="352" href="llpo.html#352" class="Generalizable">ₘ</a> <a id="354" class="Symbol">:</a> <a id="356" href="Agda.Primitive.html#597" class="Postulate">Level</a>
|
||
<a id="364" href="llpo.html#364" class="Generalizable">A</a> <a id="366" class="Symbol">:</a> <a id="368" href="llpo.html#81" class="Primitive">𝒰</a> <a id="370" href="llpo.html#340" class="Generalizable">ₙ</a>
|
||
<a id="374" href="llpo.html#374" class="Generalizable">B</a> <a id="376" class="Symbol">:</a> <a id="378" href="llpo.html#81" class="Primitive">𝒰</a> <a id="380" href="llpo.html#340" class="Generalizable">ₙ</a>
|
||
<a id="384" href="llpo.html#384" class="Generalizable">C</a> <a id="386" class="Symbol">:</a> <a id="388" href="llpo.html#81" class="Primitive">𝒰</a> <a id="390" href="llpo.html#340" class="Generalizable">ₙ</a>
|
||
|
||
<a id="393" class="Comment">{- Types -}</a>
|
||
|
||
<a id="406" class="Keyword">data</a> <a id="⊥"></a><a id="411" href="llpo.html#411" class="Datatype">⊥</a> <a id="413" class="Symbol">:</a> <a id="415" href="llpo.html#81" class="Primitive">𝒰₀</a> <a id="418" class="Keyword">where</a>
|
||
|
||
<a id="425" class="Keyword">infixr</a> <a id="432" class="Number">8</a> <a id="434" href="llpo.html#437" class="Function Operator">¬_</a>
|
||
<a id="¬_"></a><a id="437" href="llpo.html#437" class="Function Operator">¬_</a> <a id="440" class="Symbol">:</a> <a id="442" href="llpo.html#81" class="Primitive">𝒰</a> <a id="444" href="llpo.html#340" class="Generalizable">ₙ</a> <a id="446" class="Symbol">→</a> <a id="448" href="llpo.html#81" class="Primitive">𝒰</a> <a id="450" href="llpo.html#340" class="Generalizable">ₙ</a>
|
||
<a id="452" href="llpo.html#437" class="Function Operator">¬</a> <a id="454" href="llpo.html#454" class="Bound">p</a> <a id="456" class="Symbol">=</a> <a id="458" href="llpo.html#454" class="Bound">p</a> <a id="460" class="Symbol">→</a> <a id="462" href="llpo.html#411" class="Datatype">⊥</a>
|
||
|
||
<a id="465" class="Keyword">infixr</a> <a id="472" class="Number">2</a> <a id="474" href="llpo.html#483" class="Datatype Operator">_+_</a>
|
||
<a id="478" class="Keyword">data</a> <a id="_+_"></a><a id="483" href="llpo.html#483" class="Datatype Operator">_+_</a> <a id="487" class="Symbol">(</a><a id="488" href="llpo.html#488" class="Bound">A</a> <a id="490" class="Symbol">:</a> <a id="492" href="llpo.html#81" class="Primitive">𝒰</a> <a id="494" href="llpo.html#340" class="Generalizable">ₙ</a><a id="495" class="Symbol">)</a> <a id="497" class="Symbol">(</a><a id="498" href="llpo.html#498" class="Bound">B</a> <a id="500" class="Symbol">:</a> <a id="502" href="llpo.html#81" class="Primitive">𝒰</a> <a id="504" href="llpo.html#352" class="Generalizable">ₘ</a><a id="505" class="Symbol">)</a> <a id="507" class="Symbol">:</a> <a id="509" href="llpo.html#81" class="Primitive">𝒰</a> <a id="511" class="Symbol">(</a><a id="512" href="llpo.html#494" class="Bound">ₙ</a> <a id="514" href="Agda.Primitive.html#810" class="Primitive Operator">⊔</a> <a id="516" href="llpo.html#504" class="Bound">ₘ</a><a id="517" class="Symbol">)</a> <a id="519" class="Keyword">where</a>
|
||
<a id="_+_.inl"></a><a id="527" href="llpo.html#527" class="InductiveConstructor">inl</a> <a id="531" class="Symbol">:</a> <a id="533" href="llpo.html#488" class="Bound">A</a> <a id="535" class="Symbol">→</a> <a id="537" href="llpo.html#488" class="Bound">A</a> <a id="539" href="llpo.html#483" class="Datatype Operator">+</a> <a id="541" href="llpo.html#498" class="Bound">B</a>
|
||
<a id="_+_.inr"></a><a id="545" href="llpo.html#545" class="InductiveConstructor">inr</a> <a id="549" class="Symbol">:</a> <a id="551" href="llpo.html#498" class="Bound">B</a> <a id="553" class="Symbol">→</a> <a id="555" href="llpo.html#488" class="Bound">A</a> <a id="557" href="llpo.html#483" class="Datatype Operator">+</a> <a id="559" href="llpo.html#498" class="Bound">B</a>
|
||
|
||
<a id="binary-sequence"></a><a id="562" href="llpo.html#562" class="Function">binary-sequence</a> <a id="578" class="Symbol">:</a> <a id="580" href="llpo.html#81" class="Primitive">𝒰₀</a>
|
||
<a id="583" href="llpo.html#562" class="Function">binary-sequence</a> <a id="599" class="Symbol">=</a> <a id="601" href="llpo.html#130" class="Datatype">ℕ</a> <a id="603" class="Symbol">→</a> <a id="605" href="llpo.html#194" class="Datatype">𝟚</a>
|
||
|
||
<a id="all-zeros"></a><a id="610" href="llpo.html#610" class="Function">all-zeros</a> <a id="620" class="Symbol">:</a> <a id="622" href="llpo.html#562" class="Function">binary-sequence</a> <a id="638" class="Symbol">→</a> <a id="640" href="llpo.html#81" class="Primitive">𝒰₀</a>
|
||
<a id="643" href="llpo.html#610" class="Function">all-zeros</a> <a id="653" href="llpo.html#653" class="Bound">α</a> <a id="655" class="Symbol">=</a> <a id="657" class="Symbol">(</a><a id="658" href="llpo.html#658" class="Bound">n</a> <a id="660" class="Symbol">:</a> <a id="662" href="llpo.html#130" class="Datatype">ℕ</a><a id="663" class="Symbol">)</a> <a id="665" class="Symbol">→</a> <a id="667" href="llpo.html#653" class="Bound">α</a> <a id="669" href="llpo.html#658" class="Bound">n</a> <a id="671" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="673" href="llpo.html#206" class="InductiveConstructor">𝟘</a>
|
||
|
||
<a id="has-WLPO"></a><a id="676" href="llpo.html#676" class="Function">has-WLPO</a> <a id="685" class="Symbol">:</a> <a id="687" href="llpo.html#562" class="Function">binary-sequence</a> <a id="703" class="Symbol">→</a> <a id="705" href="llpo.html#81" class="Primitive">𝒰₀</a>
|
||
<a id="708" href="llpo.html#676" class="Function">has-WLPO</a> <a id="717" href="llpo.html#717" class="Bound">α</a> <a id="719" class="Symbol">=</a> <a id="721" href="llpo.html#610" class="Function">all-zeros</a> <a id="731" href="llpo.html#717" class="Bound">α</a> <a id="733" href="llpo.html#483" class="Datatype Operator">+</a> <a id="735" href="llpo.html#437" class="Function Operator">¬</a> <a id="737" class="Symbol">(</a><a id="738" href="llpo.html#610" class="Function">all-zeros</a> <a id="748" href="llpo.html#717" class="Bound">α</a><a id="749" class="Symbol">)</a>
|
||
|
||
<a id="WLPO"></a><a id="755" href="llpo.html#755" class="Function">WLPO</a> <a id="760" class="Symbol">:</a> <a id="762" href="llpo.html#81" class="Primitive">𝒰₀</a>
|
||
<a id="765" href="llpo.html#755" class="Function">WLPO</a> <a id="770" class="Symbol">=</a> <a id="772" class="Symbol">(</a><a id="773" href="llpo.html#773" class="Bound">α</a> <a id="775" class="Symbol">:</a> <a id="777" href="llpo.html#562" class="Function">binary-sequence</a><a id="792" class="Symbol">)</a> <a id="794" class="Symbol">→</a> <a id="796" href="llpo.html#676" class="Function">has-WLPO</a> <a id="805" href="llpo.html#773" class="Bound">α</a>
|
||
|
||
<a id="at-most-one-one"></a><a id="811" href="llpo.html#811" class="Function">at-most-one-one</a> <a id="827" class="Symbol">:</a> <a id="829" href="llpo.html#562" class="Function">binary-sequence</a> <a id="845" class="Symbol">→</a> <a id="847" href="llpo.html#81" class="Primitive">𝒰₀</a>
|
||
<a id="850" href="llpo.html#811" class="Function">at-most-one-one</a> <a id="866" href="llpo.html#866" class="Bound">α</a> <a id="868" class="Symbol">=</a> <a id="870" class="Symbol">(</a><a id="871" href="llpo.html#871" class="Bound">a</a> <a id="873" href="llpo.html#873" class="Bound">b</a> <a id="875" class="Symbol">:</a> <a id="877" href="llpo.html#130" class="Datatype">ℕ</a><a id="878" class="Symbol">)</a> <a id="880" class="Symbol">→</a> <a id="882" href="llpo.html#866" class="Bound">α</a> <a id="884" href="llpo.html#871" class="Bound">a</a> <a id="886" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="888" href="llpo.html#217" class="InductiveConstructor">𝟙</a> <a id="890" class="Symbol">→</a> <a id="892" href="llpo.html#866" class="Bound">α</a> <a id="894" href="llpo.html#873" class="Bound">b</a> <a id="896" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="898" href="llpo.html#217" class="InductiveConstructor">𝟙</a> <a id="900" class="Symbol">→</a> <a id="902" href="llpo.html#871" class="Bound">a</a> <a id="904" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="906" href="llpo.html#873" class="Bound">b</a>
|
||
|
||
<a id="909" class="Comment">-- needed for LLPO</a>
|
||
<a id="dup"></a><a id="928" href="llpo.html#928" class="Function">dup</a> <a id="932" class="Symbol">:</a> <a id="934" href="llpo.html#130" class="Datatype">ℕ</a> <a id="936" class="Symbol">→</a> <a id="938" href="llpo.html#130" class="Datatype">ℕ</a>
|
||
<a id="940" href="llpo.html#928" class="Function">dup</a> <a id="944" class="Number">0</a> <a id="946" class="Symbol">=</a> <a id="948" class="Number">0</a>
|
||
<a id="950" href="llpo.html#928" class="Function">dup</a> <a id="954" class="Symbol">(</a><a id="955" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="959" href="llpo.html#959" class="Bound">n</a><a id="960" class="Symbol">)</a> <a id="962" class="Symbol">=</a> <a id="964" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="968" class="Symbol">(</a><a id="969" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="973" class="Symbol">(</a><a id="974" href="llpo.html#928" class="Function">dup</a> <a id="978" href="llpo.html#959" class="Bound">n</a><a id="979" class="Symbol">))</a>
|
||
|
||
<a id="evens"></a><a id="983" href="llpo.html#983" class="Function">evens</a> <a id="989" class="Symbol">:</a> <a id="991" href="llpo.html#130" class="Datatype">ℕ</a> <a id="993" class="Symbol">→</a> <a id="995" href="llpo.html#130" class="Datatype">ℕ</a>
|
||
<a id="997" href="llpo.html#983" class="Function">evens</a> <a id="1003" class="Symbol">=</a> <a id="1005" href="llpo.html#928" class="Function">dup</a>
|
||
|
||
<a id="odds"></a><a id="1010" href="llpo.html#1010" class="Function">odds</a> <a id="1015" class="Symbol">:</a> <a id="1017" href="llpo.html#130" class="Datatype">ℕ</a> <a id="1019" class="Symbol">→</a> <a id="1021" href="llpo.html#130" class="Datatype">ℕ</a>
|
||
<a id="1023" href="llpo.html#1010" class="Function">odds</a> <a id="1028" class="Symbol">=</a> <a id="1030" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="1034" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="1036" href="llpo.html#928" class="Function">dup</a>
|
||
|
||
<a id="LLPO"></a><a id="1041" href="llpo.html#1041" class="Function">LLPO</a> <a id="1046" class="Symbol">:</a> <a id="1048" href="llpo.html#81" class="Primitive">𝒰₀</a>
|
||
<a id="1051" href="llpo.html#1041" class="Function">LLPO</a> <a id="1056" class="Symbol">=</a> <a id="1058" class="Symbol">(</a><a id="1059" href="llpo.html#1059" class="Bound">α</a> <a id="1061" class="Symbol">:</a> <a id="1063" href="llpo.html#562" class="Function">binary-sequence</a><a id="1078" class="Symbol">)</a> <a id="1080" class="Symbol">→</a> <a id="1082" href="llpo.html#811" class="Function">at-most-one-one</a> <a id="1098" href="llpo.html#1059" class="Bound">α</a> <a id="1100" class="Symbol">→</a> <a id="1102" href="llpo.html#610" class="Function">all-zeros</a> <a id="1112" class="Symbol">(</a><a id="1113" href="llpo.html#1059" class="Bound">α</a> <a id="1115" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="1117" href="llpo.html#983" class="Function">evens</a><a id="1122" class="Symbol">)</a> <a id="1124" href="llpo.html#483" class="Datatype Operator">+</a> <a id="1126" href="llpo.html#610" class="Function">all-zeros</a> <a id="1136" class="Symbol">(</a><a id="1137" href="llpo.html#1059" class="Bound">α</a> <a id="1139" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="1141" href="llpo.html#1010" class="Function">odds</a><a id="1145" class="Symbol">)</a>
|
||
|
||
<a id="1148" class="Comment">{- Eliminators -}</a>
|
||
<a id="⊥-elim"></a><a id="1166" href="llpo.html#1166" class="Function">⊥-elim</a> <a id="1173" class="Symbol">:</a> <a id="1175" href="llpo.html#411" class="Datatype">⊥</a> <a id="1177" class="Symbol">→</a> <a id="1179" href="llpo.html#364" class="Generalizable">A</a>
|
||
<a id="1181" href="llpo.html#1166" class="Function">⊥-elim</a> <a id="1188" class="Symbol">()</a>
|
||
|
||
<a id="+-elim"></a><a id="1192" href="llpo.html#1192" class="Function">+-elim</a> <a id="1199" class="Symbol">:</a> <a id="1201" href="llpo.html#364" class="Generalizable">A</a> <a id="1203" href="llpo.html#483" class="Datatype Operator">+</a> <a id="1205" href="llpo.html#374" class="Generalizable">B</a> <a id="1207" class="Symbol">→</a> <a id="1209" class="Symbol">(</a><a id="1210" href="llpo.html#364" class="Generalizable">A</a> <a id="1212" class="Symbol">→</a> <a id="1214" href="llpo.html#384" class="Generalizable">C</a><a id="1215" class="Symbol">)</a> <a id="1217" class="Symbol">→</a> <a id="1219" class="Symbol">(</a><a id="1220" href="llpo.html#374" class="Generalizable">B</a> <a id="1222" class="Symbol">→</a> <a id="1224" href="llpo.html#384" class="Generalizable">C</a><a id="1225" class="Symbol">)</a> <a id="1227" class="Symbol">→</a> <a id="1229" href="llpo.html#384" class="Generalizable">C</a>
|
||
<a id="1231" href="llpo.html#1192" class="Function">+-elim</a> <a id="1238" class="Symbol">(</a><a id="1239" href="llpo.html#527" class="InductiveConstructor">inl</a> <a id="1243" href="llpo.html#1243" class="Bound">a</a><a id="1244" class="Symbol">)</a> <a id="1246" href="llpo.html#1246" class="Bound">f</a> <a id="1248" class="Symbol">_</a> <a id="1250" class="Symbol">=</a> <a id="1252" href="llpo.html#1246" class="Bound">f</a> <a id="1254" href="llpo.html#1243" class="Bound">a</a>
|
||
<a id="1256" href="llpo.html#1192" class="Function">+-elim</a> <a id="1263" class="Symbol">(</a><a id="1264" href="llpo.html#545" class="InductiveConstructor">inr</a> <a id="1268" href="llpo.html#1268" class="Bound">b</a><a id="1269" class="Symbol">)</a> <a id="1271" class="Symbol">_</a> <a id="1273" href="llpo.html#1273" class="Bound">g</a> <a id="1275" class="Symbol">=</a> <a id="1277" href="llpo.html#1273" class="Bound">g</a> <a id="1279" href="llpo.html#1268" class="Bound">b</a>
|
||
|
||
<a id="1282" class="Comment">-- A bit funky, but comes in handy</a>
|
||
<a id="𝟚-elim"></a><a id="1317" href="llpo.html#1317" class="Function">𝟚-elim</a> <a id="1324" class="Symbol">:</a> <a id="1326" class="Symbol">(</a><a id="1327" href="llpo.html#1327" class="Bound">C</a> <a id="1329" class="Symbol">:</a> <a id="1331" href="llpo.html#194" class="Datatype">𝟚</a> <a id="1333" class="Symbol">→</a> <a id="1335" href="llpo.html#81" class="Primitive">𝒰</a> <a id="1337" href="llpo.html#340" class="Generalizable">ₙ</a><a id="1338" class="Symbol">)</a> <a id="1340" class="Symbol">→</a> <a id="1342" class="Symbol">(</a><a id="1343" href="llpo.html#1343" class="Bound">b</a> <a id="1345" class="Symbol">:</a> <a id="1347" href="llpo.html#194" class="Datatype">𝟚</a><a id="1348" class="Symbol">)</a> <a id="1350" class="Symbol">→</a> <a id="1352" class="Symbol">(</a><a id="1353" href="llpo.html#1343" class="Bound">b</a> <a id="1355" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1357" href="llpo.html#206" class="InductiveConstructor">𝟘</a> <a id="1359" class="Symbol">→</a> <a id="1361" href="llpo.html#1327" class="Bound">C</a> <a id="1363" href="llpo.html#206" class="InductiveConstructor">𝟘</a><a id="1364" class="Symbol">)</a> <a id="1366" class="Symbol">→</a> <a id="1368" class="Symbol">(</a><a id="1369" href="llpo.html#1343" class="Bound">b</a> <a id="1371" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1373" href="llpo.html#217" class="InductiveConstructor">𝟙</a> <a id="1375" class="Symbol">→</a> <a id="1377" href="llpo.html#1327" class="Bound">C</a> <a id="1379" href="llpo.html#217" class="InductiveConstructor">𝟙</a><a id="1380" class="Symbol">)</a> <a id="1382" class="Symbol">→</a> <a id="1384" href="llpo.html#1327" class="Bound">C</a> <a id="1386" href="llpo.html#1343" class="Bound">b</a>
|
||
<a id="1388" href="llpo.html#1317" class="Function">𝟚-elim</a> <a id="1395" class="Symbol">_</a> <a id="1397" href="llpo.html#206" class="InductiveConstructor">𝟘</a> <a id="1399" href="llpo.html#1399" class="Bound">z</a> <a id="1401" class="Symbol">_</a> <a id="1403" class="Symbol">=</a> <a id="1405" href="llpo.html#1399" class="Bound">z</a> <a id="1407" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
<a id="1412" href="llpo.html#1317" class="Function">𝟚-elim</a> <a id="1419" class="Symbol">_</a> <a id="1421" href="llpo.html#217" class="InductiveConstructor">𝟙</a> <a id="1423" class="Symbol">_</a> <a id="1425" href="llpo.html#1425" class="Bound">o</a> <a id="1427" class="Symbol">=</a> <a id="1429" href="llpo.html#1425" class="Bound">o</a> <a id="1431" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="1437" class="Comment">{- Lemmas -}</a>
|
||
|
||
<a id="1451" class="Comment">-- I think this is a bit ugly, but it works and I'm tired</a>
|
||
<a id="e≢o"></a><a id="1509" href="llpo.html#1509" class="Function">e≢o</a> <a id="1513" class="Symbol">:</a> <a id="1515" class="Symbol">{</a><a id="1516" href="llpo.html#1516" class="Bound">n</a> <a id="1518" href="llpo.html#1518" class="Bound">m</a> <a id="1520" class="Symbol">:</a> <a id="1522" href="llpo.html#130" class="Datatype">ℕ</a><a id="1523" class="Symbol">}</a> <a id="1525" class="Symbol">→</a> <a id="1527" href="llpo.html#437" class="Function Operator">¬</a> <a id="1529" class="Symbol">(</a><a id="1530" href="llpo.html#983" class="Function">evens</a> <a id="1536" href="llpo.html#1516" class="Bound">n</a> <a id="1538" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1540" href="llpo.html#1010" class="Function">odds</a> <a id="1545" href="llpo.html#1518" class="Bound">m</a><a id="1546" class="Symbol">)</a>
|
||
<a id="1548" href="llpo.html#1509" class="Function">e≢o</a> <a id="1552" class="Symbol">{</a><a id="1553" href="Agda.Builtin.Nat.html#210" class="InductiveConstructor">zero</a><a id="1557" class="Symbol">}</a> <a id="1559" class="Symbol">{</a><a id="1560" href="Agda.Builtin.Nat.html#210" class="InductiveConstructor">zero</a><a id="1564" class="Symbol">}</a> <a id="1566" class="Symbol">()</a>
|
||
<a id="1569" href="llpo.html#1509" class="Function">e≢o</a> <a id="1573" class="Symbol">{</a><a id="1574" href="Agda.Builtin.Nat.html#210" class="InductiveConstructor">zero</a><a id="1578" class="Symbol">}</a> <a id="1580" class="Symbol">{</a><a id="1581" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="1585" href="llpo.html#1585" class="Bound">m</a><a id="1586" class="Symbol">}</a> <a id="1588" class="Symbol">()</a>
|
||
<a id="1591" href="llpo.html#1509" class="Function">e≢o</a> <a id="1595" class="Symbol">{</a><a id="1596" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="1600" href="llpo.html#1600" class="Bound">n</a><a id="1601" class="Symbol">}</a> <a id="1603" class="Symbol">{</a><a id="1604" href="Agda.Builtin.Nat.html#210" class="InductiveConstructor">zero</a><a id="1608" class="Symbol">}</a> <a id="1610" class="Symbol">()</a>
|
||
<a id="1613" href="llpo.html#1509" class="Function">e≢o</a> <a id="1617" class="Symbol">{</a><a id="1618" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="1622" href="llpo.html#1622" class="Bound">n</a><a id="1623" class="Symbol">}</a> <a id="1625" class="Symbol">{</a><a id="1626" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="1630" href="llpo.html#1630" class="Bound">m</a><a id="1631" class="Symbol">}</a> <a id="1633" href="llpo.html#1633" class="Bound">p</a> <a id="1635" class="Symbol">=</a> <a id="1637" href="llpo.html#1509" class="Function">e≢o</a> <a id="1641" class="Symbol">{</a><a id="1642" href="llpo.html#1622" class="Bound">n</a><a id="1643" class="Symbol">}</a> <a id="1645" class="Symbol">{</a><a id="1646" href="llpo.html#1630" class="Bound">m</a><a id="1647" class="Symbol">}</a> <a id="1649" class="Symbol">(</a><a id="1650" href="llpo.html#1916" class="Function">ds</a> <a id="1653" class="Symbol">(</a><a id="1654" href="llpo.html#1829" class="Function">tr</a> <a id="1657" class="Symbol">(</a><a id="1658" href="llpo.html#1687" class="Function">he</a> <a id="1661" href="llpo.html#1622" class="Bound">n</a><a id="1662" class="Symbol">)</a> <a id="1664" class="Symbol">(</a><a id="1665" href="llpo.html#1759" class="Function">ho</a> <a id="1668" href="llpo.html#1630" class="Bound">m</a><a id="1669" class="Symbol">)</a> <a id="1671" href="llpo.html#1633" class="Bound">p</a><a id="1672" class="Symbol">))</a>
|
||
<a id="1677" class="Keyword">where</a>
|
||
<a id="1687" href="llpo.html#1687" class="Function">he</a> <a id="1690" class="Symbol">:</a> <a id="1692" class="Symbol">(</a><a id="1693" href="llpo.html#1693" class="Bound">q</a> <a id="1695" class="Symbol">:</a> <a id="1697" href="llpo.html#130" class="Datatype">ℕ</a><a id="1698" class="Symbol">)</a> <a id="1700" class="Symbol">→</a> <a id="1702" href="llpo.html#983" class="Function">evens</a> <a id="1708" class="Symbol">(</a><a id="1709" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="1713" href="llpo.html#1693" class="Bound">q</a><a id="1714" class="Symbol">)</a> <a id="1716" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1718" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="1722" class="Symbol">(</a><a id="1723" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="1727" class="Symbol">(</a><a id="1728" href="llpo.html#983" class="Function">evens</a> <a id="1734" href="llpo.html#1693" class="Bound">q</a><a id="1735" class="Symbol">))</a>
|
||
<a id="1742" href="llpo.html#1687" class="Function">he</a> <a id="1745" class="Symbol">_</a> <a id="1747" class="Symbol">=</a> <a id="1749" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="1759" href="llpo.html#1759" class="Function">ho</a> <a id="1762" class="Symbol">:</a> <a id="1764" class="Symbol">(</a><a id="1765" href="llpo.html#1765" class="Bound">q</a> <a id="1767" class="Symbol">:</a> <a id="1769" href="llpo.html#130" class="Datatype">ℕ</a><a id="1770" class="Symbol">)</a> <a id="1772" class="Symbol">→</a> <a id="1774" href="llpo.html#1010" class="Function">odds</a> <a id="1779" class="Symbol">(</a><a id="1780" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="1784" href="llpo.html#1765" class="Bound">q</a><a id="1785" class="Symbol">)</a> <a id="1787" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1789" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="1793" class="Symbol">(</a><a id="1794" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="1798" class="Symbol">(</a><a id="1799" href="llpo.html#1010" class="Function">odds</a> <a id="1804" href="llpo.html#1765" class="Bound">q</a><a id="1805" class="Symbol">))</a>
|
||
<a id="1812" href="llpo.html#1759" class="Function">ho</a> <a id="1815" class="Symbol">_</a> <a id="1817" class="Symbol">=</a> <a id="1819" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="1829" href="llpo.html#1829" class="Function">tr</a> <a id="1832" class="Symbol">:</a> <a id="1834" class="Symbol">∀</a> <a id="1836" class="Symbol">{</a><a id="1837" href="llpo.html#1837" class="Bound">a</a> <a id="1839" href="llpo.html#1839" class="Bound">b</a> <a id="1841" href="llpo.html#1841" class="Bound">c</a> <a id="1843" href="llpo.html#1843" class="Bound">d</a> <a id="1845" class="Symbol">:</a> <a id="1847" href="llpo.html#130" class="Datatype">ℕ</a><a id="1848" class="Symbol">}</a> <a id="1850" class="Symbol">→</a> <a id="1852" href="llpo.html#1837" class="Bound">a</a> <a id="1854" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1856" href="llpo.html#1839" class="Bound">b</a> <a id="1858" class="Symbol">→</a> <a id="1860" href="llpo.html#1841" class="Bound">c</a> <a id="1862" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1864" href="llpo.html#1843" class="Bound">d</a> <a id="1866" class="Symbol">→</a> <a id="1868" href="llpo.html#1837" class="Bound">a</a> <a id="1870" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1872" href="llpo.html#1841" class="Bound">c</a> <a id="1874" class="Symbol">→</a> <a id="1876" href="llpo.html#1839" class="Bound">b</a> <a id="1878" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1880" href="llpo.html#1843" class="Bound">d</a>
|
||
<a id="1886" href="llpo.html#1829" class="Function">tr</a> <a id="1889" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1894" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1899" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="1904" class="Symbol">=</a> <a id="1906" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
<a id="1916" href="llpo.html#1916" class="Function">ds</a> <a id="1919" class="Symbol">:</a> <a id="1921" class="Symbol">∀</a> <a id="1923" class="Symbol">{</a><a id="1924" href="llpo.html#1924" class="Bound">q</a> <a id="1926" href="llpo.html#1926" class="Bound">r</a> <a id="1928" class="Symbol">:</a> <a id="1930" href="llpo.html#130" class="Datatype">ℕ</a><a id="1931" class="Symbol">}</a> <a id="1933" class="Symbol">→</a> <a id="1935" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="1939" class="Symbol">(</a><a id="1940" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="1944" href="llpo.html#1924" class="Bound">q</a><a id="1945" class="Symbol">)</a> <a id="1947" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1949" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="1953" class="Symbol">(</a><a id="1954" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="1958" href="llpo.html#1926" class="Bound">r</a><a id="1959" class="Symbol">)</a> <a id="1961" class="Symbol">→</a> <a id="1963" href="llpo.html#1924" class="Bound">q</a> <a id="1965" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">≡</a> <a id="1967" href="llpo.html#1926" class="Bound">r</a>
|
||
<a id="1973" href="llpo.html#1916" class="Function">ds</a> <a id="1976" class="Symbol">{</a><a id="1977" href="Agda.Builtin.Nat.html#210" class="InductiveConstructor">zero</a><a id="1981" class="Symbol">}</a> <a id="1983" class="Symbol">{</a><a id="1984" href="Agda.Builtin.Nat.html#210" class="InductiveConstructor">zero</a><a id="1988" class="Symbol">}</a> <a id="1990" class="Symbol">_</a> <a id="1992" class="Symbol">=</a> <a id="1994" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
<a id="2003" href="llpo.html#1916" class="Function">ds</a> <a id="2006" class="Symbol">{</a><a id="2007" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="2011" href="llpo.html#2011" class="Bound">q</a><a id="2012" class="Symbol">}</a> <a id="2014" class="Symbol">{</a><a id="2015" href="Agda.Builtin.Nat.html#223" class="InductiveConstructor">suc</a> <a id="2019" href="llpo.html#2019" class="Bound">r</a><a id="2020" class="Symbol">}</a> <a id="2022" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a> <a id="2027" class="Symbol">=</a> <a id="2029" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a>
|
||
|
||
|
||
<a id="lemma"></a><a id="2036" href="llpo.html#2036" class="Function">lemma</a> <a id="2042" class="Symbol">:</a> <a id="2044" class="Symbol">(</a><a id="2045" href="llpo.html#2045" class="Bound">α</a> <a id="2047" class="Symbol">:</a> <a id="2049" href="llpo.html#562" class="Function">binary-sequence</a><a id="2064" class="Symbol">)</a> <a id="2066" class="Symbol">→</a> <a id="2068" href="llpo.html#811" class="Function">at-most-one-one</a> <a id="2084" href="llpo.html#2045" class="Bound">α</a> <a id="2086" class="Symbol">→</a> <a id="2088" href="llpo.html#437" class="Function Operator">¬</a> <a id="2090" href="llpo.html#610" class="Function">all-zeros</a> <a id="2100" class="Symbol">(</a><a id="2101" href="llpo.html#2045" class="Bound">α</a> <a id="2103" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="2105" href="llpo.html#983" class="Function">evens</a><a id="2110" class="Symbol">)</a> <a id="2112" class="Symbol">→</a> <a id="2114" href="llpo.html#610" class="Function">all-zeros</a> <a id="2124" class="Symbol">(</a><a id="2125" href="llpo.html#2045" class="Bound">α</a> <a id="2127" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="2129" href="llpo.html#1010" class="Function">odds</a><a id="2133" class="Symbol">)</a>
|
||
<a id="2135" href="llpo.html#2036" class="Function">lemma</a> <a id="2141" href="llpo.html#2141" class="Bound">α</a> <a id="2143" href="llpo.html#2143" class="Bound">am11</a> <a id="2148" href="llpo.html#2148" class="Bound">na0e</a> <a id="2153" href="llpo.html#2153" class="Bound">i</a> <a id="2155" class="Symbol">=</a> <a id="2157" href="llpo.html#1317" class="Function">𝟚-elim</a> <a id="2164" class="Symbol">(</a><a id="2165" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡</a> <a id="2168" href="llpo.html#206" class="InductiveConstructor">𝟘</a><a id="2169" class="Symbol">)</a> <a id="2171" class="Symbol">((</a><a id="2173" href="llpo.html#2141" class="Bound">α</a> <a id="2175" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="2177" href="llpo.html#1010" class="Function">odds</a><a id="2181" class="Symbol">)</a> <a id="2183" href="llpo.html#2153" class="Bound">i</a><a id="2184" class="Symbol">)</a>
|
||
<a id="2215" class="Symbol">(</a><a id="2216" href="Function.Base.html#636" class="Function">const</a> <a id="2222" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a><a id="2226" class="Symbol">)</a>
|
||
<a id="2257" class="Symbol">(λ</a> <a id="2260" href="llpo.html#2260" class="Bound">p₁</a> <a id="2263" class="Symbol">→</a> <a id="2265" href="llpo.html#1166" class="Function">⊥-elim</a> <a id="2272" class="Symbol">(</a><a id="2273" href="llpo.html#2148" class="Bound">na0e</a> <a id="2278" class="Symbol">(λ</a> <a id="2281" href="llpo.html#2281" class="Bound">j</a> <a id="2283" class="Symbol">→</a> <a id="2285" href="llpo.html#1317" class="Function">𝟚-elim</a> <a id="2292" class="Symbol">(</a><a id="2293" href="Agda.Builtin.Equality.html#151" class="Datatype Operator">_≡</a> <a id="2296" href="llpo.html#206" class="InductiveConstructor">𝟘</a><a id="2297" class="Symbol">)</a> <a id="2299" class="Symbol">((</a><a id="2301" href="llpo.html#2141" class="Bound">α</a> <a id="2303" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="2305" href="llpo.html#983" class="Function">evens</a><a id="2310" class="Symbol">)</a> <a id="2312" href="llpo.html#2281" class="Bound">j</a><a id="2313" class="Symbol">)</a>
|
||
<a id="2379" class="Symbol">(</a><a id="2380" href="Function.Base.html#636" class="Function">const</a> <a id="2386" href="Agda.Builtin.Equality.html#208" class="InductiveConstructor">refl</a><a id="2390" class="Symbol">)</a>
|
||
<a id="2456" class="Symbol">(λ</a> <a id="2459" href="llpo.html#2459" class="Bound">p₂</a> <a id="2462" class="Symbol">→</a> <a id="2464" href="llpo.html#1166" class="Function">⊥-elim</a> <a id="2471" class="Symbol">(</a><a id="2472" href="llpo.html#1509" class="Function">e≢o</a> <a id="2476" class="Symbol">(</a><a id="2477" href="llpo.html#2143" class="Bound">am11</a> <a id="2482" class="Symbol">(</a><a id="2483" href="llpo.html#983" class="Function">evens</a> <a id="2489" href="llpo.html#2281" class="Bound">j</a><a id="2490" class="Symbol">)</a> <a id="2492" class="Symbol">(</a><a id="2493" href="llpo.html#1010" class="Function">odds</a> <a id="2498" href="llpo.html#2153" class="Bound">i</a><a id="2499" class="Symbol">)</a> <a id="2501" href="llpo.html#2459" class="Bound">p₂</a> <a id="2504" href="llpo.html#2260" class="Bound">p₁</a><a id="2506" class="Symbol">))))))</a>
|
||
|
||
|
||
<a id="2515" class="Comment">{- The main dish -}</a>
|
||
<a id="WLPO→LLPO"></a><a id="2535" href="llpo.html#2535" class="Function">WLPO→LLPO</a> <a id="2545" class="Symbol">:</a> <a id="2547" href="llpo.html#755" class="Function">WLPO</a> <a id="2552" class="Symbol">→</a> <a id="2554" href="llpo.html#1041" class="Function">LLPO</a>
|
||
<a id="2559" href="llpo.html#2535" class="Function">WLPO→LLPO</a> <a id="2569" href="llpo.html#2569" class="Bound">wlpo</a> <a id="2574" href="llpo.html#2574" class="Bound">α</a> <a id="2576" href="llpo.html#2576" class="Bound">am11</a> <a id="2581" class="Symbol">=</a> <a id="2583" href="llpo.html#1192" class="Function">+-elim</a> <a id="2590" class="Symbol">(</a><a id="2591" href="llpo.html#2569" class="Bound">wlpo</a> <a id="2596" class="Symbol">(</a><a id="2597" href="llpo.html#2574" class="Bound">α</a> <a id="2599" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="2601" href="llpo.html#983" class="Function">evens</a><a id="2606" class="Symbol">))</a>
|
||
<a id="2639" href="llpo.html#527" class="InductiveConstructor">inl</a>
|
||
<a id="2673" class="Symbol">(λ</a> <a id="2676" href="llpo.html#2676" class="Bound">na0e</a> <a id="2681" class="Symbol">→</a> <a id="2683" href="llpo.html#1192" class="Function">+-elim</a> <a id="2690" class="Symbol">(</a><a id="2691" href="llpo.html#2569" class="Bound">wlpo</a> <a id="2696" class="Symbol">(</a><a id="2697" href="llpo.html#2574" class="Bound">α</a> <a id="2699" href="Function.Base.html#1031" class="Function Operator">∘</a> <a id="2701" href="llpo.html#1010" class="Function">odds</a><a id="2705" class="Symbol">))</a>
|
||
<a id="2755" href="llpo.html#545" class="InductiveConstructor">inr</a>
|
||
<a id="2806" class="Symbol">(λ</a> <a id="2809" href="llpo.html#2809" class="Bound">na0o</a> <a id="2814" class="Symbol">→</a> <a id="2816" href="llpo.html#1166" class="Function">⊥-elim</a> <a id="2823" class="Symbol">(</a><a id="2824" href="llpo.html#2809" class="Bound">na0o</a> <a id="2829" class="Symbol">(</a><a id="2830" href="llpo.html#2036" class="Function">lemma</a> <a id="2836" href="llpo.html#2574" class="Bound">α</a> <a id="2838" href="llpo.html#2576" class="Bound">am11</a> <a id="2843" href="llpo.html#2676" class="Bound">na0e</a><a id="2847" class="Symbol">))))</a>
|
||
</pre></body></html> |