4 files changed, 244 insertions, 0 deletions
diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html
new file mode 100644
index 0000000..1be20f5
--- /dev/null
+++ b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html
@@ -0,0 +1,55 @@
+<!DOCTYPE HTML>
+<html><head><meta charset="utf-8"><title>Agda.Primitive.Cubical</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">--cubical</a> <a id="23" class="Pragma">--no-subtyping</a> <a id="38" class="Symbol">#-}</a>
+
+<a id="43" class="Keyword">module</a> <a id="50" href="Agda.Primitive.Cubical.html" class="Module">Agda.Primitive.Cubical</a> <a id="73" class="Keyword">where</a>
+
+<a id="80" class="Symbol">{-#</a> <a id="84" class="Keyword">BUILTIN</a> <a id="92" class="Keyword">INTERVAL</a> <a id="I"></a><a id="101" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a>  <a id="104" class="Symbol">#-}</a>  <a id="109" class="Comment">-- I : Setω</a>
+
+<a id="122" class="Symbol">{-#</a> <a id="126" class="Keyword">BUILTIN</a> <a id="134" class="Keyword">IZERO</a>    <a id="i0"></a><a id="143" href="Agda.Primitive.Cubical.html#143" class="InductiveConstructor">i0</a> <a id="146" class="Symbol">#-}</a>
+<a id="150" class="Symbol">{-#</a> <a id="154" class="Keyword">BUILTIN</a> <a id="162" class="Keyword">IONE</a>     <a id="i1"></a><a id="171" href="Agda.Primitive.Cubical.html#171" class="InductiveConstructor">i1</a> <a id="174" class="Symbol">#-}</a>
+
+<a id="179" class="Keyword">infix</a>  <a id="186" class="Number">30</a> <a id="189" href="Agda.Primitive.Cubical.html#291" class="Primitive">primINeg</a>
+<a id="198" class="Keyword">infixr</a> <a id="205" class="Number">20</a> <a id="208" href="Agda.Primitive.Cubical.html#241" class="Primitive">primIMin</a> <a id="217" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a>
+
+<a id="227" class="Keyword">primitive</a>
+    <a id="primIMin"></a><a id="241" href="Agda.Primitive.Cubical.html#241" class="Primitive">primIMin</a> <a id="250" class="Symbol">:</a> <a id="252" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="254" class="Symbol">→</a> <a id="256" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="258" class="Symbol">→</a> <a id="260" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a>
+    <a id="primIMax"></a><a id="266" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> <a id="275" class="Symbol">:</a> <a id="277" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="279" class="Symbol">→</a> <a id="281" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="283" class="Symbol">→</a> <a id="285" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a>
+    <a id="primINeg"></a><a id="291" href="Agda.Primitive.Cubical.html#291" class="Primitive">primINeg</a> <a id="300" class="Symbol">:</a> <a id="302" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a> <a id="304" class="Symbol">→</a> <a id="306" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a>
+
+<a id="309" class="Symbol">{-#</a> <a id="313" class="Keyword">BUILTIN</a> <a id="321" class="Keyword">ISONE</a>    <a id="IsOne"></a><a id="330" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a>    <a id="339" class="Symbol">#-}</a>  <a id="344" class="Comment">-- IsOne : I → Setω</a>
+
+<a id="365" class="Keyword">postulate</a>
+  <a id="itIsOne"></a><a id="377" href="Agda.Primitive.Cubical.html#377" class="Postulate">itIsOne</a> <a id="385" class="Symbol">:</a> <a id="387" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="393" href="Agda.Primitive.Cubical.html#171" class="InductiveConstructor">i1</a>
+  <a id="IsOne1"></a><a id="398" href="Agda.Primitive.Cubical.html#398" class="Postulate">IsOne1</a>  <a id="406" class="Symbol">:</a> <a id="408" class="Symbol">∀</a> <a id="410" href="Agda.Primitive.Cubical.html#410" class="Bound">i</a> <a id="412" href="Agda.Primitive.Cubical.html#412" class="Bound">j</a> <a id="414" class="Symbol">→</a> <a id="416" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="422" href="Agda.Primitive.Cubical.html#410" class="Bound">i</a> <a id="424" class="Symbol">→</a> <a id="426" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="432" class="Symbol">(</a><a id="433" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> <a id="442" href="Agda.Primitive.Cubical.html#410" class="Bound">i</a> <a id="444" href="Agda.Primitive.Cubical.html#412" class="Bound">j</a><a id="445" class="Symbol">)</a>
+  <a id="IsOne2"></a><a id="449" href="Agda.Primitive.Cubical.html#449" class="Postulate">IsOne2</a>  <a id="457" class="Symbol">:</a> <a id="459" class="Symbol">∀</a> <a id="461" href="Agda.Primitive.Cubical.html#461" class="Bound">i</a> <a id="463" href="Agda.Primitive.Cubical.html#463" class="Bound">j</a> <a id="465" class="Symbol">→</a> <a id="467" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="473" href="Agda.Primitive.Cubical.html#463" class="Bound">j</a> <a id="475" class="Symbol">→</a> <a id="477" href="Agda.Primitive.Cubical.html#330" class="Postulate">IsOne</a> <a id="483" class="Symbol">(</a><a id="484" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> <a id="493" href="Agda.Primitive.Cubical.html#461" class="Bound">i</a> <a id="495" href="Agda.Primitive.Cubical.html#463" class="Bound">j</a><a id="496" class="Symbol">)</a>
+
+<a id="499" class="Symbol">{-#</a> <a id="503" class="Keyword">BUILTIN</a> <a id="511" class="Keyword">ITISONE</a>  <a id="520" href="Agda.Primitive.Cubical.html#377" class="Postulate">itIsOne</a>  <a id="529" class="Symbol">#-}</a>
+<a id="533" class="Symbol">{-#</a> <a id="537" class="Keyword">BUILTIN</a> <a id="545" class="Keyword">ISONE1</a>   <a id="554" href="Agda.Primitive.Cubical.html#398" class="Postulate">IsOne1</a>   <a id="563" class="Symbol">#-}</a>
+<a id="567" class="Symbol">{-#</a> <a id="571" class="Keyword">BUILTIN</a> <a id="579" class="Keyword">ISONE2</a>   <a id="588" href="Agda.Primitive.Cubical.html#449" class="Postulate">IsOne2</a>   <a id="597" class="Symbol">#-}</a>
+
+<a id="602" class="Comment">-- Partial : ∀{ℓ} (i : I) (A : Set ℓ) → Set ℓ</a>
+<a id="648" class="Comment">-- Partial i A = IsOne i → A</a>
+
+<a id="678" class="Symbol">{-#</a> <a id="682" class="Keyword">BUILTIN</a> <a id="690" class="Keyword">PARTIAL</a>  <a id="Partial"></a><a id="699" href="Agda.Primitive.Cubical.html#699" class="Primitive">Partial</a>  <a id="708" class="Symbol">#-}</a>
+<a id="712" class="Symbol">{-#</a> <a id="716" class="Keyword">BUILTIN</a> <a id="724" class="Keyword">PARTIALP</a> <a id="PartialP"></a><a id="733" href="Agda.Primitive.Cubical.html#733" class="Primitive">PartialP</a> <a id="742" class="Symbol">#-}</a>
+
+<a id="747" class="Keyword">postulate</a>
+  <a id="isOneEmpty"></a><a id="759" href="Agda.Primitive.Cubical.html#759" class="Postulate">isOneEmpty</a> <a id="770" class="Symbol">:</a> <a id="772" class="Symbol">∀</a> <a id="774" class="Symbol">{</a><a id="775" href="Agda.Primitive.Cubical.html#775" class="Bound">ℓ</a><a id="776" class="Symbol">}</a> <a id="778" class="Symbol">{</a><a id="779" href="Agda.Primitive.Cubical.html#779" class="Bound">A</a> <a id="781" class="Symbol">:</a> <a id="783" href="Agda.Primitive.Cubical.html#699" class="Primitive">Partial</a> <a id="791" href="Agda.Primitive.Cubical.html#143" class="InductiveConstructor">i0</a> <a id="794" class="Symbol">(</a><a id="795" class="PrimitiveType">Set</a> <a id="799" href="Agda.Primitive.Cubical.html#775" class="Bound">ℓ</a><a id="800" class="Symbol">)}</a> <a id="803" class="Symbol">→</a> <a id="805" href="Agda.Primitive.Cubical.html#733" class="Primitive">PartialP</a> <a id="814" href="Agda.Primitive.Cubical.html#143" class="InductiveConstructor">i0</a> <a id="817" href="Agda.Primitive.Cubical.html#779" class="Bound">A</a>
+
+<a id="820" class="Symbol">{-#</a> <a id="824" class="Keyword">BUILTIN</a> <a id="832" class="Keyword">ISONEEMPTY</a> <a id="843" href="Agda.Primitive.Cubical.html#759" class="Postulate">isOneEmpty</a> <a id="854" class="Symbol">#-}</a>
+
+<a id="859" class="Keyword">primitive</a>
+  <a id="primPOr"></a><a id="871" href="Agda.Primitive.Cubical.html#871" class="Primitive">primPOr</a> <a id="879" class="Symbol">:</a> <a id="881" class="Symbol">∀</a> <a id="883" class="Symbol">{</a><a id="884" href="Agda.Primitive.Cubical.html#884" class="Bound">ℓ</a><a id="885" class="Symbol">}</a> <a id="887" class="Symbol">(</a><a id="888" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="890" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a> <a id="892" class="Symbol">:</a> <a id="894" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="895" class="Symbol">)</a> <a id="897" class="Symbol">{</a><a id="898" href="Agda.Primitive.Cubical.html#898" class="Bound">A</a> <a id="900" class="Symbol">:</a> <a id="902" href="Agda.Primitive.Cubical.html#699" class="Primitive">Partial</a> <a id="910" class="Symbol">(</a><a id="911" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> <a id="920" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="922" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a><a id="923" class="Symbol">)</a> <a id="925" class="Symbol">(</a><a id="926" class="PrimitiveType">Set</a> <a id="930" href="Agda.Primitive.Cubical.html#884" class="Bound">ℓ</a><a id="931" class="Symbol">)}</a>
+            <a id="946" class="Symbol">→</a> <a id="948" class="Symbol">(</a><a id="949" href="Agda.Primitive.Cubical.html#949" class="Bound">u</a> <a id="951" class="Symbol">:</a> <a id="953" href="Agda.Primitive.Cubical.html#733" class="Primitive">PartialP</a> <a id="962" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="964" class="Symbol">(λ</a> <a id="967" href="Agda.Primitive.Cubical.html#967" class="Bound">z</a> <a id="969" class="Symbol">→</a> <a id="971" href="Agda.Primitive.Cubical.html#898" class="Bound">A</a> <a id="973" class="Symbol">(</a><a id="974" href="Agda.Primitive.Cubical.html#398" class="Postulate">IsOne1</a> <a id="981" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="983" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a> <a id="985" href="Agda.Primitive.Cubical.html#967" class="Bound">z</a><a id="986" class="Symbol">)))</a>
+            <a id="1002" class="Symbol">→</a> <a id="1004" class="Symbol">(</a><a id="1005" href="Agda.Primitive.Cubical.html#1005" class="Bound">v</a> <a id="1007" class="Symbol">:</a> <a id="1009" href="Agda.Primitive.Cubical.html#733" class="Primitive">PartialP</a> <a id="1018" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a> <a id="1020" class="Symbol">(λ</a> <a id="1023" href="Agda.Primitive.Cubical.html#1023" class="Bound">z</a> <a id="1025" class="Symbol">→</a> <a id="1027" href="Agda.Primitive.Cubical.html#898" class="Bound">A</a> <a id="1029" class="Symbol">(</a><a id="1030" href="Agda.Primitive.Cubical.html#449" class="Postulate">IsOne2</a> <a id="1037" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="1039" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a> <a id="1041" href="Agda.Primitive.Cubical.html#1023" class="Bound">z</a><a id="1042" class="Symbol">)))</a>
+            <a id="1058" class="Symbol">→</a> <a id="1060" href="Agda.Primitive.Cubical.html#733" class="Primitive">PartialP</a> <a id="1069" class="Symbol">(</a><a id="1070" href="Agda.Primitive.Cubical.html#266" class="Primitive">primIMax</a> <a id="1079" href="Agda.Primitive.Cubical.html#888" class="Bound">i</a> <a id="1081" href="Agda.Primitive.Cubical.html#890" class="Bound">j</a><a id="1082" class="Symbol">)</a> <a id="1084" href="Agda.Primitive.Cubical.html#898" class="Bound">A</a>
+
+  <a id="1089" class="Comment">-- Computes in terms of primHComp and primTransp</a>
+  <a id="primComp"></a><a id="1140" href="Agda.Primitive.Cubical.html#1140" class="Primitive">primComp</a> <a id="1149" class="Symbol">:</a> <a id="1151" class="Symbol">∀</a> <a id="1153" class="Symbol">{</a><a id="1154" href="Agda.Primitive.Cubical.html#1154" class="Bound">ℓ</a><a id="1155" class="Symbol">}</a> <a id="1157" class="Symbol">(</a><a id="1158" href="Agda.Primitive.Cubical.html#1158" class="Bound">A</a> <a id="1160" class="Symbol">:</a> <a id="1162" class="Symbol">(</a><a id="1163" href="Agda.Primitive.Cubical.html#1163" class="Bound">i</a> <a id="1165" class="Symbol">:</a> <a id="1167" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="1168" class="Symbol">)</a> <a id="1170" class="Symbol">→</a> <a id="1172" class="PrimitiveType">Set</a> <a id="1176" class="Symbol">(</a><a id="1177" href="Agda.Primitive.Cubical.html#1154" class="Bound">ℓ</a> <a id="1179" href="Agda.Primitive.Cubical.html#1163" class="Bound">i</a><a id="1180" class="Symbol">))</a> <a id="1183" class="Symbol">{</a><a id="1184" href="Agda.Primitive.Cubical.html#1184" class="Bound">φ</a> <a id="1186" class="Symbol">:</a> <a id="1188" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="1189" class="Symbol">}</a> <a id="1191" class="Symbol">(</a><a id="1192" href="Agda.Primitive.Cubical.html#1192" class="Bound">u</a> <a id="1194" class="Symbol">:</a> <a id="1196" class="Symbol">∀</a> <a id="1198" href="Agda.Primitive.Cubical.html#1198" class="Bound">i</a> <a id="1200" class="Symbol">→</a> <a id="1202" href="Agda.Primitive.Cubical.html#699" class="Primitive">Partial</a> <a id="1210" href="Agda.Primitive.Cubical.html#1184" class="Bound">φ</a> <a id="1212" class="Symbol">(</a><a id="1213" href="Agda.Primitive.Cubical.html#1158" class="Bound">A</a> <a id="1215" href="Agda.Primitive.Cubical.html#1198" class="Bound">i</a><a id="1216" class="Symbol">))</a> <a id="1219" class="Symbol">(</a><a id="1220" href="Agda.Primitive.Cubical.html#1220" class="Bound">a</a> <a id="1222" class="Symbol">:</a> <a id="1224" href="Agda.Primitive.Cubical.html#1158" class="Bound">A</a> <a id="1226" href="Agda.Primitive.Cubical.html#143" class="InductiveConstructor">i0</a><a id="1228" class="Symbol">)</a> <a id="1230" class="Symbol">→</a> <a id="1232" href="Agda.Primitive.Cubical.html#1158" class="Bound">A</a> <a id="1234" href="Agda.Primitive.Cubical.html#171" class="InductiveConstructor">i1</a>
+
+<a id="1238" class="Keyword">syntax</a> <a id="1245" href="Agda.Primitive.Cubical.html#871" class="Primitive">primPOr</a> <a id="1253" class="Bound">p</a> <a id="1255" class="Bound">q</a> <a id="1257" class="Bound">u</a> <a id="1259" class="Bound">t</a> <a id="1261" class="Symbol">=</a> <a id="1263" class="Primitive">[</a> <a id="1265" class="Bound">p</a> <a id="1267" class="Primitive">↦</a> <a id="1269" class="Bound">u</a> <a id="1271" class="Primitive">,</a> <a id="1273" class="Bound">q</a> <a id="1275" class="Primitive">↦</a> <a id="1277" class="Bound">t</a> <a id="1279" class="Primitive">]</a>
+
+<a id="1282" class="Keyword">primitive</a>
+  <a id="primTransp"></a><a id="1294" href="Agda.Primitive.Cubical.html#1294" class="Primitive">primTransp</a> <a id="1305" class="Symbol">:</a> <a id="1307" class="Symbol">∀</a> <a id="1309" class="Symbol">{</a><a id="1310" href="Agda.Primitive.Cubical.html#1310" class="Bound">ℓ</a><a id="1311" class="Symbol">}</a> <a id="1313" class="Symbol">(</a><a id="1314" href="Agda.Primitive.Cubical.html#1314" class="Bound">A</a> <a id="1316" class="Symbol">:</a> <a id="1318" class="Symbol">(</a><a id="1319" href="Agda.Primitive.Cubical.html#1319" class="Bound">i</a> <a id="1321" class="Symbol">:</a> <a id="1323" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="1324" class="Symbol">)</a> <a id="1326" class="Symbol">→</a> <a id="1328" class="PrimitiveType">Set</a> <a id="1332" class="Symbol">(</a><a id="1333" href="Agda.Primitive.Cubical.html#1310" class="Bound">ℓ</a> <a id="1335" href="Agda.Primitive.Cubical.html#1319" class="Bound">i</a><a id="1336" class="Symbol">))</a> <a id="1339" class="Symbol">(</a><a id="1340" href="Agda.Primitive.Cubical.html#1340" class="Bound">φ</a> <a id="1342" class="Symbol">:</a> <a id="1344" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="1345" class="Symbol">)</a> <a id="1347" class="Symbol">(</a><a id="1348" href="Agda.Primitive.Cubical.html#1348" class="Bound">a</a> <a id="1350" class="Symbol">:</a> <a id="1352" href="Agda.Primitive.Cubical.html#1314" class="Bound">A</a> <a id="1354" href="Agda.Primitive.Cubical.html#143" class="InductiveConstructor">i0</a><a id="1356" class="Symbol">)</a> <a id="1358" class="Symbol">→</a> <a id="1360" href="Agda.Primitive.Cubical.html#1314" class="Bound">A</a> <a id="1362" href="Agda.Primitive.Cubical.html#171" class="InductiveConstructor">i1</a>
+  <a id="primHComp"></a><a id="1367" href="Agda.Primitive.Cubical.html#1367" class="Primitive">primHComp</a>  <a id="1378" class="Symbol">:</a> <a id="1380" class="Symbol">∀</a> <a id="1382" class="Symbol">{</a><a id="1383" href="Agda.Primitive.Cubical.html#1383" class="Bound">ℓ</a><a id="1384" class="Symbol">}</a> <a id="1386" class="Symbol">{</a><a id="1387" href="Agda.Primitive.Cubical.html#1387" class="Bound">A</a> <a id="1389" class="Symbol">:</a> <a id="1391" class="PrimitiveType">Set</a> <a id="1395" href="Agda.Primitive.Cubical.html#1383" class="Bound">ℓ</a><a id="1396" class="Symbol">}</a> <a id="1398" class="Symbol">{</a><a id="1399" href="Agda.Primitive.Cubical.html#1399" class="Bound">φ</a> <a id="1401" class="Symbol">:</a> <a id="1403" href="Agda.Primitive.Cubical.html#101" class="Datatype">I</a><a id="1404" class="Symbol">}</a> <a id="1406" class="Symbol">(</a><a id="1407" href="Agda.Primitive.Cubical.html#1407" class="Bound">u</a> <a id="1409" class="Symbol">:</a> <a id="1411" class="Symbol">∀</a> <a id="1413" href="Agda.Primitive.Cubical.html#1413" class="Bound">i</a> <a id="1415" class="Symbol">→</a> <a id="1417" href="Agda.Primitive.Cubical.html#699" class="Primitive">Partial</a> <a id="1425" href="Agda.Primitive.Cubical.html#1399" class="Bound">φ</a> <a id="1427" href="Agda.Primitive.Cubical.html#1387" class="Bound">A</a><a id="1428" class="Symbol">)</a> <a id="1430" class="Symbol">(</a><a id="1431" href="Agda.Primitive.Cubical.html#1431" class="Bound">a</a> <a id="1433" class="Symbol">:</a> <a id="1435" href="Agda.Primitive.Cubical.html#1387" class="Bound">A</a><a id="1436" class="Symbol">)</a> <a id="1438" class="Symbol">→</a> <a id="1440" href="Agda.Primitive.Cubical.html#1387" class="Bound">A</a>
+</pre></body></html>
+\ No newline at end of file
diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html
new file mode 100644
index 0000000..5829754
--- /dev/null
+++ b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html
@@ -0,0 +1,35 @@
+<!DOCTYPE HTML>
+<html><head><meta charset="utf-8"><title>Agda.Primitive</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Comment">-- The Agda primitives (preloaded).</a>
+
+<a id="38" class="Symbol">{-#</a> <a id="42" class="Keyword">OPTIONS</a> <a id="50" class="Pragma">--without-K</a> <a id="62" class="Pragma">--no-subtyping</a> <a id="77" class="Symbol">#-}</a>
+
+<a id="82" class="Keyword">module</a> <a id="89" href="Agda.Primitive.html" class="Module">Agda.Primitive</a> <a id="104" class="Keyword">where</a>
+
+<a id="111" class="Comment">------------------------------------------------------------------------</a>
+<a id="184" class="Comment">-- Universe levels</a>
+<a id="203" class="Comment">------------------------------------------------------------------------</a>
+
+<a id="277" class="Keyword">infixl</a> <a id="284" class="Number">6</a> <a id="286" href="Agda.Primitive.html#636" class="Primitive Operator">_⊔_</a>
+
+<a id="291" class="Comment">-- Level is the first thing we need to define.</a>
+<a id="338" class="Comment">-- The other postulates can only be checked if built-in Level is known.</a>
+
+<a id="411" class="Keyword">postulate</a>
+  <a id="Level"></a><a id="423" href="Agda.Primitive.html#423" class="Postulate">Level</a> <a id="429" class="Symbol">:</a> <a id="431" class="PrimitiveType">Set</a>
+
+<a id="436" class="Comment">-- MAlonzo compiles Level to (). This should be safe, because it is</a>
+<a id="504" class="Comment">-- not possible to pattern match on levels.</a>
+
+<a id="549" class="Symbol">{-#</a> <a id="553" class="Keyword">BUILTIN</a> <a id="561" class="Keyword">LEVEL</a> <a id="567" href="Agda.Primitive.html#423" class="Postulate">Level</a> <a id="573" class="Symbol">#-}</a>
+
+<a id="578" class="Keyword">postulate</a>
+  <a id="lzero"></a><a id="590" href="Agda.Primitive.html#590" class="Postulate">lzero</a> <a id="596" class="Symbol">:</a> <a id="598" href="Agda.Primitive.html#423" class="Postulate">Level</a>
+  <a id="lsuc"></a><a id="606" href="Agda.Primitive.html#606" class="Postulate">lsuc</a>  <a id="612" class="Symbol">:</a> <a id="614" class="Symbol">(</a><a id="615" href="Agda.Primitive.html#615" class="Bound">ℓ</a> <a id="617" class="Symbol">:</a> <a id="619" href="Agda.Primitive.html#423" class="Postulate">Level</a><a id="624" class="Symbol">)</a> <a id="626" class="Symbol">→</a> <a id="628" href="Agda.Primitive.html#423" class="Postulate">Level</a>
+  <a id="_⊔_"></a><a id="636" href="Agda.Primitive.html#636" class="Postulate Operator">_⊔_</a>   <a id="642" class="Symbol">:</a> <a id="644" class="Symbol">(</a><a id="645" href="Agda.Primitive.html#645" class="Bound">ℓ₁</a> <a id="648" href="Agda.Primitive.html#648" class="Bound">ℓ₂</a> <a id="651" class="Symbol">:</a> <a id="653" href="Agda.Primitive.html#423" class="Postulate">Level</a><a id="658" class="Symbol">)</a> <a id="660" class="Symbol">→</a> <a id="662" href="Agda.Primitive.html#423" class="Postulate">Level</a>
+
+<a id="669" class="Symbol">{-#</a> <a id="673" class="Keyword">BUILTIN</a> <a id="681" class="Keyword">LEVELZERO</a> <a id="691" href="Agda.Primitive.html#590" class="Primitive">lzero</a> <a id="697" class="Symbol">#-}</a>
+<a id="701" class="Symbol">{-#</a> <a id="705" class="Keyword">BUILTIN</a> <a id="713" class="Keyword">LEVELSUC</a>  <a id="723" href="Agda.Primitive.html#606" class="Primitive">lsuc</a>  <a id="729" class="Symbol">#-}</a>
+<a id="733" class="Symbol">{-#</a> <a id="737" class="Keyword">BUILTIN</a> <a id="745" class="Keyword">LEVELMAX</a>  <a id="755" href="Agda.Primitive.html#636" class="Primitive Operator">_⊔_</a>   <a id="761" class="Symbol">#-}</a>
+
+<a id="766" class="Symbol">{-#</a> <a id="770" class="Keyword">BUILTIN</a> <a id="778" class="Keyword">SETOMEGA</a> <a id="Setω"></a><a id="787" href="Agda.Primitive.html#787" class="Primitive">Setω</a> <a id="792" class="Symbol">#-}</a>
+</pre></body></html>
+\ No newline at end of file
diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.css b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.css
new file mode 100644
index 0000000..3a4b225
--- /dev/null
+++ b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.css
@@ -0,0 +1,39 @@
+/* Aspects. */
+.Agda .Comment       { color: #B22222 }
+.Agda .Background    {}
+.Agda .Markup        { color: #000000 }
+.Agda .Keyword       { color: #CD6600 }
+.Agda .String        { color: #B22222 }
+.Agda .Number        { color: #A020F0 }
+.Agda .Symbol        { color: #404040 }
+.Agda .PrimitiveType { color: #0000CD }
+.Agda .Pragma        { color: black   }
+.Agda .Operator      {}
+
+/* NameKinds. */
+.Agda .Bound                  { color: black   }
+.Agda .Generalizable          { color: black   }
+.Agda .InductiveConstructor   { color: #008B00 }
+.Agda .CoinductiveConstructor { color: #8B7500 }
+.Agda .Datatype               { color: #0000CD }
+.Agda .Field                  { color: #EE1289 }
+.Agda .Function               { color: #0000CD }
+.Agda .Module                 { color: #A020F0 }
+.Agda .Postulate              { color: #0000CD }
+.Agda .Primitive              { color: #0000CD }
+.Agda .Record                 { color: #0000CD }
+
+/* OtherAspects. */
+.Agda .DottedPattern        {}
+.Agda .UnsolvedMeta         { color: black; background: yellow         }
+.Agda .UnsolvedConstraint   { color: black; background: yellow         }
+.Agda .TerminationProblem   { color: black; background: #FFA07A        }
+.Agda .IncompletePattern    { color: black; background: #F5DEB3        }
+.Agda .Error                { color: red;   text-decoration: underline }
+.Agda .TypeChecks           { color: black; background: #ADD8E6        }
+.Agda .Deadcode             { color: black; background: #808080        }
+.Agda .ShadowingInTelescope { color: black; background: #808080        }
+
+/* Standard attributes. */
+.Agda a { text-decoration: none }
+.Agda a[href]:hover { background-color: #B4EEB4 }
diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html b/sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html
new file mode 100644
index 0000000..308e205
--- /dev/null
+++ b/sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html
@@ -0,0 +1,115 @@
+<!DOCTYPE HTML>
+<html><head><meta charset="utf-8"><title>DFA</title><link rel="stylesheet" href="Agda.css"></head><body><pre class="Agda"><a id="1" class="Keyword">module</a> <a id="8" href="DFA.html" class="Module">DFA</a> <a id="12" class="Keyword">where</a>
+
+<a id="19" class="Comment">-- A pair type </a>
+<a id="35" class="Keyword">record</a> <a id="_×_"></a><a id="42" href="DFA.html#42" class="Record Operator">_×_</a> <a id="46" class="Symbol">(</a><a id="47" href="DFA.html#47" class="Bound">A</a> <a id="49" href="DFA.html#49" class="Bound">B</a> <a id="51" class="Symbol">:</a> <a id="53" class="PrimitiveType">Set</a><a id="56" class="Symbol">)</a> <a id="58" class="Symbol">:</a> <a id="60" class="PrimitiveType">Set</a> <a id="64" class="Keyword">where</a>
+  <a id="72" class="Keyword">constructor</a> <a id="_,_"></a><a id="84" href="DFA.html#84" class="InductiveConstructor Operator">_,_</a>
+  <a id="90" class="Keyword">field</a>
+    <a id="_×_.fst"></a><a id="100" href="DFA.html#100" class="Field">fst</a> <a id="104" class="Symbol">:</a> <a id="106" href="DFA.html#47" class="Bound">A</a>
+    <a id="_×_.snd"></a><a id="112" href="DFA.html#112" class="Field">snd</a> <a id="116" class="Symbol">:</a> <a id="118" href="DFA.html#49" class="Bound">B</a>
+
+<a id="121" class="Comment">-- A list type</a>
+<a id="136" class="Keyword">infixr</a> <a id="143" class="Number">5</a> <a id="145" href="DFA.html#197" class="InductiveConstructor Operator">_∷_</a>
+<a id="149" class="Keyword">data</a> <a id="List"></a><a id="154" href="DFA.html#154" class="Datatype">List</a> <a id="159" class="Symbol">(</a><a id="160" href="DFA.html#160" class="Bound">a</a> <a id="162" class="Symbol">:</a> <a id="164" class="PrimitiveType">Set</a><a id="167" class="Symbol">)</a> <a id="169" class="Symbol">:</a> <a id="171" class="PrimitiveType">Set</a> <a id="175" class="Keyword">where</a>
+  <a id="List.[]"></a><a id="183" href="DFA.html#183" class="InductiveConstructor">[]</a> <a id="186" class="Symbol">:</a> <a id="188" href="DFA.html#154" class="Datatype">List</a> <a id="193" href="DFA.html#160" class="Bound">a</a>
+  <a id="List._∷_"></a><a id="197" href="DFA.html#197" class="InductiveConstructor Operator">_∷_</a> <a id="201" class="Symbol">:</a> <a id="203" href="DFA.html#160" class="Bound">a</a> <a id="205" class="Symbol">→</a> <a id="207" href="DFA.html#154" class="Datatype">List</a> <a id="212" href="DFA.html#160" class="Bound">a</a> <a id="214" class="Symbol">→</a> <a id="216" href="DFA.html#154" class="Datatype">List</a> <a id="221" href="DFA.html#160" class="Bound">a</a>
+
+<a id="224" class="Comment">-- Elements of type x ∈ xs is a proof that x is somewhere in xs</a>
+<a id="288" class="Keyword">data</a> <a id="_∈_"></a><a id="293" href="DFA.html#293" class="Datatype Operator">_∈_</a> <a id="297" class="Symbol">{</a><a id="298" href="DFA.html#298" class="Bound">A</a> <a id="300" class="Symbol">:</a> <a id="302" class="PrimitiveType">Set</a><a id="305" class="Symbol">}(</a><a id="307" href="DFA.html#307" class="Bound">x</a> <a id="309" class="Symbol">:</a> <a id="311" href="DFA.html#298" class="Bound">A</a><a id="312" class="Symbol">)</a> <a id="314" class="Symbol">:</a> <a id="316" class="Symbol">(</a><a id="317" href="DFA.html#317" class="Bound">xs</a> <a id="320" class="Symbol">:</a> <a id="322" href="DFA.html#154" class="Datatype">List</a> <a id="327" href="DFA.html#298" class="Bound">A</a><a id="328" class="Symbol">)</a> <a id="330" class="Symbol">→</a> <a id="332" class="PrimitiveType">Set</a> <a id="336" class="Keyword">where</a>
+  <a id="_∈_.here"></a><a id="344" href="DFA.html#344" class="InductiveConstructor">here</a> <a id="349" class="Symbol">:</a> <a id="351" class="Symbol">∀</a> <a id="353" class="Symbol">{</a><a id="354" href="DFA.html#354" class="Bound">xs</a><a id="356" class="Symbol">}</a> <a id="358" class="Symbol">→</a> <a id="360" href="DFA.html#307" class="Bound">x</a> <a id="362" href="DFA.html#293" class="Datatype Operator">∈</a> <a id="364" class="Symbol">(</a><a id="365" href="DFA.html#307" class="Bound">x</a> <a id="367" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="369" href="DFA.html#354" class="Bound">xs</a><a id="371" class="Symbol">)</a>
+  <a id="_∈_.there"></a><a id="375" href="DFA.html#375" class="InductiveConstructor">there</a> <a id="381" class="Symbol">:</a> <a id="383" class="Symbol">∀</a> <a id="385" class="Symbol">{</a><a id="386" href="DFA.html#386" class="Bound">y</a> <a id="388" href="DFA.html#388" class="Bound">xs</a><a id="390" class="Symbol">}</a> <a id="392" class="Symbol">→</a> <a id="394" href="DFA.html#307" class="Bound">x</a> <a id="396" href="DFA.html#293" class="Datatype Operator">∈</a> <a id="398" href="DFA.html#388" class="Bound">xs</a> <a id="401" class="Symbol">→</a> <a id="403" href="DFA.html#307" class="Bound">x</a> <a id="405" href="DFA.html#293" class="Datatype Operator">∈</a> <a id="407" class="Symbol">(</a><a id="408" href="DFA.html#386" class="Bound">y</a> <a id="410" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="412" href="DFA.html#388" class="Bound">xs</a><a id="414" class="Symbol">)</a>
+
+<a id="417" class="Comment">-- Elements of type a ≡ b is a proof that a and b are the same</a>
+<a id="480" class="Keyword">data</a> <a id="_≡_"></a><a id="485" href="DFA.html#485" class="Datatype Operator">_≡_</a> <a id="489" class="Symbol">{</a><a id="490" href="DFA.html#490" class="Bound">A</a> <a id="492" class="Symbol">:</a> <a id="494" class="PrimitiveType">Set</a><a id="497" class="Symbol">}(</a><a id="499" href="DFA.html#499" class="Bound">x</a> <a id="501" class="Symbol">:</a> <a id="503" href="DFA.html#490" class="Bound">A</a><a id="504" class="Symbol">)</a> <a id="506" class="Symbol">:</a> <a id="508" href="DFA.html#490" class="Bound">A</a> <a id="510" class="Symbol">→</a> <a id="512" class="PrimitiveType">Set</a> <a id="516" class="Keyword">where</a>
+  <a id="_≡_.refl"></a><a id="524" href="DFA.html#524" class="InductiveConstructor">refl</a> <a id="529" class="Symbol">:</a> <a id="531" href="DFA.html#499" class="Bound">x</a> <a id="533" href="DFA.html#485" class="Datatype Operator">≡</a> <a id="535" href="DFA.html#499" class="Bound">x</a>
+
+<a id="538" class="Comment">-- The empty type. There are no members of this type, so it is the same as false</a>
+<a id="619" class="Keyword">data</a> <a id="⊥"></a><a id="624" href="DFA.html#624" class="Datatype">⊥</a> <a id="626" class="Symbol">:</a> <a id="628" class="PrimitiveType">Set</a> <a id="632" class="Keyword">where</a>
+
+<a id="639" class="Comment">-- Negation is defined by a function that takes a proof and returns ⊥, which is impossible. In agda an inhabited type means a proof, and an uninhabited means no proof.</a>
+<a id="¬_"></a><a id="807" href="DFA.html#807" class="Function Operator">¬_</a> <a id="810" class="Symbol">:</a> <a id="812" class="PrimitiveType">Set</a> <a id="816" class="Symbol">→</a> <a id="818" class="PrimitiveType">Set</a>
+<a id="822" href="DFA.html#807" class="Function Operator">¬</a> <a id="824" href="DFA.html#824" class="Bound">A</a> <a id="826" class="Symbol">=</a> <a id="828" href="DFA.html#824" class="Bound">A</a> <a id="830" class="Symbol">→</a> <a id="832" href="DFA.html#624" class="Datatype">⊥</a>
+
+<a id="835" class="Comment">-- A DFA is a five tuple of Q Σ q₀ δ F</a>
+<a id="874" class="Keyword">record</a> <a id="DFA"></a><a id="881" href="DFA.html#881" class="Record">DFA</a> <a id="885" class="Symbol">(</a><a id="886" href="DFA.html#886" class="Bound">Q</a> <a id="888" class="Symbol">:</a> <a id="890" class="PrimitiveType">Set</a><a id="893" class="Symbol">)</a> <a id="895" class="Symbol">(</a><a id="896" href="DFA.html#896" class="Bound">Σ</a> <a id="898" class="Symbol">:</a> <a id="900" class="PrimitiveType">Set</a><a id="903" class="Symbol">)</a> <a id="905" class="Symbol">(</a><a id="906" href="DFA.html#906" class="Bound">q₀</a> <a id="909" class="Symbol">:</a> <a id="911" href="DFA.html#886" class="Bound">Q</a><a id="912" class="Symbol">)</a> <a id="914" class="Symbol">(</a><a id="915" href="DFA.html#915" class="Bound">δ</a> <a id="917" class="Symbol">:</a> <a id="919" href="DFA.html#886" class="Bound">Q</a> <a id="921" href="DFA.html#42" class="Record Operator">×</a> <a id="923" href="DFA.html#896" class="Bound">Σ</a> <a id="925" class="Symbol">→</a> <a id="927" href="DFA.html#886" class="Bound">Q</a><a id="928" class="Symbol">)</a> <a id="930" class="Symbol">(</a><a id="931" href="DFA.html#931" class="Bound">F</a> <a id="933" class="Symbol">:</a> <a id="935" href="DFA.html#154" class="Datatype">List</a> <a id="940" href="DFA.html#886" class="Bound">Q</a><a id="941" class="Symbol">)</a> <a id="943" class="Symbol">:</a> <a id="945" class="PrimitiveType">Set</a> <a id="949" class="Keyword">where</a>
+
+<a id="956" class="Comment">-- The DFArun data type keeps track of a running dfa.</a>
+<a id="1010" class="Keyword">data</a> <a id="DFArun"></a><a id="1015" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1022" class="Symbol">{</a><a id="1023" href="DFA.html#1023" class="Bound">Q</a> <a id="1025" href="DFA.html#1025" class="Bound">Σ</a> <a id="1027" href="DFA.html#1027" class="Bound">q₀</a> <a id="1030" href="DFA.html#1030" class="Bound">δ</a> <a id="1032" href="DFA.html#1032" class="Bound">F</a><a id="1033" class="Symbol">}(</a><a id="1035" href="DFA.html#1035" class="Bound">dfa</a> <a id="1039" class="Symbol">:</a> <a id="1041" href="DFA.html#881" class="Record">DFA</a> <a id="1045" href="DFA.html#1023" class="Bound">Q</a> <a id="1047" href="DFA.html#1025" class="Bound">Σ</a> <a id="1049" href="DFA.html#1027" class="Bound">q₀</a> <a id="1052" href="DFA.html#1030" class="Bound">δ</a> <a id="1054" href="DFA.html#1032" class="Bound">F</a><a id="1055" class="Symbol">)</a> <a id="1057" class="Symbol">:</a> <a id="1059" class="Symbol">(</a><a id="1060" href="DFA.html#1060" class="Bound">q</a> <a id="1062" class="Symbol">:</a> <a id="1064" href="DFA.html#1023" class="Bound">Q</a><a id="1065" class="Symbol">)</a> <a id="1067" class="Symbol">→</a> <a id="1069" class="Symbol">(</a><a id="1070" href="DFA.html#1070" class="Bound">w</a> <a id="1072" class="Symbol">:</a> <a id="1074" href="DFA.html#154" class="Datatype">List</a> <a id="1079" href="DFA.html#1025" class="Bound">Σ</a><a id="1080" class="Symbol">)</a> <a id="1082" class="Symbol">→</a> <a id="1084" class="PrimitiveType">Set</a> <a id="1088" class="Keyword">where</a>
+  <a id="DFArun.empty"></a><a id="1096" href="DFA.html#1096" class="InductiveConstructor">empty</a> <a id="1102" class="Symbol">:</a> <a id="1104" class="Symbol">{</a><a id="1105" href="DFA.html#1105" class="Bound">q</a> <a id="1107" class="Symbol">:</a> <a id="1109" href="DFA.html#1023" class="Bound">Q</a><a id="1110" class="Symbol">}</a> <a id="1112" class="Symbol">→</a> <a id="1114" href="DFA.html#1105" class="Bound">q</a> <a id="1116" href="DFA.html#293" class="Datatype Operator">∈</a> <a id="1118" href="DFA.html#1032" class="Bound">F</a> <a id="1120" class="Symbol">→</a> <a id="1122" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1129" href="DFA.html#1035" class="Bound">dfa</a> <a id="1133" href="DFA.html#1105" class="Bound">q</a> <a id="1135" href="DFA.html#183" class="InductiveConstructor">[]</a>
+  <a id="DFArun.acceptOne"></a><a id="1140" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="1150" class="Symbol">:</a> <a id="1152" class="Symbol">{</a><a id="1153" href="DFA.html#1153" class="Bound">ws</a> <a id="1156" class="Symbol">:</a> <a id="1158" href="DFA.html#154" class="Datatype">List</a> <a id="1163" href="DFA.html#1025" class="Bound">Σ</a><a id="1164" class="Symbol">}</a> <a id="1166" class="Symbol">→</a>
+              <a id="1182" class="Symbol">(</a><a id="1183" href="DFA.html#1183" class="Bound">w</a> <a id="1185" class="Symbol">:</a> <a id="1187" href="DFA.html#1025" class="Bound">Σ</a><a id="1188" class="Symbol">)</a> <a id="1190" class="Symbol">→</a>
+              <a id="1206" class="Symbol">(</a><a id="1207" href="DFA.html#1207" class="Bound">q</a> <a id="1209" class="Symbol">:</a> <a id="1211" href="DFA.html#1023" class="Bound">Q</a><a id="1212" class="Symbol">)</a> <a id="1214" class="Symbol">→</a>
+              <a id="1230" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1237" href="DFA.html#1035" class="Bound">dfa</a> <a id="1241" class="Symbol">(</a><a id="1242" href="DFA.html#1030" class="Bound">δ</a> <a id="1244" class="Symbol">(</a><a id="1245" href="DFA.html#1207" class="Bound">q</a> <a id="1247" href="DFA.html#84" class="InductiveConstructor Operator">,</a> <a id="1249" href="DFA.html#1183" class="Bound">w</a><a id="1250" class="Symbol">))</a> <a id="1253" href="DFA.html#1153" class="Bound">ws</a> <a id="1256" class="Symbol">→</a>
+              <a id="1272" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1279" href="DFA.html#1035" class="Bound">dfa</a> <a id="1283" href="DFA.html#1207" class="Bound">q</a> <a id="1285" class="Symbol">(</a><a id="1286" href="DFA.html#1183" class="Bound">w</a> <a id="1288" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="1290" href="DFA.html#1153" class="Bound">ws</a><a id="1292" class="Symbol">)</a>
+
+<a id="1295" class="Comment">-- Accepts dfa w is a proof that running the dfa with input w is possible form the start state q₀</a>
+<a id="1393" class="Keyword">data</a> <a id="Accepts"></a><a id="1398" href="DFA.html#1398" class="Datatype">Accepts</a> <a id="1406" class="Symbol">{</a><a id="1407" href="DFA.html#1407" class="Bound">Q</a> <a id="1409" href="DFA.html#1409" class="Bound">Σ</a> <a id="1411" href="DFA.html#1411" class="Bound">q₀</a> <a id="1414" href="DFA.html#1414" class="Bound">δ</a> <a id="1416" href="DFA.html#1416" class="Bound">F</a><a id="1417" class="Symbol">}(</a><a id="1419" href="DFA.html#1419" class="Bound">dfa</a> <a id="1423" class="Symbol">:</a> <a id="1425" href="DFA.html#881" class="Record">DFA</a> <a id="1429" href="DFA.html#1407" class="Bound">Q</a> <a id="1431" href="DFA.html#1409" class="Bound">Σ</a> <a id="1433" href="DFA.html#1411" class="Bound">q₀</a> <a id="1436" href="DFA.html#1414" class="Bound">δ</a> <a id="1438" href="DFA.html#1416" class="Bound">F</a><a id="1439" class="Symbol">)</a> <a id="1441" class="Symbol">:</a> <a id="1443" class="Symbol">(</a><a id="1444" href="DFA.html#1444" class="Bound">w</a> <a id="1446" class="Symbol">:</a> <a id="1448" href="DFA.html#154" class="Datatype">List</a> <a id="1453" href="DFA.html#1409" class="Bound">Σ</a><a id="1454" class="Symbol">)</a> <a id="1456" class="Symbol">→</a> <a id="1458" class="PrimitiveType">Set</a> <a id="1462" class="Keyword">where</a>
+  <a id="Accepts.accepts"></a><a id="1470" href="DFA.html#1470" class="InductiveConstructor">accepts</a> <a id="1478" class="Symbol">:</a> <a id="1480" class="Symbol">∀{</a><a id="1482" href="DFA.html#1482" class="Bound">w</a><a id="1483" class="Symbol">}</a> <a id="1485" class="Symbol">→</a> <a id="1487" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1494" href="DFA.html#1419" class="Bound">dfa</a> <a id="1498" href="DFA.html#1411" class="Bound">q₀</a> <a id="1501" href="DFA.html#1482" class="Bound">w</a> <a id="1503" class="Symbol">→</a> <a id="1505" href="DFA.html#1398" class="Datatype">Accepts</a> <a id="1513" href="DFA.html#1419" class="Bound">dfa</a> <a id="1517" href="DFA.html#1482" class="Bound">w</a>
+
+<a id="1520" class="Comment">-- CantAccept dfa q w is a proof that running the dfa on imput w is impossible if we want to start at state q₀. It has to start in q instead.</a>
+<a id="1662" class="Keyword">data</a> <a id="CantAccept"></a><a id="1667" href="DFA.html#1667" class="Datatype">CantAccept</a> <a id="1678" class="Symbol">{</a><a id="1679" href="DFA.html#1679" class="Bound">Q</a> <a id="1681" href="DFA.html#1681" class="Bound">Σ</a> <a id="1683" href="DFA.html#1683" class="Bound">q₀</a> <a id="1686" href="DFA.html#1686" class="Bound">δ</a> <a id="1688" href="DFA.html#1688" class="Bound">F</a><a id="1689" class="Symbol">}(</a><a id="1691" href="DFA.html#1691" class="Bound">dfa</a> <a id="1695" class="Symbol">:</a> <a id="1697" href="DFA.html#881" class="Record">DFA</a> <a id="1701" href="DFA.html#1679" class="Bound">Q</a> <a id="1703" href="DFA.html#1681" class="Bound">Σ</a> <a id="1705" href="DFA.html#1683" class="Bound">q₀</a> <a id="1708" href="DFA.html#1686" class="Bound">δ</a> <a id="1710" href="DFA.html#1688" class="Bound">F</a><a id="1711" class="Symbol">)</a> <a id="1713" class="Symbol">:</a> <a id="1715" class="Symbol">(</a><a id="1716" href="DFA.html#1716" class="Bound">q</a> <a id="1718" class="Symbol">:</a> <a id="1720" href="DFA.html#1679" class="Bound">Q</a><a id="1721" class="Symbol">)</a> <a id="1723" class="Symbol">→</a> <a id="1725" class="Symbol">(</a><a id="1726" href="DFA.html#1726" class="Bound">w</a> <a id="1728" class="Symbol">:</a> <a id="1730" href="DFA.html#154" class="Datatype">List</a> <a id="1735" href="DFA.html#1681" class="Bound">Σ</a><a id="1736" class="Symbol">)</a> <a id="1738" class="Symbol">→</a> <a id="1740" class="PrimitiveType">Set</a> <a id="1744" class="Keyword">where</a>
+  <a id="CantAccept.cantAccept"></a><a id="1752" href="DFA.html#1752" class="InductiveConstructor">cantAccept</a> <a id="1763" class="Symbol">:</a> <a id="1765" class="Symbol">∀</a> <a id="1767" class="Symbol">{</a><a id="1768" href="DFA.html#1768" class="Bound">w</a> <a id="1770" href="DFA.html#1770" class="Bound">q</a><a id="1771" class="Symbol">}</a> <a id="1773" class="Symbol">→</a> <a id="1775" href="DFA.html#1015" class="Datatype">DFArun</a> <a id="1782" href="DFA.html#1691" class="Bound">dfa</a> <a id="1786" href="DFA.html#1770" class="Bound">q</a> <a id="1788" href="DFA.html#1768" class="Bound">w</a> <a id="1790" class="Symbol">→</a> <a id="1792" href="DFA.html#807" class="Function Operator">¬</a><a id="1793" class="Symbol">(</a><a id="1794" href="DFA.html#1770" class="Bound">q</a> <a id="1796" href="DFA.html#485" class="Datatype Operator">≡</a> <a id="1798" href="DFA.html#1683" class="Bound">q₀</a><a id="1800" class="Symbol">)</a> <a id="1802" class="Symbol">→</a> <a id="1804" href="DFA.html#1667" class="Datatype">CantAccept</a> <a id="1815" href="DFA.html#1691" class="Bound">dfa</a> <a id="1819" href="DFA.html#1770" class="Bound">q</a> <a id="1821" href="DFA.html#1768" class="Bound">w</a>
+
+
+<a id="1825" class="Comment">-- w ∈Lang dfa gives either a proof that w is in the language of the dfa, or that it isn&#39;t.</a>
+<a id="1917" class="Keyword">data</a> <a id="_∈Lang_"></a><a id="1922" href="DFA.html#1922" class="Datatype Operator">_∈Lang_</a> <a id="1930" class="Symbol">{</a><a id="1931" href="DFA.html#1931" class="Bound">Q</a> <a id="1933" href="DFA.html#1933" class="Bound">Σ</a> <a id="1935" href="DFA.html#1935" class="Bound">q₀</a> <a id="1938" href="DFA.html#1938" class="Bound">δ</a> <a id="1940" href="DFA.html#1940" class="Bound">F</a><a id="1941" class="Symbol">}(</a><a id="1943" href="DFA.html#1943" class="Bound">w</a> <a id="1945" class="Symbol">:</a> <a id="1947" href="DFA.html#154" class="Datatype">List</a> <a id="1952" href="DFA.html#1933" class="Bound">Σ</a><a id="1953" class="Symbol">)(</a><a id="1955" href="DFA.html#1955" class="Bound">dfa</a> <a id="1959" class="Symbol">:</a> <a id="1961" href="DFA.html#881" class="Record">DFA</a> <a id="1965" href="DFA.html#1931" class="Bound">Q</a> <a id="1967" href="DFA.html#1933" class="Bound">Σ</a> <a id="1969" href="DFA.html#1935" class="Bound">q₀</a> <a id="1972" href="DFA.html#1938" class="Bound">δ</a> <a id="1974" href="DFA.html#1940" class="Bound">F</a><a id="1975" class="Symbol">)</a> <a id="1977" class="Symbol">:</a> <a id="1979" class="PrimitiveType">Set</a> <a id="1983" class="Keyword">where</a>
+  <a id="_∈Lang_.inLang"></a><a id="1991" href="DFA.html#1991" class="InductiveConstructor">inLang</a> <a id="1998" class="Symbol">:</a> <a id="2000" href="DFA.html#1398" class="Datatype">Accepts</a> <a id="2008" href="DFA.html#1955" class="Bound">dfa</a> <a id="2012" href="DFA.html#1943" class="Bound">w</a> <a id="2014" class="Symbol">→</a> <a id="2016" href="DFA.html#1943" class="Bound">w</a> <a id="2018" href="DFA.html#1922" class="Datatype Operator">∈Lang</a> <a id="2024" href="DFA.html#1955" class="Bound">dfa</a>
+  <a id="_∈Lang_.notInLang"></a><a id="2030" href="DFA.html#2030" class="InductiveConstructor">notInLang</a> <a id="2040" class="Symbol">:</a> <a id="2042" class="Symbol">∀{</a><a id="2044" href="DFA.html#2044" class="Bound">q</a><a id="2045" class="Symbol">}</a> <a id="2047" class="Symbol">→</a> <a id="2049" href="DFA.html#1667" class="Datatype">CantAccept</a> <a id="2060" href="DFA.html#1955" class="Bound">dfa</a> <a id="2064" href="DFA.html#2044" class="Bound">q</a> <a id="2066" href="DFA.html#1943" class="Bound">w</a> <a id="2068" class="Symbol">→</a> <a id="2070" href="DFA.html#1943" class="Bound">w</a> <a id="2072" href="DFA.html#1922" class="Datatype Operator">∈Lang</a> <a id="2078" href="DFA.html#1955" class="Bound">dfa</a>
+
+
+
+
+<a id="2086" class="Comment">-- Test stuff. Create a DFA which only accepts an input with an even number of a&#39;s</a>
+
+<a id="2170" class="Keyword">data</a> <a id="TestQ"></a><a id="2175" href="DFA.html#2175" class="Datatype">TestQ</a> <a id="2181" class="Symbol">:</a> <a id="2183" class="PrimitiveType">Set</a> <a id="2187" class="Keyword">where</a>
+  <a id="TestQ.evenNumberOfAs"></a><a id="2195" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="2210" class="Symbol">:</a> <a id="2212" href="DFA.html#2175" class="Datatype">TestQ</a>
+  <a id="TestQ.oddNumberOfAs"></a><a id="2220" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> <a id="2234" class="Symbol">:</a> <a id="2236" href="DFA.html#2175" class="Datatype">TestQ</a>
+
+<a id="2243" class="Keyword">data</a> <a id="TestΣ"></a><a id="2248" href="DFA.html#2248" class="Datatype">TestΣ</a> <a id="2254" class="Symbol">:</a> <a id="2256" class="PrimitiveType">Set</a> <a id="2260" class="Keyword">where</a>
+  <a id="TestΣ.a"></a><a id="2268" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2270" class="Symbol">:</a> <a id="2272" href="DFA.html#2248" class="Datatype">TestΣ</a>
+  <a id="TestΣ.b"></a><a id="2280" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2282" class="Symbol">:</a> <a id="2284" href="DFA.html#2248" class="Datatype">TestΣ</a>
+
+<a id="Testδ"></a><a id="2291" href="DFA.html#2291" class="Function">Testδ</a> <a id="2297" class="Symbol">:</a> <a id="2299" href="DFA.html#2175" class="Datatype">TestQ</a> <a id="2305" href="DFA.html#42" class="Record Operator">×</a> <a id="2307" href="DFA.html#2248" class="Datatype">TestΣ</a> <a id="2313" class="Symbol">→</a> <a id="2315" href="DFA.html#2175" class="Datatype">TestQ</a>
+<a id="2321" href="DFA.html#2291" class="Function">Testδ</a> <a id="2327" class="Symbol">(</a><a id="2328" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="2343" href="DFA.html#84" class="InductiveConstructor Operator">,</a> <a id="2345" href="DFA.html#2268" class="InductiveConstructor">a</a><a id="2346" class="Symbol">)</a> <a id="2348" class="Symbol">=</a> <a id="2350" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a>
+<a id="2364" href="DFA.html#2291" class="Function">Testδ</a> <a id="2370" class="Symbol">(</a><a id="2371" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="2386" href="DFA.html#84" class="InductiveConstructor Operator">,</a> <a id="2388" href="DFA.html#2280" class="InductiveConstructor">b</a><a id="2389" class="Symbol">)</a> <a id="2391" class="Symbol">=</a> <a id="2393" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a>
+<a id="2408" href="DFA.html#2291" class="Function">Testδ</a> <a id="2414" class="Symbol">(</a><a id="2415" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> <a id="2429" href="DFA.html#84" class="InductiveConstructor Operator">,</a> <a id="2431" href="DFA.html#2268" class="InductiveConstructor">a</a><a id="2432" class="Symbol">)</a> <a id="2434" class="Symbol">=</a> <a id="2436" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a>
+<a id="2451" href="DFA.html#2291" class="Function">Testδ</a> <a id="2457" class="Symbol">(</a><a id="2458" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> <a id="2472" href="DFA.html#84" class="InductiveConstructor Operator">,</a> <a id="2474" href="DFA.html#2280" class="InductiveConstructor">b</a><a id="2475" class="Symbol">)</a> <a id="2477" class="Symbol">=</a> <a id="2479" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a>
+
+<a id="TestF"></a><a id="2494" href="DFA.html#2494" class="Function">TestF</a> <a id="2500" class="Symbol">:</a> <a id="2502" href="DFA.html#154" class="Datatype">List</a> <a id="2507" href="DFA.html#2175" class="Datatype">TestQ</a>
+<a id="2513" href="DFA.html#2494" class="Function">TestF</a> <a id="2519" class="Symbol">=</a> <a id="2521" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="2536" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2538" href="DFA.html#183" class="InductiveConstructor">[]</a>
+
+<a id="TestDFA"></a><a id="2542" href="DFA.html#2542" class="Function">TestDFA</a> <a id="2550" class="Symbol">:</a> <a id="2552" href="DFA.html#881" class="Record">DFA</a> <a id="2556" href="DFA.html#2175" class="Datatype">TestQ</a> <a id="2562" href="DFA.html#2248" class="Datatype">TestΣ</a> <a id="2568" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="2583" href="DFA.html#2291" class="Function">Testδ</a> <a id="2589" href="DFA.html#2494" class="Function">TestF</a>
+<a id="2595" href="DFA.html#2542" class="Function">TestDFA</a> <a id="2603" class="Symbol">=</a> <a id="2605" class="Symbol">_</a> <a id="2607" class="Comment">-- Since a DFA is a record with no fields, agda can infer it</a>
+
+<a id="2669" class="Comment">-- Try to construct proofs for different input strings</a>
+
+<a id="input₁"></a><a id="2725" href="DFA.html#2725" class="Function">input₁</a> <a id="input₂"></a><a id="2732" href="DFA.html#2732" class="Function">input₂</a> <a id="input₃"></a><a id="2739" href="DFA.html#2739" class="Function">input₃</a> <a id="2746" class="Symbol">:</a> <a id="2748" href="DFA.html#154" class="Datatype">List</a> <a id="2753" href="DFA.html#2248" class="Datatype">TestΣ</a>
+<a id="2759" href="DFA.html#2725" class="Function">input₁</a> <a id="2766" class="Symbol">=</a> <a id="2768" href="DFA.html#183" class="InductiveConstructor">[]</a> <a id="2771" class="Comment">-- Empty string</a>
+<a id="2787" href="DFA.html#2732" class="Function">input₂</a> <a id="2794" class="Symbol">=</a> <a id="2796" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2798" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2800" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2802" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2804" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2806" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2808" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2810" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2812" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2814" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2816" href="DFA.html#183" class="InductiveConstructor">[]</a> <a id="2819" class="Comment">-- Three a&#39;s</a>
+<a id="2832" href="DFA.html#2739" class="Function">input₃</a> <a id="2839" class="Symbol">=</a> <a id="2841" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2843" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2845" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2847" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2849" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2851" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2853" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="2855" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2857" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="2859" href="DFA.html#197" class="InductiveConstructor Operator">∷</a> <a id="2861" href="DFA.html#183" class="InductiveConstructor">[]</a> <a id="2864" class="Comment">-- Two a&#39;s</a>
+
+
+<a id="2877" class="Comment">-- The proofs are found automatically by agda, and no other proofs would type check</a>
+<a id="proof₁"></a><a id="2961" href="DFA.html#2961" class="Function">proof₁</a> <a id="2968" class="Symbol">:</a> <a id="2970" href="DFA.html#2725" class="Function">input₁</a> <a id="2977" href="DFA.html#1922" class="Datatype Operator">∈Lang</a> <a id="2983" href="DFA.html#2542" class="Function">TestDFA</a> <a id="2991" class="Comment">-- Proof that input₁ is in the language</a>
+<a id="3031" href="DFA.html#2961" class="Function">proof₁</a> <a id="3038" class="Symbol">=</a> <a id="3040" href="DFA.html#1991" class="InductiveConstructor">inLang</a> <a id="3047" class="Symbol">(</a><a id="3048" href="DFA.html#1470" class="InductiveConstructor">accepts</a> <a id="3056" class="Symbol">(</a><a id="3057" href="DFA.html#1096" class="InductiveConstructor">empty</a> <a id="3063" href="DFA.html#344" class="InductiveConstructor">here</a><a id="3067" class="Symbol">))</a>
+
+<a id="proof₂"></a><a id="3071" href="DFA.html#3071" class="Function">proof₂</a> <a id="3078" class="Symbol">:</a> <a id="3080" href="DFA.html#2732" class="Function">input₂</a> <a id="3087" href="DFA.html#1922" class="Datatype Operator">∈Lang</a> <a id="3093" href="DFA.html#2542" class="Function">TestDFA</a> <a id="3101" class="Comment">-- Proof that input₂ is not in the language</a>
+<a id="3145" href="DFA.html#3071" class="Function">proof₂</a> <a id="3152" class="Symbol">=</a> <a id="3154" href="DFA.html#2030" class="InductiveConstructor">notInLang</a>
+           <a id="3175" class="Symbol">(</a><a id="3176" href="DFA.html#1752" class="InductiveConstructor">cantAccept</a>
+            <a id="3199" class="Symbol">(</a><a id="3200" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3210" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="3212" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a>
+             <a id="3239" class="Symbol">(</a><a id="3240" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3250" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="3252" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a>
+              <a id="3281" class="Symbol">(</a><a id="3282" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3292" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="3294" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a>
+               <a id="3324" class="Symbol">(</a><a id="3325" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3335" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="3337" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a>
+                <a id="3367" class="Symbol">(</a><a id="3368" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3378" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="3380" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a> <a id="3395" class="Symbol">(</a><a id="3396" href="DFA.html#1096" class="InductiveConstructor">empty</a> <a id="3402" href="DFA.html#344" class="InductiveConstructor">here</a><a id="3406" class="Symbol">))))))</a>
+            <a id="3425" class="Symbol">(λ</a> <a id="3428" class="Symbol">()))</a>
+
+<a id="proof₃"></a><a id="3434" href="DFA.html#3434" class="Function">proof₃</a> <a id="3441" class="Symbol">:</a> <a id="3443" href="DFA.html#2739" class="Function">input₃</a> <a id="3450" href="DFA.html#1922" class="Datatype Operator">∈Lang</a> <a id="3456" href="DFA.html#2542" class="Function">TestDFA</a> <a id="3464" class="Comment">-- Proof that input₃ is in the language</a>
+<a id="3504" href="DFA.html#3434" class="Function">proof₃</a> <a id="3511" class="Symbol">=</a> <a id="3513" href="DFA.html#1991" class="InductiveConstructor">inLang</a>
+           <a id="3531" class="Symbol">(</a><a id="3532" href="DFA.html#1470" class="InductiveConstructor">accepts</a>
+            <a id="3552" class="Symbol">(</a><a id="3553" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3563" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="3565" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a>
+             <a id="3593" class="Symbol">(</a><a id="3594" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3604" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="3606" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a>
+              <a id="3635" class="Symbol">(</a><a id="3636" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3646" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="3648" href="DFA.html#2195" class="InductiveConstructor">evenNumberOfAs</a>
+               <a id="3678" class="Symbol">(</a><a id="3679" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3689" href="DFA.html#2280" class="InductiveConstructor">b</a> <a id="3691" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a>
+                <a id="3721" class="Symbol">(</a><a id="3722" href="DFA.html#1140" class="InductiveConstructor">acceptOne</a> <a id="3732" href="DFA.html#2268" class="InductiveConstructor">a</a> <a id="3734" href="DFA.html#2220" class="InductiveConstructor">oddNumberOfAs</a> <a id="3748" class="Symbol">(</a><a id="3749" href="DFA.html#1096" class="InductiveConstructor">empty</a> <a id="3755" href="DFA.html#344" class="InductiveConstructor">here</a><a id="3759" class="Symbol">)))))))</a>
+
+</pre></body></html>
+\ No newline at end of file