feat(library/hott) add categories and precategories in HoTT style

some proofs esp. tactic proofs that once worked are broken and need to be fixed