This can be done as in the https://github.com/HoTT/HoTT @Zimmi48 , does the coq-community has standard template for this? It makes sense to role out this tools uniformly