Skip to content

Home

Jump to bottom Edit New page
Ali Caglayan edited this page Mar 4, 2023 · 33 revisions

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.

  • An interactive reference manual autogenerated by Alectryon.

    Hovering 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.

  • 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.

We also have solutions to some exercises from the HoTT Book:

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):

HoTT Core Library Dependency Graph

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

HoTT Library Dependency Graph

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:

Add a custom footer
Add a custom sidebar
Clone this wiki locally