Cleaning up synthetic homotopy theory #649
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
|
With this PR, we may be coming close to finishing the items in #195! 😃 |
|
It is a nontrivial task though. I might not do it all in one pull request. |
|
This one is ready for review. I'll continue refactoring in a new PR tomorrow. |
fredrik-bakke
approved these changes
Jun 9, 2023
src/synthetic-homotopy-theory/dependent-cocones-under-spans.lagda.md
Outdated
Show resolved
Hide resolved
src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md
Outdated
Show resolved
Hide resolved
|
I'm gonna merge this when the checks are done. Thanks so much for the review and the corrections! |
Comment on lines
+47
to
+71
| ## List of files directly related to identity types | ||
|
|
||
| The following table lists files that are about identity types and operations on | ||
| identifications in arbitrary types. | ||
|
|
||
| | Concept | File | | ||
| | ------------------------------------------------ | ------------------------------------------------------------------------------------------------------------------------- | | ||
| | Action on identifications of binary functions | [`foundation.action-on-identifications-binary-functions`](foundation.action-on-identifications-binary-functions.md) | | ||
| | Action on identifications of dependent functions | [`foundation.action-on-identifications-dependent-functions`](foundation.action-on-identifications-dependent-functions.md) | | ||
| | Action on identifications of functions | [`foundation.action-on-identifications-functions](foundation.action-on-identifications-functions.md) | | ||
| | Binary transport | [`foundation.binary-transport`](foundation.binary-transport.md) | | ||
| | Commuting squares of identifications | [`foundation.commuting-squares-identifications`](foundation.commuting-squares-identifications.md) | | ||
| | Dependent paths (foundation) | [`foundation.dependent-paths`](foundation.dependent-paths.md) | | ||
| | Dependent paths (foundation-core) | [`foundation-core.dependent-paths`](foundation-core.dependent-paths.md) | | ||
| | The fundamental theorem of identity types | [`foundation.fundamental-theorem-of-identity-types`](foundation.fundamental-theorem-of-identity-types.md) | | ||
| | Hexagons of identifications | [`foundation.hexagons-of-identifications`](foundation.hexagons-of-identifications.md) | | ||
| | Identity systems | [`foundation.identity-sytsemts`](foundation.identity-systems.md) | | ||
| | The identity type (foundation) | [`foundation.identity-types`](foundation.identity-types.md) | | ||
| | The identity type (foundation-core) | [`foundation-core.identity-types`](foundation-core.identity-types.md) | | ||
| | Large identity types | [`foundation.large-identity-types`](foundation.large-identity-types.md) | | ||
| | Path algebra | [`foundation.path-algebra`](foundation.path-algebra.md) | | ||
| | Symmetric identity types | [`foundation.symmetric-identity-types`](foundation.symmetric-identity-types.md) | | ||
| | Transport (foundation) | [`foundation.transport`](foundation.transport.md) | | ||
| | Transport (foundation-core) | [`foundation-core.transport`](foundation-core.transport.md) | | ||
| | The universal property of identity types | [`foundation.universal-property-identity-types`](foundation.universal-property-identity-types.md) | |
There was a problem hiding this comment.
This is a good start, but maybe it's best to write a full text guiding readers to get an overview? Or perhaps this is unmaintainable...
There was a problem hiding this comment.
If you feel inspired you're welcome to do that
|
Sorry, I fell asleep. Great work! |
fredrik-bakke
added a commit
that referenced
this pull request
Oct 22, 2023
- Hyperlinks throughout `synthetic-homotopy-theory` - Using `coherence-square-identifications` and `dependent-identifications` in `interval` - Changing the order of arguments of `coherence-square-identifications` to be the same as for maps This PR builds on #649 and #650, and works toward progressing item 8 of #195. --------- Co-authored-by: Fredrik Bakke <fredrbak@gmail.com>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
24-pushouts.lagda.mdcofiber.lagda.mdpushouts.lagda.mduniversal-property-pushouts.lagda.mdeq-htpytofunction-extensionality