English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

The Agda Universal Algebra Library (agda-algebras) is a library of types andprograms (theorems and proofs) we developed to formalize the foundations ofuniversal algebra in dependent type theory using the Agda programming languageand proof assistant. In this paper we draw on and explain many components ofthe agda-algebras library, which we extract into a single Agda module in orderto present a self-contained formal and constructive proof of Birkhoff's HSPtheorem in Martin-L\"of dependent type theory. In the course of ourpresentation, we highlight some of the more challenging aspects of formalizingthe basic definitions and theorems of universal algebra in type theory.Nonetheless, we hope this paper and the agda-algebras library serve as furtherevidence in support of the claim that dependent type theory and the Agdalanguage, despite the technical demands they place on the user, are accessibleto working mathematicians (such as ourselves) who possess sufficient patienceand resolve to formally verify their results with a proof assistant. Indeed,the agda-algebras library now includes a substantial collection of definitions,theorems, and proofs from universal algebra, illustrating the expressive powerof inductive and dependent types for representing and reasoning about generalalgebraic and relational structures.

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