search

HoTT / book

A textbook on informal homotopy type theory
2.03k stars 361 forks source link

Coinductive types? #787

Open spacekitteh opened 9 years ago

spacekitteh commented 9 years ago

Could something be said about coinductive types being derivable in the presence of inductive types in HoTT? (See http://arxiv.org/abs/1504.02949 )

andrejbauer commented 9 years ago

As in "add coinductive types" to the HoTT book? That would be something for 2nd edition.

mikeshulman commented 9 years ago

I could be convinced, but at present I don't think it would be worth including any serious development of coinductive types. But we could add a sentence or two somewhere mentioning that they exist and giving a citation, perhaps in the notes to in chapter 5.

awodey commented 9 years ago

of course, Benedikt and coauthors have recently written a paper on this that could be cited.

Steve

On Apr 22, 2015, at 5:51 PM, Mike Shulman notifications@github.com wrote:

I could be convinced, but at present I don't think it would be worth including any serious development of coinductive types. But we could add a sentence or two somewhere mentioning that they exist and giving a citation, perhaps in the notes to in chapter 5.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/book/issues/787#issuecomment-95262415.

mikeshulman commented 9 years ago

(which Sophie linked to in her first comment)

awodey commented 9 years ago

check.

On Apr 22, 2015, at 7:36 PM, Mike Shulman notifications@github.com wrote:

(which Sophie linked to in her first comment)

— Reply to this email directly or view it on GitHub https://github.com/HoTT/book/issues/787#issuecomment-95295360.