tl;dr: Read a draft of my thesis and send me your feedback by September 9!
Over the past year I’ve had several people say things along the lines of, “let me know if you want me to read through your thesis”. I never took them all that seriously (it’s easy to say you are willing to read a 200-page document…), but it never hurts to ask, right?
My thesis defense is scheduled for October 14, and I’m currently undertaking a massive writing/editing push to try to get as much of it wrapped up as I can before classes start on September 4. So, if there’s anyone out there actually interested in reading a draft and giving feedback, now is your chance!
The basic idea of my dissertation is to put combinatorial species and related variants (including a port of the theory to HoTT) in a common categorical framework, and then be able to use them for working with/talking about data types. If you’re brave enough to read it, you’ll find lots of category theory and type theory, and very little code—but I can promise lots of examples and pretty pictures. I’ve tried to make it somewhat self-contained, so it may be a good way to learn a bit of category theory or homotopy type theory, if you’ve been curious to learn more about those topics.
You can find the latest draft here (auto-updated every time I commit); more generally, you can find the git repo here. If you notice any typos or grammatical errors, feel free to open a pull request. For anything more substantial—thoughts on the organization, notes or questions about things you found confusing, suggestions for improvement, pointers to other references—please send me an email (first initial last name at gmail). And finally, please send me any feedback by September 9 at the latest (but the earlier the better). I need to have a final version to my committee by September 23.
Last but not least, if you’re interested to read it but don’t have the time or inclination to provide feedback on a draft, never fear—I’ll post an announcement when the final version is ready for your perusal!
blog :: Brent -> [String] 
I just subscribed to your blog via RSS looking for haskell feeds a day ago. If you could post a path to minimum competence, i’d be more than willing to try to get there. If it’s within my range.
Pingback: Open source dissertation | The Endeavour
Definition 1.4.4 is incomplete. Again, you need some coherence axioms (for which you will want to send the reader to Mac Lane again).
Ah, thanks, I missed that. And not only coherence but also gamma . gamma = id, otherwise it’s just a braiding. Fixed now.
I like your discussion of ends and coends; I might even be able to keep them straight now!
Haha, thanks!
Typo in first paragraph on page 37, corrected: ‘these topics require much more care in a constructive setting than in a CLASSICAL one’.
Thanks, fixed now.
Besides protoequivalence of categories, you might want to explicitly introduce weak equivalence of categories; a weak equivalence is a span of protoequivalences. The problem with protoequivalence is it doesn’t give us an equivalence relation, merely a preorder; the generated equivalence relation is the relation of weak equivalence. (This is not immediately obvious; you must show that weak equivalence is transitive.) Then later, you can point out the connection to anafunctors, which are also spans, and note that the relation of anaequivalence is the same as the relation of weak equivalence.
Thanks, I wasn’t aware of that. Do you have a good citation for this? (Your thesis, perhaps?) At this point I think I prefer to just mention it for completeness and point the reader to some reference(s).
You wouldn’t want to cite my thesis, since it actually defines only anaequivalence (and internal anaequivalence at that). But in a similar vein, you could cite [the nLab’s article](http://ncatlab.org/nlab/show/equivalence+of+categories#WeakEquivalence). I don’t know where else to cite, but I’ll try to find something for authoritative.
Brent, this is very cool! You’ve inspired me to do the same thing.
Thanks Lindsey! Awesome re: doing the same thing, I look forward to seeing it!
(You’ve asked people to e-mail, but I prefer to use blog comments than e-mail, and it looks like I’m not the only one!)
Do you have any particular bits you want comments on? It seems like a very early draft so far, but I think I followed up to Chapter 3. Here are my comments on the 16th August version.
– The definitions of ends and coends are missing the universal property.
– The intro to chapter 2 is a bit woolly, talking about weaving an insightful story. Could you be precise about the technical contribution? For example could you say you’re showing in HoTT that B is isomorphic to P, and this is useful because it allows you to state a particular theorem later in a nice way?
– In Chapter 3 you use the big circle ◯ in the sections on Pointing and Functor Compositions, but I didn’t understand the informal definition ‘the variant of E where we “do not care about” labels’, and the TODO says you’re planning to use a forward reference. I think you should make the order more logical here, or at least try to make the informal definition really clear.
Blog comments are great, thanks!
Re: ends and coends, thanks, you’re absolutely right.
Re: the chapter 2 intro, you’re right, it needs a lot of improvement, especially re: contributions.
Thanks for pointing out your confusion about the big circle species. The problem is that *as a species* it is completely isomorphic to E; the difference only arises when considering the stuff in Chapter 4 (which is still in a very sad state at the moment). I need to rethink it and figure out exactly what I want to say.