Harmonize Pushout
typos
Simplify proofs
Add \d-='-out
Rename dependent concatenation
Add dependent identity and opposite
Add tests
Add Readme for HITs