case w
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ (F.mapIso (i ≪≫ j)).hom = (F.mapIso i ≪≫ F.mapIso j).hom
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ F.mapIso (i ≪≫ j) = F.mapIso i ≪≫ F.mapIso j
ext
no goals
case w
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
X Y Z : C
i : X ≅ Y
j : Y ≅ Z
⊢ (F.mapIso (i ≪≫ j)).hom = (F.mapIso i ≪≫ F.mapIso j).hom
apply Functor.map_comp