nixsearch / pkg / coqPackages.HoTT

coqPackages.HoTT

Homotopy Type Theory library

homotopytypetheory.org coqPackages.HoTT 6 releases newest changed 6 months ago

version9.0 attributecoqPackages.HoTT rev09061f748ee21f68a089cd5d91ec1859cd93d0be 2026-03-21 · one commit for every system systems✓ aarch64-darwin✓ aarch64-linux✓ x86_64-darwin✓ x86_64-linux

$ devbox add coqPackages.HoTT@9.0

$ nix shell github:NixOS/nixpkgs/09061f748ee21f68a089cd5d91ec1859cd93d0be#coqPackages.HoTT

JSON: /v2/resolve?name=coqPackages.HoTT&version=latest

Releases

newest first, as /v2/pkg orders them

Version	arm mac	arm linux	x86 mac	x86 linux	Attribute	Commit	Date
9.0resolved	✓	✓	✓	✓	`coqPackages.HoTT`	09061f748e	2026-03-21
8.20	✓	✓	✓	✓	`coqPackages.HoTT`	0d534853a5	2025-03-11
8.19	✓	✓	✓	✓	`coqPackages.HoTT`	5629520ede	2024-08-31
8.18	✓	✓	✓	✓	`coqPackages.HoTT`	a9040b7bf8	2024-04-24
8.17	✓	✓	✓	✓	`coqPackages.HoTT`	46688f8eb5	2023-09-15
8.16	✓	✓	✓	✓	`coqPackages.HoTT`	96ba1c52e5	2023-04-13

Prereleases are listed but latest never picks one. “varies” means each system last changed at a different nixpkgs commit — the release page lists them.

Description

Homotopy Type Theory is an interpretation of Martin-Lö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.