Commit 2024-04-30 09:33 333b54ae
View on Github →feat(CategoryTheory): whiskering a fully faithful functor is full (#12527)
We already had that whiskering by a faithful functor is faithful. This PR also adds the relevant Full and Faithful instances for the sheaf version of whiskering, (sheafCompose).