A textbook on informal homotopy type theory
Switch branches/tags
Nothing to show
Clone or download
Pull request Compare This branch is 852 commits behind HoTT:master.
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
coq_introduction
cover/torus
other
.gitattributes
.gitignore
CONTRIBUTING.md
CONVENTIONS.txt
GIT_CHEATSHEET.txt
Makefile
README.md
back.tex
basics.tex
blurb.tex
categories.tex
cleveref.sty
cover-a4.tex
cover-hires-back-bw.png
cover-hires-back.png
cover-hires-bw.png
cover-hires-front-bw.png
cover-hires-front.png
cover-hires.png
cover-letter.tex
cover-lores-back-bw.png
cover-lores-back.png
cover-lores-front-bw.png
cover-lores-front.png
cover-lores.png
cover-lulu-hardcover.tex
cover-lulu-paperback.tex
equivalences.tex
errata.tex
exercise_solutions.tex
filter-errata
formal.tex
front.tex
frontpage.tex
geometry.sty
halpha.bst
hits.tex
hlevels.tex
homotopy.tex
hott-a4.tex
hott-ebook.tex
hott-letter.tex
hott-online.tex
hott-ustrade.tex
ifxetex.sty
induction.tex
introduction.tex
logic.tex
macros.tex
main.labelnumbers.first-edition
main.tex
mathpartir.sty
opt-a4.tex
opt-bastard.tex
opt-black-white.tex
opt-color.tex
opt-cover.tex
opt-ebook.tex
opt-letter.tex
opt-no-bastard.tex
opt-no-cover.tex
opt-ustrade.tex
preface.tex
preliminaries.tex
reals.tex
references.bib
setmath.tex
symbols.tex
torus-hires-bw.png
torus-lores-bw.png

README.md

This is a textbook that we are writing on informal homotopy type theory. It is part of the Univalent foundations of mathematics project which took place at the Institute for Advanced Study in 2012/13.

License

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License.

Prerequisites and compilation

To compile the book you need a fairly new version of LaTeX. Texlive 2012 is confirmed to work. You might need to install some packages, see main.tex for packages that are used by the book.

BasicTeX, which is a minimalistic version of MacTeX is confirmed to work once the following packages have been installed: tlmgr, install, braket, comment, courier, enumitem, helvetic, mathpazo, nextpage, ntheorem, palatino, rsfs, stmaryrd, symbol, titlesec, wallpaper, wasy, wasysym, xstring, zapfding.

You also need the make utility. The book is a fairly complex piece of LaTeX code. Also, the file version.tex is generated on the fly, so you will need the make utlity with which you can compile the main files, as follows:

  • make hott-online.pdf -- the book appropriate for online reading, with colors and green links
  • make hott-ebook.pdf -- the book with small margins, suitable for ebook readers
  • make hott-letter.pdf hott-cover.pdf -- the book in black & white, letter paper format, for printing at home, as well as a color cover (just two pages)
  • make hott-a4.pdf hott-a4.pdf -- the book in black & white, A4 paper format, for printing at home, as well as a color cover (just two pages)
  • make hott-ustrade.pdf cover-lulu.pdf -- the book in US Trade format, without cover, used for the bound copy available at http://lulu.com/
  • make exercise_solutions.pdf -- compile (some) solutions to exercises

If you do not have make (for example, because you are on MacOS and you did not install the XCode command-line utilities), you can still fake it as follows. Create the file version.txt and put in it (where "Joe Hacker" should be replaced with your name):

\newcommand{\OPTversion}{Joe-Hacker-version}

Then use whatever tools you normally do to compile LaTeX. The main LaTeX files are called hott-XXX.tex. But you really should have make, you know.

Once make is run so that version.txt gets generated, you need not run make again. You can just perform the usual LaTeX cycle from your favorite editor.