Valeria Vignudelli, Damien Pous
January 2018
This page is a web appendix to the following paper, to appear in proc. LiCS 2018.
Allegories were introduced by Freyd and Scedrov; they form a
fragment of Tarski's calculus of relations. We show that their
equational theory is decidable by characterising it in terms of a
specific class of graph homomorphisms.
We actually do so for an extension of allegories which we prove to
be conservative, namely allegories with top. This generalisation
makes it possible to exploit the correspondence between terms and
K4-free graphs, for which isomorphism was known to be finitely
axiomatisable.
All the equational proofs and the conservativity results in the paper have been formalised using the Coq proof assistant. The corresponding script can be browsed online or downloaded. (It compiles at least with Coq 8.6)