10 results found Sort:
- Filter by Primary Language:
- Agda (5)
- Haskell (2)
- Coq (1)
- Lean (1)
- OCaml (1)
- +
A Coq library for Homotopy Type Theory
Created
2011-03-26
6,731 commits to master branch, last one 2 days ago
Experimental implementation of Cubical Type Theory
Created
2015-02-26
689 commits to master branch, last one about a year ago
A formalised, cross-linked reference resource for mathematics done in Homotopy Type Theory
Created
2021-12-05
856 commits to main branch, last one 13 hours ago
Logical manifestations of topological concepts, and other things, via the univalent point of view.
Created
2018-02-05
4,631 commits to master branch, last one a day ago
The agda-unimath library
trees
species
ring-theory
graph-theory
group-theory
order-theory
finite-groups
number-theory
type-theories
category-theory
structured-types
universal-algebra
commutative-algebra
higher-group-theory
homotopy-type-theory
univalent-foundations
univalent-mathematics
univalent-combinatorics
synthetic-homotopy-theory
orthogonal-factorization-systems
Created
2021-11-19
2,866 commits to master branch, last one 18 days ago
Lecture notes on univalent foundations of mathematics with Agda
Created
2019-03-20
1,048 commits to master branch, last one 8 months ago
😎TT
Created
2019-12-20
609 commits to main branch, last one about a year ago
An experimental proof assistant based on a type theory for synthetic ∞-categories.
Created
2020-11-26
800 commits to develop branch, last one 23 days ago
Agda formalisation of the Introduction to Homotopy Type Theory
Created
2020-07-28
545 commits to master branch, last one 3 years ago
Ground Zero: Lean 4 HoTT Library
Created
2022-03-21
1,013 commits to master branch, last one 11 days ago