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

Target: Sequential Colimits in Homotopy Type Theory #1080

Open
VojtechStep opened this issue Mar 15, 2024 · 0 comments
Open

Target: Sequential Colimits in Homotopy Type Theory #1080

VojtechStep opened this issue Mar 15, 2024 · 0 comments
Assignees
@VojtechStep
Labels
formalization-target synthetic-homotopy-theory

Comments

@VojtechStep
Copy link
Collaborator

I already formalized and documented parts of the paper. I'm assigning myself, because I would like to include this formalization effort in my master's thesis.
@VojtechStep VojtechStep self-assigned this Mar 15, 2024
@VojtechStep VojtechStep mentioned this issue Mar 15, 2024
Merged
@VojtechStep VojtechStep mentioned this issue Apr 11, 2024
Merged
fredrik-bakke pushed a commit that referenced this issue Apr 16, 2024
@VojtechStep
Descent data for sequential colimits and its version of the flattenin…
2c0f6a6 
…g lemma (#1109)

Sorry, this is bigger than I anticipated...

This PR
- defines morphisms and equivalences between dependent sequential
diagrams
- defines morphisms and equivalences of cocones under morphisms and
equivalences of sequential diagrams
- defines equifibered sequential diagrams
- defines descent data for sequential colimits
- shows the descent property of sequential colimits
- proves a version of the flattening lemma expressed with families with
associated descent data
- collects various helpers for converting between sequential stuff and
coequalizer stuff into one file
- adds some auxiliary infrastructure along the way

I took care to properly separate the work into commits, so it might be
more digestible to review it commit by commit.

This is progress towards #1080
@VojtechStep VojtechStep mentioned this issue Apr 17, 2024
Merged
fredrik-bakke pushed a commit that referenced this issue Apr 18, 2024
@VojtechStep
Equivalences are closed under "transfinite composition" (#1117)
bc8998a 
- if a sequential diagram consists of equivalences, then injection maps
into its colimit are also equivalences
- as a corollary, sequential colimits of sequential diagrams of
contractible types are contractible

Progress towards #1080
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@VojtechStep VojtechStep

Labels
formalization-target synthetic-homotopy-theory
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@VojtechStep