blass1983-free-algebra-coequalizer

Abstract

For a variety of infinitary algebras subject to no identities, the classical construction of free algebras as algebras of words is shown to work in any topos. Although coequalizers in such varieties cannot be constructed in the usual way, as algebras of equivalence classes, unless the internal axiom of choice holds, they do exist and can be obtained as algebras of words in any Boolean topos.

Contributions

• This paper proves that the construction of W-types (which he calls words) can be carried out entirely within the internal logic of any topos. %TODO