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: learning: questions

Topic: polynomial functors and powerset

Henry Story (Aug 07 2021 at 07:06):

So I quickly searched through the pdf of Polynomial Functors - a general theory of interaction and could not find a mention of power sets, which are what Kripke Polynomial functors are as defined by Bart Jacobs in his introductory book on coalgebras. The Kleisli category of the Powerset monad is equivalent to Rel the category of Sets and Relations, which I am particularly interested in.
I gather the book is not finished, as the course is not finished yet either. So it could be that it will show up. Just wondering what the status of that functor is.

Matteo Capucci (he/him) (Aug 07 2021 at 08:34):

I think powerset is not polynomial, since it's the functor $X \mapsto 2^X$ -- an exponential! @David Spivak and @Tim Hosgood recently wrote a paper about Dirichlet polynomials though, which are 'polynomials' where basis and exponent are inverted, afair. There's also another paper with David Jaz Myers about such polynomials

Matteo Capucci (he/him) (Aug 07 2021 at 08:37):

What instead is a polynomial is the finite powerset functor, i.e. the functor that sends a set $X$ to its set $\mathcal P_{fin}(X)$ of finite subsets. It is polynomials because can be expressed as $X \mapsto 1 + X^1 + X^2/2! + X^3/3! + \ldots$ (where $n!$ is the $n$-th symmetric group), or, more succinctly, as $\sum_{n \in \mathbb N} y^n / n!$

Notification Bot (Aug 07 2021 at 08:38):

This topic was moved here from #general > the Topos Institute is open! by Matteo Capucci (he/him)

James Wood (Aug 07 2021 at 08:39):

Don't you also need to quotient by permutations? I'd expect the polynomial you gave to be for lists.

Matteo Capucci (he/him) (Aug 07 2021 at 08:41):

James Wood said:

Don't you also need to quotient by permutations? I'd expect the polynomial you gave to be for lists.

Of course! :face_palm: I edited the message

Henry Story (Aug 07 2021 at 08:43):

I think for Rel all I need is $\mathcal P_{fin}(X)$. So that's fine. I guess I have all I need.
Mind you it looks like Poly is pretty powerful.
"Basically you can recover any category within the category of polynomial functors" min 21 of the second course from the Topos institute and also the end of chapter 1 of the book.

Henry Story (Aug 07 2021 at 08:44):

The dynamic aspect of poly is particularly exciting. I am writing a web server that is built on actors. So I am thinking poly should work here...

Matteo Capucci (he/him) (Aug 07 2021 at 08:45):

Henry Story said:

I think for Rel all I need is $\mathcal P_{fin}(X)$. So that's fine. I guess I have all I need.

I'm skeptical of this, because $\mathcal PX \neq \mathcal P_{fin}X$ unless $X$ is finite! The cat of relations you get is quite small in comparison, since every relation there is relating a finite number of elements

Henry Story (Aug 07 2021 at 08:46):

for programming, finite sets is quite a lot! I mean if finite is more than the particles in the universe then I think I can live with that. Is there a place where I would need more?

Matteo Capucci (he/him) (Aug 07 2021 at 08:48):

Henry Story said:

"Basically you can recover any category within the category of polynomial functors" min 21 of the second course from the Topos institute and also the end of chapter 1 of the book.

Is this a reference to Uustalu's (and someone else I can't remember right now!) observation that some comonads in poly recover small cats? Beware that you recover a different category of small cats, since morphisms turn out to be cofunctors. Indeed I don't like to call them cats since they don't transform like cats :)

Matteo Capucci (he/him) (Aug 07 2021 at 08:49):

Henry Story said:

for programming, finite sets is quite a lot! I mean if finite is more than the particles in the universe then I think I can live with that.

sure, you're free to use as little infinity as you like, but $Rel$ is a pre-existing, infinitary object so I was commenting on the equivalence $Kl(\mathcal P_{fin}) \cong Rel$ :)

Matteo Capucci (he/him) (Aug 07 2021 at 08:50):

Henry Story said:

Is there a place where I would need more?

geometry is pretty enamoured with infinity :)

Henry Story (Aug 07 2021 at 09:09):

Don't coalgebras give one access to infinity? I saw @Thorsten Altenkirch present conatural numbers with Agda. These start from infinity and go down. Also I think I saw papers such as On coalgebra of real numbers. (I guess both of those only use polynomial functors)

Here is a very nice introduction on coinductive proofs of equality using Cubical Agda by @taooftypes . One can prove that an equality of streams is a stream of equalities in 2 copattern matches that mirror inductive proofs. https://www.youtube.com/watch?v=-fhaZvgDaZk

- The 🐟‍‍ BabelFish (@bblfish)

Henry Story (Aug 07 2021 at 09:31):

