# Morphisms from equations between objects. #

When working categorically, sometimes one encounters an equation `h : X = Y` between objects.

Your initial aversion to this is natural and appropriate: you're in for some trouble, and if there is another way to approach the problem that won't rely on this equality, it may be worth pursuing.

You have two options:

1. Use the equality `h` as one normally would in Lean (e.g. using `rw` and `subst`). This may immediately cause difficulties, because in category theory everything is dependently typed, and equations between objects quickly lead to nasty goals with `eq.rec`.
2. Promote `h` to a morphism using `eqToHom h : X ⟶ Y`, or `eqToIso h : X ≅ Y`.

This file introduces various `simp` lemmas which in favourable circumstances result in the various `eqToHom` morphisms to drop out at the appropriate moment!

source
def CategoryTheory.eqToHom {C : Type u₁} [CategoryStruct.{v₁, u₁} C] {X Y : C} (p : X = Y) :
X ⟶ Y

An equality `X = Y` gives us a morphism `X ⟶ Y`.

It is typically better to use this, rather than rewriting by the equality then using `𝟙 _` which usually leads to dependent type theory hell.

Equations

- CategoryTheory.eqToHom p = ⋯.mpr (CategoryTheory.CategoryStruct.id Y)

Instances For

source
@[simp]
theorem CategoryTheory.eqToHom_refl {C : Type u₁} [CategoryStruct.{v₁, u₁} C] (X : C) (p : X = X) :
eqToHom p = CategoryStruct.id X
source
@[simp]
theorem CategoryTheory.eqToHom_trans {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y = Z) :
CategoryStruct.comp (eqToHom p) (eqToHom q) = eqToHom ⋯
source
@[simp]
theorem CategoryTheory.eqToHom_trans_assoc {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y = Z) {Z✝ : C} (h : Z ⟶ Z✝) :
CategoryStruct.comp (eqToHom p) (CategoryStruct.comp (eqToHom q) h) = CategoryStruct.comp (eqToHom ⋯) h
source
theorem CategoryTheory.eqToHom_heq_id_dom {C : Type u₁} [Category.{v₁, u₁} C] (X Y : C) (h : X = Y) :
eqToHom h ≍ CategoryStruct.id X

`eqToHom h` is heterogeneously equal to the identity of its domain.

source
theorem CategoryTheory.eqToHom_heq_id_cod {C : Type u₁} [Category.{v₁, u₁} C] (X Y : C) (h : X = Y) :
eqToHom h ≍ CategoryStruct.id Y

`eqToHom h` is heterogeneously equal to the identity of its codomain.

source
theorem CategoryTheory.conj_eqToHom_iff_heq {C : Type u₁} [Category.{v₁, u₁} C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : X = Z) :
f = CategoryStruct.comp (eqToHom h) (CategoryStruct.comp g (eqToHom ⋯)) ↔ f ≍ g

Two morphisms are conjugate via eqToHom if and only if they are heterogeneously equal. Note this used to be in the Functor namespace, where it doesn't belong.

