All Categories → No Category → homotopy-type-theory

Top 7 homotopy-type-theory open source projects

A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory

✭ 93

Agda haskell SCSS Nix HTML javascript shell agda homotopy-type-theory

An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle

✭ 30

Standard ML Isabelle type-theory interactive-theorem-proving homotopy-type-theory

formal-topology-in-UF

Formal Topology in Univalent Foundations (WIP).

✭ 27

CSS shell Makefile topology homotopy-type-theory univalent-foundations univalent-mathematics formal-topologies locale-theory pointless-topology constructive-topology

Homotopy Type Theory proofs in Idris

✭ 19

Idris type-theory homotopy-type-theory

A formalization of category theory in cubical Agda

✭ 50

Agda Makefile category-theory agda homotopy-type-theory

Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.

✭ 132

Agda TeX type-theory agda ordinal homotopy-type-theory univalent-foundations constructive-mathematics compact-type totally-separated-type injective-type searchable-set univalent-mathematics

1-7 of 7 homotopy-type-theory projects