Commit 2025-08-15 09:40 1a4e58c1
View on Github →feat(CategoryTheory/Sites/SheafOfTypes): composition of a sheaf with uliftFunctor is still a sheaf (#27816)
Prove that if a presheaf of types is a sheaf, then its composition with uliftFunctor is still a sheaf.