Home - HoTT/Coq-HoTT GitHub Wiki
Welcome to the Wiki for the Coq-HoTT library!
Important and helpful information for anyone using or contributing to the library can be found in the STYLE.md file in the repository.
Documentation
Reference manual
We have various bits of browsable documentation for the HoTT library:
-
A reference manual autogenerated by coqdoc.
- Coqdoc - Table of Contents
- Coqdoc - Index - Warning: This page is very large.
-
Alectryon.
An interactive reference manual autogenerated byHovering over a line of code will display the feedback given by Coq at that point in the code. You can also step through the proofs as if interacting with Coq.
- Alectryon - Table of Contents
- Alectryon - Index - Warning: This page is very large.
-
An interactive view of the timing information for each line in each file.
Autogenerated by a script adapted from Microsoft Research's SSReflect library. Hovering over a line will display the time taken for the command to run as a tooltip.
The HoTT Book
We have an index linking various theorems and definitions from the HoTT Book to the HoTT library.
- Index for the HoTT Book - autogenerated by Alectryon.
- Index for the HoTT Book - autogenerated by Coqdoc.
We also have solutions to some exercises from the HoTT Book:
- HoTT Book Exercises - autogenerated by Alectryon.
- HoTT Book Exercises - autogenerated by Coqdoc.
Dependency graphs
We autogenerate dependency graphs using the dpdgraph tool of Anne Pacalet and Yves Bertot. This allows us to create the following images using GraphViz, borrowing a script from MathClasses.
Dependency graphs of theorems in files, created by the dpdgraph tool of Anne Pacalet and Yves Bertot.
Hyperlinked dependency graph of the core library (click to enlarge):
Hyperlinked dependency graph of the entire library (click to enlarge):
JsHoTT - Run the HoTT library in Javascript!
Coq can be run in your browser with JsCoq/JsHoTT.
Coq-bench
HoTT is routinely benched in Coq-bench. See: