Univalent Mathematics
Grow your team on GitHub
GitHub is home to over 50 million developers working together. Join them to grow your own development teams, manage permissions, and collaborate on projects.
Sign upRepositories
-
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.
-
UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
-
TypeTheory
The mathematical study of type theories, in univalent foundations
-
largecatmodules
Large category of modules over monads on top of UniMaths and Display category
-
unimath.github.io
Various websites
-
opam-repository
This repository makes it easy to build and install UniMath using opam.
-
ICMS2016UniMath.github.io
Forked from ICMS2016UniMath/ICMS2016UniMath.github.ioA webpage Vladimir made for a conference.
-
lBsystems
Voevodsky's work on B-systems, transferred from his github account
-
lCsystems
Voevodsky's work on C-systems, transferred from his github account
-
2006_03_Homotopy_lambda_calculus
Voevodsky's 2006 paper on homotopy lambda calculus
-
Foundations
Voevodsky's original development of the univalent foundations of mathematics in Coq
-
Universe_Polymorphic_Type_System
Voevodsky's notes from the summer of 2012 on a design of a universe polymorphic type system with Tarski universes
-
old_notes_on_type_systems
Voevodsky's notes on type systems. This version contains more material than the one on his website.