big cleanup

47 files changed, 12 insertions, 1035 deletions

diff --git a/sites/apl.pmikkelsen.com/_werc/lib/footer.inc b/sites/apl.pmikkelsen.com/_werc/lib/footer.inc
deleted file mode 100644
index 2deed52..0000000
--- a/sites/apl.pmikkelsen.com/_werc/lib/footer.inc
+++ /dev/null
@@ -1 +0,0 @@
-<a href="http://werc.cat-v.org">Powered by werc</a> © Peter Mikkelsen 2022
\ No newline at end of file
diff --git a/sites/apl.pmikkelsen.com/_werc/lib/top_bar.inc b/sites/apl.pmikkelsen.com/_werc/lib/top_bar.inc
deleted file mode 100644
index 4c23cf3..0000000
--- a/sites/apl.pmikkelsen.com/_werc/lib/top_bar.inc
+++ /dev/null
@@ -1,8 +0,0 @@
-    <div class="left">
-		<a href="https://git.sr.ht/~pmikkelsen/APL9">APL9 source code</a> |
-		<a href="https://pmikkelsen.com">pmikkelsen's site</a> |
-		<a href="http://9front.org">9front</a>
-    </div>
-
-    <div class="right">
-    </div>
diff --git a/sites/apl.pmikkelsen.com/favicon.ico b/sites/apl.pmikkelsen.com/favicon.ico
deleted file mode 100644
index 745367e..0000000
--- a/sites/apl.pmikkelsen.com/favicon.ico
+++ /dev/null
diff --git a/sites/apl.pmikkelsen.com/index.md b/sites/apl.pmikkelsen.com/index.md
index f27aac5..3e3eb8a 100644
--- a/sites/apl.pmikkelsen.com/index.md
+++ b/sites/apl.pmikkelsen.com/index.md
@@ -57,5 +57,5 @@ time, to get `⍶⍸⍹⍷⍣` and so on. Please email me if you have questions
 
 [![A picture of APL9 in action][2]][2]
 
-[2]: /_images/apl-screenshot.png
+[2]: https://images.pmikkelsen.com/apl-screenshot.png
 [1]: https://dyalog.com
