You are viewing the staging branch of the website @ 58d46ed, not the live version.

package coq-hott

Overview
Homepage

You can search for identifiers within the package.

in-package search v0.2.0

The Homotopy Type Theory library

Install

Dune Dependency

homotopytypetheory.org Edit opam file Versions (15)

Authors

T

The HoTT Library Development Team

Maintainers

J

Jason Gross <jgross@mit.edu>
A

Ali Caglayan <alizter@gmail.com>

Sources

V9.0.tar.gz

sha512=8f386158a51315904bfda64399aeaff7eb43cc6ecd0bf1c48b95ca316a51cf7e2c824c9aa795c357754b98f6069400d4184f8c83f9c7ce53197c420c9f65d832

Description

To use the HoTT library, the following flags must be passed to coqc: -noinit -indices-matter To use the HoTT library in a project, add the following to _CoqProject: -arg -noinit -arg -indices-matter

Published: 29 Sep 2025

Dependencies (4)

coq >= "8.19.0" & < "9~"
coq-core >= "9.0" & < "9.1~"
rocq-core >= "9.0" & < "9.1~"
dune >= "3.13"

Dev Dependencies

None

Used by (1)

coq-trocq-hott

Conflicts