Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory & logic

Topic: ✔ geometric series of types

Naïm Favier (Jun 13 2024 at 12:47):

I don't remember where I first saw that you can make sense of the equation 1 + A + A² + ... = 1/(1 - A), where A is a type (or an object of a category): the left side is the usual definition of lists of A, while the right side is obtained from the fixed-point definition [A] = 1 + A × [A] by criminally rearranging things.

Does anyone know of a source for this? I am aware of adjacent things like Seven trees in one, Objects of categories as complex numbers, https://math.ucr.edu/home/baez/week202.html

John Baez (Jun 13 2024 at 14:05):

Are you interested in this one particular famous example, or the general theory of how to solve type equations like $F(x) \cong 1 + xF(x)$ using power series? I believe

• François Bergeron, Gilbert Labelle, Pierre Leroux, Théorie des espèces et combinatoire des structures arborescentes, LaCIM, Montréal (1994). English version: Combinatorial Species and Tree-like Structures, Cambridge University Press (1998).

does a pretty good job handling the general theory.

John Baez (Jun 13 2024 at 14:07):

Maybe chapter 3, "Combinatorial Functional Equations", is the most relevant.

Naïm Favier (Jun 13 2024 at 14:10):

I am looking for that particular example, but general references are also welcome

Josh Chen (Jun 13 2024 at 18:24):

Are you thinking of McBride's note The Derivative of a Regular Type is its Type of One-Hole Contexts? (See Section 3 of http://strictlypositive.org/diff.pdf)

Naïm Favier (Jun 13 2024 at 18:29):

yes, that might be it! thanks

Notification Bot (Jun 13 2024 at 18:44):

Naïm Favier has marked this topic as resolved.