-
Notifications
You must be signed in to change notification settings - Fork 138
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
Gysin #965
Gysin #965
Conversation
some assumptions can be weakened. Converting to draft for now |
# Conflicts: # Cubical/Cohomology/EilenbergMacLane/Base.agda # Cubical/Cohomology/EilenbergMacLane/EilenbergSteenrod.agda
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Great stuff! Only some small requests for changes
substIso B p = pathToIso (cong B p) | ||
|
||
substEquiv' : ∀ {ℓ ℓ'} {A : Type ℓ} (B : A → Type ℓ') {x y : A} (p : x ≡ y) → B x ≃ B y | ||
substEquiv' B p = isoToEquiv (substIso B p) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This seems like a roundabout way to define this? Can't you use the one without the prime that's already in the library?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't remember why I need this but I can imagine a it being more useful than the one already in the lib. The one in the lib doesn't have an explicitly defined inverse (it's an isEquiv proof by J) which I want to remember was causing issues. But maybe I could add a comment?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A comment would be good
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I seem to recall that we had different proofs of this before...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So maybe move it so that it's next to substEquiv and add a comment explaining that the inverse gets more direct this way
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Couldn't move it next to it due to it needing pathToIso, but I added a comment.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Two small things left to fix
substIso B p = pathToIso (cong B p) | ||
|
||
substEquiv' : ∀ {ℓ ℓ'} {A : Type ℓ} (B : A → Type ℓ') {x y : A} (p : x ≡ y) → B x ≃ B y | ||
substEquiv' B p = isoToEquiv (substIso B p) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So maybe move it so that it's next to substEquiv and add a comment explaining that the inverse gets more direct this way
Should be ok now @mortberg |
Great! Will merge once the CI is happy |
* done * stuff * almost * done (not clean) * done * generalisation * minor * changes * minor * Update Cubical/Foundations/Transport.agda --------- Co-authored-by: Anders Mörtberg <[email protected]>
The Thom isomorphism and Gysin sequence for cohomology with coefficients in a commutative ring.
Depends on #955 and #954.