Bas Spitters edited this page Jun 15, 2016 · 22 revisions

Welcome to the wiki for the HoTT/HoTT library!

Important and helpful information for anyone using or contributing to the library can be found in the STYLE file in the repository.

A reference manual autogenerated by coqdoc. (index) (table of contents)

An interactive reference manual autogenerated by proviola; hovering over a line of code will display the feedback given by Coq at that point in the code. (index) (table of contents)

Coq can also be run in your browser with JsCoq/JsHoTT.

An index for the HoTT library based on the HoTT book (in order of appearance in the book), autogenerated by coqdoc.

An interactive index for the HoTT library based on the HoTT book, autogenerated by proviola.

A table of contents for the HoTT library which includes timing information for the lines in each file, autogenerated by a script adapted from Microsoft Research's SSReflect library.

Solutions to some exercises from the HoTT book, autogenerated by proviola.

Hyperlinked dependency graph of the core library, created using GraphViz, borrowing a script from MathClasses (click to enlarge):

HoTT Core Library Dependency Graph

Hyperlinked dependency graph of the entire library (click to enlarge):

HoTT Library Dependency Graph

Dependency graphs of theorems in files, created by the dpdgraph tool of Anne Pacalet and Yves Bertot.

HoTT in the Coq bench marking tool.

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.