Daily Archives: 24 April 2011

Higher Inductive Types: a tour of the menagerie

(This was written in inadvertent parallel with Mike’s latest post at the Café, so there’s a little overlap — Mike’s discusses the homotopy-theoretic aspects more, this post the type-theoretic nitty-gritty.) Higher inductive types have been mentioned now in several other … Continue reading

Posted in Code, Higher Inductive Types | 7 Comments