This paper presents a formalisation of algebraic effects with equations in Cubical Agda. Where previous work employed setoids to deal with equations, the library presented here uses quotient types to encode faithfully the type of terms quotiented by laws. Apart from tools for equational reasoning, the library also provides an effect-generic Hoare logic for algebraic effects, which enables reasoning about effectful programs in terms of their pre- and post- conditions. A particularly novel aspect is that equational reasoning and Hoare-style reasoning are related by an elimination principle of Hoare logic.