Well they seem to allow for real exponents on p19 of the Poly book

Henry Story (Aug 07 2021 at 09:53):

Solutions to exercises 2.6 has this to say

Matteo Capucci (he/him) (Aug 07 2021 at 11:58):

Henry Story said:

Don't coalgebras give one access to infinity? I saw Thorsten Altenkirch present conatural numbers with Agda. These start from infinity and go down. Also I think I saw papers such as On coalgebra of real numbers. (I guess both of those only use polynomial functors)

yeah most infinities we deal with are actually 'finitary', in the sense that they can be described with finite means. in fact, all infinities are such, in a sense, since anything which requires infinitely many symbols to be defined cannot be defined by a mortal mathematician!
that's why i'm very at ease with infinity -- it's just a convenient short hand (as every mathematical concept, after all)

Thorsten Altenkirch (Aug 07 2021 at 13:15):

Matteo Capucci (he/him) said:

Henry Story said:

Don't coalgebras give one access to infinity? I saw Thorsten Altenkirch present conatural numbers with Agda. These start from infinity and go down. Also I think I saw papers such as On coalgebra of real numbers. (I guess both of those only use polynomial functors)

yeah most infinities we deal with are actually 'finitary', in the sense that they can be described with finite means. in fact, all infinities are such, in a sense, since anything which requires infinitely many symbols to be defined cannot be defined by a mortal mathematician!
that's why i'm very at ease with infinity -- it's just a convenient short hand (as every mathematical concept, after all)

This is a confusion between metalevel (the language we use) and object level (the things we speak about). We speak about infinite objects that is what we mean even though we always use finite means to speak about them. Don't confuse the levels!

Thorsten Altenkirch (Aug 07 2021 at 13:22):

Henry Story said:

Don't coalgebras give one access to infinity? I saw Thorsten Altenkirch present conatural numbers with Agda. These start from infinity and go down. Also I think I saw papers such as On coalgebra of real numbers. (I guess both of those only use polynomial functors)

Thank you for mentioning the clip. Yes terminal coalgebras are usually infinte objects, we get infinite trees instead of finite trees. However, you also get infinite Objects using just the mundane function type and indeed Streams over A are equivalent to functions from Nat to A. In my view the function type itself is 'coinductive' because it is defined by its destructor (application). Hence this is maybe no surprise.

What I like about the cubical approach is that it makes type theory more symmetric. In conventional type theory you can use recursion and pattern matching to reason about inductive types but you are left with nothing when it goes to coinductive types. Indeed even functional extensionality is not provable. However, in cubical type theory not only functional extensionality is provable but also we can reason about other coinductive types using copattern matching and corecursion.

The balance of the universe is restored. :-)

Matteo Capucci (he/him) (Aug 07 2021 at 13:39):

Thorsten Altenkirch said:

Matteo Capucci (he/him) said:

Henry Story said:

Don't coalgebras give one access to infinity? I saw Thorsten Altenkirch present conatural numbers with Agda. These start from infinity and go down. Also I think I saw papers such as On coalgebra of real numbers. (I guess both of those only use polynomial functors)

yeah most infinities we deal with are actually 'finitary', in the sense that they can be described with finite means. in fact, all infinities are such, in a sense, since anything which requires infinitely many symbols to be defined cannot be defined by a mortal mathematician!
that's why i'm very at ease with infinity -- it's just a convenient short hand (as every mathematical concept, after all)

This is a confusion between metalevel (the language we use) and object level (the things we speak about). We speak about infinite objects that is what we mean even though we always use finite means to speak about them. Don't confuse the levels!

I'm aware :)

Henry Story (Aug 07 2021 at 14:35):

conatural numbers are really quite mind boggling idea. I'd be surprised if one could not use those to prove the existence of God too, a theme being discussed over in philosophy. :grinning_face_with_smiling_eyes:

John Baez (Aug 08 2021 at 07:08):

If conatural numbers prove the existence of god, then natural numbers prove the existence of dog.

Stelios Tsampas (Sep 30 2021 at 19:43):

Matteo Capucci (he/him) said:

What instead is a polynomial is the finite powerset functor, i.e. the functor that sends a set $X$ to its set $\mathcal P_{fin}(X)$ of finite subsets. It is polynomials because can be expressed as $X \mapsto 1 + X^1 + X^2/2! + X^3/3! + \ldots$ (where $n!$ is the $n$-th symmetric group), or, more succinctly, as $\sum_{n \in \mathbb N} y^n / n!$

Do you have any references for this?

Conor McBride (Sep 30 2021 at 20:41):

Looks like finite multisets to me. But to do better is gnarly and not so obviously of value.

Stelios Tsampas (Oct 01 2021 at 00:29):

Yes indeed, it should be finite multisets. And someone remarked that it should be analytical and not polynomial.