convert x=_A y to use the \id macro, twice
made a start on the last subsection of the appendix, introducing the propositions
that go into the statments of the hott axioms