-
Notifications
You must be signed in to change notification settings - Fork 69
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
Target: Sequential Colimits in Homotopy Type Theory #1080
Comments
fredrik-bakke
pushed a commit
that referenced
this issue
Apr 16, 2024
…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
fredrik-bakke
pushed a commit
that referenced
this issue
Apr 18, 2024
- 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
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.
The text was updated successfully, but these errors were encountered: