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

Fix some problems with Lemma 7.5.12 #731

Merged
merged 2 commits into from Oct 23, 2014
Merged

Conversation

@mikeshulman
Copy link
Contributor

mikeshulman commented Oct 21, 2014

The converse direction of Lemma 7.5.12 is false unless Q is fiberwise merely inhabited. Also, there was a typo in the proof. (I discovered both of these things while Coqing it.)

@EgbertRijke

This comment has been minimized.

Copy link
Contributor

EgbertRijke commented Oct 23, 2014

We said above the lemma that it is going to be useful, but I didn't find any explicit references to it. I've quickly gone through section 7.6 to see if there were any implicit uses of this lemma, but I couldn't find any.

Did you also check whether there are any uses of this theorem where we should verify the new hypothesis?

@mikeshulman

This comment has been minimized.

Copy link
Contributor Author

mikeshulman commented Oct 23, 2014

Yes, I never needed it in formalizing these sections either; I suspect we never use it.

EgbertRijke added a commit that referenced this pull request Oct 23, 2014
Fix some problems with Lemma 7.5.12
@EgbertRijke EgbertRijke merged commit 01922a8 into HoTT:master Oct 23, 2014
1 check passed
1 check passed
continuous-integration/travis-ci The Travis CI build passed
Details
@mikeshulman mikeshulman deleted the mikeshulman:lemma7.5.12 branch Jan 28, 2015
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants
You can’t perform that action at this time.