Fix category theory scripts in light of pat_assum rename

Fixes to category theory example in light of 92317114

remove TruePrefix from category theory example

Update to category theory example.

Main new result is a Yoneda embedding into the category of zfset-valued
presheaves, whose properties are (mostly) simply inherited from the
simpler embedding into the category of (predicate-)set-valued
presheaves.

More work on categoryTheory example

Highlights include:
- proof that an embedding is essentially injective on objects
- one direction of the proof that an equivalence of categories is full,
faithful, and essentially surjective on objects
- proof that the binary product functor is a functor; characterization
of binary products

Major reworking of categoryTheory example

Major changes include:

- Reuse a polymorphic type of "morphisms" for morphisms in a category as
well as for functors and natural transformations. The category record
no longer has dom and cod fields.

- Only store the id_map in a category (and the comp map) because the dom
and cod of these morphisms is forced.

- O'Keefe style treatment of the category of sets: have a separate
category of sets for each HOL type (so really a subcategory of the
real category of sets). Have not yet linked this up with a
Katovsky-style zfset theory (would want to exhibit embeddings).

- Use overloading and Parse rules for nicer syntax.

- Split category theory into category, functor, and nat_trans theories.

- Make many (all?) partial functions extensional, that is, explicitly
set to ARB outside their domain (so that they are comparable).

- Use the constants 'full' and 'faithful' and (new) 'inj_obj' to
characterize the Yoneda embedding. Katovsky said it was injective on
objects in "YonedaEmbedding", which is the wrong term.

- Start a theory of limits (barely started).