C : Type u
inst✝³ : Category C
A✝ B X✝ X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A✝
A X : C
inst✝ : Exponentiable A
⊢ (exp.coev A).app ((𝟭 C).obj X) ≫ 𝟙 (A ⟹ A ⨯ (𝟭 C).obj X) = (exp.coev A).app X
C : Type u
inst✝³ : Category C
A✝ B X✝ X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A✝
A X : C
inst✝ : Exponentiable A
⊢ curry (𝟙 (A ⨯ (𝟭 C).obj X)) = (exp.coev A).app X
rw [curry_eq, (exp A).map_id (A ⨯ _)]
no goals
C : Type u
inst✝³ : Category C
A✝ B X✝ X' Y Y' Z : C
inst✝² : HasFiniteProducts C
inst✝¹ : Exponentiable A✝
A X : C
inst✝ : Exponentiable A
⊢ (exp.coev A).app ((𝟭 C).obj X) ≫ 𝟙 (A ⟹ A ⨯ (𝟭 C).obj X) = (exp.coev A).app X
apply comp_id