case refl
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X : C
⊢ F.map (eqToHom (_ : X = X)) = eqToHom (_ : F.obj X = F.obj X)
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y : C
p : X = Y
⊢ F.map (eqToHom p) = eqToHom (_ : F.obj X = F.obj Y)
cases p
no goals
case refl
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X : C
⊢ F.map (eqToHom (_ : X = X)) = eqToHom (_ : F.obj X = F.obj X)
simp