We present an ongoing effort to implement Universal Algebra in the UniMath system [12]. 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. After introducing the classical definition of signature, we give the related formalization of the category of algebras using the notion of a displayed category over the univalent category of sets; in this way, we easily obtain a proof that the corresponding total category of algebras is univalent. Our formalization also includes the notion of equations and varieties associated with a signature; as for the category of algebras, we construct the category of varieties over a given signature, and prove in a modular way that it is univalent by using the formalism of displayed categories. Our code is publicly available from https://github.com/amato-gianluca/UniMath. The revision discussed in this paper is tagged as hott-uf-2020.

Universal Algebra in UniMath (preprint) Presented at Workshop on Homotopy Type Theory and Univalent Foundations 2020 / Gianluca Amato, Marco Maggesi, Maurizio Parton, Cosimo Perini Brogi. - ELETTRONICO. - (2020), pp. 1-4.

Universal Algebra in UniMath (preprint) Presented at Workshop on Homotopy Type Theory and Univalent Foundations 2020

Marco Maggesi;Maurizio Parton;Cosimo Perini Brogi
2020

Abstract

We present an ongoing effort to implement Universal Algebra in the UniMath system [12]. 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. After introducing the classical definition of signature, we give the related formalization of the category of algebras using the notion of a displayed category over the univalent category of sets; in this way, we easily obtain a proof that the corresponding total category of algebras is univalent. Our formalization also includes the notion of equations and varieties associated with a signature; as for the category of algebras, we construct the category of varieties over a given signature, and prove in a modular way that it is univalent by using the formalism of displayed categories. Our code is publicly available from https://github.com/amato-gianluca/UniMath. The revision discussed in this paper is tagged as hott-uf-2020.
Goal 17: Partnerships for the goals
Gianluca Amato, Marco Maggesi, Maurizio Parton, Cosimo Perini Brogi
File in questo prodotto:
File Dimensione Formato  
HoTTUF_2020_paper_13.pdf

accesso aperto

Descrizione: Abstract for the talk at HoTT/UF 2020
Tipologia: Versione finale referata (Postprint, Accepted manuscript)
Licenza: Open Access
Dimensione 214.15 kB
Formato Adobe PDF
214.15 kB Adobe PDF Visualizza/Apri

I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2158/1199467
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact