Make code quality/cleaning pass over files

[peterlefanulumsdaine]

Before making public, would be good to have a rough quality/cleanup pass over all files (at least all of ALV1). Doesn’t need to be too thorough, but should at least:

• make sure all terminology/naming conventions are up-to-date and consistent;
• make sure all names are somewhat meaningful
• remove obsolete code and comments

To make sure we’ve had at least one pair of eyes (preferably two) over each file before going public, mark below when you’ve checked a file.

File	BA	PLL	VV
Auxiliary/Auxiliary.v
Auxiliary/CategoryTheoryImports.v
Auxiliary/UnicodeNotations.v
ALV1/CwF_RelUnivYoneda.v	2016-10-06	2016-10-07
ALV1/CwF_SplitTypeCat_Cats_Standalone.v
ALV1/CwF_SplitTypeCat_Defs.v		2016-10-05
ALV1/CwF_SplitTypeCat_Equivalence.v
ALV1/CwF_SplitTypeCat_Maps.v		2016-10-10
ALV1/RelativeUniverses.v	2016-10-06	2016-10-07
ALV1/RelUnivYonedaCompletion.v	2016-10-06	2016-10-07
ALV1/Summary.v	2016-10-06
ALV2/CwF_SplitTypeCat_Cats.v
ALV2/CwF_SplitTypeCat_Equiv_Cats.v
ALV2/CwF_SplitTypeCat_Equiv_Comparison.v
ALV2/CwF_SplitTypeCat_Univalent_Cats.v
Categories/category_FAM.v
Categories/category_of_elements.v
Categories/ess_alg_categories.v
Categories/ess_and_gen_alg_cats.v
Displayed_Cats/Auxiliary.v
Displayed_Cats/Constructions.v
Displayed_Cats/Core.v
Displayed_Cats/Equivalences.v
Displayed_Cats/Examples.v