A Coq library for Homotopy Type Theory
-
Updated
Oct 9, 2026 - Rocq Prover
#
homotopy-type-theory
Here are 73 public repositories matching this topic...
Experimental implementation of Cubical Type Theory
-
Updated
Sep 21, 2023 - Haskell
A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
-
Updated
Oct 7, 2026 - Agda
The agda-unimath library
category-theory graph-theory species trees group-theory number-theory commutative-algebra homotopy-type-theory univalent-foundations finite-groups order-theory univalent-mathematics universal-algebra ring-theory structured-types univalent-combinatorics synthetic-homotopy-theory higher-group-theory type-theories orthogonal-factorization-systems
-
Updated
Oct 8, 2026 - Agda
An experimental proof assistant based on a type theory for synthetic ∞-categories.
-
Updated
Oct 10, 2026 - Haskell
Logical manifestations of topological concepts, and other things, via the univalent point of view.
type-theory agda ordinal homotopy-type-theory univalent-foundations constructive-mathematics compact-type totally-separated-type injective-type searchable-set univalent-mathematics
-
Updated
Oct 10, 2026 - Agda
😎TT
-
Updated
Nov 20, 2025 - OCaml
Lecture notes on univalent foundations of mathematics with Agda
dependent-types type-theory agda lecture-notes mltt homotopy-type-theory univalent-foundations univalent-mathematics hott-uf martin-lof-type-theory univalence-axiom function-extensionality propositional-truncation univalent-type-theory
-
Updated
Dec 30, 2025 - Agda
Agda formalisation of the Introduction to Homotopy Type Theory
mathematics agda textbook univalence homotopy-type-theory univalent-foundations mathematics-library univalent-mathematics hott-uf univalence-axiom
-
Updated
Nov 27, 2021 - Agda
Ground Zero: Lean 4 HoTT Library
-
Updated
Feb 17, 2026 - Lean
A formalization of category theory in cubical Agda
-
Updated
May 24, 2020 - Agda
Formal Topology in Univalent Foundations (WIP).
topology homotopy-type-theory univalent-foundations univalent-mathematics formal-topologies locale-theory pointless-topology constructive-topology
-
Updated
Jul 29, 2022 - CSS
An experimental implementation of homotopy type theory in the interactive proof assistant Isabelle
-
Updated
Nov 30, 2022 - Standard ML
Two-Level Type Theory
-
Updated
Dec 13, 2019 - Lean
🧊 An indexed construction of semi-simplicial and semi-cubical sets
-
Updated
Oct 11, 2026 - Rocq Prover
Anders: Cubical Type Checker
dependent-types proof-assistant cubical-type-theory type-system hott theorem-prover type-checker mltt ctt homotopy-type-theory dependent-type-theory
-
Updated
Oct 23, 2023 - OCaml
🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory
-
Updated
Nov 20, 2025 - OCaml
Homotopy Type Theory proofs in Idris
-
Updated
May 22, 2019 - Idris
Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda
type-theory category-theory agda uni hott univalence agda-library homotopy-type-theory univalent-foundations univalent-mathematics martin-lof-type-theory univalence-axiom
-
Updated
Aug 25, 2026 - Agda
Personal research notes
dependent-types functional-programming proof-assistant type-theory cubical-type-theory programming-languages term-rewriting nominal-set homotopy-type-theory
-
Updated
Oct 18, 2024 - Coq
Add this topic to your repo
To associate your repository with the homotopy-type-theory topic, visit your repo's landing page and select "manage topics."