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.