UsingTheRingSolver-Talk

Since this page seemed to get attention: I noticed elsewhere that you're apparently not supposed to export .Core modules directly; is there a better place to get equality and refl than Relation.Binary.Core?

Yes, Relation.Binary.PropositionalEquality. Please direct questions to the Agda mailing list, where you are more likely to receive a response.