Prove Admitted theorems in types.ObjectClassifier

They are not very pretty, but they are no longer admits.  This is
partial work on #195.
Add a theorem with issig equivalence about hProps
Merge pull request #197 from JasonGross/hProp-theorem

Add a theorem with issig equivalence about hProps
Merge pull request #196 from JasonGross/remove-admitted-objclassifier

Prove Admitted theorems in types.ObjectClassifier