gasche
commented
10 years ago I guess I should clarify where I personally want to go here: I would like the branch to be merged -- after maybe some changes.
On one hand, I regret the use of focusing vocabulary (@braibant speaks of "proper morphisms", I guess its "each our own turf"), and I think there are some aspects of the change that make things more complex than they need to be.
On the other, I think that this commit is a good basis on which to attack some not-so-easy questions such as the witness-reconstruction one (issue #17), so I plan to work on top of it and hope we decide to merge it relatively soon to avoid painful rebases.
I think we will be able to eventually simplify the presentation (compress functions, product and sums in a single datatype, and drop the focusing stuff), but it's not clear how to do that yet, and I think more (unrelated) work on top of the current presentation can help clear things up..
This pull request is a way to centralize the online discussion in this rather invasive change. I believe we'll eventually need to get something equivalent in master, but hopefully this can be discussed, simplified and better understood before. I have spent a copious amount of time rebasing against @protz additional comments, and this is a good thing as it forced me to equivalently comment the new functions.