Univalent mathematics and homotopy type theory provide a structural approach to formalizing mathematical concepts. Inspired by the role of displayed categories in the univalent treatment of category theory, we develop an analogous notion of displayed algebras for universal algebra. This modular and layered approach allows us to construct and reason about algebraic structures over a fixed base. Classical constructions such as cartesian products, pullbacks, semidirect products, and subalgebras naturally arise as total algebras of suitable displayed algebras. The main results are fully formalized in the UniMath library.
Displayed Universal Algebra in UniMath: Basic Definitions and Results
Amato G.
;
2025-01-01
Abstract
Univalent mathematics and homotopy type theory provide a structural approach to formalizing mathematical concepts. Inspired by the role of displayed categories in the univalent treatment of category theory, we develop an analogous notion of displayed algebras for universal algebra. This modular and layered approach allows us to construct and reason about algebraic structures over a fixed base. Classical constructions such as cartesian products, pullbacks, semidirect products, and subalgebras naturally arise as total algebras of suitable displayed algebras. The main results are fully formalized in the UniMath library.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
