online seminar tomorrow: Free Algebras for functors

[Paul Taylor]

Free Algebras for functors, with not an ordinal in sight

Paul Taylor
Friday 26 April 2024, 11am BST (UK time)
see researchseminars.org for your own time zone

https://researchseminars.org/seminar/TheoryCSBham
https://bham-ac-uk.zoom.us/j/81873335084 Passcode: 217

Martin Escardo challenged me to make Pataraia's fixed point
theorem "predicative". Whilst I have never understood the
motivation for that notion, I have eliminated one instance
of impredicativity and isolated the infinitary aspects to
a single specific directed join.

So then I looked for the categorical version. Pataraia's
idea plays a quite small part: the construction uses ideas
from categorical algebra since its origins, and if I were
to credit one person it would be Joachim Lambek.

The problem breaks into two parts, one finitary and the
other infinitary. The infinitary part says that the
category of pointed endofunctors of a small category
with coequalisers is filtered, so has a terminal object
if the given category has the required filtered colimit.
This is probably widely applicable as an alternative to
transfinite methods.

The finitary construction is that of fragments of the
initial algebra. It may be done in several ways, but
one is to consider coalgebras for the given functor
that are have a cone over all algebras for it. We
identify a "special condition" that this construction
satisfies and that ensures that the terminal endofunctor
(applied to any object) yields the terminal object of
the finitary category, which is the required initial
algebra of the functor.

The hope is that a similar finitary category of
partial models could be found for more complex
systems of algebra and logic and that these would
correspond to the intermediate stages in proof
theoretic arguments for normalisation, cut
elimination etc.