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 (16)

Authors

T

The HoTT Library Development Team

Maintainers

J

Jason Gross <jgross@mit.edu>
A

Ali Caglayan <alizter@gmail.com>

Sources

V9.1.tar.gz

sha512=134caf34ea9353967325699fc211b7df0eb32654b34b70c8eed321da3da937b45e823c5e925058840593c9cb3c26617dac945a3e64d2cf04e9d9bc9216d7616d

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: 09 Jul 2026

Dependencies (5)

coq >= "8.19.0" & < "9.2~"
coq-core >= "9.0" & < "9.2~"
rocq-core >= "9.0" & < "9.2~"
dune >= "3.13"
ocaml >= "4.14"

Dev Dependencies

None

Used by (1)

coq-trocq-hott

Conflicts