Three-HITs
Three-HITs copied to clipboard
nmvdw
All higher inductive types can be obtained from three simple HITs.
Three-HITs
Theorem: if we have the coequalizers, path coequalizers, and colimits, then we have all HITs (work in progress). Uses function extensionality.
nmvdw