Rewrite of adjoint equivalence proofs

[imeckler]

I've added types for iso' (qinv in the book) and what was previously calledadj-iso' (hae in the book) and rewritten the proofs relating them to match those given in the book using the equational reasoning combinators. Although, to be honest, I'm not sure they're more readable.

[favonia]

Thanks for the code! I don't see a reason to say no. What do other people think?

[imeckler]

I didn't intend to submit my most recent commit involving the group file. I just don't know how to keep new commits out of this pull request.

[JasonGross]

@imeckler If you want to keep commits out of this pull request, don't push to your master branch again until this pull request is merged. To remove the latest commit, you can do git push origin 23712a8:master -f. To avoid this problem in the future, make sure that you branch (git checkout -b <new branch name> and git push origin <new-branch-name>:<new-branch-name>) before making a pull request, and don't make pull requests from master. GitHub uses branches to track pull requests; when you update a branch, it updates the pull request.

[imeckler]

Thanks @JasonGross. I've reverted the latest commit.

[favonia]

I just realized that this is based on the old branch master. Are you willing to take a look at the new branch 2.0?

[andrejbauer]

You should have the old version on a separate branch and the new development version on master. People who look at your repository expect master to be whatever current development is, not some old stuff.

[imeckler]

@favonia It looks like the proofs in the 2.0 version are all tidy enough. Is there a particular issue with them that I could take on?

[favonia]

@andrejbauer I would say the biggest mistake is that we mindlessly picked master as the branch name. It should be 1.0 or something. Now that 2.0 is online, I'm wondering if we can rename master.

[favonia]

@imeckler Probably not. Thanks for your contribution. 😃

[andrejbauer]

@favonia I think you should definitely do it. You shoudl rename master to 1.0 and then rename 2.0 to master (by the way, you may want to do this carefully, @JasonGross is the man to ask).

[guillaumebrunerie]

I think the plan was to merge 2.0 into master eventually (when it contains enough stuff). Not sure why the 2.0 is considered the default branch, but I agree that we should probably merge it into master soon.

[andrejbauer]

Is it worth preserving some version of 1.0? If so, you should maybe branch off 1.0 just before you merge 2.0 into master.

[JasonGross]

If you want to preserve a version of 1.0, you probably want tags, rather than branches; tags are generally for things you don't plan to work on any more but want to keep track of, branches are for things you plan to keep working on. Simply merging 2.0 into master is certainly the easiest and least confusing way to do this; if you rename branches (which is possible), you're going to confuse people who have local copies, because you're essentially changing the history of 1.0. If merging results in too many conflicts, you can probably use the "take other" strategy, or create a commit that is "replace everything with 2.0 versions" first, and then merge afterwards to keep history.

[favonia]

Sorry for starting this conversation in a closed issue. I think we should continue our discussion and make decisions in another thread. Thanks.