Dilettante here: What's interesting about *TT is that people have built mechanical theorem checkers [Coq, Agda, Lean, ...], and people are working on building automated theorem provers based on those programatic foundations.
Have somebody done it for the more general foundations based on category theory? If I understand correctly, Metamath is a set of tools enabling such a formulation, but not the formulation itself. See ML vs. theorem prover implemented in ML.