ToucanIan

@de_Jong_Tom@mathstodon.xyz @ljungstrom@mathstodon.xyz @Nicolai_Kraus@mathstodon.xyz Nice work!

@julesh@mathstodon.xyz P should be injective on sets by uniqueness of top elements in a sup lattice.

@pigworker but I know what a functor and a polynomial are and I don’t know why one should call it a container.

@jonmsterling@mathstodon.xyz looking forward to trying it as I am onboard with a lot of your goals!

@sophiehuiberts@mathstodon.xyz wait I noticed this yesterday and thought I was crazy.

@ltchen @qbane @banacorn that’s awesome

@dwarn I have so far failed to come up with an alternative proof showing that there is an Id-collapsible map on the type. Now that I see your solution as a formalization of a homotopical proof maybe thinking about loop spaces is essential.

@MartinEscardo thanks for this! I tried and failed to do the very same thing. @dwarn

@boarders is it terrible?

@boarders maybe be explicit? As far as I know, and I don’t claim to know much, the argument of a polynomial functor is relegated to the codomain/base.

@pigworker can’t wait.

@carloangiuli@mathstodon.xyz are you saying replace both with keytheorems or just thmtools? I’ll try it