case refl
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
⊢ ↑(homEquiv adj A B).symm (↑(homEquiv adj A B) f) = f
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : g = ↑(homEquiv adj A B) f
⊢ ↑(homEquiv adj A B).symm g = f
cases h
no goals
case refl
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
⊢ ↑(homEquiv adj A B).symm (↑(homEquiv adj A B) f) = f
simp
case refl
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
g : A ⟶ G.obj B
⊢ g = ↑(homEquiv adj A B) (↑(homEquiv adj A B).symm g)
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : ↑(homEquiv adj A B).symm g = f
⊢ g = ↑(homEquiv adj A B) f
cases h
no goals
case refl
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X' X : C
Y Y' : D
A : C
B : D
g : A ⟶ G.obj B
⊢ g = ↑(homEquiv adj A B) (↑(homEquiv adj A B).symm g)
simp