Dependent Composition

[nimarasekh]

Why does this PR have such an exciting history (closed, reopened, marked draft, ... )

[emilyriehl]

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.

[jonweinb]

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 Happy to do that soon, and coordinate as appropriate.

[nimarasekh]

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.

Did you commit these changes you are suggesting or is something wrong on my side? Cause I can't see them.

[nimarasekh]

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 Happy to do that soon, and coordinate as appropriate.

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?

[thchatzidiamantis]

Updated the names as suggested by @emilyriehl.

[emilyriehl]

I'm happy with everything in the covariant file. @fizruk should the change to settings.json be kept or reversed?

I also possibly introduced a formatting error that I don't understand.

[thchatzidiamantis]

Fixed formatting, removed agda thing