hott
Here are 33 public repositories matching this topic...
An introductory course to Homotopy Type Theory
-
Updated
Jul 24, 2020 - Agda
Ground Zero: Lean 4 HoTT Library
-
Updated
Feb 17, 2026 - Lean
Anders: Cubical Type Checker
-
Updated
Oct 23, 2023 - OCaml
Kitcat is an experimental Univalent mathematics library for proof theory, category theory, and computer science formalization in Agda
-
Updated
Aug 25, 2026 - Agda
-
Updated
Jun 8, 2026 - Agda
Castle Bravo: Experimental HoTT Implementation
-
Updated
Jun 16, 2023 - OCaml
-
Updated
Dec 17, 2018
Hurricane: HoTT-I Type System
-
Updated
Jun 17, 2026 - OCaml
Proving Ground: Tools for Automated Mathematics
-
Updated
Aug 21, 2018 - Jupyter Notebook
Diagnostic extension for redtt prover
-
Updated
Feb 26, 2022 - TypeScript
-
Updated
Oct 2, 2018
Formalizing Homotopy-Bridge and Hodge Cycles alignment via Cubical Agda & HoTT in Observation Log David 8.
-
Updated
Sep 6, 2026 - Agda
Write function for one data type, let it work with all sorts of variations of it
-
Updated
Feb 9, 2024 - TypeScript
Self-hostable paraconsistent HoTT LLM-to-Lean acceptance gateway. Runs proof attempts through security preflight, Lean checks, theorem-fingerprint locks, and ShadowHoTT bilattice routing for accept/repair/reject/human-review decisions.
-
Updated
May 26, 2026 - Python
Construction of the Hopf fibration in Homotopy Type Theory, using the HoTT library for Coq.
-
Updated
Mar 23, 2020 - HTML
Add this topic to your repo
To associate your repository with the hott topic, visit your repo's landing page and select "manage topics."