Univalent Mathematics
A unified approach to formalization of mathematical knowledge based on Univalent Foundations.
Pinned Repositories
2006_03_Homotopy_lambda_calculus
Voevodsky's 2006 paper on homotopy lambda calculus
agda-unimath
The agda-unimath library
book
A textbook on informal homotopy type theory -- Vladimir's fork, retained because there is a pull request based on it.
Foundations
Voevodsky's original development of the univalent foundations of mathematics in Coq
largecatmodules
Large category of modules over monads on top of UniMaths and Display category
Schools
SetHITs
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
UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Univalent Mathematics's Repositories
UniMath/UniMath
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
UniMath/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/Foundations
Voevodsky's original development of the univalent foundations of mathematics in Coq
UniMath/agda-unimath
The agda-unimath library
UniMath/TypeTheory
The mathematical study of type theories, in univalent foundations
UniMath/Schools
UniMath/2006_03_Homotopy_lambda_calculus
Voevodsky's 2006 paper on homotopy lambda calculus
UniMath/largecatmodules
Large category of modules over monads on top of UniMaths and Display category
UniMath/book
A textbook on informal homotopy type theory -- Vladimir's fork, retained because there is a pull request based on it.
UniMath/SetHITs
UniMath/Universe_Polymorphic_Type_System
Voevodsky's notes from the summer of 2012 on a design of a universe polymorphic type system with Tarski universes
UniMath/GrpdHITs
UniMath/Computability
UniMath/old_notes_on_type_systems
Voevodsky's notes on type systems. This version contains more material than the one on his website.
UniMath/lBsystems
Voevodsky's work on B-systems, transferred from his github account
UniMath/lCsystems
Voevodsky's work on C-systems, transferred from his github account
UniMath/opam-repository
This repository makes it easy to build and install UniMath using opam.
UniMath/UniMath-jsCoq
UniMath in jsCoq
UniMath/unimath.github.io
Various websites
UniMath/Contrib
UniMath/ICMS2016UniMath.github.io
A webpage Vladimir made for a conference.
UniMath/live