Universal Algebra in UniMath
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , , |
|---|---|
| Format: | Preprint |
| Publié: |
2020
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866917864179499008 |
|---|---|
| author | Amato, Gianluca Maggesi, Marco Parton, Maurizio Brogi, Cosimo Perini |
| author_facet | Amato, Gianluca Maggesi, Marco Parton, Maurizio Brogi, Cosimo Perini |
| contents | We present an ongoing effort to implement Universal Algebra in the UniMath system. Our aim is to develop a general framework for formalizing and studying Universal Algebra in a proof assistant. By constituting a formal system for isolating the invariants of the theory we are interested in -- that is, general algebraic structures modulo isomorphism -- Univalent Mathematics seems to provide a suitable environment to carry on our endeavour. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2007_04840 |
| institution | arXiv |
| publishDate | 2020 |
| record_format | arxiv |
| spellingShingle | Universal Algebra in UniMath Amato, Gianluca Maggesi, Marco Parton, Maurizio Brogi, Cosimo Perini Logic in Computer Science F.4.0 We present an ongoing effort to implement Universal Algebra in the UniMath system. Our aim is to develop a general framework for formalizing and studying Universal Algebra in a proof assistant. By constituting a formal system for isolating the invariants of the theory we are interested in -- that is, general algebraic structures modulo isomorphism -- Univalent Mathematics seems to provide a suitable environment to carry on our endeavour. |
| title | Universal Algebra in UniMath |
| topic | Logic in Computer Science F.4.0 |
| url | https://arxiv.org/abs/2007.04840 |