C : Type u
inst✝² : Category C
inst✝¹ : MonoidalCategory C
A B X X' Y Y' Z : C
inst✝ : Closed A
⊢ (ihom.coev A).app ((𝟭 C).obj X) ≫ 𝟙 ((ihom A).obj (A ⊗ (𝟭 C).obj X)) = (ihom.coev A).app X
C : Type u
inst✝² : Category C
inst✝¹ : MonoidalCategory C
A B X X' Y Y' Z : C
inst✝ : Closed A
⊢ curry (𝟙 (A ⊗ (𝟭 C).obj X)) = (ihom.coev A).app X
rw [curry_eq, (ihom A).map_id (A ⊗ _)]
no goals
C : Type u
inst✝² : Category C
inst✝¹ : MonoidalCategory C
A B X X' Y Y' Z : C
inst✝ : Closed A
⊢ (ihom.coev A).app ((𝟭 C).obj X) ≫ 𝟙 ((ihom A).obj (A ⊗ (𝟭 C).obj X)) = (ihom.coev A).app X
apply comp_id