<div dir="ltr"><p style="margin:3px 0px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">Dear all,</p><p style="margin:3px 0px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">After a recent discussion on Zulip, various members of the Agda community have come to the conclusion that we have accumulated enough bad design decisions in the Agda standard library that it is now worth starting work on a v2.0. This isn't envisaged to be a radical overhaul, and although we will be fixing things that require unavoidable backwards incompatible changes, we still expect the vast majority of code written with v1.7 to work in v2.0. We will however be removing all code that was deprecated before the release of v1.0.</p><p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">We know making breaking changes is always somewhat unpopular. However, the art of designing large developments in dependently-typed systems such as Agda is still relatively poorly understood, and we believe that in the long term it's more important to find and implement the right design decisions, rather than build upon the sub-optimal ones! After the temporary disruption, we hope that the changes will make all the users of the standard library's lives easier going forward.</p><p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">Obviously community feedback on this process is vital! Over the coming weeks and months, in the hope of starting discussions with those interested, we'll be posting on Zulip and on the mailing list about the bigger changes before we start work on them. Equally, if there's any parts of the standard library that you've always thought could be done better, now's the time to open an issue on the <a href="https://github.com/agda/agda-stdlib/issues" target="_blank" rel="noopener noreferrer" title="https://github.com/agda/agda-stdlib/issues" style="color:rgb(0,136,204);text-decoration-line:none">issue tracker</a>.</p><p style="margin:10px 0px 3px;color:rgb(51,51,51);font-family:"Source Sans 3",sans-serif;font-size:14px">Many thanks,<br>Matthew, on behalf of the Agda Team</p></div>