search

rzk-lang / sHoTT

Formalisations for simplicial HoTT and synthetic ∞-categories.
https://rzk-lang.github.io/sHoTT/
44 stars 12 forks source link

Formalise horizontal composition (Section 6.3 of RS17 paper) #10

Closed fizruk closed 1 year ago

fizruk commented 1 year ago

Should be straightforward.

emilyriehl commented 1 year ago

It looks (to me) like essentially all of this appears in the library already written by @fredrik-bakke (who made a nice observation that horizontal composition does not require any Segal hypothesis). In the adjunctions pull request I added whiskering as a special case of this to be used there.

I propose we close this issue and perhaps open a new one proving middle four interchange?

fredrik-bakke commented 1 year ago

That's right. You can find it here: https://rzk-lang.github.io/sHoTT/simplicial-hott/06-2cat-of-segal-types.rzk/#horizontal-composition

fredrik-bakke commented 1 year ago

By the way, have you shifted your focus from the Yoneda repository to this one completely at this point?

fizruk commented 1 year ago

My understanding is that this repository has a different goal: formalising as mush simplicial HoTT as we (including all the contributors) can, such as results by Jonathan Weinberger, Ulrich Buchholtz, and César Bardomiano Martínez. The Yoneda repository will still get updated with at least the cocartesian version of the lemma (when we have it), and, possibly, with formalisations in other proof assistants (or at least links to such formalisations and some comparisons). Perhaps, @emilyriehl can provide a more precise relationship of the two repositories.

fizruk commented 1 year ago

I propose we close this issue and perhaps open a new one proving middle four interchange?

Sounds good to me :)