<div dir="ltr"><div dir="ltr"><div>Dear all,</div><div><br></div><div>I'd like to share some facts on our platform for collaborative interactive polyglot notebooks <a href="https://nextjournal.com">https://nextjournal.com</a> where we’re working on some experimental support for Agda. Some example first:</div><div><br></div><div>- <a href="https://nextjournal.com/plfa/ToC">https://nextjournal.com/plfa/ToC</a> (Programming Language Foundations in Agda; Kokke, Siek, Wadler)</div><div>- <a href="https://nextjournal.com/agda/euclid-theorem">https://nextjournal.com/agda/euclid-theorem</a> (Strickland)</div><div>- <a href="https://nextjournal.com/zampino/russell-paradox">https://nextjournal.com/zampino/russell-paradox</a> (based on an Altenkirch’s lecture)</div><div>- <a href="https://nextjournal.com/zampino/finite-decidable-setoids">https://nextjournal.com/zampino/finite-decidable-setoids</a></div><div><br></div><div>You can get started by remixing any of the above articles, or our Agda template</div><div><br></div><div>- <a href="https://nextjournal.com/nextjournal/agda-template">https://nextjournal.com/nextjournal/agda-template</a></div><div>- <a href="https://nextjournal.com/try/nextjournal/agda-template">https://nextjournal.com/try/nextjournal/agda-template</a></div><div><br></div><div>On the teaching side, students at University of Bergen collaborate on shared notes for their PhD seminar on MLTT and Univalence:</div><div><br></div><div>- <a href="https://nextjournal.com/uib-types/journal-part-2">https://nextjournal.com/uib-types/journal-part-2</a> (shared with permission from the authors)</div><div><br></div><div>This is how our Agda environment is built, it’s also a Notebook :-) which I try to update on a regular basis:</div><div><br></div><div>- <a href="https://nextjournal.com/nextjournal/agda-environment">https://nextjournal.com/nextjournal/agda-environment</a></div><div><br></div><div>but you could build your own as long as you install our fork of Agda Jupyter Kernel along with Agda dependencies: <a href="https://github.com/nextjournal/agda-kernel">https://github.com/nextjournal/agda-kernel</a>.</div><div><br></div><div>We currently support only a subset of Agda Emacs Mode given the constraints of Jupyter interaction: apart from type-checking code, the kernel currently supports Agsy Auto, Give, Split, Refine (via Tab) and Context Inspection (via Shift+Tab). It would be nice to explore richer interactions in the future, possibly via a custom Haskell Socket REPL-ish thing, is there prior work in that direction?</div><div><br></div><div>Nextjournal runtimes/environments are easily shareable and reusable (both in the same notebook or across different documents) and in the specific case of Agda, exported runtimes are immediately importable as Agda modules (see Euclid's Theorem formalisation above).</div><div><br></div><div>I'll be very glad to help anyone willing to port existing work to nextjournal for teaching, publication or blogging. So far we’re able to import markdown and jupyter ipynb formats (Strickland's essay above was converted from LaTeX (.lagda) to markdown via <a href="https://pandoc.org">Pandoc</a> first). More built-in conversions might come soon.</div><div><br></div><div>Signup is free and there’s special deals for students/academics should anyone need more computing power than the free plan allows... but that shouldn’t be the most common case with Agda.</div><div><br></div><div>Looking forward for feedback, have a nice day,</div><div>Andrea</div></div></div>