Universal Algebra in UniMath
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2021
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866916606790074368 |
|---|---|
| author | Amato, Gianluca Calosci, Matteo Maggesi, Marco Brogi, Cosimo Perini |
| author_facet | Amato, Gianluca Calosci, Matteo Maggesi, Marco Brogi, Cosimo Perini |
| contents | We present our library for Universal Algebra in the UniMath framework dealing with multi-sorted signatures, their algebras, and the basics for equation systems. We show how to implement term algebras over a signature without resorting to general inductive constructions (currently not allowed in UniMath) still retaining the computational nature of the definition. We prove that our single sorted ground term algebras are instances of homotopy W-types. From this perspective, the library enriches UniMath with a computationally well-behaved implementation of a class of W-types. Moreover, we give neat constructions of the univalent categories of algebras and equational algebras by using the formalism of displayed categories, and show that the term algebra over a signature is the initial object of the category of algebras. Finally, we showcase the computational relevance of our work by sketching some basic examples from algebra and propositional logic. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2102_05952 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | Universal Algebra in UniMath Amato, Gianluca Calosci, Matteo Maggesi, Marco Brogi, Cosimo Perini Logic in Computer Science Logic 68V15, 03B38, 03B35, 08A70 I.2.3; F.4.1 We present our library for Universal Algebra in the UniMath framework dealing with multi-sorted signatures, their algebras, and the basics for equation systems. We show how to implement term algebras over a signature without resorting to general inductive constructions (currently not allowed in UniMath) still retaining the computational nature of the definition. We prove that our single sorted ground term algebras are instances of homotopy W-types. From this perspective, the library enriches UniMath with a computationally well-behaved implementation of a class of W-types. Moreover, we give neat constructions of the univalent categories of algebras and equational algebras by using the formalism of displayed categories, and show that the term algebra over a signature is the initial object of the category of algebras. Finally, we showcase the computational relevance of our work by sketching some basic examples from algebra and propositional logic. |
| title | Universal Algebra in UniMath |
| topic | Logic in Computer Science Logic 68V15, 03B38, 03B35, 08A70 I.2.3; F.4.1 |
| url | https://arxiv.org/abs/2102.05952 |