its pretty wild (no pun intended) that one cool trick (representability predicates) allows you to derive the pentagon and triangle coherences in untruncated hom types in higher #category-theory in #hott. its even nicer that this trick straightforwardly generalizes to monoidal categories and allows you define both levels of monoidal structure, braided structures, and even goes on to derive the hexagon coherence. all proven in cubical agda.