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 thay may inform the theoretical development, but it's a non-trivial amount of work.

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.