Doctrine-specific ur-algorithms

Talk at The Berkeley Seminar
Topos Institute
Berekely, California
18 March 2024

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.