A Machine-checked proof of Birkhoff's Variety Theorem in Martin-L\"of Type Theory

arXiv2101.10166MaRDI QIDQ6358975

William J. DeMeo, Jacques Carette

Publication date: 25 January 2021

Mathematics Subject Classification ID

Equational classes, universal algebra in model theory (03C05) Formalization of mathematics in connection with theorem provers (68V20)

This page was built for publication: A Machine-checked proof of Birkhoff's Variety Theorem in Martin-L\"of Type Theory