Add references
This commit is contained in:
commit
453063e51b
1
.gitignore
vendored
Normal file
1
.gitignore
vendored
Normal file
|
@ -0,0 +1 @@
|
|||
cat.pdf
|
40
Makefile
Normal file
40
Makefile
Normal file
|
@ -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)
|
26
cat.md
Normal file
26
cat.md
Normal file
|
@ -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
|
||||
==========
|
42
refs.bib
Normal file
42
refs.bib
Normal file
|
@ -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}
|
||||
}
|
Loading…
Reference in a new issue