search

HoTT / book

A textbook on informal homotopy type theory
2.01k stars 358 forks source link

Polynomial functor in Ch. 4 #58

Closed awodey closed 11 years ago

awodey commented 11 years ago

Chapter 4 doesn't use the idea of W-types as initial algebras of polynomial functors! Unless someone else is willing to do it, I propose to add a bit on this point of view in section 4.4 -- it will mostly be lifted from our LICS paper.

mikeshulman commented 11 years ago

Isn't this 4.4.9, except that it doesn't say the words "polynomial functor"?

awodey commented 11 years ago

the proof of 4.4.9 is what I added last night. today I realized that it uses the polynomial point of view, which doesn't come up previously.

mikeshulman commented 11 years ago

Mentioning the polynomial PoV sounds good to me.

awodey commented 11 years ago

I'll patch in something, but someone else should then read it for coherence with the rest.

mikeshulman commented 11 years ago

I reorganized it a bit, to start with nat-algebras as a lead-in and then define the polynomial endofunctor and its algebras just before proving the theorem. I think it reads better this way, what do you think?

awodey commented 11 years ago

yes, more clear this way.