I can think of practical HITs in verified software that capture some form of alpha equivalence, context equivalence or the example which defines well-typed syntax of type theory from Signatures and Induction principles for HIITs. Now I am trying to think of one which also includes higher equalities, i.e. non-trivial equality of these equalities? Can someone point me to interesting examples where higher equalities play crucial role or at least improve reasoning? Actual examples of both HITs and HIITs with non-trivial higher equalities with applications to programming are what I am looking for.