Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(CategoryTheory): more universe polymorphism for limits in sheaf …
…categories (#12222) We prove that sheaf categories have limits and colimits of the same size as the target category. Before, the universe levels were too restrictive. We change the construction of the colimit: it now uses the formal properties of sheafification instead of an explicit construction.
- Loading branch information
1 parent
fa2a388
commit f83fe2f
Showing
4 changed files
with
40 additions
and
84 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters