plus): Adds a functorial version of `J.diagram P`, functorial in `P`. (#11155)

Commit

4 years ago

feat(category_theory/sites/plus): Adds a functorial version of `J.diagram P`, functorial in `P`. (#11155)

Author

adamtopaz

Parents