Further overhaul and beautification. Reached start of weak
equivalences.