Coq-HoTT
Homotopy Type Theory Library
A Coq library for interpreting Martin-Löf's intensional type theory into abstract homotopy theory and relating it to higher category theory.
A Coq library for Homotopy Type Theory
1k stars
59 watching
193 forks
Language: Coq
last commit: 6 days ago
Linked from 3 awesome lists
homotopy-type-theorytype-theoryunivalent-foundations
44bits/awesome-opensource-documents
uhub/awesome-coqRelated projects:
| Repository | Description | Stars |
|---|---|---|
 uds-psl/mpctt | A research project on using the Coq proof assistant to develop and prove mathematical models of computation in computational type theory | 80 |
 jwiegley/category-theory | An axiomatic formalization of category theory in Coq for personal study and practical work | 754 |
 hivert/coq-combi | Formalizes algebraic combinatorics in Coq with an emphasis on symmetric functions and their properties. | 1 |
 geohot/coq-hardy | Formalizing mathematical theorems from Hardy's book in Coq to create a rigorous and reproducible formalization of number theory | 53 |
 mgrabovsky/fm-notes | A collection of notes and resources on formal methods, type theory, and theorem proving using Coq. | 20 |
 coq-community/graph-theory | A comprehensive Coq library formalizing various results in graph theory, providing a rigorous foundation for theoretical and applied graph theory research. | 34 |
 andrejbauer/homotopy-type-theory-course | Teaching materials and resources for a doctoral course on homotopy theory and type theory | 287 |
 amintimany/categories | An implementation of category theory in the Coq proof assistant. | 93 |
| coq-community/topology | Develops and formalizes basic concepts and results of general topology in Coq. | 47 |
 affeldt-aist/infotheo | A Coq formalization of mathematical foundations for information theory and error-correcting codes | 64 |
 jozefg/learn-tt | A collection of resources for learning type theory and related fields | 2,167 |
 vrahli/nuprlincoq | Formalizes Nuprl's Constructive Type Theory in Coq, focusing on its computation system, type system, inference rules, and consistency. | 44 |
 math-comp/abel | Formalization of mathematical theorems about solvability and Galois theory for polynomials | 28 |
 namin/dot | Mechanized proof of soundness for a type-theoretic foundation for languages like Scala | 154 |