C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
ι : Type u_1
F G : ι → C
α : (i : ι) → F i ⟶ G i
i : ι
⊢ α i = eqToHom (_ : F i = F i) ≫ α i ≫ eqToHom (_ : G i = G i)
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
ι : Type u_1
F G : ι → C
α : (i : ι) → F i ⟶ G i
i j : ι
h : i = j
⊢ α i = eqToHom (_ : F i = F j) ≫ α j ≫ eqToHom (_ : G j = G i)
subst h
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
ι : Type u_1
F G : ι → C
α : (i : ι) → F i ⟶ G i
i : ι
⊢ α i = eqToHom (_ : F i = F i) ≫ α i ≫ eqToHom (_ : G i = G i)
simp