Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

small grammar correction (between vs. among) #932

Merged
merged 2 commits into from Feb 7, 2017
Merged

small grammar correction (between vs. among) #932

merged 2 commits into from Feb 7, 2017

Conversation

OliveiraHermogenes
Copy link
Contributor

Although "between" can be used to compare more than 2 things in some specific cases, I don't think this sentence qualifies as one of them. Furthermore, when I first read the sentence, I kept wondering if it was meant a relationship between the $n$-types and some other thing (which should be inferred from context) or among the $n$-types themselves. I suppose that it was meant the latter.

Although "between" can be used to compare more than 2 things in some specific cases, I don't think this sentence qualifies as one of them. Furthermore, when I first read the sentence, I kept wondering if it was meant a relationship between the $n$-types and some other thing (which should be inferred from context) or among the $n$-types themselves. I suppose that it was meant the later.
@mikeshulman
Copy link
Contributor

Thanks for the suggestion. Even less ambiguous might be "relationships between n-types for different values of n"; what do you think?

@OliveiraHermogenes
Copy link
Contributor Author

@mikeshulman Yes, that sounds even better. Thanks for your quick reply.

@mikeshulman
Copy link
Contributor

Do you want to update this PR or make a new one?

@OliveiraHermogenes
Copy link
Contributor Author

@mikeshulman I don't know. I am familiar with git but I just started using Github. I guess it would be easier if you just ignore the pull request and implement the changes youself, no? After all, it is just a very minor issue.

@mikeshulman mikeshulman merged commit e5a9d85 into HoTT:master Feb 7, 2017
@mikeshulman
Copy link
Contributor

Thanks! This way is easier for me; the other way would be easier for you. (-:O

@OliveiraHermogenes OliveiraHermogenes deleted the patch-1 branch February 7, 2017 20:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants