Commit 2024-07-01 14:30 20856f07
View on Github →feat(CategoryTheory/Shift): more compatibilities for NatTrans.CommShift (#14187)
In this file, we show various compatibilities for the commutation of natural transformations with shifts. In particular, if F, G, H are composable functors which commute with shifts on the categories, then the associator isomorphism
(F ⋙ G) ⋙ H ≅ F ⋙ (G ⋙ H) commutes with the shifts.