From 453063e51badfb6e4742a9f282e8e36c260d6521 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= <fhi.1990@gmail.com>
Date: Sat, 27 May 2017 16:09:52 +0200
Subject: [PATCH] Add references

---
 .gitignore |  1 +
 Makefile   | 40 ++++++++++++++++++++++++++++++++++++++++
 cat.md     | 26 ++++++++++++++++++++++++++
 refs.bib   | 42 ++++++++++++++++++++++++++++++++++++++++++
 4 files changed, 109 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 Makefile
 create mode 100644 cat.md
 create mode 100644 refs.bib

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..acf395a
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+cat.pdf
diff --git a/Makefile b/Makefile
new file mode 100644
index 0000000..0e61431
--- /dev/null
+++ b/Makefile
@@ -0,0 +1,40 @@
+PROJECT = cat
+PDF = $(PROJECT).pdf
+NOTES = $(PROJECT).md
+
+preview: report
+	xdg-open $(PDF)
+
+report: $(PDF)
+
+$(PDF): $(NOTES)
+	pandoc $(NOTES) \
+		-o $(PDF) \
+		--latex-engine=xelatex \
+		--variable urlcolor=cyan \
+		-V papersize:a4 \
+		-V geometry:margin=1.5in \
+		--filter pandoc-citeproc
+
+github: README.md
+
+README.md: $(NOTES)
+	pandoc $(NOTES) \
+		-o README.md
+
+run:
+	stack exec lab4
+
+build:
+	stack build
+
+dist: report
+	tar \
+		--transform "s/^/$(PROJECT)\//" \
+		-zcvf $(PROJECT).tar.gz \
+		$(SOURCE) \
+		LICENSE \
+		stack.yaml \
+		lab4.cabal \
+		Makefile \
+		$(PDF)
diff --git a/cat.md b/cat.md
new file mode 100644
index 0000000..9ba319d
--- /dev/null
+++ b/cat.md
@@ -0,0 +1,26 @@
+---
+title: Formalizing category theory in Agda - Project description
+date: May 27th 2017
+author: Frederik Hanghøj Iversen
+bibliography: refs.bib
+---
+
+Background
+==========
+
+Aim
+===
+
+Timeplan
+========
+
+Resources
+=========
+
+* Cubical demo by Andrea Vezossi: [@cubical-demo]
+* Book on cubical type theory [@cohen-2016]
+* Book on homotopy type theory: [@hott-2013]
+* Book on category theory: [@awodey-2006]
+
+References
+==========
diff --git a/refs.bib b/refs.bib
new file mode 100644
index 0000000..855fcf9
--- /dev/null
+++ b/refs.bib
@@ -0,0 +1,42 @@
+@article{cohen-2016,
+  author    = {Cyril Cohen and
+               Thierry Coquand and
+               Simon Huber and
+               Anders M{\"{o}}rtberg},
+  title     =
+    { Cubical Type Theory:
+      a constructive interpretation of the univalence axiom
+    },
+  journal   = {CoRR},
+  volume    = {abs/1611.02108},
+  year      = {2016},
+  url       = {http://arxiv.org/abs/1611.02108},
+  timestamp = {Thu, 01 Dec 2016 19:32:08 +0100},
+  biburl    = {http://dblp.uni-trier.de/rec/bib/journals/corr/CohenCHM16},
+  bibsource = {dblp computer science bibliography, http://dblp.org}
+}
+@book{hott-2013,
+  author =    {The {Univalent Foundations Program}},
+  title =     {Homotopy Type Theory: Univalent Foundations of Mathematics},
+  publisher = {\url{https://homotopytypetheory.org/book}},
+  address =   {Institute for Advanced Study},
+  year =      2013
+}
+@book{awodey-2006,
+  title={Category Theory},
+  author={Awodey, S.},
+  isbn={9780191513824},
+  series={Oxford Logic Guides},
+  url={https://books.google.se/books?id=IK\_sIDI2TCwC},
+  year={2006},
+  publisher={Ebsco Publishing}
+}
+@misc{cubical-demo,
+  author = {Andrea Vezzosi},
+  title = {Cubical Type Theory Demo},
+  year = {2017},
+  publisher = {GitHub},
+  journal = {GitHub repository},
+  howpublished = {\url{https://github.com/Saizan/cubical-demo}},
+  commit = {a51d5654c439111110d5b6df3605b0043b10b753}
+}
\ No newline at end of file