C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G : C ⥤ D
α : F ⟶ G
X Y : C
h : X = Y
⊢ α.app X = α.app X ≫ G.map (eqToHom h) ≫ G.map (eqToHom (_ : Y = X))
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G : C ⥤ D
α : F ⟶ G
X Y : C
h : X = Y
⊢ α.app X = F.map (eqToHom h) ≫ α.app Y ≫ G.map (eqToHom (_ : Y = X))
rw [α.naturality_assoc]
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G : C ⥤ D
α : F ⟶ G
X Y : C
h : X = Y
⊢ α.app X = α.app X ≫ G.map (eqToHom h) ≫ G.map (eqToHom (_ : Y = X))
simp [eqToHom_map]