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.
Universal Algebra in UniMath
Gianluca Amato;Maurizio Parton;
2020-01-01
Abstract
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.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.
