Repositories list

• UniMath

  Public
  This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.

  coqmathematicscoq-library+ 4

  coqmathematicscoq-libraryfoundationsunimathrocqrocq-library

  Rocq Prover

  •

  Other

  •187187 forks•1k1k stars•140140 issues•1010 pull requests•Updated Sep 24, 2026Sep 24, 2026

• Schools

  Public
  Rocq Prover

  •2727 forks•9393 stars•33 issues•00 pull requests•Updated Sep 4, 2026Sep 4, 2026

• GrpdHITs

  Public
  Rocq Prover

  •44 forks•77 stars•22 issues•00 pull requests•Updated Sep 4, 2026Sep 4, 2026

• SetHITs

  Public
  Rocq Prover

  •55 forks•99 stars•55 issues•00 pull requests•Updated Sep 4, 2026Sep 4, 2026

• largecatmodules

  Public
  Large category of modules over monads on top of UniMaths and Display category

  Rocq Prover

  •88 forks•1212 stars•88 issues•00 pull requests•Updated Sep 4, 2026Sep 4, 2026

• TypeTheory

  Public
  The mathematical study of type theories, in univalent foundations

  Rocq Prover

  •2525 forks•122122 stars•1515 issues•22 pull requests•Updated Sep 4, 2026Sep 4, 2026

• Computability

  Public
  Rocq Prover

  •11 fork•66 stars•00 issues•00 pull requests•Updated Jul 6, 2025Jul 6, 2025

• Contrib

  Public
  Coq

  •55 forks•11 star•00 issues•00 pull requests•Updated Jun 26, 2023Jun 26, 2023

• lBsystems

  Public
  Voevodsky's work on B-systems, transferred from his github account

  Coq

  •22 forks•33 stars•00 issues•00 pull requests•Updated Feb 28, 2016Feb 28, 2016

• lCsystems

  Public
  Voevodsky's work on C-systems, transferred from his github account

  Coq

  •22 forks•33 stars•00 issues•00 pull requests•Updated Apr 7, 2015Apr 7, 2015

• Foundations

  Public
  Voevodsky's original development of the univalent foundations of mathematics in Coq

  Coq

  •2222 forks•247247 stars•00 issues•00 pull requests•Updated Sep 10, 2014Sep 10, 2014