C : Type u
A : Type u_1
inst✝² : Category C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv = (shiftFunctor C 0).map f
C : Type u
A : Type u_1
inst✝² : Category C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftFunctor C 0).map f = (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv
symm
no goals
C : Type u
A : Type u_1
inst✝² : Category C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
X Y : C
f : X ⟶ Y
⊢ (shiftZero A X).hom ≫ f ≫ (shiftZero A Y).inv = (shiftFunctor C 0).map f
apply NatIso.naturality_2