Weak higher categories generalize the traditional notion of category by comprising higher-dimensional cells and using those in order to provide witnesses for structural axioms. Due to their very general nature, they are difficult to manipulate and even to define. In this talk, we will present two recently developed (theoretical and software) tools in order to assist the mathematician working with those structures. Firstly, we will describe a type theory whose models are precisely the globular categories, thus providing a proof assistant in order to ensure the validity of coherence laws in those categories. Secondly, we will generalize higher-dimensional rewriting techniques to Gray categories (a semi-strict variant of tricategories) in order to obtain coherence results for algebraic structures in low dimensional weak categories.