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