Skip to content
@UniMath

Univalent Mathematics

A unified approach to formalization of mathematical knowledge based on Univalent Foundations.

Popular repositories Loading

  1. UniMath UniMath Public

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

    Rocq Prover 1k 188

  2. SymmetryBook SymmetryBook Public

    This book will be a textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.

    HTML 440 27

  3. agda-unimath agda-unimath Public

    The agda-unimath library

    Agda 294 96

  4. Foundations Foundations Public

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

    Coq 245 22

  5. TypeTheory TypeTheory Public

    The mathematical study of type theories, in univalent foundations

    Coq 118 25

  6. Schools Schools Public

    Coq 94 27

Repositories

Showing 10 of 22 repositories
  • agda-unimath Public

    The agda-unimath library

    UniMath/agda-unimath’s past year of commit activity
    Agda 294 MIT 96 145 (3 issues need help) 130 Updated Mar 23, 2026
  • UniMath Public

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

    UniMath/UniMath’s past year of commit activity
    Rocq Prover 1,002 188 141 (7 issues need help) 11 Updated Mar 19, 2026
  • SymmetryBook Public

    This book will be a textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.

    UniMath/SymmetryBook’s past year of commit activity
    HTML 440 CC-BY-SA-4.0 27 71 5 Updated Feb 26, 2026
  • live Public
    UniMath/live’s past year of commit activity
    HTML 2 2 0 0 Updated Feb 3, 2026
  • Computability Public
    UniMath/Computability’s past year of commit activity
    Rocq Prover 6 1 0 0 Updated Jul 6, 2025
  • largecatmodules Public

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

    UniMath/largecatmodules’s past year of commit activity
    Coq 12 8 8 0 Updated Jun 6, 2025
  • SetHITs Public
    UniMath/SetHITs’s past year of commit activity
    Coq 9 5 5 0 Updated Jun 2, 2025
  • Schools Public
    UniMath/Schools’s past year of commit activity
    Coq 94 27 3 0 Updated Apr 19, 2025
  • GrpdHITs Public
    UniMath/GrpdHITs’s past year of commit activity
    Coq 7 4 2 0 Updated Apr 12, 2025
  • TypeTheory Public

    The mathematical study of type theories, in univalent foundations

    UniMath/TypeTheory’s past year of commit activity
    Coq 118 25 14 1 Updated Feb 15, 2025

Top languages

Loading…

Most used topics

Loading…