A Coq library for Homotopy Type Theory
-
Updated
Nov 7, 2024 - Coq
#
univalent-foundations
Here are 14 public repositories matching this topic...
Experimental implementation of Cubical Type Theory
-
Updated
Sep 21, 2023 - 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
Nov 10, 2024 - 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
Nov 5, 2024 - 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
Apr 16, 2024 - 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
My undergradate thesis on coinductive types in univalent type theory
-
Updated
May 10, 2018 - TeX
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
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
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
Oct 25, 2024 - Agda
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
-
Updated
Feb 11, 2024 - Coq
Formalized Mathematics
-
Updated
Nov 9, 2017 - Coq
My implementation of the HOTT/UF book
-
Updated
Jun 9, 2023 - Coq
Improve this page
Add a description, image, and links to the univalent-foundations topic page so that developers can more easily learn about it.
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."