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.