Thursday, December 5: Paige North "Coinductive control of inductive data types"

[Emily Riehl]

The HoTTEST seminar continues this week, on Thursday (November 7), at 11:30am EST = 16:30pm UTC. 

Our speaker is Paige North, whose talk is titled  Coinductive control of inductive data types." The talk will be 60 minutes long, followed by
up to 30 minutes for questions.  The abstract is below.

The Zoom link is https://zoom.us/j/994874377

Further information, including the list of upcoming speakers, and videos and slides from past talks, is at:

 

https://www.math.uwo.ca/faculty/kapulkin/seminars/hottest.html

Emily

(On behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen, Chris Kapulkin, and Emily Riehl.)

 

Title: Coinductive control of inductive data types

Abstract: In classical programming language theory, characterizing data types as initial algebras of an endofunctor that represents a specification of the data types is an important tool. In this work, we observe that the category of algebras of such an endofunctor is often enriched in its category of coalgebras. This enrichment carries strictly more information than the traditional, unenriched category. For example, when considering the endofunctor whose initial algebra is the natural numbers, we find that the enrichment encodes a notion of `partial' homomorphism, while the unenriched category encodes only `total' homomorphisms. We can also leverage this extra information to generalize the notion of initial algebras, following the theory of weighted limits. This is joint work with Maximilien Péroux and Lukas Mulder.