C : Type u
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
A✝ B X X' Y Y' Z : C
inst✝² : Closed A✝
inst✝¹ : Closed B
A : C
inst✝ : Closed A
⊢ ↑(transferNatTransSelf (ihom.adjunction A) (ihom.adjunction A)) (𝟙 ((tensoringLeft C).obj A)) = 𝟙 (ihom A)
C : Type u
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
A✝ B X X' Y Y' Z : C
inst✝² : Closed A✝
inst✝¹ : Closed B
A : C
inst✝ : Closed A
⊢ pre (𝟙 A) = 𝟙 (ihom A)
simp only [pre, Functor.map_id]
C : Type u
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
A✝ B X X' Y Y' Z : C
inst✝² : Closed A✝
inst✝¹ : Closed B
A : C
inst✝ : Closed A
⊢ ↑(transferNatTransSelf (ihom.adjunction A) (ihom.adjunction A)) (𝟙 (tensorLeft A)) = 𝟙 (ihom A)
C : Type u
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
A✝ B X X' Y Y' Z : C
inst✝² : Closed A✝
inst✝¹ : Closed B
A : C
inst✝ : Closed A
⊢ ↑(transferNatTransSelf (ihom.adjunction A) (ihom.adjunction A)) (𝟙 ((tensoringLeft C).obj A)) = 𝟙 (ihom A)
dsimp
no goals
C : Type u
inst✝⁴ : Category C
inst✝³ : MonoidalCategory C
A✝ B X X' Y Y' Z : C
inst✝² : Closed A✝
inst✝¹ : Closed B
A : C
inst✝ : Closed A
⊢ ↑(transferNatTransSelf (ihom.adjunction A) (ihom.adjunction A)) (𝟙 (tensorLeft A)) = 𝟙 (ihom A)
simp