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