Big news: My friend William DeMeo has announced that he's formalised Birkhoff HSP Theorem in Martin-Löf type theory using Agda. Details on ualib.gitlab.io.

Responses (?)

Indieweb interactions: Like/Reshare/Reply/Bookmark with Quill or Like/Reshare/Reply/Bookmark with Micropublish.