There are some developments, for example "Globular": https://arxiv.org/abs/1612.01093 https://arxiv.org/abs/1612.01093 I don't think there is a proof assistant

There are some developments, for example "Globular": https://arxiv.org/abs/1612.01093 https://arxiv.org/abs/1612.01093 I don't think there is a proof assistant that's really based on categorical foundations. I'd love to see something like that though.