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.

Sign up for GitHub

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

Jump to bottom

Rebase infrastructure for pushouts to span diagrams #885

Closed
wants to merge 288 commits into from
Closed

Rebase infrastructure for pushouts to span diagrams #885

wants to merge 288 commits into from

Conversation

EgbertRijke
Copy link
Collaborator

In this PR I refactor the definitions of spans, morphisms of spans, and equivalences of spans (previously called homotopies of spans), and I will work on a better integration of this infrastructure in the theory of pushouts.

Since this touches upon earlier work of @VojtechStep and @tomdjong, perhaps you two can have a look at this PR when it's ready. (That's not to exclude @fredrik-bakke from also having a look)

@VojtechStep VojtechStep mentioned this pull request Oct 28, 2023
Merged
@EgbertRijke EgbertRijke mentioned this pull request Dec 2, 2023
Merged
@fredrik-bakke fredrik-bakke mentioned this pull request Dec 2, 2023
Merged
@EgbertRijke EgbertRijke mentioned this pull request Dec 5, 2023
Merged
@VojtechStep
Copy link
Collaborator

@EgbertRijke do you have a timeline in mind for finishing this PR? I'm not sure if I should be continuing my development with the old infrastructure, or if it's feasible to start using the shiny new spans

@EgbertRijke
Copy link
Collaborator Author

Ok let me get it to a decent state so that you can start using it. I’ll try to get it done by the weekend.

@VojtechStep
Copy link
Collaborator

Great! Thanks

fredrik-bakke
fredrik-bakke reviewed Dec 25, 2023
View reviewed changes
src/synthetic-homotopy-theory/26-descent.lagda.md Outdated
Comment on lines 419 to 423
cone-family-dependent-pullback-property P γ =
pair
( precompose-lifts P (horizontal-map-cocone-span s c) γ)
( pair
( precompose-lifts P (vertical-map-cocone-span s c) γ)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

copattern match

@EgbertRijke
Copy link
Collaborator Author

I'm converting span-fixed-domain-codomain to span and span to span-diagram. This should make our terminology more in use with the common mathematical use of a span, which is from one given object to another. Furthermore, cocones will be on span diagrams, which is analogous to cocones on sequential diagrams, so a recurring scheme is emerging.

@EgbertRijke
Copy link
Collaborator Author

In order to complete this refactoring I'm gonna have to deal with pointed spans as well. Please hang on tight everyone:P

@EgbertRijke
Copy link
Collaborator Author

EgbertRijke commented Jan 2, 2024 •
edited
Loading

...and morphisms of pointed arrows too

EgbertRijke and others added 25 commits March 17, 2024 11:08
@EgbertRijke
add file
aa353af
@EgbertRijke
work
ddde9ea
@EgbertRijke
work
bc93d28
@VojtechStep
Fix imports
35b81e9
@VojtechStep
make-span
0da3854
@VojtechStep
Temporarily allow unsolved metas
bd8ca3b
@VojtechStep
Rebase cocones under pointed span diagrams to pointed span diagrams
0bf0093
@VojtechStep
Standard pointed pushouts
e5f630d
@VojtechStep
Bring back cofibers
5662155
@VojtechStep
Bring back wedges
2d8a563
@VojtechStep
Bring back smash products
80205ad
@EgbertRijke
Merge branch 'master' of github.com:UniMath/agda-unimath into spans
944fe14
@EgbertRijke
Merge pull request #5 from VojtechStep/spans
5141988 
Rebase infrastructure for pointed pushouts to pointed span diagrams
@EgbertRijke
dependent span diagrams
041d016
@EgbertRijke
cartesian morphisms of arrows
7066eab
@EgbertRijke
base changes of span diagrams
47cf8bd
@EgbertRijke
infrastructure
5c9a05f
@EgbertRijke
new files
daf7a19
@EgbertRijke
make pre-commit
5ca02c2
@EgbertRijke
make pre-commit
2dce70a
@EgbertRijke
Merge branch 'master' of github.com:UniMath/agda-unimath into spans
9eaef8d
@EgbertRijke
cartesian dependent span diagrams
b0a319a
@EgbertRijke
flattening dependent span diagrams
3cbc16f
@EgbertRijke
display
7700d5c
@EgbertRijke
cartesian dependent span diagrams
44d26a3
@VojtechStep VojtechStep mentioned this pull request Mar 23, 2024
Merged
@EgbertRijke
Copy link
Collaborator Author

I am closing this pull request now, as I am not expecting to make progress on this any time soon.

@EgbertRijke EgbertRijke closed this Apr 6, 2024
VojtechStep added a commit that referenced this pull request Apr 6, 2024
@VojtechStep
Rebase infrastructure for coequalizers to double arrows (#1098)
f7b8de0 
In anticipation of #885. The proof of the universal property of
coequalizers being preserved by equivalences of coforks got a bit
unwieldy, but it should become more conceptual once morphisms and
equivalences of cocones under spans are integrated (for now they exist
only in the other PR).
VojtechStep pushed a commit that referenced this pull request Apr 19, 2024
@fredrik-bakke
Rewrite rules for pushouts (#1021)
378ff01 
Adds strict β-laws for the standard pushouts in a new module
`synthetic-homotopy-theory.rewriting-pushouts`.

### Todo
- [x] Wait for #885.
- [x] ~Refactor postulates of universal properties to be phrased in
terms of coherently invertible maps.~
- [x] Add separate file for rewrites
`synthetic-homotopy-theory.rewriting-pushouts`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@VojtechStep VojtechStep VojtechStep left review comments

@fredrik-bakke fredrik-bakke fredrik-bakke left review comments

Assignees
No one assigned
Labels
documentation Improvements or additions to documentation refactoring synthetic-homotopy-theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@EgbertRijke @VojtechStep @fredrik-bakke