Doctrine-specific ur-algorithms

Abstract

Various constructions of categories have a universal property expressing the freeness/initiality of the construction within a specific categorical doctrine. Expressed in an algorithmic framework, it turns out that this universal property is in a certain sense a doctrine-specific “ur-algorithm” from which various known categorical constructions/algorithms (including spectral sequences of bicomplexes) can be derived in a purely computational way. This can be viewed as a categorical version of the Curry-Howard correspondence to extract programs from proofs.