A textbook on informal homotopy type theory
TeX Python Coq Mathematica Shell Makefile Other
Latest commit e5a9d85 Feb 7, 2017 @mikeshulman mikeshulman committed on GitHub Merge pull request #932 from OliveiraHermogenes/patch-1
small grammar correction (between vs. among)
Permalink
Failed to load latest commit information.
coq_introduction Fix a few typos in HoTT in Coq intro. Jun 4, 2016
cover/torus Fix file permissions Jun 27, 2013
etc/ci fix the keep-old-nightly-builds code Dec 10, 2015
other index-helper: exclude \indexdefs containing backslashes May 24, 2013
.gitattributes Try to prevent line ending problems Apr 13, 2013
.gitignore Updated \`.gitignore\` to include all generated covers (\`cover-A4\` … Nov 2, 2016
.travis.yml Update .travis.yml to avoid 404 - better new URI Jul 29, 2016
CONTRIBUTING.md improve CONTRIBUTING.md to mention issues in addition to PRs Jun 2, 2015
CONVENTIONS.txt Removed references to natbib, since not actually used since 2013. Nov 2, 2016
GIT_CHEATSHEET.txt Changed instructions that tell people to use `git add --all`, Apr 27, 2013
Makefile Add dvimode, remove pagecolor package Apr 16, 2014
README.md Update README, close #857 Aug 28, 2015
back.tex omit header on blank versos, fix #269 Jun 17, 2013
basics.tex Explain "equality reasoning" for path-concatenation, close #913 Sep 8, 2016
blurb.tex justify back cover Jun 19, 2013
bmpsize-hack.tex Add dvimode, remove pagecolor package Apr 16, 2014
build-nightlies Create a file `version` with the latest identifier Aug 6, 2015
categories.tex Clarify wording Jan 26, 2016
cleveref.sty Update cleveref from 0.17.9 to 0.19 Mar 28, 2014
cover-a4.tex Add dvimode, remove pagecolor package Apr 16, 2014
cover-hires-back-bw.png Blue-gray cover, B&W version of cover for home printing Jun 4, 2013
cover-hires-back.png Blue-gray cover, B&W version of cover for home printing Jun 4, 2013
cover-hires-bw.png Blue-gray cover, B&W version of cover for home printing Jun 4, 2013
cover-hires-front-bw.png Blue-gray cover, B&W version of cover for home printing Jun 4, 2013
cover-hires-front.png Blue-gray cover, B&W version of cover for home printing Jun 4, 2013
cover-hires.png Blue Steve with dark gray torus Jun 4, 2013
cover-letter.tex Add dvimode, remove pagecolor package Apr 16, 2014
cover-lores-back-bw.png Reduce size of low resolution images Jun 19, 2013
cover-lores-back.png Reduce size of low resolution images Jun 19, 2013
cover-lores-front-bw.png Reduce size of low resolution images Jun 19, 2013
cover-lores-front.png Reduce size of low resolution images Jun 19, 2013
cover-lores.png Reduce size of low resolution images Jun 19, 2013
cover-lulu-hardcover.png Remove alpha channel from Lulu cover images Jun 18, 2014
cover-lulu-hardcover.tex Remove transparency from lulu.com covers Jun 4, 2014
cover-lulu-paperback.png Remove alpha channel from Lulu cover images Jun 18, 2014
cover-lulu-paperback.tex Remove transparency from lulu.com covers Jun 4, 2014
equivalences.tex Obey style in Definition 4.2.1 Aug 16, 2016
errata.tex Mark Errata (auto) Nov 21, 2016
exercise_solutions.tex Removed references to natbib, since not actually used since 2013. Nov 2, 2016
filter-errata rename filtered-errata files to not clash with those posted on the we… Aug 5, 2013
formal.tex remove incorrect sentence about Streicher, close #866 Dec 3, 2015
front.tex Made the visible URL's fixed-width Dec 31, 2014
frontpage.tex white letters on gray-blue Jun 4, 2013
geometry.sty Added geometry.sty and ifxetex.sty. Mar 8, 2013
halpha.bst replace natbib by halpha, close #220 May 21, 2013
hits.tex 6.4: fix induction principle for S^2 Aug 11, 2016
hlevels.tex Add reference to thm:ttac Oct 3, 2016
homotopy.tex Merge branch '8.8.3' of https://github.com/peterlefanulumsdaine/book Nov 21, 2016
hott-a4.tex A4 version Jun 20, 2013
hott-ebook.tex changed "resultion" to "resolution" on line 3 Dec 17, 2014
hott-letter.tex Bastard title, fix ebook format. Jun 17, 2013
hott-online.tex Bastard title, fix ebook format. Jun 17, 2013
hott-ustrade.tex Bastard title, fix ebook format. Jun 17, 2013
ifxetex.sty Added geometry.sty and ifxetex.sty. Mar 8, 2013
induction.tex Merge pull request #830 from danielgerigk/Walgebra Jul 6, 2015
introduction.tex Merge pull request #775 from mikeshulman/church Dec 4, 2015
logic.tex better formulation suggested by Mike Shulman Feb 7, 2017
macros.tex Mention a higher coherence path, close #785 Apr 16, 2015
main.labelnumbers.first-edition A script to automatically check whether label numbers have changed Jul 3, 2013
main.tex Removed references to natbib, since not actually used since 2013. Nov 2, 2016
mark-errata Make the errata marker work after merges Nov 27, 2013
mathpartir.sty Misspellings run Jun 21, 2013
opt-a4.tex fix ebook-overfulls Nov 22, 2013
opt-bastard.tex Bastard title, fix ebook format. Jun 17, 2013
opt-black-white.tex Tweaks to allow latex (and not only pdflatex) to compile the book Apr 14, 2014
opt-color.tex Tweaks to allow latex (and not only pdflatex) to compile the book Apr 14, 2014
opt-cover.tex New and shiny cover Jun 4, 2013
opt-ebook.tex fix ebook-overfulls Nov 22, 2013
opt-letter.tex fix ebook-overfulls Nov 22, 2013
opt-no-bastard.tex Bastard title, fix ebook format. Jun 17, 2013
opt-no-cover.tex New and shiny cover Jun 4, 2013
opt-ustrade.tex fix ebook-overfulls Nov 22, 2013
preface.tex "univalent foundations" is not capitalized Jun 10, 2013
preliminaries.tex Merge pull request #884 from jeffersoncarpenter/Id Jan 10, 2016
reals.tex Fix typo in Thm. 11.3.16 Sep 6, 2016
references.bib Made Sambin credit visible in bib entry for Martin-Löf Biliopolis boo… Nov 2, 2016
setmath.tex Fix notation $\in V$ Sep 3, 2016
symbols.tex removed hyphens in path constructor and point constructor for consist… Jan 29, 2016
torus-hires-bw.png Half-title page, variable quality of images. Jun 5, 2013
torus-lores-bw.png Reduce size of low resolution images Jun 19, 2013

README.md

This is a textbook on informal homotopy type theory. It is part of the Univalent foundations of mathematics project that 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.

Distribution

Compiled and printed versions of the book are available at the homotopy type theory website, and nightly builds are available on the github wiki.

Prerequisites and compilation

To compile the book for yourself 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 utility 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-hardcover.pdf cover-lulu-paperback.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
  • make errata.pdf -- Errata for the HoTT Book, first edition

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.tex 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.tex gets generated, you need not run make again. You can just perform the usual LaTeX cycle from your favorite editor.