MyNixOS website logo
Description

The Homotopy Type Theory library.

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.

Metadata

Version

8.18

License

Unknown

Platforms (44)

    Darwin
    FreeBSD 13
    Linux
    NetBSD
    OpenBSD
    Redox
    Solaris
    Windows
Show all
  • aarch64-darwin
  • aarch64-linux
  • aarch64-netbsd
  • armv5tel-linux
  • armv6l-linux
  • armv6l-netbsd
  • armv7a-darwin
  • armv7a-linux
  • armv7a-netbsd
  • armv7l-linux
  • armv7l-netbsd
  • i686-cygwin
  • i686-darwin
  • i686-freebsd13
  • i686-linux
  • i686-netbsd
  • i686-openbsd
  • loongarch64-linux
  • m68k-linux
  • m68k-netbsd
  • microblaze-linux
  • microblazeel-linux
  • mips-linux
  • mips64-linux
  • mips64el-linux
  • mipsel-linux
  • mipsel-netbsd
  • powerpc-netbsd
  • powerpc64-linux
  • powerpc64le-linux
  • riscv32-linux
  • riscv32-netbsd
  • riscv64-linux
  • riscv64-netbsd
  • s390-linux
  • s390x-linux
  • x86_64-cygwin
  • x86_64-darwin
  • x86_64-freebsd13
  • x86_64-linux
  • x86_64-netbsd
  • x86_64-openbsd
  • x86_64-redox
  • x86_64-solaris