Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Development of the univalent foundations of mathematics in Coq
Coq
branch: master

This branch is 5 commits ahead, 28 commits behind vladimirias:master

Fetching latest commit…

Cannot retrieve the latest commit at this time

Failed to load latest commit information.
Coq_patches
Generalities
IT
Proof_of_Extensionality
hlevel1
hlevel2
.gitignore
README
README.md
forcoqdoc

README.md

A fork of Vladimir Voevodsky's Foundations with additions.

We use this fork of Vladimir Voevodsky's Foundations repository to supplement it with our own additions. Currently the only addition is a treatment of inductive type (W-types) in HoTT by S. Awodey, N. Gambino, and K. Sojakova, see the IT subdirectory.

Something went wrong with that request. Please try again.