I remember asking this question on agda subreddit a while ago (maybe 3 years ago? I don't know) and they told me it's not possible. However, they implemented Cubical type theory and a few other stuff (universe levels? Has it been implemented last couple years?) so maybe it's possible now.m

I love doing algebra proofs with agda as a hobby but I'm by no means, even remotely, experienced in everything agda capable of.