A Coq library for Homotopy Type Theory
-
Updated
Nov 2, 2026 - Rocq Prover
#
univalent-foundations
Here are 16 public repositories matching this topic...
Experimental implementation of Cubical Type Theory
-
Updated
Sep 21, 2023 - Haskell
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 18, 2026 - Agda
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 31, 2026 - Agda
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
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
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
Experiments with Realizability in Univalent Type Theory
cubical-type-theory category-theory univalent-foundations univalent-mathematics univalent-type-theory realizability
-
Updated
Oct 21, 2024 - HTML
My undergradate thesis on coinductive types in univalent type theory
-
Updated
May 10, 2018 - TeX
Castle Bravo: Experimental HoTT Implementation
dependent-types proof-assistant hott theorem-prover type-checker mltt homotopy-type-theory univalent-foundations hott-uf
-
Updated
Jun 16, 2023 - OCaml
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
-
Updated
Mar 15, 2025 - Coq
Formalized Mathematics
-
Updated
Nov 9, 2017 - Coq
My implementation of the HOTT/UF book
-
Updated
Apr 4, 2025 - Coq
A constructive formalization of first-order logic, Peano Arithmetic, syntax trees, and Gödel numbering within Homotopy Type Theory (HoTT)
dependent-types latex inductive-types mathematical-logic homotopy-type-theory univalent-foundations proof-theory formal-systems peano-axioms peano-arithmetic
-
Updated
Oct 31, 2026 - TeX
Continuous-time, sheaf-theoretic optimization substrate implementing Girard's Geometry of Interaction via parallelized JAX Neural ODE self-synthesis loops.
sheaf-theory homotopy-type-theory univalent-foundations jax topos neural-ode mathematical-optimization neuro-symbolic geometry-of-interaction
-
Updated
Jul 18, 2026 - Python
Add this topic to your repo
To associate your repository with the univalent-foundations topic, visit your repo's landing page and select "manage topics."