The Agda Universal Algebra Library, Part 1: Foundation (2021-03-09T00:00:00.000000Z)

TL;DR

Several important aspects of the logical foundations on which the Agda Universal Algebra Library is built are described, including all of the types defined in the first 13 modules of the library, with special attention given to those details that seem most interesting or challenging from a type theory or mathematical foundations perspective.

Abstract

The Agda Universal Algebra Library (UALib) is a library of types and programs (theorems and proofs) we developed to formalize the foundations of universal algebra in dependent type theory using the Agda programming language and proof assistant. The UALib includes a substantial collection of definitions, theorems, and proofs from general algebra and equational logic, including many examples that exhibit the power of inductive and dependent types for representing and reasoning about relations, algebraic structures, and equational theories. In this paper we describe several important aspects of the logical foundations on which the library is built. We also discuss (though sometimes only briefly) all of the types defined in the first 13 modules of the library, with special attention given to those details that seem most interesting or challenging from a type theory or mathematical foundations perspective.

Authors

William DeMeo

1 papers

TL;DR

Abstract

Authors

References37 items

The Agda Universal Algebra Library, Part 2: Structure

The Agda Universal Algebra Library and Birkhoff's Theorem in Dependent Type Theory

Introduction to Univalent Foundations of Mathematics with Agda

Programming Language Foundations in Agda

Formalization of Universal Algebra in Agda

Concluding Remarks

Homotopy Type Theory: Univalent Foundations of Mathematics

Universal Algebra: Fundamentals and Selected Topics

Type classes for mathematics in type theory†

Hidden

Dependent Types at Work

Dependently typed programming in Agda

A constructive version of Birkhoff's theorem

Universal Algebra in Type Theory

A formulation of the simple theory of types

The Agda Team

Agda Language Reference section on Safe Agda

Agda Tools Documentation section on Pattern matching and equality

Edinburgh Research Explorer Propositions as Types

Homotopy Type Theory: Univalent Foundations of Mathematics

An Intuitionistic Theory of Types: Predicative Part

specifically the section on “Prop extensionality and the powerset”

Previous proofs of the class-extensionality’ theorem required function extensionality (§2.3)

, from the Overture.Preliminaries module (§2.1.3), the special notation we use to denote

If you haven’t already seen this before, do yourself a favor and give it some thought; see if the correct type comes to you organically

Most of these types are already defined in the Type Topology library, so the UALib imports the definitions from there

The definiendum is the left-hand side of a defining equation

The function defined by MonicInv f fM is a (left-)pseudo-inverse of f , and the proof is trivial

For unabridged docs and source code

Unicode Hints . Some of our types are denoted with with Gothic (“mathfrak”) symbols

if one assumes the univalence axiom of Homotopy Type Theory [17], then point-wise equality of functions is equivalent to definitional equality of functions

nLab authors

We obtain the left-inverse by applying the function MonicInv to g and a proof that g is monic

Sections marked with an asterisk include new types that are more abstract and general (and frankly more interesting) than the ones defined in other sections

The empty type is defined in Type Topology’s Empty-Type module as an inductive type with no constructors; that is, data 0 { U } : U (cid:5) where – (empty body)

For consistency and readability, throughout the UALib we reserve two universe variables for special purposes

Truncations and truncated higher inductive types

Field of Study

Journal Information

Name

Volume

Venue Information

Name

Type

URL

Alternate Names