Consider Formally verifying the properties in Category Theory using proof assistants.

In the book, we have so many theorems and properties defined, which cannot be formally proved by Haskell or C++.

Is it a good Idea if we use proof assistants to prove these theorems, for example Coq, Idris or Agda ...?

BTW, I have started a project to interpret the book "conceptual mathematics" in Coq when learning category theory: https://github.com/HaoYang670/conceptual_mathematics