<div dir="ltr"><div>Hi Agda people,</div><div><br></div><div>I wrote a new blog post on formalizing things in Agda: <a href="https://jesper.sikanda.be/posts/formalize-all-the-things.html">https://jesper.sikanda.be/posts/formalize-all-the-things.html</a> I hope you find it useful. It is meant to be an introductory post, so let me know if there's anything that can be clarified!</div><div><br></div><div>-- Jesper<br></div></div>