From 1dde3f8e747dce6ab29d83b7c236cc2eaf79ade8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Frederik=20Hangh=C3=B8j=20Iversen?= Date: Fri, 23 Mar 2018 11:22:17 +0100 Subject: [PATCH] Restructure latex-stuff --- doc/Makefile | 6 +++--- doc/main.tex | 52 ++++++++++++++++++++++++++++++++++++++++++++++++ doc/proposal.tex | 51 ----------------------------------------------- 3 files changed, 55 insertions(+), 54 deletions(-) create mode 100644 doc/main.tex diff --git a/doc/Makefile b/doc/Makefile index 8561a59..4d43828 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -3,7 +3,7 @@ # Originally from : http://tex.stackexchange.com/a/40759 # # Change only the variable below to the name of the main tex file. -PROJNAME=proposal +PROJNAME=univalent-categories # You want latexmk to *always* run, because make does not have all the info. # Also, include non-file targets in .PHONY so they are run regardless of any @@ -36,8 +36,8 @@ all: $(PROJNAME).pdf # -interactive=nonstopmode keeps the pdflatex backend from stopping at a # missing file reference and interactively asking you for an alternative. -$(PROJNAME).pdf: $(PROJNAME).tex - latexmk -pdf -pdflatex="pdflatex -interactive=nonstopmode" -use-make $< +$(PROJNAME).pdf: main.tex + latexmk -jobname=$(PROJNAME) -pdf -pdflatex="pdflatex -interactive=nonstopmode" -use-make $< cleanall: latexmk -C diff --git a/doc/main.tex b/doc/main.tex new file mode 100644 index 0000000..fd5f132 --- /dev/null +++ b/doc/main.tex @@ -0,0 +1,52 @@ +\documentclass{article} + + + +\usepackage[utf8]{inputenc} + +\usepackage{natbib} +\usepackage[hidelinks]{hyperref} + +\usepackage{graphicx} + +\usepackage{parskip} +\usepackage{multicol} +\usepackage{amsmath,amssymb} +\usepackage[toc,page]{appendix} +\usepackage{xspace} + +% \setlength{\parskip}{10pt} + +% \usepackage{tikz} +% \usetikzlibrary{arrows, decorations.markings} + +% \usepackage{chngcntr} +% \counterwithout{figure}{section} + +\usepackage{chalmerstitle} +\input{macros.tex} + +\title{Category Theory and Cubical Type Theory} +\author{Frederik Hanghøj Iversen} +\authoremail{hanghj@student.chalmers.se} +\supervisor{Thierry Coquand} +\supervisoremail{coquand@chalmers.se} +\cosupervisor{Andrea Vezzosi} +\cosupervisoremail{vezzosi@chalmers.se} +\institution{Chalmers University of Technology} + +\begin{document} + +\maketitle + +\input{proposal.tex} + +\bibliographystyle{plainnat} +\nocite{cubical-demo} +\nocite{coquand-2013} +\bibliography{refs} +\begin{appendices} +\input{planning.tex} +\input{halftime.tex} +\end{appendices} +\end{document} diff --git a/doc/proposal.tex b/doc/proposal.tex index 073ecb5..aad24c5 100644 --- a/doc/proposal.tex +++ b/doc/proposal.tex @@ -1,44 +1,3 @@ -\documentclass{article} - - - -\usepackage[utf8]{inputenc} - -\usepackage{natbib} -\usepackage[hidelinks]{hyperref} - -\usepackage{graphicx} - -\usepackage{parskip} -\usepackage{multicol} -\usepackage{amsmath,amssymb} -\usepackage[toc,page]{appendix} -\usepackage{xspace} - -% \setlength{\parskip}{10pt} - -% \usepackage{tikz} -% \usetikzlibrary{arrows, decorations.markings} - -% \usepackage{chngcntr} -% \counterwithout{figure}{section} - -\usepackage{chalmerstitle} -\input{macros.tex} - -\title{Category Theory and Cubical Type Theory} -\author{Frederik Hanghøj Iversen} -\authoremail{hanghj@student.chalmers.se} -\supervisor{Thierry Coquand} -\supervisoremail{coquand@chalmers.se} -\cosupervisor{Andrea Vezzosi} -\cosupervisoremail{vezzosi@chalmers.se} -\institution{Chalmers University of Technology} - -\begin{document} - -\maketitle -% \section{Introduction} % Functional extensionality and univalence is not expressible in @@ -277,13 +236,3 @@ intend to formally implement the language of dependent type theory in this project. The thesis shall conclude with a discussion about the benefits of Cubical Agda. -% -\bibliographystyle{plainnat} -\nocite{cubical-demo} -\nocite{coquand-2013} -\bibliography{refs} -\begin{appendices} -\input{planning.tex} -\input{halftime.tex} -\end{appendices} -\end{document}