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 (?)
JavaScript needs to be enabled to show responses. (Although, it is not necessary for posting them.)