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
UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
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.
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.
