Foundations icon indicating copy to clipboard operation
Foundations copied to clipboard

Published 20 hours ago • verified publisher icon HoTT
→

Metadata

Development of the univalent foundations of mathematics in Coq

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.

← Metadata

17
Stars
2
Forks
Watchers

Owner

verified publisher icon HoTT

Metadata

Development of the univalent foundations of mathematics in Coq

Back