Univalent Mathematics (@UniMath)
Guthub

UniMath

Twitter logo Share LinkedIn logo Share Facebook logo Share
  • Stars
    star
    2,055
  • Global Org. Rank 9,314 (Top 3 %)
  • Registered over 10 years ago
  • Most used languages
    Coq     69.2 %
    HTML
         23.1 %
    Agda     7.7 %

Top repositories

1

UniMath

This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Coq
955
star
2

SymmetryBook

This book will be an undergraduate textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.
HTML
377
star
3

Foundations

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

agda-unimath

The agda-unimath library
Agda
219
star
5

TypeTheory

The mathematical study of type theories, in univalent foundations
Coq
113
star
6

Schools

Coq
77
star
7

2006_03_Homotopy_lambda_calculus

Voevodsky's 2006 paper on homotopy lambda calculus
14
star
8

largecatmodules

Large category of modules over monads on top of UniMaths and Display category
Coq
11
star
9

SetHITs

Coq
8
star
10

Universe_Polymorphic_Type_System

Voevodsky's notes from the summer of 2012 on a design of a universe polymorphic type system with Tarski universes
8
star
11

GrpdHITs

Coq
6
star
12

old_notes_on_type_systems

Voevodsky's notes on type systems. This version contains more material than the one on his website.
6
star
13

Computability

5
star
14

opam-repository

This repository makes it easy to build and install UniMath using opam.
2
star
15

lBsystems

Voevodsky's work on B-systems, transferred from his github account
Coq
2
star
16

lCsystems

Voevodsky's work on C-systems, transferred from his github account
Coq
2
star
17

UniMath-jsCoq

UniMath in jsCoq
HTML
1
star
18

unimath.github.io

Various websites
HTML
1
star