<div dir="ltr"><div><div><div><div>Hi all,<br><br></div>Yesterday I posted a blog post on the recent work I did on Agda's handling of sorts. You can read it here: <a href="https://jesper.sikanda.be/posts/agdas-new-sorts.html">https://jesper.sikanda.be/posts/agdas-new-sorts.html</a> <br><br></div>Any comments are very welcome here on this list!<br><br></div>Cheers,<br></div>Jesper<br></div>