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.



Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.