blob: 970591264d73aa3dc126588b5fa96ef9cd50d38d (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
|
{ lib, mkCoqDerivation, coq, version ? null }:
mkCoqDerivation {
pname = "HoTT";
repo = "Coq-HoTT";
owner = "HoTT";
inherit version;
defaultVersion = with lib.versions; lib.switch coq.coq-version [
{ case = range "8.14" "8.18"; out = coq.coq-version; }
] null;
releaseRev = v: "V${v}";
release."8.14".sha256 = "sha256-7kXk2pmYsTNodHA+Qts3BoMsewvzmCbYvxw9Sgwyvq0=";
release."8.15".sha256 = "sha256-JfeiRZVnrjn3SQ87y6dj9DWNwCzrkK3HBogeZARUn9g=";
release."8.16".sha256 = "sha256-xcEbz4ZQ+U7mb0SEJopaczfoRc2GSgF2BGzUSWI0/HY=";
release."8.17".sha256 = "sha256-GjTUpzL9UzJm4C2ilCaYEufLG3hcj7rJPc5Op+OMal8=";
release."8.18".sha256 = "sha256-URoUoQOsG0432wg9i6pTRomWQZ+ewutq2+V29TBrVzc=";
# versions of HoTT for Coq 8.17 and onwards will use dune
# opam-name = if lib.versions.isLe "8.17" coq.coq-version then "coq-hott" else null;
opam-name = "coq-hott";
useDune = lib.versions.isGe "8.17" coq.coq-version;
patchPhase = ''
patchShebangs etc
'';
meta = {
homepage = "https://homotopytypetheory.org/";
description = "The Homotopy Type Theory library";
longDescription = ''
Homotopy Type Theory is an interpretation of Martin-Löf’s intensional
type theory into abstract homotopy theory. Propositional equality is
interpreted as homotopy and type isomorphism as homotopy equivalence.
Logical constructions in type theory then correspond to
homotopy-invariant constructions on spaces, while theorems and even
proofs in the logical system inherit a homotopical meaning. As the
natural logic of homotopy, type theory is also related to higher
category theory as it is used e.g. in the notion of a higher topos.
The HoTT library is a development of homotopy-theoretic ideas in the Coq
proof assistant. It draws many ideas from Vladimir Voevodsky's
Foundations library (which has since been incorporated into the Unimath
library) and also cross-pollinates with the HoTT-Agda library.
'';
maintainers = with lib.maintainers; [ alizter siddharthist ];
};
}
|