New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(AlgebraicTopology): the monoidal category structure on simplicial sets #11396
Conversation
This PR/issue depends on:
|
instance : ChosenFiniteProducts SSet.{u} where | ||
terminal := FunctorToTypes.functorEmptyLimitCone _ | ||
product := FunctorToTypes.binaryProductLimitCone |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It should now be possible to provide such an instance for the category of functors from C
to D
whenever D
has chosen finite products. In fact, it seems that pretty much everything in this file can be similarly generalized.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for the suggestions. The simp lemmas were slightly more difficult to obtain in general, but it works.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm perfectly happy with the code you wrote in the general context. In the case of the monoidal structure on simplicial sets, I had a slight concern that mixing the ChosenFiniteProducts
api and the (type-theoretic) Prod
, but it seems that the necessary simp lemmas already exist for the monoidal structure on Type*
, so it seems that everything (especially simp
) should work as expected!
Thanks!
bors r+
…l sets (#11396) If a category `C` has chosen finite products, then the functor category `J ⥤ C` also. In particular, the category of simplicial sets is endowed with the monoidal category given by the explicit terminal object and binary products. Simplifications lemmas have also been added in the context of categories with chosen finite products. For terminal objects in such categories, the terminal object is given as a limit cone of `Functor.empty.{0} C` rather than `Functor.empty.{v} C` so as to be consistent with the limits API for terminal objects. Co-authored-by: Jack McKoen <mckoen@ualberta.ca>
Pull request successfully merged into master. Build succeeded: |
…l sets (#11396) If a category `C` has chosen finite products, then the functor category `J ⥤ C` also. In particular, the category of simplicial sets is endowed with the monoidal category given by the explicit terminal object and binary products. Simplifications lemmas have also been added in the context of categories with chosen finite products. For terminal objects in such categories, the terminal object is given as a limit cone of `Functor.empty.{0} C` rather than `Functor.empty.{v} C` so as to be consistent with the limits API for terminal objects. Co-authored-by: Jack McKoen <mckoen@ualberta.ca>
…l sets (#11396) If a category `C` has chosen finite products, then the functor category `J ⥤ C` also. In particular, the category of simplicial sets is endowed with the monoidal category given by the explicit terminal object and binary products. Simplifications lemmas have also been added in the context of categories with chosen finite products. For terminal objects in such categories, the terminal object is given as a limit cone of `Functor.empty.{0} C` rather than `Functor.empty.{v} C` so as to be consistent with the limits API for terminal objects. Co-authored-by: Jack McKoen <mckoen@ualberta.ca>
…l sets (#11396) If a category `C` has chosen finite products, then the functor category `J ⥤ C` also. In particular, the category of simplicial sets is endowed with the monoidal category given by the explicit terminal object and binary products. Simplifications lemmas have also been added in the context of categories with chosen finite products. For terminal objects in such categories, the terminal object is given as a limit cone of `Functor.empty.{0} C` rather than `Functor.empty.{v} C` so as to be consistent with the limits API for terminal objects. Co-authored-by: Jack McKoen <mckoen@ualberta.ca>
…l sets (#11396) If a category `C` has chosen finite products, then the functor category `J ⥤ C` also. In particular, the category of simplicial sets is endowed with the monoidal category given by the explicit terminal object and binary products. Simplifications lemmas have also been added in the context of categories with chosen finite products. For terminal objects in such categories, the terminal object is given as a limit cone of `Functor.empty.{0} C` rather than `Functor.empty.{v} C` so as to be consistent with the limits API for terminal objects. Co-authored-by: Jack McKoen <mckoen@ualberta.ca>
If a category
C
has chosen finite products, then the functor categoryJ ⥤ C
also. In particular, the category of simplicial sets is endowed with the monoidal category given by the explicit terminal object and binary products.Simplifications lemmas have also been added in the context of categories with chosen finite products. For terminal objects in such categories, the terminal object is given as a limit cone of
Functor.empty.{0} C
rather thanFunctor.empty.{v} C
so as to be consistent with the limits API for terminal objects.Co-authored-by: Jack McKoen mckoen@ualberta.ca