More work on Hom Functors
Switch to just propositional equality for now

It is faster, simpler, and although it will make it difficult to prove
that Set preserves all colimits, we can upgrade to higher inductive
types later.  Setoids have their own family of pains, and are both
complex and slow.