source
theorem CategoryTheory.conj_eqToHom_iff_heq' {C : Type u_1} [Category.{u_2, u_1} C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y) (h' : Z = X) :
f = CategoryStruct.comp (eqToHom h) (CategoryStruct.comp g (eqToHom h')) ↔ f ≍ g
source
theorem CategoryTheory.comp_eqToHom_iff {C : Type u₁} [Category.{v₁, u₁} C] {X Y Y' : C} (p : Y = Y') (f : X ⟶ Y) (g : X ⟶ Y') :
CategoryStruct.comp f (eqToHom p) = g ↔ f = CategoryStruct.comp g (eqToHom ⋯)
source
theorem CategoryTheory.eqToHom_comp_iff {C : Type u₁} [Category.{v₁, u₁} C] {X X' Y : C} (p : X = X') (f : X ⟶ Y) (g : X' ⟶ Y) :
CategoryStruct.comp (eqToHom p) g = f ↔ g = CategoryStruct.comp (eqToHom ⋯) f
source
theorem CategoryTheory.eqToHom_comp_heq {C : Type u_1} [Category.{u_2, u_1} C] {W X Y : C} (f : Y ⟶ X) (h : W = Y) :
CategoryStruct.comp (eqToHom h) f ≍ f
source
@[simp]
theorem CategoryTheory.eqToHom_comp_heq_iff {C : Type u_1} [Category.{u_2, u_1} C] {W X Y Z Z' : C} (f : Y ⟶ X) (g : Z ⟶ Z') (h : W = Y) :
CategoryStruct.comp (eqToHom h) f ≍ g ↔ f ≍ g
source
@[simp]
theorem CategoryTheory.heq_eqToHom_comp_iff {C : Type u_1} [Category.{u_2, u_1} C] {W X Y Z Z' : C} (f : Y ⟶ X) (g : Z ⟶ Z') (h : W = Y) :
g ≍ CategoryStruct.comp (eqToHom h) f ↔ g ≍ f
source
theorem CategoryTheory.comp_eqToHom_heq {C : Type u_1} [Category.{u_2, u_1} C] {X Y Z : C} (f : X ⟶ Y) (h : Y = Z) :
CategoryStruct.comp f (eqToHom h) ≍ f
source
@[simp]
theorem CategoryTheory.comp_eqToHom_heq_iff {C : Type u_1} [Category.{u_2, u_1} C] {W X Y Z Z' : C} (f : X ⟶ Y) (g : Z ⟶ Z') (h : Y = W) :
CategoryStruct.comp f (eqToHom h) ≍ g ↔ f ≍ g
source
@[simp]
theorem CategoryTheory.heq_comp_eqToHom_iff {C : Type u_1} [Category.{u_2, u_1} C] {W X Y Z Z' : C} (f : X ⟶ Y) (g : Z ⟶ Z') (h : Y = W) :
g ≍ CategoryStruct.comp f (eqToHom h) ↔ g ≍ f
source
theorem CategoryTheory.heq_comp {C : Type u_1} [Category.{u_2, u_1} C] {X Y Z X' Y' Z' : C} {f : X ⟶ Y} {g : Y ⟶ Z} {f' : X' ⟶ Y'} {g' : Y' ⟶ Z'} (eq1 : X = X') (eq2 : Y = Y') (eq3 : Z = Z') (H1 : f ≍ f') (H2 : g ≍ g') :
CategoryStruct.comp f g ≍ CategoryStruct.comp f' g'
source
@[simp]
theorem CategoryTheory.eqToHom_naturality {C : Type u₁} [Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ⟶ g b) {j j' : β} (w : j = j') :
CategoryStruct.comp (z j) (eqToHom ⋯) = CategoryStruct.comp (eqToHom ⋯) (z j')

We can push `eqToHom` to the left through families of morphisms.

source
@[simp]
theorem CategoryTheory.eqToHom_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ⟶ g b) {j j' : β} (w : j = j') {Z : C} (h : g j' ⟶ Z) :
CategoryStruct.comp (z j) (CategoryStruct.comp (eqToHom ⋯) h) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (z j') h)
source
@[simp]
theorem CategoryTheory.eqToHom_iso_hom_naturality {C : Type u₁} [Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b) {j j' : β} (w : j = j') :
CategoryStruct.comp (z j).hom (eqToHom ⋯) = CategoryStruct.comp (eqToHom ⋯) (z j').hom

A variant on `eqToHom_naturality` that helps Lean identify the families `f` and `g`.

source
@[simp]
theorem CategoryTheory.eqToHom_iso_hom_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b) {j j' : β} (w : j = j') {Z : C} (h : g j' ⟶ Z) :
CategoryStruct.comp (z j).hom (CategoryStruct.comp (eqToHom ⋯) h) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (z j').hom h)
source
@[simp]
theorem CategoryTheory.eqToHom_iso_inv_naturality {C : Type u₁} [Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b) {j j' : β} (w : j = j') :
CategoryStruct.comp (z j).inv (eqToHom ⋯) = CategoryStruct.comp (eqToHom ⋯) (z j').inv

A variant on `eqToHom_naturality` that helps Lean identify the families `f` and `g`.

source
@[simp]
theorem CategoryTheory.eqToHom_iso_inv_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b) {j j' : β} (w : j = j') {Z : C} (h : f j' ⟶ Z) :
CategoryStruct.comp (z j).inv (CategoryStruct.comp (eqToHom ⋯) h) = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (z j').inv h)
source
@[simp]
theorem CategoryTheory.congrArg_cast_hom_left {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y ⟶ Z) :
cast ⋯ q = CategoryStruct.comp (eqToHom p) q

Reducible form of congrArg_mpr_hom_left

source
theorem CategoryTheory.congrArg_mpr_hom_left {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y ⟶ Z) :
⋯.mpr q = CategoryStruct.comp (eqToHom p) q

If we (perhaps unintentionally) perform equational rewriting on the source object of a morphism, we can replace the resulting `_.mpr f` term by a composition with an `eqToHom`.

It may be advisable to introduce any necessary `eqToHom` morphisms manually, rather than relying on this lemma firing.

source
@[simp]
theorem CategoryTheory.congrArg_cast_hom_right {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (p : X ⟶ Y) (q : Z = Y) :
cast ⋯ p = CategoryStruct.comp p (eqToHom ⋯)

Reducible form of `congrArg_mpr_hom_right`

source
theorem CategoryTheory.congrArg_mpr_hom_right {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (p : X ⟶ Y) (q : Z = Y) :
⋯.mpr p = CategoryStruct.comp p (eqToHom ⋯)

If we (perhaps unintentionally) perform equational rewriting on the target object of a morphism, we can replace the resulting `_.mpr f` term by a composition with an `eqToHom`.

It may be advisable to introduce any necessary `eqToHom` morphisms manually, rather than relying on this lemma firing.

source
def CategoryTheory.eqToIso {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (p : X = Y) :
X ≅ Y

An equality `X = Y` gives us an isomorphism `X ≅ Y`.

It is typically better to use this, rather than rewriting by the equality then using `Iso.refl _` which usually leads to dependent type theory hell.

Equations

- CategoryTheory.eqToIso p = { hom := CategoryTheory.eqToHom p, inv := CategoryTheory.eqToHom ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

source
@[simp]
theorem CategoryTheory.eqToIso.hom {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (p : X = Y) :
(eqToIso p).hom = eqToHom p
source
@[simp]
theorem CategoryTheory.eqToIso.inv {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (p : X = Y) :
(eqToIso p).inv = eqToHom ⋯
source
@[simp]
theorem CategoryTheory.eqToIso_refl {C : Type u₁} [Category.{v₁, u₁} C] {X : C} (p : X = X) :
eqToIso p = Iso.refl X
source
@[simp]
theorem CategoryTheory.eqToIso_trans {C : Type u₁} [Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y = Z) :
eqToIso p ≪≫ eqToIso q = eqToIso ⋯
source
@[simp]
theorem CategoryTheory.eqToHom_op {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (h : X = Y) :
(eqToHom h).op = eqToHom ⋯
source
@[simp]
theorem CategoryTheory.eqToHom_unop {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C ᵒᵖ} (h : X = Y) :
(eqToHom h).unop = eqToHom ⋯
source
instance CategoryTheory.instIsIsoEqToHom {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (h : X = Y) :
IsIso (eqToHom h)
source
@[simp]
theorem CategoryTheory.inv_eqToHom {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (h : X = Y) :
inv (eqToHom h) = eqToHom ⋯
source
theorem CategoryTheory.Functor.ext {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (h_obj : ∀ (X : C), F.obj X = G.obj X) (h_map : ∀ (X Y : C) (f : X ⟶ Y), F.map f = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G.map f) (eqToHom ⋯)) := by cat_disch) :
F = G

Proving equality between functors. This isn't an extensionality lemma, because usually you don't really want to do this.

source
theorem CategoryTheory.Functor.ext_of_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (e : F ≅ G) (hobj : ∀ (X : C), F.obj X = G.obj X) (happ : ∀ (X : C), e.hom.app X = eqToHom ⋯ := by cat_disch) :
F = G
source
theorem CategoryTheory.Functor.hext {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (h_obj : ∀ (X : C), F.obj X = G.obj X) (h_map : ∀ (X Y : C) (f : X ⟶ Y), F.map f ≍ G.map f) :
F = G

Proving equality between functors using heterogeneous equality.

source
theorem CategoryTheory.Functor.congr_obj {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (h : F = G) (X : C) :
F.obj X = G.obj X
source
theorem CategoryTheory.Functor.congr_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (h : F = G) {X Y : C} (f : X ⟶ Y) :
F.map f = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G.map f) (eqToHom ⋯))
source
theorem CategoryTheory.Functor.congr_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (h : F = G) {X Y : C} (f : X ⟶ Y) {Z : D} (h✝ : F.obj Y ⟶ Z) :
CategoryStruct.comp (F.map f) h✝ = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G.map f) (CategoryStruct.comp (eqToHom ⋯) h✝))
source
theorem CategoryTheory.Functor.congr_inv_of_congr_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F G : Functor C D) {X Y : C} (e : X ≅ Y) (hX : F.obj X = G.obj X) (hY : F.obj Y = G.obj Y) (h₂ : F.map e.hom = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G.map e.hom) (eqToHom ⋯))) :
F.map e.inv = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (G.map e.inv) (eqToHom ⋯))
source
theorem CategoryTheory.Functor.map_comp_heq {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y) (hz : F.obj Z = G.obj Z) (hf : F.map f ≍ G.map f) (hg : F.map g ≍ G.map g) :
F.map (CategoryStruct.comp f g) ≍ G.map (CategoryStruct.comp f g)
source
theorem CategoryTheory.Functor.map_comp_heq' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z} (hobj : ∀ (X : C), F.obj X = G.obj X) (hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f) :
F.map (CategoryStruct.comp f g) ≍ G.map (CategoryStruct.comp f g)
source
theorem CategoryTheory.Functor.precomp_map_heq {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C D} (H : Functor E C) (hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f) {X Y : E} (f : X ⟶ Y) :
(H.comp F).map f ≍ (H.comp G).map f
source
theorem CategoryTheory.Functor.postcomp_map_heq {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C D} {X Y : C} {f : X ⟶ Y} (H : Functor D E) (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y) (hmap : F.map f ≍ G.map f) :
(F.comp H).map f ≍ (G.comp H).map f
source
theorem CategoryTheory.Functor.postcomp_map_heq' {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C D} {X Y : C} {f : X ⟶ Y} (H : Functor D E) (hobj : ∀ (X : C), F.obj X = G.obj X) (hmap : ∀ {X Y : C} (f : X ⟶ Y), F.map f ≍ G.map f) :
(F.comp H).map f ≍ (G.comp H).map f
source
theorem CategoryTheory.Functor.hcongr_hom {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (h : F = G) {X Y : C} (f : X ⟶ Y) :
F.map f ≍ G.map f
source
theorem CategoryTheory.eqToHom_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (p : X = Y) :
F.map (eqToHom p) = eqToHom ⋯

This is not always a good idea as a `@[simp]` lemma, as we lose the ability to use results that interact with `F`, e.g. the naturality of a natural transformation.

In some files it may be appropriate to use `attribute [local simp] eqToHom_map`, however.

source
@[simp]
theorem CategoryTheory.eqToHom_map_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (p : X = Y) (q : Y = Z) :
CategoryStruct.comp (F.map (eqToHom p)) (F.map (eqToHom q)) = F.map (eqToHom ⋯)
source
@[simp]
theorem CategoryTheory.eqToHom_map_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (p : X = Y) (q : Y = Z) {Z✝ : D} (h : F.obj Z ⟶ Z✝) :
CategoryStruct.comp (F.map (eqToHom p)) (CategoryStruct.comp (F.map (eqToHom q)) h) = CategoryStruct.comp (F.map (eqToHom ⋯)) h
source
theorem CategoryTheory.eqToIso_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} (p : X = Y) :
F.mapIso (eqToIso p) = eqToIso ⋯

See the note on `eqToHom_map` regarding using this as a `simp` lemma.

source
@[simp]
theorem CategoryTheory.eqToIso_map_trans {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y Z : C} (p : X = Y) (q : Y = Z) :
F.mapIso (eqToIso p) ≪≫ F.mapIso (eqToIso q) = F.mapIso (eqToIso ⋯)
source
@[simp]
theorem CategoryTheory.eqToHom_app {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (h : F = G) (X : C) :
(eqToHom h).app X = eqToHom ⋯
source
theorem CategoryTheory.NatTrans.congr {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F G : Functor C D} (α : F ⟶ G) {X Y : C} (h : X = Y) :
α.app X = CategoryStruct.comp (F.map (eqToHom h)) (CategoryStruct.comp (α.app Y) (G.map (eqToHom ⋯)))
source
theorem CategoryTheory.eq_conj_eqToHom {C : Type u₁} [Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) :
f = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp f (eqToHom ⋯))
source
theorem CategoryTheory.dcongr_arg {C : Type u₁} [Category.{v₁, u₁} C] {ι : Type u_2} {F G : ι → C} (α : (i : ι) → F i ⟶ G i) {i j : ι} (h : i = j) :
α i = CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (α j) (eqToHom ⋯))
source
def CategoryTheory.Equivalence.induced {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) :
InducedCategory D ⇑e ≌ D

If `T ≃ D` is a bijection and `D` is a category, then `InducedCategory D e` is equivalent to `D`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem CategoryTheory.Equivalence.induced_inverse_obj {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) (a : D) :
(induced e).inverse.obj a = e.symm a
source
@[simp]
theorem CategoryTheory.Equivalence.induced_functor {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) :
(induced e).functor = inducedFunctor ⇑e
source
@[simp]
theorem CategoryTheory.Equivalence.induced_counitIso {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) :
(induced e).counitIso = NatIso.ofComponents (fun (x : D) => eqToIso ⋯) ⋯
source
@[simp]
theorem CategoryTheory.Equivalence.induced_inverse_map {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) {X Y : D} (f : X ⟶ Y) :
(induced e).inverse.map f = have this := CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp f (eqToHom ⋯)); this
source
@[simp]
theorem CategoryTheory.Equivalence.induced_unitIso {D : Type u₂} [Category.{v₂, u₂} D] {T : Type u_2} (e : T ≃ D) :
(induced e).unitIso = NatIso.ofComponents (fun (x : InducedCategory D ⇑e) => eqToIso ⋯) ⋯