Well founded coalgebras: online seminar TODAY

[Paul Taylor]

TITLE: Well Founded Coalgebras

SPEAKER: me, Paul Taylor
(Honorary Senior Research Fellow, University of Birmingham)

14:00 UTC (FOUR hours after this message is sent)

Zoom details and papers: see www.paultaylor.eu/ordinals/

Jointly organised by
the Logic & Semantics and Applied Category Theory
research groups in Tallinn University of Technology
and
The Theoretical Computer Science group
at the University of Birmingham.


ABSTRACT:

Categorical set theory explores ideas taken from set theory
to develop mathematics using category theoretic tools.
It began in the 1970s when Mikkelsen and Osius interpreted
recursion and epsilon-structures in an elementary topos.
Well founded coalgebras generalise epsilon-structures to give
approximations to the free algebra for a functor even when
this does not exist.

The main recursion theorem is based on the one of von Neumann
for ordinals. Originally that was based on fixed points in
complete lattices, but in order to consider more general
categories and functors, we must use Pataraia's Theorem for
dcpos instead.

However, for our more complicated constructions, we need
to find a scalpel not a sledgehammer, so a more subtle form
of Pataraia's Theorem is developed.

The paper develops analogues of the recursion theorem and
Mostowski extensional quotient potentially in much more
general categories, with factorisation systems intead of
1-1 functions.

The obvious first application of this generalisation
replaces Set with Pos to study the different forms of
intuitionistic ordinals that were introduced in the 1990s.
This in turn leads to a formulation of transfinite iteration
of functors, based on a categorical axiom instead of the
set-theoretic axiom-scheme of replacement.


NOTE ALSO:

I gave another online seminar in December, about the history
of order-theoretic fixed point theorems, including Pataraia's.

I posted on MathOverflow about this too:
mathoverflow.net/questions/441882

PLEASE, if you have a MathOverflow login, visit this question
(and my others about the history of induction) and UPVOTE them.

The MO bullies have piled in to me there, because I utter the
heresy that there is better way to do constructions by recursion
than merely reciting the ordinals (without even citing the relevant
work that justifies this).