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.