C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X : C
⊢ (eqToHom (_ : F = F)).app X = eqToHom (_ : F.obj X = F.obj X)
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F G : C ⥤ D
h : F = G
X : C
⊢ (eqToHom h).app X = eqToHom (_ : F.obj X = G.obj X)
subst h
no goals
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X : C
⊢ (eqToHom (_ : F = F)).app X = eqToHom (_ : F.obj X = F.obj X)
rfl