Universal algebra in type theory

Abstract

We present a development of Universal Algebra inside Type Theory, formalized using the proof assistant Coq. We define the notion of a signature and of an algebra over a signature. We use setoids, i.e. types endowed with an arbitrary equivalence relation, as carriers for algebras. In this way it is possible to de_ne the quotient of an algebra by a congruence. Standard constructions over algebras are de_ned and their basic properties are proved formally. To overcome the problem of de_ning term algebras in a uniform way, we use types of trees that generalize wellorderings. Our implementation gives tools to define new algebraic structures, to manipulate them and to prove their properties.