Minor change in title
Better equiv_inverse, lemmas for moving equivalences accross =
Removed Batman and Robin
Cosmetic changes + changed a proof which got stuck, I think we are seeing sensitivity to Qed vs Defined.
Ploughing through h-levels. We should separate out HProp and HSet.