/Three-HITs

All higher inductive types can be obtained from three simple HITs.

Primary LanguageCoq

Three-HITs

Theorem: if we have the coequalizers, path coequalizers, and colimits, then we have all HITs (work in progress). Uses function extensionality.