{"name":"coqPackages.HoTT","summary":"Homotopy Type Theory library","description":"Homotopy Type Theory is an interpretation of Martin-Löf’s intensional\ntype theory into abstract homotopy theory. Propositional equality is\ninterpreted as homotopy and type isomorphism as homotopy equivalence.\nLogical constructions in type theory then correspond to\nhomotopy-invariant constructions on spaces, while theorems and even\nproofs in the logical system inherit a homotopical meaning. As the\nnatural logic of homotopy, type theory is also related to higher\ncategory theory as it is used e.g. in the notion of a higher topos.\n\nThe HoTT library is a development of homotopy-theoretic ideas in the Coq\nproof assistant. It draws many ideas from Vladimir Voevodsky's\nFoundations library (which has since been incorporated into the Unimath\nlibrary) and also cross-pollinates with the HoTT-Agda library.","homepage_url":"https://homotopytypetheory.org/","license":"","attribute_paths":["coqPackages.HoTT"],"releases":[{"version":"9.0","last_updated":"2026-03-21T07:29:51Z","platforms":[{"arch":"arm64","os":"macOS","system":"aarch64-darwin","attribute_path":"coqPackages.HoTT","commit_hash":"09061f748ee21f68a089cd5d91ec1859cd93d0be","date":"2026-03-21T07:29:51Z","outputs":[{"name":"out","path":"/nix/store/8djkn1w0bsi77w317r8k3c8fzbagvh3a-coq9.0-HoTT-9.0","default":true}],"broken":false,"insecure":false},{"arch":"arm64","os":"Linux","system":"aarch64-linux","attribute_path":"coqPackages.HoTT","commit_hash":"09061f748ee21f68a089cd5d91ec1859cd93d0be","date":"2026-03-21T07:29:51Z","outputs":[{"name":"out","path":"/nix/store/b2r2vsw5zk8cm0gb1x7bqaz2lfydn042-coq9.0-HoTT-9.0","default":true}],"broken":false,"insecure":false},{"arch":"x86-64","os":"macOS","system":"x86_64-darwin","attribute_path":"coqPackages.HoTT","commit_hash":"09061f748ee21f68a089cd5d91ec1859cd93d0be","date":"2026-03-21T07:29:51Z","outputs":[{"name":"out","path":"/nix/store/x49jan3w1cy15m3ny3yrwb47a2yhmmw1-coq9.0-HoTT-9.0","default":true}],"broken":false,"insecure":false},{"arch":"x86-64","os":"Linux","system":"x86_64-linux","attribute_path":"coqPackages.HoTT","commit_hash":"09061f748ee21f68a089cd5d91ec1859cd93d0be","date":"2026-03-21T07:29:51Z","outputs":[{"name":"out","path":"/nix/store/d3ijdrdlpiwd6vnalf5vhyi32k181wg1-coq9.0-HoTT-9.0","default":true}],"broken":false,"insecure":false}],"platforms_summary":"Linux and macOS","outputs_summary":"","prerelease":false,"broken":false,"insecure":false},{"version":"8.20","last_updated":"2025-03-11T17:52:14Z","platforms":[{"arch":"arm64","os":"macOS","system":"aarch64-darwin","attribute_path":"coqPackages.HoTT","commit_hash":"0d534853a55b5d02a4ababa1d71921ce8f0aee4c","date":"2025-03-11T17:52:14Z","outputs":[{"name":"out","path":"/nix/store/iacvqfnh6wlkrqy2m404m5xgz5qlzl9m-coq8.20-HoTT-8.20","default":true}],"broken":false,"insecure":false},{"arch":"arm64","os":"Linux","system":"aarch64-linux","attribute_path":"coqPackages.HoTT","commit_hash":"0d534853a55b5d02a4ababa1d71921ce8f0aee4c","date":"2025-03-11T17:52:14Z","outputs":[{"name":"out","path":"/nix/store/8mshwn0qg2wvhdw1skgcrk6iln3lkh2i-coq8.20-HoTT-8.20","default":true}],"broken":false,"insecure":false},{"arch":"x86-64","os":"macOS","system":"x86_64-darwin","attribute_path":"coqPackages.HoTT","commit_hash":"0d534853a55b5d02a4ababa1d71921ce8f0aee4c","date":"2025-03-11T17:52:14Z","outputs":[{"name":"out","path":"/nix/store/zjnkk8rnp4mvqdvp2ygfj8w622fapnch-coq8.20-HoTT-8.20","default":true}],"broken":false,"insecure":false},{"arch":"x86-64","os":"Linux","system":"x86_64-linux","attribute_path":"coqPackages.HoTT","commit_hash":"0d534853a55b5d02a4ababa1d71921ce8f0aee4c","date":"2025-03-11T17:52:14Z","outputs":[{"name":"out","path":"/nix/store/li05b1jhkl624jqhn70yhjxqldwgljaf-coq8.20-HoTT-8.20","default":true}],"broken":false,"insecure":false}],"platforms_summary":"Linux and macOS","outputs_summary":"","prerelease":false,"broken":false,"insecure":false},{"version":"8.19","last_updated":"2024-08-31T10:12:23Z","platforms":[{"arch":"arm64","os":"macOS","system":"aarch64-darwin","attribute_path":"coqPackages.HoTT","commit_hash":"5629520edecb69630a3f4d17d3d33fc96c13f6fe","date":"2024-08-31T10:12:23Z","outputs":[{"name":"out","path":"/nix/store/dgvjdk61hnwq86idhqa3160kyfm1x1vs-coq8.19-HoTT-8.19","default":true}],"broken":false,"insecure":false},{"arch":"arm64","os":"Linux","system":"aarch64-linux","attribute_path":"coqPackages.HoTT","commit_hash":"5629520edecb69630a3f4d17d3d33fc96c13f6fe","date":"2024-08-31T10:12:23Z","outputs":[{"name":"out","path":"/nix/store/mbzq6sk69m25wpfh9z42i49mlb7zaxgn-coq8.19-HoTT-8.19","default":true}],"broken":false,"insecure":false},{"arch":"x86-64","os":"macOS","system":"x86_64-darwin","attribute_path":"coqPackages.HoTT","commit_hash":"5629520edecb69630a3f4d17d3d33fc96c13f6fe","date":"2024-08-31T10:12:23Z","outputs":[{"name":"out","path":"/nix/store/m5bh2hnndqywlz1l7zj0zabbppiad5v5-coq8.19-HoTT-8.19","default":true}],"broken":false,"insecure":false},{"arch":"x86-64","os":"Linux","system":"x86_64-linux","attribute_path":"coqPackages.HoTT","commit_hash":"5629520edecb69630a3f4d17d3d33fc96c13f6fe","date":"2024-08-31T10:12:23Z","outputs":[{"name":"out","path":"/nix/store/920f5lmn2abdi90c7n9x3yn9miw9lb50-coq8.19-HoTT-8.19","default":true}],"broken":false,"insecure":false}],"platforms_summary":"Linux and macOS","outputs_summary":"","prerelease":false,"broken":false,"insecure":false},{"version":"8.18","last_updated":"2024-04-24T04:52:23Z","platforms":[{"arch":"arm64","os":"macOS","system":"aarch64-darwin","attribute_path":"coqPackages.HoTT","commit_hash":"a9040b7bf8adcd322493722106dd603eb87694ea","date":"2024-04-24T04:52:23Z","outputs":[{"name":"out","path":"/nix/store/nnxkwwhaphx0rzcx51rnrs90fq1yj9zn-coq8.18-HoTT-8.18","default":true}],"broken":false,"insecure":false},{"arch":"arm64","os":"Linux","system":"aarch64-linux","attribute_path":"coqPackages.HoTT","commit_hash":"a9040b7bf8adcd322493722106dd603eb87694ea","date":"2024-04-24T04:52:23Z","outputs":[{"name":"out","path":"/nix/store/v8jz3m0v237wxpr9xq5gf9s6cqs0dskp-coq8.18-HoTT-8.18","default":true}],"broken":false,"insecure":false},{"arch":"x86-64","os":"macOS","system":"x86_64-darwin","attribute_path":"coqPackages.HoTT","commit_hash":"a9040b7bf8adcd322493722106dd603eb87694ea","date":"2024-04-24T04:52:23Z","outputs":[{"name":"out","path":"/nix/store/c6zsj7dkjgc8l0chlmgz3cnf0p6ncbam-coq8.18-HoTT-8.18","default":true}],"broken":false,"insecure":false},{"arch":"x86-64","os":"Linux","system":"x86_64-linux","attribute_path":"coqPackages.HoTT","commit_hash":"a9040b7bf8adcd322493722106dd603eb87694ea","date":"2024-04-24T04:52:23Z","outputs":[{"name":"out","path":"/nix/store/kgmvmvhgm2jqd1blr2cbi01vd6chnbj7-coq8.18-HoTT-8.18","default":true}],"broken":false,"insecure":false}],"platforms_summary":"Linux and macOS","outputs_summary":"","prerelease":false,"broken":false,"insecure":false},{"version":"8.17","last_updated":"2023-09-15T06:49:28Z","platforms":[{"arch":"arm64","os":"macOS","system":"aarch64-darwin","attribute_path":"coqPackages.HoTT","commit_hash":"46688f8eb5cd6f1298d873d4d2b9cf245e09e88e","date":"2023-09-15T06:49:28Z","outputs":[{"name":"out","path":"/nix/store/h1da92kdkkj2plk9kdr0w4ggwrr4lly3-coq8.17-HoTT-8.17","default":true}],"broken":false,"insecure":false},{"arch":"arm64","os":"Linux","system":"aarch64-linux","attribute_path":"coqPackages.HoTT","commit_hash":"46688f8eb5cd6f1298d873d4d2b9cf245e09e88e","date":"2023-09-15T06:49:28Z","outputs":[{"name":"out","path":"/nix/store/s9w7pfpix59px1pv8xrw99n031pllg4i-coq8.17-HoTT-8.17","default":true}],"broken":false,"insecure":false},{"arch":"x86-64","os":"macOS","system":"x86_64-darwin","attribute_path":"coqPackages.HoTT","commit_hash":"46688f8eb5cd6f1298d873d4d2b9cf245e09e88e","date":"2023-09-15T06:49:28Z","outputs":[{"name":"out","path":"/nix/store/9n5ldl3lgdvz0fnrib6hpcbzhsan96rd-coq8.17-HoTT-8.17","default":true}],"broken":false,"insecure":false},{"arch":"x86-64","os":"Linux","system":"x86_64-linux","attribute_path":"coqPackages.HoTT","commit_hash":"46688f8eb5cd6f1298d873d4d2b9cf245e09e88e","date":"2023-09-15T06:49:28Z","outputs":[{"name":"out","path":"/nix/store/q6299c3khdi9a430myszwb29sxg52prz-coq8.17-HoTT-8.17","default":true}],"broken":false,"insecure":false}],"platforms_summary":"Linux and macOS","outputs_summary":"","prerelease":false,"broken":false,"insecure":false},{"version":"8.16","last_updated":"2023-04-13T03:55:09Z","platforms":[{"arch":"arm64","os":"macOS","system":"aarch64-darwin","attribute_path":"coqPackages.HoTT","commit_hash":"96ba1c52e54e74c3197f4d43026b3f3d92e83ff9","date":"2023-04-13T03:55:09Z","outputs":[{"name":"out","path":"/nix/store/f0li294frjlrimcdy909agmxr8f8cvd2-coq8.16-HoTT-8.16","default":true}],"broken":false,"insecure":false},{"arch":"arm64","os":"Linux","system":"aarch64-linux","attribute_path":"coqPackages.HoTT","commit_hash":"96ba1c52e54e74c3197f4d43026b3f3d92e83ff9","date":"2023-04-13T03:55:09Z","outputs":[{"name":"out","path":"/nix/store/iwsli98qi3s629bsliiidppxlnbc8645-coq8.16-HoTT-8.16","default":true}],"broken":false,"insecure":false},{"arch":"x86-64","os":"macOS","system":"x86_64-darwin","attribute_path":"coqPackages.HoTT","commit_hash":"96ba1c52e54e74c3197f4d43026b3f3d92e83ff9","date":"2023-04-13T03:55:09Z","outputs":[{"name":"out","path":"/nix/store/q5bm6s7q8s01mp1p5l22nqfh2qkafg67-coq8.16-HoTT-8.16","default":true}],"broken":false,"insecure":false},{"arch":"x86-64","os":"Linux","system":"x86_64-linux","attribute_path":"coqPackages.HoTT","commit_hash":"96ba1c52e54e74c3197f4d43026b3f3d92e83ff9","date":"2023-04-13T03:55:09Z","outputs":[{"name":"out","path":"/nix/store/0264kkrmhrqfakh3rmhbds23c3w04h2a-coq8.16-HoTT-8.16","default":true}],"broken":false,"insecure":false}],"platforms_summary":"Linux and macOS","outputs_summary":"","prerelease":false,"broken":false,"insecure":false}]}