Dependent Composition #144
Conversation
…s, does one of them produce composition over a Segal type?
.vscode/settings.json
Outdated
There was a problem hiding this comment.
Do you really want to add this line about agdaLanguageServer?
There was a problem hiding this comment.
I don't know how this ended up here, I assume I should just delete it.
There was a problem hiding this comment.
@fizruk can you comment on this?
| along an arrow f : hom A x y to give a term in C y. | ||
|
|
||
| ```rzk title="RS17, covariant transport from beginning of Section 8.2" | ||
| #def covariant-transport |
There was a problem hiding this comment.
Why are you removing this?
There was a problem hiding this comment.
If I go to my repository this is in my file, other things above it were removed. Again, don't know what is happening.
There was a problem hiding this comment.
It might be an issue about which branch you are.
There was a problem hiding this comment.
This is also still in the file we are now if you expand it, starting at line 702. I can delete all of this and start a new PR if this is all too messy.
There was a problem hiding this comment.
I see you moved it. Sorry you are right.
|
Why does this PR have such an exciting history (closed, reopened, marked draft, ... ) |
|
The code looks great. I've suggested a few renamings (feel free to push back @thchatzidiamantis). Let's also have someone else figure out what happened with the agda thing in the settings file. |
|
Great work @thchatzidiamantis and @nimarasekh! I also have a version for a more general setting over in the yoneda repo, not yet integrated into sHoTT: https://github.com/emilyriehl/yoneda/blob/master/src/simplicial-hott/12-cocartesian.rzk.md |
Did you commit these changes you are suggesting or is something wrong on my side? Cause I can't see them. |
I think all the work here is @thchatzidiamantis with tremendous help by @emilyriehl and nothing by me. Also yeah you should add your result to the library, why not? |
.vscode/settings.json
Outdated
There was a problem hiding this comment.
@fizruk can you comment on this?
|
|
||
| We can compose dependent arrows given a covariant type family. | ||
|
|
||
| ```rzk title="RS17, Remark 8.11" |
There was a problem hiding this comment.
I'd move this label down to the definition of dcomp, since "is-contr-ext-is-covariant" is proving contractibility of a different type than is discussed there (which is fine).
There was a problem hiding this comment.
The name "is-covariant-family-is-segal-base" is used for some definitions that depend on both of these hypotheses but not for all of them (some just use "is-covariant"). I'd add it to all the definitions here that use these hypotheses.
If this is too long perhaps "is-covariant-is-segal" could work everywhere. But I'd adopt whatever convention uniformly.
| We can compose dependent arrows given a covariant type family. | ||
|
|
||
| ```rzk title="RS17, Remark 8.11" | ||
| #def is-contr-ext-is-covariant uses (extext) |
There was a problem hiding this comment.
perhaps "ext" should be "horn-ext"; as revealed by the proof, up to equivalence, this proves contractibility of horn extension (into a sigma type).
| A C is-covariant-C is-segal-A) | ||
| ( \ t → (a t , c t))) | ||
|
|
||
| #def equiv-ext-is-segal-base |
There was a problem hiding this comment.
Similarly perhaps "ext" should be "comp-horn-ext". Here I've added "comp" because this is a special case of the sort of horns considered above (over a composition witness in the base). This also differentiates the term below.
| ( witness-comp-is-segal A is-segal-A (a (0₂ , 0₂)) (a (1₂ , 0₂)) | ||
| ( a (1₂ , 1₂)) (\ s → a (s , 0₂)) (\ s → a (1₂ , s))) | ||
|
|
||
| #def is-contr-horn-ext-is-covariant uses (extext) |
There was a problem hiding this comment.
If the above renamings are adopted then perhaps "horn-ext" is "comp-horn-ext".
| ( s ≡ 0₂ ↦ ff t | ||
| , t ≡ 1₂ ↦ gg s) | ||
|
|
||
| #def compositions-are-dhorn-fillings |
There was a problem hiding this comment.
Maybe "dcompositions-are-dhorn-fillings"?
| ( is-contr-ext-dhom-is-covariant | ||
| A is-segal-A C is-covariant-C x y z f g u v w ff gg))) | ||
| ``` | ||
|
|
There was a problem hiding this comment.
No need to leave an rzk code block here unless you want to add a comment (eg "Like ordinary composition, dependent composition is unique."
|
Updated the names as suggested by @emilyriehl. |
No description provided.