I've read that Isabelle and Metamath (and maybe Andromeda) are "generic" proof assistants in some sense that allows them to be used to implement different theories such as HOL, ZF and dependent type theory. I'm curious how generic these proof assistants can really be, especially if you can use them to implement linear and ordered logics and/or logics over restricted term languages.
In particular, Dan Licata and I have developed in recent work a domain-specific type theory for category theory (https://arxiv.org/abs/2210.08663) that is a kind of "proof-relevant ordered linear higher-order logic over a unary term language". A proof assistant based on this type theory would be somewhat similar to Isabelle/HOL since it is a kind of (weird) HOL. Are Isabelle or Metamath generic enough to handle such a bizarre system?