diff --git a/sites/lpa.pmikkelsen.com/_werc/lib/footer.inc b/sites/lpa.pmikkelsen.com/_werc/lib/footer.inc
deleted file mode 100644
index d69228a..0000000
--- a/sites/lpa.pmikkelsen.com/_werc/lib/footer.inc
+++ /dev/null
@@ -1 +0,0 @@
-<a href="http://werc.cat-v.org">Powered by werc</a> © Peter Mikkelsen 2024
\ No newline at end of file
diff --git a/sites/lpa.pmikkelsen.com/_werc/lib/top_bar.inc b/sites/lpa.pmikkelsen.com/_werc/lib/top_bar.inc
deleted file mode 100644
index 730a160..0000000
--- a/sites/lpa.pmikkelsen.com/_werc/lib/top_bar.inc
+++ /dev/null
@@ -1,8 +0,0 @@
-    <div class="left">
-		<a href="https://git.sr.ht/~pmikkelsen/LPA">LPA source code</a> |
-		<a href="https://pmikkelsen.com">pmikkelsen's site</a> |
-		<a href="http://9front.org">9front</a>
-    </div>
-
-    <div class="right">
-    </div>
diff --git a/sites/lpa.pmikkelsen.com/favicon.ico b/sites/lpa.pmikkelsen.com/favicon.ico
deleted file mode 100644
index 745367e..0000000
--- a/sites/lpa.pmikkelsen.com/favicon.ico
+++ /dev/null
diff --git a/sites/pmikkelsen.com/_files/djv.tar b/sites/pmikkelsen.com/_files/djv.tar
deleted file mode 100644
index 5d60262..0000000
--- a/sites/pmikkelsen.com/_files/djv.tar
+++ /dev/null
diff --git a/sites/pmikkelsen.com/_files/djvmono.tar b/sites/pmikkelsen.com/_files/djvmono.tar
deleted file mode 100644
index 1fb0c7d..0000000
--- a/sites/pmikkelsen.com/_files/djvmono.tar
+++ /dev/null
diff --git a/sites/pmikkelsen.com/_files/faces.patch b/sites/pmikkelsen.com/_files/faces.patch
deleted file mode 100644
index 3309c1b..0000000
--- a/sites/pmikkelsen.com/_files/faces.patch
+++ /dev/null
@@ -1,105 +0,0 @@
-From 5595dbb332eae353832dbc2ad11ef92aeb8fcab0
-From: Peter Mikkelsen <peter@pmikkelsen.com>
-Date: Mon, 28 Jun 2021 21:45:53 +0000
-Subject: [PATCH] Add -u flag to faces, making it only show unread messages.
-
----
-diff 658757abed7be283e06bae3b1722fc2703334d74 5595dbb332eae353832dbc2ad11ef92aeb8fcab0
---- a/sys/man/1/faces	Sun Jun 27 02:13:58 2021
-+++ b/sys/man/1/faces	Mon Jun 28 23:45:53 2021
-@@ -4,7 +4,7 @@
- .SH SYNOPSIS
- .B faces
- [
--.B -ihc
-+.B -ihcu
- ] [
- .B -m
- .I maildir
-@@ -99,6 +99,15 @@
- rather than the current state of the mail box.
- In particular, faces are not removed from the screen when messages are deleted.
- Also, in this mode clicking button 1 in the display will clear the window.
-+.PP
-+The
-+.B -u
-+flag causes
-+.I faces
-+to read in the mailbox like with the
-+.B -i
-+flag, but it only shows the unread ones.
-+When right-clicking on a message icon in this mode, the message is both plumbed and removed from the view.
- .PP
- .I Seemail
- is an
---- a/sys/src/cmd/faces/main.c	Sun Jun 27 02:13:58 2021
-+++ b/sys/src/cmd/faces/main.c	Mon Jun 28 23:45:53 2021
-@@ -10,6 +10,7 @@
- int	history = 0;	/* use old interface, showing history of mailbox rather than current state */
- int	initload = 0;	/* initialize program with contents of mail box */
- int	clickrm = 0;	/* allows removing mail faces by left clicking */
-+int	onlyunread = 0;	/* initialize program with unread messages, remove when clicked */
- 
- enum
- {
-@@ -358,6 +359,28 @@
- 	unlockdisplay(display);
- }
- 
-+int
-+isunread(char *dir, char *num)
-+{
-+	char buf[1024], flags[8];
-+	int n, fd, unread;
-+
-+	snprint(buf, sizeof(buf), "%s/%s/flags", dir, num);
-+	fd = open(buf, OREAD);
-+	if(fd < 0)
-+		return 0;
-+	n = readn(fd, flags, 7);
-+	close(fd);
-+	if(n != 7)
-+		return 0;
-+	flags[n] = '\0';
-+	if(strchr(flags, 's') != nil)
-+		unread = 0;
-+	else
-+		unread = 1;
-+	return unread;
-+}
-+
- void
- loadmboxfaces(char *maildir)
- {
-@@ -370,7 +393,8 @@
- 		chdir(maildir);
- 		while((n = dirread(dirfd, &d)) > 0){
- 			for(i=0; i<n; i++)
--				addface(dirface(maildir, d[i].name));
-+				if(onlyunread && isunread(maildir, d[i].name))
-+					addface(dirface(maildir, d[i].name));
- 			free(d);
- 		}
- 		close(dirfd);
-@@ -616,6 +640,10 @@
- 		for(i=first; i<last; i++)
- 			if(ptinrect(p, facerect(i-first))){
- 				showmail(faces[i]);
-+				if(onlyunread){
-+					delface(i);
-+					flushimage(display, 1);
-+				}
- 				break;
- 			}
- 		unlockdisplay(display);
-@@ -698,6 +726,10 @@
- 		break;
- 	case 'c':
- 		clickrm++;
-+		break;
-+	case 'u':
-+		initload++;
-+		onlyunread++;
- 		break;
- 	default:
- 		usage();
diff --git a/sites/pmikkelsen.com/_files/ndb.diff b/sites/pmikkelsen.com/_files/ndb.diff
deleted file mode 100644
index b752cd4..0000000
--- a/sites/pmikkelsen.com/_files/ndb.diff
+++ /dev/null
@@ -1,70 +0,0 @@
-diff -r 4adb989bc93e sys/src/cmd/ndb/dblookup.c
---- a/sys/src/cmd/ndb/dblookup.c	Tue Nov 03 20:47:14 2020 +0100
-+++ b/sys/src/cmd/ndb/dblookup.c	Sun Nov 29 16:42:47 2020 +0100
-@@ -40,7 +40,7 @@
- static RR*	srvrr(Ndbtuple*, Ndbtuple*);
- static RR*	txtrr(Ndbtuple*, Ndbtuple*);
- 
--static int	implemented[Tall] =
-+static int	implemented[Tcaa] =
- {
- 	[Ta]		1,
- 	[Taaaa]		1,
-@@ -118,7 +118,7 @@
- 	rp = nil;
- 
- 	if(type == Tall){
--		for (type = Ta; type < Tall; type++)
-+		for (type = Ta; type < Tcaa; type++)
- 			if(implemented[type])
- 				rrcat(&rp, dblookup(name, class, type, auth, ttl));
- 
-diff -r 4adb989bc93e sys/src/cmd/ndb/dn.c
---- a/sys/src/cmd/ndb/dn.c	Tue Nov 03 20:47:14 2020 +0100
-+++ b/sys/src/cmd/ndb/dn.c	Sun Nov 29 16:42:47 2020 +0100
-@@ -97,6 +97,7 @@
- [Tmailb]	"mailb",
- [Tmaila]	"maila",
- [Tall]		"all",
-+[Tcaa]		"caa",
- 		0,
- };
- 
-@@ -1042,7 +1043,7 @@
- {
- 	int i;
- 
--	for(i = 0; i <= Tall; i++)
-+	for(i = 0; i <= Tcaa; i++)
- 		if(rrtname[i] && strcmp(rrtname[i], atype) == 0)
- 			return i;
- 
-@@ -1061,7 +1062,7 @@
- int
- rrsupported(int type)
- {
--	if(type < 0 || type >Tall)
-+	if(type < 0 || type >Tcaa)
- 		return 0;
- 	return rrtname[type] != nil;
- }
-@@ -1891,7 +1892,7 @@
- 	char *t;
- 
- 	t = nil;
--	if(type >= 0 && type <= Tall)
-+	if(type >= 0 && type <= Tcaa)
- 		t = rrtname[type];
- 	if(t==nil){
- 		snprint(buf, len, "%d", type);
-diff -r 4adb989bc93e sys/src/cmd/ndb/dns.h
---- a/sys/src/cmd/ndb/dns.h	Tue Nov 03 20:47:14 2020 +0100
-+++ b/sys/src/cmd/ndb/dns.h	Sun Nov 29 16:42:47 2020 +0100
-@@ -71,6 +71,7 @@
- 	Tmailb=	253,	/* { Tmb, Tmg, Tmr } */
- 	Tmaila= 254,	/* obsolete */
- 	Tall=	255,	/* all records */
-+	Tcaa=	257,	/* Certification authority restriction */
- 
- 	/* classes */
- 	Csym=	0,	/* internal symbols */
diff --git a/sites/pmikkelsen.com/_files/websocket-webfs.patch b/sites/pmikkelsen.com/_files/websocket-webfs.patch
deleted file mode 100644
index 77c44b0..0000000
--- a/sites/pmikkelsen.com/_files/websocket-webfs.patch
+++ /dev/null
@@ -1,565 +0,0 @@
-From 424bcc25db6c3de73678fe43d44e4b408cd0434d
-From: Peter Mikkelsen <petermikkelsen10@gmail.com>
-Date: Wed, 23 Jun 2021 15:44:24 +0000
-Subject: [PATCH] Initial buggy version of adding websocket support to webfs
-
-
-It can create connections but doesn't handle errors very well yet.
----
-diff ce73821f3575921e24f839b21c7be60520a9dc42 424bcc25db6c3de73678fe43d44e4b408cd0434d
---- a/sys/src/cmd/webfs/fns.h	Mon Jun 21 17:38:11 2021
-+++ b/sys/src/cmd/webfs/fns.h	Wed Jun 23 17:44:24 2021
-@@ -41,3 +41,6 @@
- int authenticate(Url *u, Url *ru, char *method, char *s);
- void flushauth(Url *u, char *t);
- void http(char *m, Url *u, Key *shdr, Buq *qbody, Buq *qpost);
-+
-+/* websocket */
-+void websocket(int fd, Buq *qbody, Buq *qpost);
---- a/sys/src/cmd/webfs/fs.c	Mon Jun 21 17:38:11 2021
-+++ b/sys/src/cmd/webfs/fs.c	Wed Jun 23 17:44:24 2021
-@@ -4,6 +4,7 @@
- #include <fcall.h>
- #include <thread.h>
- #include <9p.h>
-+#include <libsec.h>
- 
- #include "dat.h"
- #include "fns.h"
-@@ -19,10 +20,12 @@
- 	Url	*baseurl;
- 	Url	*url;
- 	Key	*hdr;
-+	int	wantwebsocket;
- 
- 	int	obody;	/* body opend */
- 	int	cbody;	/* body closed */
- 	Buq	*qbody;
-+	Buq	*websocketin;	/* websocket input */
- };
- 
- struct Webfid
-@@ -121,6 +124,8 @@
- 
- 	buclose(cl->qbody, 0);
- 	bufree(cl->qbody);
-+	buclose(cl->websocketin, 0);
-+	bufree(cl->websocketin);
- 
- 	while(k = cl->hdr){
- 		cl->hdr = k->next;
-@@ -384,6 +389,25 @@
- 		if(cl->qbody == nil){
- 			char *m;
- 
-+			if(f->level == Qbody && (!strcmp(cl->url->scheme, "ws") || !strcmp(cl->url->scheme, "wss"))){
-+				cl->wantwebsocket = 1;
-+				cl->websocketin = bualloc(64*1024);
-+				if(!lookkey(cl->hdr, "Upgrade"))
-+					cl->hdr = addkey(cl->hdr, "Upgrade", "websocket");
-+				if(!lookkey(cl->hdr, "Connection"))
-+					cl->hdr = addkey(cl->hdr, "Connection", "upgrade");
-+				if(!lookkey(cl->hdr, "Sec-WebSocket-Version"))
-+					cl->hdr = addkey(cl->hdr, "Sec-WebSocket-Version", "13");
-+				if(!lookkey(cl->hdr, "Sec-WebSocket-Key")){
-+					uchar nonce[16];
-+					char *b64nonce;
-+					genrandom(nonce, 16);
-+					b64nonce = smprint("%.*[", 16, nonce);
-+					cl->hdr = addkey(cl->hdr, "Sec-WebSocket-Key", b64nonce);
-+					free(b64nonce);
-+				}
-+			}
-+
- 			if(cl->url == nil){
- 				respond(r, "no url set");
- 				return;
-@@ -413,7 +437,7 @@
- 			if(agent && !lookkey(cl->hdr, "User-Agent"))
- 				cl->hdr = addkey(cl->hdr, "User-Agent", agent);
- 
--			http(m, cl->url, cl->hdr, cl->qbody, f->buq);
-+			http(m, cl->url, cl->hdr, cl->qbody, cl->wantwebsocket ? cl->websocketin : f->buq);
- 			cl->request[0] = 0;
- 			cl->url = nil;
- 			cl->hdr = nil;
-@@ -683,6 +707,11 @@
- 	case Qpost:
- 		bureq(f->buq, r);
- 		return;
-+	case Qbody:
-+		if(f->client->wantwebsocket){
-+			bureq(f->client->websocketin, r);
-+			return;
-+		}
- 	}
- 	respond(r, "not implemented");
- }
---- a/sys/src/cmd/webfs/http.c	Mon Jun 21 17:38:11 2021
-+++ b/sys/src/cmd/webfs/http.c	Wed Jun 23 17:44:24 2021
-@@ -131,7 +131,7 @@
- 		if(strcmp(proxy->scheme, "https") == 0)
- 			fd = tlswrap(fd, proxy->host);
- 	} else {
--		if(strcmp(u->scheme, "https") == 0)
-+		if(strcmp(u->scheme, "https") == 0 || strcmp(u->scheme, "wss") == 0)
- 			fd = tlswrap(fd, u->host);
- 	}
- 	if(fd < 0){
-@@ -520,7 +520,7 @@
- void
- http(char *m, Url *u, Key *shdr, Buq *qbody, Buq *qpost)
- {
--	int i, l, n, try, pid, fd, cfd, needlength, chunked, retry, nobody, badauth;
-+	int i, l, n, try, pid, fd, cfd, needlength, chunked, retry, nobody, badauth, wantwebsocket;
- 	char *s, *x, buf[8192+2], status[256], method[16], *host;
- 	vlong length, offset;
- 	Url ru, tu, *nu;
-@@ -549,8 +549,13 @@
- 		break;
- 	}
- 
-+	if(!strcmp(u->scheme, "ws") || !strcmp(u->scheme, "wss"))
-+		wantwebsocket = 1;
-+	else
-+		wantwebsocket = 0;
-+
- 	notify(catch);
--	if(qpost){
-+	if(qpost && !wantwebsocket){
- 		/* file for spooling the postbody if we need to restart the request */
- 		snprint(buf, sizeof(buf), "/tmp/http.%d.%d.post", getppid(), getpid());
- 		fd = create(buf, OEXCL|ORDWR|ORCLOSE, 0600);
-@@ -565,7 +570,7 @@
- 	badauth = 0;
- 	for(try = 0; try < 12; try++){
- 		strcpy(status, "0 No status");
--		if(u == nil || (strcmp(u->scheme, "http") && strcmp(u->scheme, "https"))){
-+		if(u == nil || (strcmp(u->scheme, "http") && strcmp(u->scheme, "https") && strcmp(u->scheme, "ws") && strcmp(u->scheme, "wss"))){
- 			werrstr("bad url scheme");
- 			break;
- 		}
-@@ -591,7 +596,7 @@
- 
- 		length = 0;
- 		chunked = 0;
--		if(qpost){
-+		if(qpost && !wantwebsocket){
- 			/* have to read it to temp file to figure out the length */
- 			if(fd >= 0 && needlength && lookkey(shdr, "Content-Length") == nil){
- 				seek(fd, 0, 2);
-@@ -700,7 +705,7 @@
- 			goto Retry;
- 		}
- 
--		if(qpost && !h->tunnel){
-+		if(qpost && !h->tunnel && !wantwebsocket){
- 			h->cancel = 0;
- 			if((pid = rfork(RFMEM|RFPROC)) <= 0){
- 				int ifd;
-@@ -802,8 +807,42 @@
- 				goto Status;
- 			}
- 			goto Error;
--		case 100:	/* Continue */
- 		case 101:	/* Switching Protocols */
-+			if(wantwebsocket){
-+				int ok = 1;
-+				char *wskey = lookkey(shdr, "Sec-WebSocket-Key");
-+
-+				k = getkey(rhdr, "Upgrade");
-+				if(k == nil || cistrcmp(k->val, "websocket") != 0)
-+					ok = 0;
-+
-+				k = getkey(rhdr, "Connection");
-+				if(k == nil && cistrcmp(k->val, "upgrade") != 0)
-+					ok = 0;
-+
-+				k = getkey(rhdr, "Sec-WebSocket-Accept");
-+				if(k == nil || wskey == nil)
-+					ok = 0;
-+				else{
-+					uchar digest[SHA1dlen];
-+					char *str = smprint("%s258EAFA5-E914-47DA-95CA-C5AB0DC85B11", wskey);
-+					
-+					sha1((uchar*)str, strlen(str), digest, nil);
-+					char *val = smprint("%.*[", SHA1dlen, digest);
-+					if(strcmp(val, k->val) != 0)
-+						ok = 0;
-+					free(str);
-+					free(val);
-+				}
-+		
-+				if(ok){
-+					qbody->url = u; u = nil;
-+					qbody->hdr = rhdr; rhdr = nil;
-+					websocket(h->fd, qbody, qpost);
-+				}
-+				goto Error;
-+			}
-+		case 100:	/* Continue */
- 		case 102:	/* Processing */
- 		case 103:	/* Early Hints */
- 			while(k = rhdr){
---- a/sys/src/cmd/webfs/mkfile	Mon Jun 21 17:38:11 2021
-+++ b/sys/src/cmd/webfs/mkfile	Wed Jun 23 17:44:24 2021
-@@ -3,6 +3,6 @@
- TARG=webfs
- 
- HFILES=fns.h dat.h
--OFILES=sub.$O url.$O buq.$O http.$O fs.$O
-+OFILES=sub.$O url.$O buq.$O http.$O websocket.$O fs.$O
- 
- </sys/src/cmd/mkone
---- /dev/null	Mon Jun 21 23:24:08 2021
-+++ b/sys/src/cmd/webfs/websocket.c	Wed Jun 23 17:44:24 2021
-@@ -0,0 +1,349 @@
-+#include <u.h>
-+#include <libc.h>
-+#include <fcall.h>
-+#include <thread.h>
-+#include <9p.h>
-+#include <libsec.h>
-+
-+#include "dat.h"
-+#include "fns.h"
-+
-+typedef struct Frame Frame;
-+typedef struct Message Message;
-+
-+struct Frame
-+{
-+	int	final;
-+	int	opcode;
-+	int	masked;
-+	uchar	maskkey[4];
-+	uvlong	length;
-+	uchar	*data;
-+
-+	Frame	*next; /* Chain frames in a message together */
-+};
-+
-+struct Message
-+{
-+	int	type;
-+	uvlong	length;
-+	uchar	*data;
-+};
-+
-+enum {
-+	ContinueFrame	= 0x0,
-+	TextFrame	= 0x1,
-+	BinaryFrame	= 0x2,
-+	CloseFrame	= 0x8,
-+	PingFrame	= 0x9,
-+	PongFrame	= 0xA,
-+};
-+
-+void writemessage(int, Message *);
-+
-+void
-+maskframe(Frame *f)
-+{
-+	uvlong i;
-+	for(i = 0; i < f->length; i++)
-+		f->data[i] = f->data[i] ^ f->maskkey[i%4];
-+}
-+
-+Frame *
-+readframe(int fd)
-+{
-+	Frame *f = malloc(sizeof(Frame));
-+	long n;
-+	int offset;
-+	uchar len;
-+
-+	uchar buf[4096];
-+
-+Again:
-+	offset = 0;
-+	n = read(fd, buf, 2);
-+	if(n != 2)
-+		goto Error;
-+
-+	f->final = (buf[offset] >> 7) & 0x1;
-+	/* ignore rsv1, rsv2, rsv3 */
-+	f->opcode = buf[offset] & 0x0F;
-+	offset++;
-+
-+	f->masked = (buf[offset] >> 7) & 0x1;
-+	len = buf[offset] & 0x7F;
-+	offset++;
-+
-+	if(len <= 125)
-+		f->length = len;
-+	else if(len == 126){
-+		n = read(fd, buf+offset, 2);
-+		if(n != 2)
-+			goto Error;
-+		
-+		f->length = buf[offset++] << 8;
-+		f->length |= buf[offset++];
-+	}else if(len == 127){
-+		n = read(fd, buf+offset, 8);
-+		if(n != 8)
-+			goto Error;
-+		f->length = (uvlong)buf[offset++] << 56;
-+		f->length |= (uvlong)buf[offset++] << 48;
-+		f->length |= (uvlong)buf[offset++] << 40;
-+		f->length |= (uvlong)buf[offset++] << 32;
-+		f->length |= buf[offset++] << 24;
-+		f->length |= buf[offset++] << 16;
-+		f->length |= buf[offset++] << 8;
-+		f->length |= buf[offset++];
-+	}
-+
-+	if(f->masked){
-+		n = read(fd, buf+offset, 4);
-+		if(n != 4)
-+			goto Error;
-+
-+		f->maskkey[0] = buf[offset++];
-+		f->maskkey[1] = buf[offset++];
-+		f->maskkey[2] = buf[offset++];
-+		f->maskkey[3] = buf[offset];
-+	}
-+
-+	f->data = malloc(f->length);
-+	readn(fd, f->data, f->length);
-+	if(f->masked)
-+		maskframe(f);
-+
-+	if(f->opcode == PingFrame){
-+		Message *m = malloc(sizeof(Message));
-+		m->type = PongFrame;
-+		m->length = f->length;
-+		m->data = f->data;
-+		writemessage(fd, m); /* SHOULD LOCK */
-+		free(m);
-+		free(f->data);
-+		goto Again;
-+	}
-+
-+	return f;
-+Error:
-+	exits("Readframe failed");
-+	return nil;
-+}
-+
-+Message *
-+framestomessage(Frame *frames)
-+{
-+	Message *m = malloc(sizeof(Message));
-+	uvlong length = 0;
-+	uvlong offset = 0;
-+
-+	Frame *f;
-+	for(f = frames; f != nil; f = f->next)
-+		length += f->length;
-+
-+	m->type = frames->opcode;
-+	m->length = length;
-+	m->data = malloc(length);
-+	for(f = frames; f != nil; f = f->next){
-+		memcpy(m->data + offset, f->data, f->length);
-+		offset += f->length;
-+	}
-+
-+	return m;
-+}
-+
-+Message *
-+readmsg(int fd)
-+{
-+	Frame *frames = readframe(fd);
-+	Frame *last = frames;
-+	Message *m;
-+
-+	while(!last->final){
-+		last->next = readframe(fd);
-+		last = last->next;
-+	}
-+	last->next = nil;
-+
-+	m = framestomessage(frames);
-+	while(frames){
-+		Frame *f = frames->next;
-+		free(frames->data);
-+		free(frames);
-+		frames = f;
-+	}
-+	return m;
-+}
-+
-+void
-+writeframe(int fd, Frame *f)
-+{
-+	uchar *buf;
-+	uvlong totsize = 0;
-+	uvlong offset = 0;
-+	int lenbytes = 0;
-+
-+	totsize += 2; /* Always there */
-+	if(f->length == 126)
-+		lenbytes = 2;
-+	else if(f->length == 127)
-+		lenbytes = 8;
-+	totsize += lenbytes;
-+
-+	if(f->masked)
-+		totsize += 4;
-+	
-+	totsize += f->length;
-+
-+	buf = malloc(totsize);
-+
-+	buf[offset] = f->final << 7;
-+	buf[offset++] |= f->opcode;
-+	buf[offset] = f->masked << 7;
-+
-+	if(lenbytes == 0)
-+		buf[offset++] |= f->length;
-+	else if(lenbytes == 2)
-+		buf[offset++] |= 126;
-+	else if(lenbytes == 8)
-+		buf[offset++] |= 127;
-+
-+	if(lenbytes == 2){
-+		buf[offset++] = 0xFF & (f->length >> 8);
-+		buf[offset++] = 0xFF & f->length;
-+	}else if(lenbytes == 8){
-+		buf[offset++] = 0xFF & (f->length >> 56);
-+		buf[offset++] = 0xFF & (f->length >> 48);
-+		buf[offset++] = 0xFF & (f->length >> 40);
-+		buf[offset++] = 0xFF & (f->length >> 32);
-+		buf[offset++] = 0xFF & (f->length >> 24);
-+		buf[offset++] = 0xFF & (f->length >> 16);
-+		buf[offset++] = 0xFF & (f->length >> 8);
-+		buf[offset++] = 0xFF & f->length;
-+	}
-+
-+	if(f->masked){
-+		buf[offset++] = f->maskkey[0];
-+		buf[offset++] = f->maskkey[1];
-+		buf[offset++] = f->maskkey[2];
-+		buf[offset++] = f->maskkey[3];
-+	}
-+
-+	memcpy(buf + offset, f->data, f->length);
-+	write(fd, buf, totsize);
-+}
-+
-+void
-+writemessage(int fd, Message *m)
-+{
-+	/* Could split up the message into frames but not right now. */
-+
-+	Frame *f = malloc(sizeof(Frame));
-+	f->final = 1;
-+	f->opcode = m->type;
-+	f->masked = 1;
-+	genrandom(f->maskkey, 4);
-+	f->length = m->length;
-+	f->data = malloc(f->length);
-+	memcpy(f->data, m->data, f->length);
-+	maskframe(f);
-+	f->next = nil;
-+	
-+	writeframe(fd, f);
-+	free(f->data);
-+	free(f);
-+}
-+
-+void
-+websocketrecv(int fd, Buq *qbody)
-+{
-+	/*
-+	 * Plan: Read frames and when we have a whole message do:
-+	 * 1) If control, act on it
-+	 * 2) If data, format as text and buwrite it
-+	*/
-+	while(1){
-+		Message *m = readmsg(fd);
-+		//print("Received message type=%d length=%ulld\n", m->type, m->length);
-+
-+		if(m->type == TextFrame || m->type == BinaryFrame){
-+			char *header;
-+			if(m->type == TextFrame)
-+				header = smprint("t %0.20ulld", m->length);
-+			else
-+				header = smprint("b %0.20ulld", m->length);
-+			buwrite(qbody, header, 22);
-+			buwrite(qbody, m->data, m->length);
-+		}
-+		free(m->data);
-+		free(m);
-+	}
-+}
-+
-+void
-+websocketsend(int fd, Buq *qpost)
-+{
-+	/* buread messages and pack them up in frames and send them */
-+	char buf[64];
-+	long n;
-+	Message *m;
-+	while(1){
-+		n = buread(qpost, buf, 22);
-+		if(n != 22){
-+			buclose(qpost, "Header short");
-+			return;
-+		}
-+		buf[n] = 0;
-+
-+		m = malloc(sizeof(Message));
-+		if(buf[0] == 't')
-+			m->type = TextFrame;
-+		else if(buf[0] == 'b')
-+			m->type = BinaryFrame;
-+
-+		char *ret;
-+		m->length = strtoull(buf+2, &ret, 10);
-+		if(ret != buf+22){
-+			buclose(qpost, "Header format wrong");
-+			return;
-+		}
-+
-+		m->data = malloc(m->length);
-+		n = 0;
-+		while(n < m->length){
-+			uvlong missing = m->length - n;
-+			n += buread(qpost, m->data + n, (missing < 8192) ? missing : 8192);
-+		}
-+
-+		writemessage(fd, m);
-+		free(m->data);
-+		free(m);
-+	}
-+}
-+
-+void
-+websocket(int fd, Buq *qbody, Buq *qpost)
-+{
-+	buwrite(qbody, "websocket ready\n", 16);
-+	switch(rfork(RFPROC|RFMEM)){
-+	default:
-+		websocketrecv(fd, qbody);
-+		break;
-+	case 0:
-+		websocketsend(fd, qpost);
-+		goto End;
-+	case -1:
-+		buclose(qbody, "can't fork");
-+		bufree(qbody);
-+		buclose(qpost, "can't fork");
-+		bufree(qpost);
-+		break;
-+	}
-+End:
-+	close(fd);
-+	buclose(qbody, nil);
-+	bufree(qbody);
-+	buclose(qpost, nil);
-+	bufree(qpost);
-+	exits(nil);
-+}
diff --git a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html b/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html
deleted file mode 100644
index 1be20f5..0000000
--- a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.Cubical.html
+++ /dev/null
@@ -1,55 +0,0 @@
-<!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
deleted file mode 100644
index 5829754..0000000
--- a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.Primitive.html
+++ /dev/null
@@ -1,35 +0,0 @@
-<!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
deleted file mode 100644
index 3a4b225..0000000
--- a/sites/pmikkelsen.com/_tmp/agda-dfa/Agda.css
+++ /dev/null
@@ -1,39 +0,0 @@
-/* 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
deleted file mode 100644
index 308e205..0000000
--- a/sites/pmikkelsen.com/_tmp/agda-dfa/DFA.html
+++ /dev/null
@@ -1,115 +0,0 @@
-<!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
diff --git a/sites/pmikkelsen.com/_werc/config b/sites/pmikkelsen.com/_werc/config
index 85a49d9..c71d503 100644
--- a/sites/pmikkelsen.com/_werc/config
+++ b/sites/pmikkelsen.com/_werc/config
@@ -1,3 +1,3 @@
 masterSite=pmikkelsen.com
 siteTitle='Peter&#39;s website'
-siteSubTitle='random notes'
+siteSubTitle='- random notes'
diff --git a/sites/pmikkelsen.com/_werc/lib/footer.inc b/sites/pmikkelsen.com/_werc/lib/footer.inc
deleted file mode 100644
index 90fc345..0000000
--- a/sites/pmikkelsen.com/_werc/lib/footer.inc
+++ /dev/null
@@ -1 +0,0 @@
-<a href="http://werc.cat-v.org">Powered by werc</a> © Peter Mikkelsen 2019-2024
diff --git a/sites/pmikkelsen.com/_werc/lib/top_bar.inc b/sites/pmikkelsen.com/_werc/lib/top_bar.inc
deleted file mode 100644
index 5e5c7bc..0000000
--- a/sites/pmikkelsen.com/_werc/lib/top_bar.inc
+++ /dev/null
@@ -1,11 +0,0 @@
-    <div class="left">
-		<a href="https://git.sr.ht/~pmikkelsen">sourcehut</a> |
-		<a href="https://gitlab.com/pmikkelsen">gitlab</a> |
-		<a href="https://prolog.pmikkelsen.com">prolog</a> |
-		<a href="https://apl.pmikkelsen.com">APL9</a> |
-		<a href="http://9front.org">9front</a>
-    </div>
-
-    <div class="right">
-    </div>
-
diff --git a/sites/pmikkelsen.com/favicon.ico b/sites/pmikkelsen.com/favicon.ico
deleted file mode 100644
index 745367e..0000000
--- a/sites/pmikkelsen.com/favicon.ico
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/2048.gif b/sites/pmikkelsen.com/images/2048.gif
deleted file mode 100644
index 19dd98f..0000000
--- a/sites/pmikkelsen.com/images/2048.gif
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/acme-in-action.png b/sites/pmikkelsen.com/images/acme-in-action.png
deleted file mode 100644
index b74d9dc..0000000
--- a/sites/pmikkelsen.com/images/acme-in-action.png
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/cdude.png b/sites/pmikkelsen.com/images/cdude.png
deleted file mode 100644
index 66ee18d..0000000
--- a/sites/pmikkelsen.com/images/cdude.png
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/creepy_glenda.jpg b/sites/pmikkelsen.com/images/creepy_glenda.jpg
deleted file mode 100644
index c1a35ba..0000000
--- a/sites/pmikkelsen.com/images/creepy_glenda.jpg
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/cursed.png b/sites/pmikkelsen.com/images/cursed.png
deleted file mode 100644
index f92e06e..0000000
--- a/sites/pmikkelsen.com/images/cursed.png
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/discordgif.gif b/sites/pmikkelsen.com/images/discordgif.gif
deleted file mode 100644
index 207af41..0000000
--- a/sites/pmikkelsen.com/images/discordgif.gif
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/djvfonts.png b/sites/pmikkelsen.com/images/djvfonts.png
deleted file mode 100644
index 86d58a4..0000000
--- a/sites/pmikkelsen.com/images/djvfonts.png
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/fear.jpg b/sites/pmikkelsen.com/images/fear.jpg
deleted file mode 100644
index b585dfc..0000000
--- a/sites/pmikkelsen.com/images/fear.jpg
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/hehegame.gif b/sites/pmikkelsen.com/images/hehegame.gif
deleted file mode 100644
index 5c385cb..0000000
--- a/sites/pmikkelsen.com/images/hehegame.gif
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/hehegame2.gif b/sites/pmikkelsen.com/images/hehegame2.gif
deleted file mode 100644
index 5c385cb..0000000
--- a/sites/pmikkelsen.com/images/hehegame2.gif
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/hehegame3.gif b/sites/pmikkelsen.com/images/hehegame3.gif
deleted file mode 100644
index 231f8ef..0000000
--- a/sites/pmikkelsen.com/images/hehegame3.gif
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/kykeliky.png b/sites/pmikkelsen.com/images/kykeliky.png
deleted file mode 100644
index 0144cae..0000000
--- a/sites/pmikkelsen.com/images/kykeliky.png
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/linuxreverse.gif b/sites/pmikkelsen.com/images/linuxreverse.gif
deleted file mode 100644
index 6684116..0000000
--- a/sites/pmikkelsen.com/images/linuxreverse.gif
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/mordor.gif b/sites/pmikkelsen.com/images/mordor.gif
deleted file mode 100644
index fe13c09..0000000
--- a/sites/pmikkelsen.com/images/mordor.gif
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/rustdude.png b/sites/pmikkelsen.com/images/rustdude.png
deleted file mode 100644
index c184664..0000000
--- a/sites/pmikkelsen.com/images/rustdude.png
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/walkoff.png b/sites/pmikkelsen.com/images/walkoff.png
deleted file mode 100644
index 871bb7c..0000000
--- a/sites/pmikkelsen.com/images/walkoff.png
+++ /dev/null
diff --git a/sites/pmikkelsen.com/images/wip-discord.png b/sites/pmikkelsen.com/images/wip-discord.png
deleted file mode 100644
index 2ecafcc..0000000
--- a/sites/pmikkelsen.com/images/wip-discord.png
+++ /dev/null
diff --git a/sites/pmikkelsen.com/me/how-i-started-using-acme.md b/sites/pmikkelsen.com/me/how-i-started-using-acme.md
index 9e37dd7..143839b 100644
--- a/sites/pmikkelsen.com/me/how-i-started-using-acme.md
+++ b/sites/pmikkelsen.com/me/how-i-started-using-acme.md
@@ -114,4 +114,4 @@ text in sam with is another editor written by Rob Pike, and I quite like
 that one too for smaller projects. You can read more about sam
 [here](http://sam.cat-v.org/).
 
-[1]: /images/acme-in-action.png
\ No newline at end of file
+[1]: https://images.pmikkelsen.com/acme-in-action.png
diff --git a/sites/pmikkelsen.com/plan9/discord.md b/sites/pmikkelsen.com/plan9/discord.md
index 8a9815f..fd7a508 100644
--- a/sites/pmikkelsen.com/plan9/discord.md
+++ b/sites/pmikkelsen.com/plan9/discord.md
@@ -80,4 +80,4 @@ I don't even notice it is not running locally.
 * No, this has not been tested very much, it just seems to do the job
 well enough for now.
 
-[1]: /images/discordgif.gif
+[1]: https://images.pmikkelsen.com/discordgif.gif
diff --git a/sites/pmikkelsen.com/plan9/fonts.md b/sites/pmikkelsen.com/plan9/fonts.md
index 6cd6780..d062276 100644
--- a/sites/pmikkelsen.com/plan9/fonts.md
+++ b/sites/pmikkelsen.com/plan9/fonts.md
@@ -4,9 +4,9 @@ By default 9front uses a font called VGA but its too small for my eyes.
 
 The fonts I use (dejavu) look like this[![an image showing the fonts][1]][1] and are attached below:
 
-[proportional font](/_files/djv.tar)
+[proportional font](https://files.pmikkelsen.com/djv.tar)
 
-[monospace font](/_files/djvmono.tar)
+[monospace font](https://files.pmikkelsen.com/djvmono.tar)
 
 They can be recreated by having them installed on linux and doing the following from
 linux with plan9port installed.
@@ -26,4 +26,4 @@ Finally change your `lib/profile` to use `/lib/font/bit/djv/font` :)
 Note that 9front includes truetypefs which allows you to use `.ttf` files
 directly, but I find the results are better looking this way.
 
-[1]: /images/djvfonts.png
\ No newline at end of file
+[1]: https://images.pmikkelsen.com/djvfonts.png
diff --git a/sites/pmikkelsen.com/plan9/lets_encrypt.md b/sites/pmikkelsen.com/plan9/lets_encrypt.md
index c22d0fa..a7eae3a 100644
--- a/sites/pmikkelsen.com/plan9/lets_encrypt.md
+++ b/sites/pmikkelsen.com/plan9/lets_encrypt.md
@@ -10,7 +10,7 @@ Install certbot on linux and run the following command
 	certbot certonly --manual -d pmikkelsen.com -d vps1.pmikkelsen.com
 
 and do the challenges, they should be easy.
-I use the diff [here](/_files/ndb.diff) to make 9fronts dns server understand the needed records.
+I use the diff [here](https://files.pmikkelsen.com/ndb.diff) to make 9fronts dns server understand the needed records.
 
 *EDIT*: As of Sun Feb 14 2021, this patch is no longer needed since cinap pushed a [proper fix](http://code.9front.org/hg/plan9front/rev/73935ff27172).
 
diff --git a/sites/pmikkelsen.com/plan9/mounting-9p-over-drawterm.md b/sites/pmikkelsen.com/plan9/mounting-9p-over-drawterm.md
index 414b9f2..cb04b97 100644
--- a/sites/pmikkelsen.com/plan9/mounting-9p-over-drawterm.md
+++ b/sites/pmikkelsen.com/plan9/mounting-9p-over-drawterm.md
@@ -55,4 +55,4 @@ This means I can just go into any directory on the server, type `linux ghci` and
 The bind net trick still blows my mind a bit, since it is so trivial, yet so powerful. It is also fun to think about how one would do this
 on other systems than plan9, which I can't even imagine.
 
-[1]: /images/linuxreverse.gif
+[1]: https://images.pmikkelsen.com/linuxreverse.gif
diff --git a/sites/pmikkelsen.com/plan9/webfs-websocket.md b/sites/pmikkelsen.com/plan9/webfs-websocket.md
index c229f95..084411b 100644
--- a/sites/pmikkelsen.com/plan9/webfs-websocket.md
+++ b/sites/pmikkelsen.com/plan9/webfs-websocket.md
@@ -1,7 +1,7 @@
 # Creating websocket connections via 9front's webfs
 
 With the following patch (note: work in progress, contains bugs), 9front's webfs can be used
-to create websocket connections. The patch is available [here](/_files/websocket-webfs.patch).
+to create websocket connections. The patch is available [here](https://files.pmikkelsen.com/websocket-webfs.patch).
 
 ## The idea
 
@@ -74,4 +74,4 @@ back to the user.
 ## Bugs
 
 Yes. The code doesn't really handle errors or connection shutdowns yet. Also, I need to add proper cleanup code
-around in different places.
\ No newline at end of file
+around in different places.
diff --git a/sites/prolog.pmikkelsen.com/_werc/lib/footer.inc b/sites/prolog.pmikkelsen.com/_werc/lib/footer.inc
deleted file mode 100644
index 996a89a..0000000
--- a/sites/prolog.pmikkelsen.com/_werc/lib/footer.inc
+++ /dev/null
@@ -1 +0,0 @@
-<a href="http://werc.cat-v.org">Powered by werc</a> © Peter Mikkelsen 2020-2022
\ No newline at end of file
diff --git a/sites/prolog.pmikkelsen.com/_werc/lib/top_bar.inc b/sites/prolog.pmikkelsen.com/_werc/lib/top_bar.inc
deleted file mode 100644
index e6a79eb..0000000
--- a/sites/prolog.pmikkelsen.com/_werc/lib/top_bar.inc
+++ /dev/null
@@ -1,8 +0,0 @@
-    <div class="left">
-		<a href="https://git.sr.ht/~pmikkelsen/pprolog">pprolog source code</a> |
-		<a href="https://pmikkelsen.com">pmikkelsen's site</a> |
-		<a href="http://9front.org">9front</a>
-    </div>
-
-    <div class="right">
-    </div>
diff --git a/sites/prolog.pmikkelsen.com/favicon.ico b/sites/prolog.pmikkelsen.com/favicon.ico
deleted file mode 100644
index 745367e..0000000
--- a/sites/prolog.pmikkelsen.com/favicon.ico
+++ /dev/null
diff --git a/sites/prolog.pmikkelsen.com/index.md b/sites/prolog.pmikkelsen.com/index.md
index 730d8c0..e1e24df 100644
--- a/sites/prolog.pmikkelsen.com/index.md
+++ b/sites/prolog.pmikkelsen.com/index.md
@@ -69,4 +69,4 @@ and many more all listed [here](https://git.sr.ht/~pmikkelsen/pprolog/tree/maste
 
 [![A picture of pprolog in action][1]][1]
 
-[1]: /_images/prolog-screenshot.png
+[1]: https://images.pmikkelsen.com/prolog-screenshot.png