UniMath/Universe_Polymorphic_Type_System UniMath/Universe_Polymorphic_Type_System

  • Stars
    star
    8
  • Rank 2,098,883 (Top 42 %)
  • Language
  • Created over 10 years ago
  • Updated over 10 years ago
Twitter logo Share LinkedIn logo Share Facebook logo Share
UniMath/Universe_Polymorphic_Type_System
github

UniMath

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

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

More 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

GrpdHITs

Coq
6
star
11

old_notes_on_type_systems

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

Computability

5
star
13

opam-repository

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

lBsystems

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

lCsystems

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

UniMath-jsCoq

UniMath in jsCoq
HTML
1
star
17

unimath.github.io

Various websites
HTML
1
star