I have seen many examples of working with categories inside a proof assistant, even some proof assistants like rzk created in part with this as a motivating purpose. Given trinitarianism, it seems at least plausible to me that one might create a proof assistant whose core is based on category theory instead of type theory.
Has this been tried previously in any experimental proof assistants? Are there any immediately apparent reasons that this would or would not be useful?
It only makes sense to embed a certain aspect of mathematics into the core of a proof assistant if that has a significant advantage over defining the same aspect on top of the core. For example, it makes sense to embed dependent types into the core, because implementing dependencies on top of a non-dependent foundation (first-order logic or simple type theory) is a royal pain.
We may therefore rule out approaches such as "first order logic + everything is a category", as that can also be achieved by having just first-order logic in the core, and some general support for defining structures (which we will want anyway).
There is a taunting possibility though. Homotopy type theory is like type theory with built-in higher category theory in which all morphisms are equivalences. This is so because every identification $p : \mathsf{Id}(x,y)$ has an inverse $p^{-1} : \mathsf{Id}(y,x)$ and these two compose to give reflexivity. So, if we could just get rid of the inverses, we would obtain a type theory in which the identity types correspond to category-theoretic $\mathsf{Hom}$-sets. Such a thing is called directed homotopy type theory and is currently being developed by several people. Every year it seems to be a little different, so it's kind of hard to implement it. One could certainly play around with prototypes, and that may inform the theoretical development, but it's a non-trivial amount of work.
