[Merged by Bors] - feat(CategoryTheory): inductive construction of composable arrows#8146
[Merged by Bors] - feat(CategoryTheory): inductive construction of composable arrows#8146
Conversation
joelriou
commented
Nov 3, 2023
joelriou
commented
ghost
added
the
merge-conflict
ghost
removed
the
merge-conflict
| namespace Nerve | ||
|
|
||
| variable {C} | ||
|
|
||
| lemma δ₀_eq_composableArrows_δ₀ {n : ℕ} | ||
| (x : (nerve C).obj (Opposite.op (SimplexCategory.mk (n + 1)))) : | ||
| (nerve C).δ (0 : Fin (n + 2)) x = ComposableArrows.δ₀ x := rfl | ||
|
|
||
| end Nerve |
There was a problem hiding this comment.
I wonder whether we should revert the import. If so, then we can do that in another PR.
There was a problem hiding this comment.
@jcommelin Do you mean have Nerve import ComposableArrows rather than the other direction, so that we may use ComposableArrows without relying on the whole simplicial stuff?
There was a problem hiding this comment.
Exactly! And it would also allow us to use ComposableArrows from the start in setting up API for Nerve.
There was a problem hiding this comment.
As bors failed, I shall do it in this PR.
There was a problem hiding this comment.
This is done in 6a9f235 (I had to introduce some basic functoriality of ComposableArrows).
|
Thanks 🎉 bors merge |
github-actions
bot
added
ready-to-merge
|
Build failed (retrying...): |
|
bors d+ |
|
✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
the
delegated
|
Canceled. |
joelriou
added
awaiting-review
and removed
delegated
ghost
added
ready-to-merge
|
GitHub was flaking and bors crashed so we need to try this again bors merge |
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
3 participants
