C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
S S' S'' : D
Y Y' : C
T : C ⥤ D
f : S ⟶ S'
f' : S' ⟶ S''
h : StructuredArrow S'' T
⊢ (map (f ≫ f')).obj (mk h.hom) = (map f).obj ((map f').obj (mk h.hom))
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
S S' S'' : D
Y Y' : C
T : C ⥤ D
f : S ⟶ S'
f' : S' ⟶ S''
h : StructuredArrow S'' T
⊢ (map (f ≫ f')).obj h = (map f).obj ((map f').obj h)
rw [eq_mk h]
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
S S' S'' : D
Y Y' : C
T : C ⥤ D
f : S ⟶ S'
f' : S' ⟶ S''
h : StructuredArrow S'' T
⊢ (map (f ≫ f')).obj (mk h.hom) = (map f).obj ((map f').obj (mk h.hom))
simp