Doctrine-specific ur-algorithms
Doctrine-specific ur-algorithms
Talk at The Berkeley Seminar
Topos Institute
Berekely, California
18 March 2024
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.